22 June 2018

Different Flavors of Petri Nets and Their Monads

by Jade Master


I have a question about the correspondence between Lawvere theories and finitary monads. I feel uneasy about asking it without giving some context so I have provided some. On the other hand, if you don't have much familiarity with the theory of Petri nets you may have trouble following the next section. If you want me to explain something please ask, I am very happy to do so.
Why I am interested in the correspondence
I am trying to understand how different types of Petri nets relate to each other. A friend of mine had the great idea that Petri nets are functors $ F: C \to \mathrm{Kl}(\mathbb{N}))$ where $ C$ is the category of two parallel arrows and $ \mathrm{Kl}(\mathbb{N})$ is the Kleisli category of the free commutative monoid monad N. in general there is an equivalence
$ \mathtt{Petri} \cong [ C, \mathrm{Kl}(\mathbb{N}) ]$
This definition lends itself to generalization: if you replace $ \mathbb{N}$ with $ <>$, the free monoid monad, you get the category of pre-nets. Pre-nets have a much smoother way of presenting free symmetric monoidal categories. That is there is straightforward left adjoint from the category of Petri nets to a category whose objects are a special type of monoidal categories. In section 3 of this paper they talk about this functor compare this functor with a corresponding functor for regular Petri nets. See this paper by Vladimiro Sassone where he fixes an earlier attempt at presenting Petri nets at cost of making it a pseudofunctor .
There is another type of Petri net called integer nets which Fabrizio Genovese and Jelle Herold wrote about in their shiny new paper. The nice thing about integer nets is that they present free compact closed categories. In terms of applications, this allows for the concept of borrowing resources when performing a process represented by an integer net. In a similar way to pre-nets and Petri nets, we have an equivalence of categories
$ \mathbb{Z}-\mathtt{Net}\cong [C,\mathrm{Kl}(\mathbb{Z})]$
where $ \mathbb{Z}$is the free abelian group monad.
It seems to me that these different flavors of Petri nets are hinting at a bigger picture. With this in mind I am interested in trying to understand the relationship between the categories $ [ C, \mathrm{Kl}(T)]$ for different monads $ T$. I am starting with $ T=\mathbb{N}$ and $ T=<>$.
The Question
Let Th($ \mathbb{N}$) be the Lawvere theory for commutative monoids and let Th($ <>$) be the Lawvere theory for monoids. I claim that there is a morphism of Lawvere theories  from Th($ <>$)  to Th($ \mathbb{N}$) which is the identity on objects and morphisms but there isn't a morphism of Lawvere theories in the other direction.
Suppose there were a product preserving functor $ F : \mathrm{Th}(\mathbb{N}) \to \mathrm{Th}(<> )$. Then it would have to be the identity on objects and morphisms as well because this the only option which preserves arities on the morphisms. Because $ m \circ \tau = m$ in Th($ \mathbb{N}$) where $ m$ is the multiplication map and $ \tau$ is a symmetry
 $ F(m \circ \tau) = F(m) \circ F(\tau) = m \circ \tau \neq m$.
By the equivalence between Lawvere theories and finitary monads this should induce morphism of monads $ A : <> \to \mathbb{N}$. That is for each set $ X$, a function
$ A_X : <X> \to \mathbb{N}[X]$
satisfying certain axioms. I am hoping that this is given by abelianization. In a more straightforward way, F induces a functor in the opposite direction between the models of Th($ \mathbb{N}$) to the models of Th($ <>$)
$ F^* : \mathrm{Mod} ( \mathrm{Th}(\mathbb{N})) \to \mathrm{Mod}(\mathrm{Th} (<>))$.
This functor takes a model $ f : \mathrm{Th} \mathbb{N} \to Set$ and precomposes it with the functor $ F$. You can work this out yourself but the effect is that it takes a commutative monoid and does nothing to it except forget that its commutative.  It turns out that abelianization is a left adjoint to $ F*$. This is what I think should constitute the morphism of monads from $ <>$ to $ \mathbb{N}$.  I am hypothesizing that this is true in general. For a morphism of Lawvere theories $ F: S \to T$ to get the corresponding morphism of monads, you
  1. Take the functor $ F^* : \mathrm{Mod}(T) \to \mathrm{Mod}(S)$
  2. Take its left adjoint $ G$
  3. Then the components of the monad morphism are given by this functor $ G$.
Does anyone know if this is true? I can't find a reference for this which I have managed to understand. So really I am looking for someone to explain to me, in the context of a specific example, how to turn a morphism of Lawvere theories into a morphism of monads.

tags: