siiky
2023/10/10
2023/10/10
2023/10/10
whitepaper,petri_nets,mathematics,programming
The category theory approach to compiling Petri nets to "executable code".
p18, *Prop6* proof, the set bijections have something wrong... The first line is j,k/j,k while the second is k,j/j,k.
This correspondence between Petri nets and free strict symmetric monoidal categories defnes a process semantics for nets: The FSSMC is interpreted as a deterministic version of its corresponding net, in which the history of every single token is tracked. This, in principle, could be implemented using a dependently typed language such as Idris [4] and, even more satisfactorily, such an implementation would allow one to map the FSSMC corresponding to a net to any other monoidal category representing a semantics, for instance the category Hask [8] of Haskell types and functions. The result is a procedure to formally compile a Petri net down to computations, with the net itself used as control to trigger the execution of algorithms and the passing of data between them. This is the approach adopted in defning the Statebox programming language [19].
On *p.2* they write about converting the FSSMC of a net to other categories, such as Hask! This is the first hint that it should be possible to literally compile a Petri net to executable code! See also *Def1.3*.
"Open Petri Nets" is mentioned several times. On *p.8* it's mentioned that its approach has something to do with net modularity.
"Pre-nets, Read Arcs and Unfolding: A Functorial Presentation" is mentioned on *p.8*.
This is a problem when it comes to mapping net computations to a semantics: As tuples are not commutative in the general case, our functorial correspondence cannot be symmetric monoidal.
From *p.11*. Is the order of the tokens consumed from a single place by a transition that important?
; T1 () -> a ; T2 () -> a ; T3 a a -> ()
If it is so important to tell if a token consumed by =T3= was produced by =T1= or =T2= then two places could (and maybe should) be used instead:
; T1 () -> a ; T2 () -> b ; T3 a b -> ()
Plus, from the Statebox monograph, markings are represented as multisets, so transitions (theoretically) can't even know where tokens come from. Why that paragraph about non-commutativity of tuples then?
If transition code is written in a way that doesn't need to know the order of the elements, then there's no need to linearize multisets into strings.
What happened in *Def11*, *Def12*, and *Prop1*?
Putting everything together, the situation is as in Figure 4. There is a way to go back and forth from nets to FSSMCs, and a way to functorially map FSSMC morphisms to net morphisms. This suggests the following course of action: In our implementation, we always manipulate FSSMCs. The user can nevertheless draw Petri nets, which are automatically mapped to their corresponding FSSMC through F. When the user wants to fetch information regarding some Petri net N, the corresponding FSSMC FN is retrieved instead, and NFN is displayed.