arXiv subjects

Jelle Herold

Publications and source records attributed to Jelle Herold.

6 recordsLinked to original sources

arXiv2021

A Categorical Semantics for Hierarchical Petri Nets

We show how a particular variety of hierarchical nets, where the firing of a transition in the parent net must correspond to an execution in some child net, can be modelled utilizing a functorial semantics from a free category -- representing the parent net -- to the category of sets and spans between them. This semantics can be internalized via Grothendieck construction, resulting in the category of executions of a Petri net representing the semantics of the overall hierarchical net. We conclude the paper by giving an engineering-oriented overview of how our model of hierarchical nets can be implemented in a transaction-based smart contract environment.

math.CT↗

arXiv2020

idris-ct: A Library to do Category Theory in Idris

We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business. Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties.

cs.LO↗

arXiv2019

Foundations of brick diagrams

We discuss the foundations of 2-dimensional graphical languages, with a view towards their computer implementation in a 'compiler' for monoidal categories. In particular, we discuss the close relationship between string diagrams, pasting diagrams, linear logic proof trees and k-d trees, the last being a data structure from computational geometry and computer graphics that recursively partitions a space. We introduce a minor variant of cubical pasting diagrams, which we call 'brick diagrams', which are used in the Statebox visual programming language. This paper is intended as a discussion and literature review, and contains little mathematics.

math.CT↗

arXiv2019

The Mathematical Specification of the Statebox Language

This document defines the mathematical backbone of the Statebox programming language. In the simplest way possible, Statebox can be seen as a clever way to tie together different theoretical structures to maximize their benefits and limit their downsides. Since consistency and correctness are central requisites for our language, it became clear from the beginning that such tying could not be achieved by just hacking together different pieces of code representing implementations of the structures we wanted to leverage: Rigorous mathematics is employed to ensure both conceptual consistency of the language and reliability of the code itself. The mathematics presented here is what guided the implementation process, and we deemed very useful to release it to the public to help people wanting to audit our work to better understand the code itself.

cs.PL↗

arXiv2019

Computational Petri Nets: Adjunctions Considered Harmful

We review some of the endeavors in trying to connect Petri nets with free symmetric monoidal categories. We give a list of requirement such connections should respect if they are meant to be useful for practical/implementation purposes. We show how previous approaches do not satisfy them, and give compelling evidence that this depends on trying to make the correspondence functorial in the direction from nets to free symmetric monoidal categories, in order to produce an adjunction. We show that dropping this immediately honors our desiderata, and conclude by introducing an Idris library which implements them.

math.CT↗

arXiv2019

Executions in (Semi-)Integer Petri Nets are Compact Closed Categories

In this work, we analyse Petri nets where places are allowed to have a negative number of tokens. For each net we build its correspondent category of executions, which is compact closed, and prove that this procedure is functorial. We moreover exhibit a procedure to recover the original net from its category of executions, show that it is again functorial, and that this gives rise to an adjoint pair. Finally, we use compact closeness to infer that allowing negative tokens in a Petri net makes the causal relations between transition firings non-trivial, and we use this to model interesting phenomena in economics and computer science.

math.CT↗