💾 Archived View for siiky.srht.site › wiki › wp.statebox.mathematical_specification_statebox_languag… captured on 2024-08-25 at 00:20:17. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Statebox, "The Mathematical Specification of the Statebox Language"

siiky

2023/10/10

2024/03/10

whitepaper,petri_nets,mathematics

https://doi.org/10.48550/arXiv.1906.07629

My first venture intro Petri nets.

Errors

p12, "We will often denote with T_N, P_N, (...) the set of places, transitions (...)", order of T_N and P_N is flipped.

p13, "(...) if and only if in any input place for =t= (...)", should be "all"

p22, "not the right place for an in-dept exposition"

p28, Fig3.3, (b) =id_B * lambda_A= on the right of the diagram should be =id_A * lambda_B= instead.

p37-38, Def3.6.7, Fig3.13a, the description and the diagram don't match? Def3.6.7 is probably the one needing an adjustment, since the examples and remarks following the figure match the figure.

p44, Def4.2.5, "A morphism of Petri nets M → N", should be "N → M".

p48, Fig4.6, mentions *Fig4.3* but it should be *Fig4.1*?

p52, Def4.5.1, s/occurrencies/occurrences/

p53, "This is again related to the fact that a Petri net carries less information that its corresponding FSSMC, (...)", "that" should be "than".

p55, "It is clear then than even if (...)", s/than/that/

p57, "Clearly, the fact that any net can now fire (...)", s/net/transition/ ?

p62, "(...) mapping from the net execution to the actual code takes care of (...)", s/code/& that/

Improvements

p15, Eg2.4.2, "(...) as in the figure above, (...)" The figure is in the following page.

p16, Def2.5.1, transition notation is different from Def2.3.7.

Questions

