Showing 1–5 of 5 results for author: Herold, J

A Categorical Semantics for Hierarchical Petri Nets

Authors: Fabrizio Romano Genovese, Jelle Herold, Fosco Loregian, Daniele Palombi

Abstract: 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… ▽ More 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. △ Less

Submitted 21 December, 2021; v1 submitted 29 January, 2021; originally announced February 2021.

Comments: In Proceedings GCM 2021, arXiv:2112.10217

Journal ref: EPTCS 350, 2021, pp. 51-68

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

Authors: Fabrizio Genovese, Alex Gryzlov, Jelle Herold, Andre Knispel, Marco Perone, Erik Post, André Videla

Abstract: 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 t… ▽ More 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. △ Less

Submitted 14 September, 2020; v1 submitted 25 November, 2019; originally announced December 2019.

Comments: In Proceedings ACT 2019, arXiv:2009.06334

Journal ref: EPTCS 323, 2020, pp. 246-254

The Mathematical Specification of the Statebox Language

Authors: Statebox Team, Fabrizio Genovese, Jelle Herold

Abstract: 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 achie… ▽ More 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. △ Less

Submitted 26 June, 2019; v1 submitted 18 June, 2019; originally announced June 2019.

MSC Class: 5Uxx

Computational Petri Nets: Adjunctions Considered Harmful

Authors: Fabrizio Genovese, Alex Gryzlov, Jelle Herold, Marco Perone, Erik Post, André Videla

Abstract: 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 directio… ▽ More 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. △ Less

Submitted 8 May, 2019; v1 submitted 29 April, 2019; originally announced April 2019.

Comments: 29 Pages, 6 Figures, 1 Listing

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

Authors: Fabrizio Genovese, Jelle Herold

Abstract: 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 pa… ▽ More 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. △ Less

Submitted 29 January, 2019; v1 submitted 15 May, 2018; originally announced May 2018.

Comments: In Proceedings QPL 2018, arXiv:1901.09476

Journal ref: EPTCS 287, 2019, pp. 127-144