p14, Def2.3.7, "Figure 2.5 is an example of this, where °(t)_N ∧ (t)°_N is non-empty." Intersection of multisets is not defined (that I've seen).

p16, Def2.5.3, a net in a certain state is considered deadlocked even if a deadlock state isn't inevitable to be reached? (Not reachable, but reached)

p17, Def2.5.5, what does "can never fire" mean? There's no reachable state where the transition is enabled? And why is there a need for an intermediary state Y in the definition of "alive"? Isn't "Z reachable from X where the transition is enabled" enough? Doesn't "there is a firing sequence that, from Y, leads to a marking Z" mean the same as "Z is reachable from Y"?

p17, Rem2.5.6, "(...) it is trivial to prove that an alive Petri net is not deadlocked, and that every transition will always be enabled in the future (...)". Why? Isn't the net from Fig2.6 alive? Eventually, all transitions become dead (and so does the net).

p18-19, how to represent multiplicities of arcs other than 1?

p37, how do pushouts and coproducts differ?

p62, what do they meant with "we cannot concatenate tokens or perform any sort of list operation on them", refering to [Int]?

Petri Nets

Informal definition

Petri nets are composed of /places/, /transitions/, and /arcs/ (weighted on natural numbers). Places contain any number of /tokens/ (representing resources). Transitions are connected to places through arcs and can transform resources into other resources (this "transformation" is called /firing/).

A transition may be in one of two "states":

Enabled :: when all the places connected into the transition have a number of tokens greater or equal to the weight of the corresponding arc. When a transition has no incoming arcs it is vacuously enabled.
Disabled :: otherwise. That is, there's at least one place without enough tokens.

E.g.: If a transition has 2 incoming arcs of weight 2 and 3, then the corresponding places of each of the arcs must have at least 2 and 3 tokens, respectively.

-----

This is just one of the possible behaviours for preti nets, however, these constraints help studying the system as a whole with regards to reachability, existence or not of deadlocks, &c. More on how to improve/generalize this theory later.

Multisets

Multisets will be formalized as functions =X_S^{N_0} : S -> N_0= (=X= is the notation meaning "multiset of S"). Subsets of =S= are functions =S -> 2=. The /powermultiset/ of =S= is written as =S^+= (a circled plus sign) and is simply the set of =X_S^{N_0}(s)>0= with a finite number of =s= in =S=.

Squared =U= will be used for the disjoint union.

-----

Remark 2.2.8:* The =f= of the left is the mentioned "notation abuse". Since =f : S1 -> S2^+=, the left =f= would be some =F : S1^+ -> S2^+= such that for a multiset =X_S1=, for all =s1= of =S1= =F(X_S1)= is the union of =X_S1(s1) * f(s1)= (the scalar =X_S1(s1)= applied to the multiset =f(s1)=).

Formal definition

A Petri net =N= is a quadruple =(P_N, T_N, °(-)_N, (-)°_N)=:

=P_N= :: finite set of places;
=T_N= :: finite set of transitions;
=°(-)_N : T_N -> P_N^+= :: input places of each transition;
=(-)°_N : T_N -> P_N^+= :: output places of each transition.

=P_N= and =T_N= are disjoint!*

=°(t)_N(p)= is the weight of place =p= going into transition =t= -- input weight; =(t)°_N(p)= is the weight of place =p= coming out of transition =t= -- output weight.

As mentioned later on *Def2.3.7*, =°(-)_N= and =(-)°_N= needn't be disjunctive, that is, a place may be simultaneously an input and an output place of a transition.

Remark 2.3.3:* Similar to *Rem2.2.8*, this is just the =fmap= of =°(-)_N= and =(-)°_N=.

Markings

/Markings/ are the (so called) "states" of a Petri net, that is, the number of tokens currently in each place: =X_{P_N}^{N_0}=.

Definition 2.3.5:* Formally, a transition =t= is enabled if =°(t)_N < X^N= (is contained in).

Remark 2.3.6:* A function that determines whether some transition is enabled given a marking. Also a function that

Firing

Definition 2.3.7:* How a transition "fires": =N_X --t-> N_Y= means =t= fires carrying =N= from (state/marking) =X= to =Y=. The third condition of the conjunction represents the transfer of tokens: =Y^N = X^N - °(t)_N + (t)°_N=.

Remark 2.3.8:* Again, similar to *Rem2.3.3* and *Rem2.2.8*, this is just the =fmap= of =N_X --t-> N_Y=.

Examples

Example 2.4.2:* Very weird and interesting! Petri nets are very different from automata in that there isn't one single active/current place ("state" in automata theory); instead the state of the net is really just the markings, as defined previously, because that is the only mutable "state" of the net, and thus has necessarily to define the "meaning" of the current "state". Plus, since there isn't one active/current place, and several transitions may be enabled simultaneously, several transitions may fire simultaneously as well, thus (methinks) modeling concurrent behaviour! Assuming the "requirements" (input tokens) of all the transitions don't collide, or prevent each other(1).

(1) e.g., if transitions =t1= and =t2= have both a single input of 1 token from the same place, and that place a single token in it, then both transitions are enabled, but they can't fire simultaneously.

Reachability, safety, deadlocks

Definition 2.5.1:* For some Petri net =N= in state =X=, we say that state =Y= is reachable from =X= if there's a finite sequence of transitions =s = (t0, t1, ..., tn-1, tn)= such that =X --t0-> X1 --t1-> ... --tn-1-> Xn --tn-> Y= -- or simply =X --s-> Y=.

Definition 2.5.3:* A Petri net =N= in state =X= is said to be deadlocked if there's some state =Y= reachable from =X=, where no transition is enabled.

So a net is considered deadlocked even if the deadlock state isn't for sure to be reached? E.g., if it is possible to reach =Y= and =Z= from =X=, such that =Y= never reaches a deadlock state, but =Z= is a deadlock state (or it is certain to lead to a deadlock state), then =X= is considered deadlocked?

Definition 2.5.5:* Of a net =N= in state =X=, a transition is said to be

Dead :: if it is never enabled; (There's no reachable state where the transition is enabled?)
Alive :: if there's some state =Y= reachable from =X= where the transition is enabled. (Reworded definition, that I think is equivalent but simpler)

A net in a certain state is said to be alive if all its transitions are alive. In other words, when a net is alive in a certain state, all its transitions can (inevitably) eventually fire (in some future state).

An alive transition may become dead, that is, being alive doesn't guarantee that it will /always/ eventually be enabled (see the following remark).

Remark 2.5.6:* A transition needn't necessarily be dead or alive, there are intermediate degrees of "aliveness". E.g., =t= is enabled (therefore alive) in

state =X=, but after =X --t-> Y=, on =Y= it becomes dead.

Definition 2.5.8:* A place of a net in state =X= is said to be =k=-bounded if it doesn't contain more than =k= tokens in any of the states reachable from =X=. a place is said to be bounded if it is =k=-bounded for some =k=. A net is said to be =k=-bounded (resp. bounded) if all its places are =k=-bounded (resp. bounded). And a net is said to be /safe/ if it is 1-bounded.

Remark 2.5.10:* Making a non-bounded place bounded is as simple as adding a =k=-semaphore, that is, adding an extra place with =k= tokens, making it an input of the ("producer") transition(s), that make the unbounded place unbounded, and an output of the ("consumer") transition(s), that consume tokens off the unbounded place. For an example see *Fig2.11*, a bounded version of *Fig2.6*.

Implementation

GreatSPN

Why is this useful?

Behavioral Programming with Petri Nets à la Functional Way -- Smart Contracts

Category Theory

What is category theory?

References [[id:56c62b63-739f-43d1-a5f7-afa4119cc425][/Mathematics: Form and Function/, Saunders MacLane]].

Mentions /compositionality/.

Definition 3.1.1:* The expected definition. A category =C= consists of a set of objects (=Obj C=), a set of morphisms (=Hom_C=), a domain and codomain function (=s(-)= and =t(-)=), a composition partial function (=(-);(-)=), and an identity function (=Obj C -> Hom_C=).

References [[id:570ea143-65ce-4e14-a713-e7ef5b450e5a][/Categories for the Working Mathematician/, Saunders MacLane]].

Remark 3.1.8:* The collection of objects of a category are a class, not just any set. This detail is probably safe to ignore for our purposes.

Class

Remark 3.1.9:* Commutative diagrams. See *Fig3.1*.

Definition 3.1.10:* Isomorphisms.

Functors, natural transformations, natural isomorphisms

Definition 3.2.1:* Functors. Nothing new here either.

Definition 3.2.6:* We can make a category of categories, with functors as morphisms, and the concept of isomorphism extends to this category. That is, a functor is an isomorphism if it has an inverse, and the (pre or post) composition of itself with its inverse is the identity functor.

Definition 3.2.7:* The definition of an isomorphic functor is too strong. So instead, the definitions of /full/ (pleno) and /faithful/ (fiel) are used together for the idea of "equivalence" of categories (presented next). The idea of a /full/ functor is similar to the idea of surjectiveness (for both objects and morphisms); and the idea of a /faithful/ functor is similar to that of injectiveness (for both objects and morphisms).

Definition 3.2.8:* Two categories =C= and =D= are said to be equivalent if there exists a /fully faithful/ functor =F : C -> D=, and each object of =D= is isomorphic to some object =F A= (for some object =A= of =C=).

Definition 3.2.9:* A /natural transformation/ is a way to transform one functor into another in a diagram, such that the diagram still commutes for any objects used. More strictly, for functors =F,G:C->D=, the natural transformation =eta : F -> G= is the set of all morphisms =eta_A : F A -> G A=, for all objects =A= of =C= -- these morphisms are called "components".

Definition 3.2.10:* A natural transformation =eta : F -> G= is said to be a natural isomorphism if all of its components are isomorphisms in the category =D= (the target category).

Monoidal categories

Definition 3.3.1:* A monoidal structure of a category =C= consists of a functor called (monoidal) /product/, some object =I= of =C= to be used as the /monoidal unit/, the natural isomorphism =alpha_A,B,C : (A*B)*C -> A*(B*C)= (expressing that the product is associative), and the natural isomorphisms =lambda_A : I*A -> A= and =rho_A : A*I -> A= (expressing that the unit behaves as a unit in the product). Additionally, the natural isomorphisms have to respect some extra conditions (coherence conditions), of *Fig3.3*. A category with a monoidal structure is called a /monoidal category/.

Definition 3.3.8:* If nothing is said, a monoidal structure *is not* commutative! That is, =A*B= is different from =B*A=, *and* you may not go from one to the other. For this property, a /symmetric monoidal category/ is necessary, which on top of the previously defined properties, adds a natural isomorphism =sigma_A,B : A*B -> B*A=, called /symmetry/ (or /swap/). It obviously has the property that =sigma_B,A . sigma_A,B = id_A*B=.

Definition 3.3.11:* A strict monoidal category is a monoidal category where associators and unitors are identities. That is, =(A*B)*C = A*(B*C)= and =I*A = A = A*I=.

Mentions [[id:82994ef9-43fe-4437-be77-52ccb2b4e1ba][/Picturing Quantum Processes/, Bob Coecke, Aleks Kissinger]].

Mentions [[id:9c2f7406-83e7-4f7a-8d96-14d942157c3f][/A Survey of Graphical Languages for Monoidal Categories/, Bob Coecke]].

Monoidal functors

Definition 3.5.1:* Lax monoidal functor.

Definition 3.5.2:* Symmetric, strong, strict monoidal functor.

Remark 3.5.3:* If a functor =F= is symmetric and strict, then *Fig3.9* implies =F sigma_A,B = sigma_F A, F B=.

Products, coproducts, pushouts

Definition 3.6.2:* Products. A category =C= has products when for any two objects =A= and =B= of =C=, there are morphisms =p1 : A*B -> A= and =p2 : A*B -> B=, and for any two morphisms =f : C -> A= and =g : C -> B=, for some object =C=, there's a morphism =<f, g> : C -> A*B=, such that the diagram of Fig3.10 commutes.

Definition 3.6.5:* Coproducts (sums).

Executions of Petri nets

Problem overview

Distinguishing between tokens becomes important, since different tokens will be processed differently by transitions.

Remark 4.1.2:* Petri nets can't tell the difference between two tokens.

Remark 4.1.3:* /Tokens are considered to represent the same resource if they have the same history,/ with history meaning the path that resulted in the token. For example, in *Fig4.1* =t1= may produce tokens that are different from those produced by =t2=. Thus the result of =t3= may differ depending on whether the token was produced by =t1= or =t2=. See *Eg4.1.1*.

Remark 4.1.4:* Briefly discusses different approaches to formalize Petri nets as categories, with references.

The category Petri

Definition 4.2.1:* A multiset homomorphism is a function =g : P → T= (with =P= & =T= multisets), such that =g(∅ₚ) = ∅ₜ= and =g(p₁ ∪ p₂) = g(p₁) ∪ g(p₂)=.

Proposition 4.2.3:* Given a function =g : P → T= (with =P= & =T= sets), it can be extended to a multiset homomorphism. (See PDF for definition)

Definition 4.2.4:* If =g= is the multiset homomorphism extended from a function =h=, =g= is said to be /grounded/.

Definition 4.2.5:* A morphism between Petri nets =N= and =M= is specified by a pair =<f, g>= of functions where =f : T_N → T_M=; =g= is a multiset homomorphism between the multisets over =P_N= and =P_M=, respectively; and the diagrams of *Fig4.2* commute, i.e., =°(-)_M · f = g · °(-)_N= & =(-)°_M · f = g · (-)°_N=, that is, the input and output multiplicities are maintained.

Remark 4.2.6:* Given net morphism =s : N → M=, =M= can be thought of as being a "super net" of =N=, in that, a subnet of =M= simulates =N=, according to morphism =s=.

Definition 4.2.7:* The category *Petri* is that whose objects are Petri nets, and the morphisms are net morphisms, as defined in *Def4.2.5*. It's easy to define the identity morphisms and morphism composition so that *Petri* is indeed a category.

Definition 4.2.8:* The *Petri_G* sub-category of *Petri*, where the places multiset homomorphism (the right component of the net morphism) must be grounded.

The Execution of a net

Markings are represented by the product of places of the net.

Example 4.3.2:* The "life" of a net, i.e., in what order transitions fire, and what tokens they consume/produce, can be represented as a string diagram. See *Fig4.3* & *Fig4.4*.

Remark 4.3.3:* There necessarily has to be a swap operation in the markings category. See *Fig4.5*.

Remark 4.3.4:* The same firing sequence may correspond to more than one string diagram. *Fig4.6* has examples of string diagrams that represent the firing sequence of *Fig4.1*.

Free strict symmetric monoidal categories (FSSMCs)

Definition 4.4.1:* (Finite-length) Strings generated by some set (=S^*=; the "power" set of a set in language theory).

Remark 4.4.2:* Bixo! =S ∈ Obj(C) ⇒ S^* ∈ Obj(C)= because =C= is a monoidal category.

Thinking of =S= as the set of places of a net, =S^*= are the objects of =C=.

Definition 4.4.4:* (Too many details to note here) A category =C= is a FSSMC if it's generated by some =S= and =T= (explained in the text). Explains the "plumbing" of transition firings too, i.e., a huge composition of morphisms, to deal with the order of tokens in a given state (which is a sequence of tokens).

Notes that Categories require the identity morphisms and associativity of composition, but requiring isn't the same as guaranteeing, and so *Axioms (4.3)* are there to provide for them.

Remark 4.4.8:* FSSMCs are called free because they satisfy only the bare minimum amount of equations to be a strict symmetric monoidal category.

Definition 4.4.9:* Abusing notation/terminology: we'll call "symmetry" a morphism obtained by composing sequentially and monoidally identities and symmetries. That is, a morphism that changes the order of the elements of a product: =A*B*C → C*B*A=, as in *Fig4.7*.

Definition 4.4.12:* TODO wut?

Lemma 4.4.13:* The composition of generator-preserving functors is a generator-preserving functor. Proof in /Computational Petri Nets: Adjunctions Considered Harmful/.

Definition 4.4.14:* =FSSMC= is the category of FSSMCs as objects and generator-preserving functors as morphisms.

Lemma 4.4.15:* A generator-preserving functor is called grounded if it maps generating objects to generating obejcts. Composition of grounded functors is grounded, and the identity functor on any FSSMC is grounded. Hence FSSMCs and grounded functors between them form a subcategory of =FSSMC=, denoted with =FSSMC_G=.

The categories =F(N)= and =U(C)=

Definition 4.5.1:* The multiplicity of =s∈S= in a sequence =S^*= is the number of occurrences in the sequence: =M_S(str)(s)=.

Definition 4.5.3:* TODO An ordering function on =S= is a function =D_S : S^+ → S^*= such that =M_S . D_S = id_{S^+}=. +That is, orderings are permutations; or, orderings are the sets of all permutations of certain multiplicities.+ Calculates a sequence of a given multiplicity.

Remark 4.5.5:* To simplify things, Petri nets are assumed to have a fixed ordering, and these are called "ordered Petri nets".

Remark 4.5.6:* Ordered Petri nets don't require any change to the theory. Proof in /Computational Petri Nets: Adjunctions Considered Harmful/.

Remark 4.5.7:* Ordered Petri nets can be represented in a computer. Abstractly, for a Petri net, one requires a type of places and another of transitions, and two functions to define inputs and outputs. For ordered Petri nets the extra requirement is that the type of places be ordered, so that making an ordering procedure is easily achieved. Details in /Computational Petri Nets: Adjunctions Considered Harmful/.

Definition 4.5.8:* =F(N)= is the category of executions of a Petri net =N= (see *Def4.4.4* for details).

Definition 4.5.9:* TODO =U= is the inverse of =F=: from an execution (in FSSMC), it associates a Petri net.

Lemma 4.5.10:* ∀ Petri net =N=: =U(F(N))= and =N= are isomorphic. ∀ FSSMC =C=: =F(U(C))= and =C= are isomorphic. *NOTE:* This does not imply that the categories of Petri nets and FSSMCs are isomorphic!

Functors between executions

There is no general functorial definition for functors from Petri net morphisms to generator-preserving functor(?).

Lack of functoriality is not the end of the world

The fact established in the previous section is not such a big deal when the intent is to implement a programming language. Argues that the fact that FSSMCs use strings as part of their definition is actually a win for programming language implementers, the reason being that, historically, strings (sequences of elements, i.e., arrays) are one of the basic data structures available in programming languages.

This "manipulating strings is way easier than manipulating multisets" argument is doubtful...

Beyond standard Petri nets

Discusses slightly different Petri nets, such as /integer Petri nets/, where tokens may negative. Mentions /Executions in (Semi-)Integer Petri Nets are Compact Closed Categories/ and /Generalized Petri Nets/.

Briefly discusses how integer Petri nets may be used to represent (real) distributed behaviour with a simple example (*Fig4.10*): two entities (connected through the internet) choose simultaneously to fire a transition, that wouldn't be possible in a standard Petri net, were both transitions fired sequentially.

Also gives the idea that integer Petri nets may be used to represent faulty subnets of the system (i.e., bugs).

Fig4.11* shows the axioms that the cup and cap morphisms must satisfy; and *Fig4.12* has an example of the cup and cap solving a conflict, where the sequence of firings in real-world time is different from the sequence of firings of the network, with cup and cap twisting the flow of "network time" into a legal firing sequence.

Also, the two events (users) think they fired first (because otherwise the one that fired second wouldn't have fired at all!). This is another conflict. While the network sequence of firings can be reconstructed with cup&cap if one knows the (absolute) real-world sequence of firings, each independent event (user) can't, because their (relative) real-world times differ.

Mentions /On the Category of Petri Net Computations/, [[id:96d36d95-0dc6-4f3b-a066-d3e03bbd0586][/Compositional Game Theory/]], and /Representations of Petri Net Interactions/.

Implementation

They're using (still? or has this changed in the meantime?) Idris to build the formal basis of the project. Specifically, they're using =idris-ct= as a start.

Why is this useful?

They present the "traditional" way of using Petri nets: model the system as a Petri net and verify the needed/desired properties; manually convert the net into code. This approach has at least a couple of problems: for one, Petri nets are only used as modelling tool, not a programming one; the manual Petri net to code conversion is error prone, which could lead to bugs.

They seem to imply that Statebox is looking to do things differently. Are they?

Folds

Problem Overview

In *Eg5.1.1* and *Eg5.1.2* presents the "problem", and an argument in favor of, of Petri nets not being able to represent algorithms in general (quicksort specifically in the examples). The counterargument by Statebox is "the right tool for the job": Petri nets could be used to specify more of the behaviour of an algorithm such as quicksort, but it's not their strong point. On top of that, many correct and performant implementations of these algorithms (such as quicksort) already exist, so writing them with Petri nets wouldn't be a good use of someone's time.

This seems to support my supposition that they seemed to imply that they don't mean to make yet another modelling tool but a real programming language based on Petri nets.

Mapping executions

They describe a Petri net as "infrastructure" in *Eg5.2.1*.

Definition 5.2.2:* ∀ =N= Petri net, =S= symmetric monoidal category: a fold for =N= is a symmetric lax monoidal functor (*Def3.5.1*) =F(N) → S=.

Remark 5.2.3:* There's a trivial fold, the identity. (=F= stands for "fold", and is the reason why it's used to denote the executions of a net)

Definition 5.2.4:* Defines *Hask*, the category of Haskell.

Remark 5.2.5:* *Hask* is not quite the category of Haskell? *Hask* is the so-called /platonic Haskell category/, as described in [[id:59740c4d-6149-4cfd-8e9e-1422164bb6ee][Hask]].

Example 5.2.6:* The fold =F : F(N) → Hask=.

Remark 5.2.7:* TODO wut?

Example 5.2.8:* Quicksort (in code) is used as a transition of a net.

Remark 5.2.9:* Totality and how it relates to Petri nets. Non-terminating transitions (functions) consume tokens but don't produce them. This obviously breaks the system, and properties are no longer ensured.

Different folds, shared types

Brings up the idea of subnets in folds, or composition of nets.

Definition 5.3.1:* There are morphisms between folds, and all together form a category. =F1 : F(N) → S1=, =F2 : F(N) → S2= folds, a morphism of folds =G : S1 → S2= is a lax monoidal functor such that =G·F1 = F2=.

Remark 5.3.2:* TODO More CT fuckery.

Why is this useful?

Mentions [[id:dbf1e72e-2acc-4c40-98c7-6c22512dc534][Typedefs]].