Petri Nets Based on Lawvere Theories

TL;DR

This paper introduces a generalized framework for Petri nets based on Lawvere theories, unifying various existing variants and providing a functorial, categorical semantics for these models.

Contribution

It defines $ ext{Q}$-nets as a generalization of Petri nets using Lawvere theories, establishing their functoriality and categorical semantics.

Findings

Unified framework for various Petri net variants

Functorial semantics for $ ext{Q}$-nets

Construction of semantics for multiple net types

Abstract

We give a definition of $\mathsf{Q}$-net, a generalization of Petri nets based on a Lawvere theory $\mathsf{Q}$, for which many existing variants of Petri nets are a special case. This definition is functorial with respect to change in Lawvere theory, and we exploit this to explore the relationships between different kinds of $\mathsf{Q}$-nets. To justify our definition of $\mathsf{Q}$-net, we construct a family of adjunctions for each Lawvere theory explicating the way in which $\mathsf{Q}$-nets present free models of $\mathsf{Q}$ in $\mathsf{Cat}$. This gives a functorial description of the operational semantics for an arbitrary category of $\mathsf{Q}$-nets. We show how this can be used to construct the semantics for Petri nets, pre-nets, integer nets, and elementary net systems.

Equations

$$\mathsf{Petri}$$

$$\mathsf{Q}\text{mathchar}45\mathsf{Net}$$

$$\mathbb{N}:\mathsf{Set}\to \mathsf{Set}$$

$$T\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$(f,g)\circ (f^{\prime },g^{\prime })=(f\circ f^{\prime },g\circ g^{\prime }).$$

$$a\otimes b=b\otimes a\text{ and }f\otimes g=g\otimes f.$$

$$\mathsf{Set}$$

$$T$$

$$T\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$f_{\ast }:\mathsf{Mod}(\mathsf{R})\to \mathsf{Mod}(\mathsf{Q})$$

$$f^{\ast }:\mathsf{Mod}(\mathsf{Q})\to \mathsf{Mod}(\mathsf{R})$$

$$\mathsf{Mod}(\mathsf{Q})\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$M^f=R_{\mathsf{Q}}\eta L_{\mathsf{Q}}:M_{\mathsf{Q}}\Rightarrow M_{\mathsf{R}}$$

$$(-)\text{mathchar}45\mathsf{Net}:\mathsf{Law}\to \text{Cat}$$

$$T$$

$$\mathsf{PreNet}$$

$$e:0\to 1\text{, }i:1\to 1\text{, and }m:2\to 1$$

$$T\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$T$$

$$m:2\to 1\text{ and }e:0\to 1$$

$$2$$

$$2^{(-)}:\mathsf{Set}\to \mathsf{Set}$$

$$c\text{mathchar}45\mathsf{Net}:\mathsf{PreNet}\to \mathsf{Petri}$$

$$b\text{mathchar}45\mathsf{Net}:\mathsf{Petri}\to \mathbb{Z}\text{mathchar}45\mathsf{Net}$$

$$a\text{mathchar}45\mathsf{Net}:\mathsf{Petri}\to \mathsf{SLAT}\text{mathchar}45\mathsf{Net}$$

$$\mathsf{Set}\downarrow (\times \circ \Delta \circ M_{\mathsf{Q}})$$

Full text

1 Introduction

Following the introduction of Petri nets in Carl Petri’s 1962 thesis [23], there has been an explosion of work on Petri nets. The bibliography hosted by Petri Nets World has over 8500 citations [22]. These papers include many variations of Petri nets which change both the structure of the nets and their semantics. In this work we help organize these definitions by putting some of the more popular variants under a common framework.

Petri nets can be thought of as commutative monoidal graphs: graphs whose edges have elements of a free commutative monoid as their source and target. In this paper we generalize this to graphs which are based in some other algebraic gadget — as long as that gadget comes from a Lawvere theory. Petri nets are given by a pair of functions from a set of transitions to the free commutative monoid on a set of places. For a Lawvere theory $\mathsf{Q}$, a $\mathsf{Q}$-net is a pair of functions from a set of transitions to a free model of $\mathsf{Q}$ in $\mathsf{Set}$.

Many instances of this generalization are already studied. In 2000 Bruni, Meseguer, Montanari, and Sassone introduced pre-nets; a type of Petri net that has a free non-commutative monoid on its places [7]. The semantics of these showcase the individual token philosophy, which distinguishes between identical tokens and keeps track of causality within sequences of processes. In 2018, Herold and Genovese introduced integer nets, a type of Petri net which has a free abelian group of places [14] and are similar to lending nets introduced in [3]. These are useful for modeling credit in propositional contract logic [11]. The last example of $\mathsf{Q}$-nets that we consider are elementary net systems [25]. These are Petri nets that can have a maximum of one token in each place. The above three examples give categories $\mathsf{PreNet}$, ${\mathsf{\mathbb{Z}}}\mathchar 45\relax\mathsf{Net}$, and ${\mathsf{SLAT}}\mathchar 45\relax\mathsf{Net}$ of pre-nets, integer nets, and elementary net systems respectively. These are given by setting $\mathsf{Q}$ equal to $\mathsf{MON}$ the Lawvere theory of monoids, $\mathsf{ABGRP}$ the Lawvere theory of abelian groups, and $\mathsf{SLAT}$ the Lawvere theory of semi-lattices in the definition of ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$.

To elegantly illustrate the power of Petri nets, Messeguer and Montanari show that they present free monoidal categories [21]. The objects in these monoidal categories are given by the markings of our Petri net and the morphisms represent all possible firing sequences of the transitions in sequence and in parallel. In general, a description of the operational semantics of Petri nets consists of an adjunction between a category of Petri nets and a category of strictly commutative, strictly associative monoidal categories (see Definition 2.6). There are many ways to do this. In [6] the authors construct an adjunction from $\mathsf{Petri}$ into a particular subcategory of $\mathsf{CMC}$, the category of commutative monoidal categories. Here we analyze and alter this adjunction to get an adjunction

[TABLE]

To justify our definition of $\mathsf{Q}$-nets, we take a similar tack. We show that every $\mathsf{Q}$-net presents a free model of the Lawvere theory $\mathsf{Q}$ in Cat by constructing an adjunction

[TABLE]

where $\mathsf{Mod}(\mathsf{Q},\textup{{Cat}})$ is the category of models of $\mathsf{Q}$ in Cat. To turn a $\mathsf{Q}$-net into a free model of $\mathsf{Q}$ in Cat, there are two steps which must be completed:

• •

the transitions of the $\mathsf{Q}$-net must be freely closed under the operations of $\mathsf{Q}$, and

• •

the transitions must be freely turned into a category by freely adding identities and composites.

Thus the adjunction $F_{\mathsf{Q}}\dashv U_{\mathsf{Q}}$ is constructed as the composite of two smaller adjunctions corresponding to these steps. This adjunction defines an operational semantics for $\mathsf{Q}$-nets. The objects and morphisms in the free $\mathsf{Q}$-category on a $\mathsf{Q}$-net represent all the possible firing sequences which can be built using composition and the operations and axioms of the Lawvere theory $\mathsf{Q}$.

An outline of this paper is as follows:

• •

In Section 2 we review definitions for Petri nets and their categorical semantics.

• •

In Section 3 we define $\mathsf{Q}$-nets, and we extend this definition to a functor from the category of Lawvere theories to $\mathsf{CAT}$. This allows us to explore various functors between different kinds of $\mathsf{Q}$-nets. We also show that the category ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$ is complete and cocomplete.

• •

In Section 4 we construct a semantics functor for Petri nets as a two part composite. This serves as a blueprint for the more general construction.

• •

In Section 5 we prove the main theorem of this paper. For every Lawvere theory $\mathsf{Q}$, there is an adjunction

[TABLE]

which gives the operational semantics of $\mathsf{Q}$-nets.

• •

In Section 6 we show how our main theorem can give categorical descriptions of existing forms of semantics for various types of $\mathsf{Q}$-nets. We show how to build the semantics of Petri nets, pre-nets, and integer nets using the individual and collective token philosophies. We also construct an operational semantics functor for elementary net systems.

• •

In Appendix A we give a brief introduction to Lawvere theories.

2 Petri Nets and Their Executions

Definition 2.1**.**

Let $L\colon\mathsf{Set}\to\mathsf{CMon}$ be the free commutative monoid functor, that is, the left adjoint of the functor $R\colon\mathsf{CMon}\to\mathsf{Set}$ that sends commutative monoids to their underlying sets and monoid homomorphisms to their underlying functions. Let

[TABLE]

be the free commutative monoid monad given by the composite $R\circ L$.

For any set $X$, $\mathbb{N}[X]$ is the set of formal finite linear combinations of elements of $X$ with natural number coefficients. The unit of $\mathbb{N}$ is given by the natural inclusion of $X$ into $\mathbb{N}[X]$, and for any function $f\colon X\to Y$, $\mathbb{N}[f]\colon\mathbb{N}[X]\to\mathbb{N}[Y]$ is the unique monoid homomorphism that extends $f$.

Definition 2.2**.**

We define a Petri net to be a pair of functions of the following form:

[TABLE]

We call $T$ the set of transitions, $S$ the set of places, $s$ the source function, and $t$ the target function.

Definition 2.3**.**

A Petri net morphism from the Petri net

\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t}$$\scriptstyle{s}$$\textstyle{\mathbb{N}[S]} to the Petri net \textstyle{T^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t^{\prime}}$$\scriptstyle{s^{\prime}}$$\textstyle{\mathbb{N}[S^{\prime}]}

is a pair of functions $(f\colon T\to T^{\prime},g\colon S\to S^{\prime})$ such that the diagrams

[TABLE]

commute.

Definition 2.4**.**

Let $\mathsf{Petri}$ be the category of Petri nets and Petri net morphisms, with composition defined by

[TABLE]

Our definition of Petri net morphism differs from the earlier definition used by Degano–Meseguer–Montanari [12] and Sassone [26, 27, 7]. The difference is that our definition requires that the homomorphism between free commutative monoids come from a function between the sets of places whereas the above references allow arbitrary commutative monoid homomorphisms. This difference of definition is present in our definition of the category of $\mathsf{Q}$-nets as well. With this change, the categories $\mathsf{Petri}$ and ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$ become complete and cocomplete as shown in Proposition 3.11.

Petri nets have a natural semantics which is described by the token game. This is a game where each place of a Petri net is equipped with a natural number of tokens. Players are then allowed to shuffle the tokens around in proportion given by their source and target. The token game is formalized by the notions of marking and firing.

Definition 2.5**.**

A marking of a Petri net P=\leavevmode\hbox to68.22pt{\vbox to25.78pt{\pgfpicture\makeatletter\hbox{\hskip 34.10933pt\lower-17.12357pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-34.10933pt}{-8.65971pt}\pgfsys@invoke{ }\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip 7.92186pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.61632pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{T}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 7.92186pt\hfil&\hfil\hskip 38.18745pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.88194pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\mathbb{N}[S]}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip 14.18748pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{{{}}}{{{}}}}{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-18.06561pt}{-4.00694pt}\pgfsys@lineto{5.1344pt}{-4.00694pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.33438pt}{-4.00694pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.90625pt}{-1.65417pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\scriptstyle{s}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{{{}}}{{{}}}}{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-18.06561pt}{-8.31248pt}\pgfsys@lineto{5.1344pt}{-8.31248pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.33438pt}{-8.31248pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.52951pt}{-14.9708pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\scriptstyle{t}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} is an element $m\in\mathbb{N}[S]$, or equivalently, a function $m\colon S\to\mathbb{N}$ which is zero on all but a finite number of elements. A firing of $P$ is a tuple $(\tau,x,y)$, where $\tau$ is a transition and $x$ and $y$ are markings of $P$ with $x-s(\tau)\geq 0$ and $x-s(\tau)+t(\tau)=y$.

Firings can be chained together in sequence: for a firing $(\tau,x,y)$ and a firing $(\sigma,y,z)$ we can define their composite as a tuple $(\sigma\circ\tau,x,z)$ where $\circ$ is a formal symbol. Firings can also be performed in parallel: for two firings $(\tau,x,y)$ and $(\tau^{\prime},x^{\prime},y^{\prime})$ there is a parallelization $(\tau+\tau^{\prime},x+x^{\prime},y+y^{\prime})$. This suggests that firings of a Petri net have the structure of a monoidal category. Meseguer and Montanari were the first to notice this and show how Petri nets can be turned into commutative monoidal categories [21].

Definition 2.6**.**

A commutative monoidal category is a commutative monoid object internal to Cat. Explicitly, a commutative monoidal category is a strict monoidal category $(C,\otimes,I)$, such that, for all objects $a$, $b$ and morphisms $f$, $g$ in $C$

[TABLE]

Note that a commutative monoidal category is the same as a strict symmetric monoidal category where the symmetry isomorphisms $\sigma_{a,b}\colon a\otimes b\stackrel{{\scriptstyle\sim}}{{\longrightarrow}}b\otimes a$ are all identity morphisms. In fact, a commutative monoidal category is precisely a category where the objects and morphisms form commutative monoids and the structure maps are commutative monoid homomorphisms. A commutative monoidal category where the morphisms represent sequences of firings of a Petri net $P$ will be referred to as a semantics for $P$. In this paper we characterize this semantics construction as an adjunction between the category of Petri nets and the following category.

Definition 2.7**.**

Let $\mathsf{CMC}$ be the category whose objects are commutative monoidal categories and whose morphisms are strict monoidal functors.

Note that every monoidal functor between commutative monoidal categories is automatically a strict symmetric monoidal functor, so the adjective symmetric is not included in the above definition.

3 Q-Nets

Petri nets need not have a free commutative monoid of places, and this aspect can be generalized using Lawvere theories. A review of the basic definitions and properties of Lawvere theories can be found in the appendix. As in Definition A.4, let $\mathsf{Mod}(\mathsf{Q})$ be the category of models of $\mathsf{Q}$ in $\mathsf{Set}$,

[TABLE]

be the adjunction generating free models of $\mathsf{Q}$ and let $M_{\mathsf{Q}}$ be the composite $R_{\mathsf{Q}}\circ L_{\mathsf{Q}}$.

Definition 3.1**.**

Let ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$ be the category where

• •

objects are $\mathsf{Q}$-nets, i.e. pairs of functions of the form

[TABLE]

• •

a morphism from the $\mathsf{Q}$-net

\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t}$$\scriptstyle{s}$$\textstyle{M_{\mathsf{Q}}S} to the $\mathsf{Q}$-net \textstyle{T^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t^{\prime}}$$\scriptstyle{s^{\prime}}$$\textstyle{M_{\mathsf{Q}}S^{\prime}}

is a pair of functions $(f\colon T\to T^{\prime},g\colon S\to S^{\prime})$ such that the following diagrams commute:

[TABLE]

This definition is a construction. Let $M_{\mathsf{Q}}$ be as before and let $M_{\mathsf{R}}\colon\mathsf{Set}\to\mathsf{Set}$ be corresponding monad induced by a Lawvere theory $\mathsf{R}$. Every morphism of Lawvere theories $f\colon\mathsf{Q}\to\mathsf{R}$ induces a functor

[TABLE]

which composes every model of $\mathsf{R}$ with $f$. A left adjoint

[TABLE]

is given by the left Kan extension of each model along $f$ [10, 9]. Now, we have the following commutative diagram of functors

[TABLE]

all of which have left adjoints. Given this set of assumptions, there is a morphism of monads $M^{f}$ given by

[TABLE]

where $\eta$ is the unit of the adjunction $f^{*}\dashv f_{*}$. This can either be verified directly, or by using the adjoint triangle theorem [13]. In what follows we will use this morphism of monads to translate between different types of generalized $\mathsf{Q}$-nets.

Definition 3.2**.**

Let

[TABLE]

be the functor which sends a Lawvere theory $\mathsf{Q}$ to the category ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$ and sends a morphism $f\colon\mathsf{Q}\to\mathsf{R}$ of Lawvere theories to the functor ${f}\mathchar 45\relax\mathsf{Net}\colon{\mathsf{Q}}\mathchar 45\relax\mathsf{Net}\to{\mathsf{R}}\mathchar 45\relax\mathsf{Net}$ which sends a $\mathsf{Q}$-net

[TABLE]

to the $\mathsf{R}$-net

[TABLE]

For a morphism of $\mathsf{Q}$-nets $(g\colon T\to T^{\prime},h\colon S\to S^{\prime})$, ${f}\mathchar 45\relax\mathsf{Net}(g,h)$ is $(g,h)$. This is well-defined because of the naturality of $M^{f}$.

Varying the Lawvere theory $\mathsf{Q}$ gives many known types of Petri nets.

Example 3.3**.**

Setting $\mathsf{Q}$ equal to $\mathsf{CMON}$, the Lawvere theory for commutative monoids, we obtain the category of Petri nets.

Definition 3.4**.**

Let $(-)^{*}\colon\mathsf{Set}\to\mathsf{Set}$ denote the monad that the Lawvere theory $\mathsf{MON}$ induces via the correspondence in [19]. For a set $X$, $X^{*}$ is given by the underlying set of the free monoid on $X$. A pre-net is a pair of functions of the form

[TABLE]

A morphism of pre-nets from a pre-net $(s,t\colon T\to S^{*})$ to a pre-net $(s^{\prime},t^{\prime}\colon T^{\prime}\to S^{\prime*})$ is a pair of functions $(f\colon T\to T^{\prime},g\colon S\to S^{\prime})$ which preserves the source and target as in Definition 2.3. This defines a category $\mathsf{PreNet}$.

Example 3.5**.**

If we take $\mathsf{Q}=\mathsf{MON}$, the Lawvere theory of monoids, we get the category $\mathsf{PreNet}$.

A description of $\mathsf{MON}$ can be found in the Appendix. $\mathsf{PreNet}$ has the same objects as the category introduced in Functorial Models for Petri Nets [7] but the morphisms are restricted as in Definition 2.3. Pre-nets are the same as tensor schemes introduced by Joyal and Street in ”The Geometry of Tensor Calculus I” [16]. The authors define a notion of free category on a tensor scheme and Bruni, Meseguer, Montanari, and Sassone construct an adjunction between pre-nets and a subcategory of the category of strict symmetric monoidal categories $\mathsf{SMC}$ [7].

In Section 6.1 we construct a closely related adjunction

[TABLE]

which does not require the restriction to a subcategory of $\mathsf{SMC}$. Pre-nets are useful because after forming an appropriate quotient, the category $Z(P)$ for a pre-net $P$ is equivalent the category of strongly concatenable processes which can be performed on the net. This equivalence is important for realizing the individual token philosophy [7]. The individual token philosophy, as opposed to the collective token philosophy, gives identities to the individual tokens and keeps track of the causality in the executions of a Petri net.

Example 3.6**.**

In 2013 Bartoletti, Cimoli, and Pinna introduced lending Petri nets [3]. These are Petri nets where arcs can have a negative multiplicity and tokens can be borrowed in order to fire a transition. Lending nets are also equipped with a partial labeling of the places and transitions so they can be composed and are required to have no transitions which can be fired spontaneously. In 2018 Genovese and Herold introduced integer nets [14]. Let $\mathsf{ABGRP}$ be the Lawvere theory of abelian groups. This Lawvere theory contains three generating operations

[TABLE]

representing the identies, inverses, and multiplication of an abelian group. These generating morphisms are required to satisfy the axioms of an abelian group; associativity, commutativity, and the existence of inverses and an identity. The category of integer nets, modulo a change in the definition of morphisms, can be obtained by taking $\mathsf{Q}=\mathsf{ABGRP}$ in the definition of ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$.

Definition 3.7**.**

Let $\mathbb{Z}\colon\mathsf{Set}\to\mathsf{Set}$ be the free abelian group monad which for a set $X$ generates the free abelian group $\mathbb{Z}[X]$ on the set $X$. Note that $\mathbb{Z}$ is the monad induced by the Lawvere theory $\mathsf{ABGRP}$ via the correspondence in [19]. An integer net is a pair of functions of the form

[TABLE]

A morphism of integer nets is a pair $(f\colon T\to T^{\prime},g\colon S\to S^{\prime})$ which makes the diagrams analogous to the definition of Petri net morphism (Definition 2.3) commute. Let ${\mathbb{Z}}\mathchar 45\relax\mathsf{Net}$ be the category where objects are integer nets and morphism are morphisms of integer nets.

Integer nets are useful for modeling the concepts of credit and borrowing. There is a correspondence between lending Petri nets and propositional contract logic; a form of logic useful for ensuring that complex networks of contracts are honored [3]. Genovese and Herold constructed a categorical semantics for integer nets [14]. In Section 6 we will construct a variation of this semantics which uses the general framework developed in this paper.

Example 3.8**.**

Elementary net systems, introduced by Rozenberg and Thiagarajan in 1986, are are Petri nets with a maximum of one edge between a given place and transition [25].

Definition 3.9**.**

An elementary net system is a pair of functions

[TABLE]

where $2^{S}$ denotes the power set of $S$.

Elementary net systems can be obtained from our general formalism. Let $\mathsf{SLAT}$ be the Lawvere theory for semi-lattices, i.e. commutative idempotent monoids. This Lawvere theory contains morphisms

[TABLE]

as in $\mathsf{MON}$ the theory of monoids. Also similar to $\mathsf{MON}$, $\mathsf{SLAT}$ is quotiented by the associativity and unitality axioms given in Example A.2. In addition, $\mathsf{SLAT}$ has the following axioms representing commutativity and idempotence

[TABLE]

where $\sigma\colon 2\to 2$ is the braiding of the cartesian product and $\Delta\colon 1\to 2$ is the diagonal. For models in $\mathsf{Set}$, The first diagram says that you can multiply two elements in either order and the get the same thing. The second diagram says that if you multiply an element by itself you get itself. As in Definition A.4, $\mathsf{SLAT}$ corresponds to a monad on $\mathsf{Set}$. It is well known that this monad is the covariant power set monad

[TABLE]

which sends a set $X$ to its power set and a function to the mapping which sends subsets of $X$ to their image. This motivates the following:

Definition 3.10**.**

Let ${\mathsf{SLAT}}\mathchar 45\relax\mathsf{Net}$ be the category of elementary net systems obtained as in Definition 3 for $\mathsf{Q}=\mathsf{SLAT}$.

The functorial nature of Definition 3 can be exploited to generate functors between different categories of $\mathsf{Q}$-nets. There is the diagram in Law

{\mathsf{SLAT}}$${\mathsf{CMON}}$${\mathsf{ABGRP}}$${\mathsf{MON}}$${\mathsf{GRP}}$$\scriptstyle{b}$$\scriptstyle{a}$$\scriptstyle{c}$$\scriptstyle{d}$$\scriptstyle{e}

where all the morphisms send their generating operations to their counterparts in the Lawvere theory of their codomain. These target Lawvere theories either have extra axioms or operations making the above functors not necessarily full or faithful:

• •

$a$ sends the morphism $m\circ\Delta$ in $\mathsf{CMON}$ to $id_{1}\colon 1\to 1$ in $\mathsf{SLAT}$ to impose the idempotent law. All other other generating components are sent to their natural counterparts.

• •

$b$ and $d$ send every object and morphism to its natural analog. However, $\mathsf{ABGRP}$ and $\mathsf{GRP}$ have an extra operation $i\colon 1\to 1$ representing inverses. This makes the functors $b$ and $d$ faithful but not full.

• •

$c$ and $e$ add the commutativity law; they send both the multiplication $m\colon 2\to 1$ and the composite $\sigma\circ m\colon 2\to 2$ of the braiding $\sigma\colon 2\to 2$ to the multiplication map $m\colon 2\to 2$ in the target Lawvere theory. This makes $c$ and $e$ not faithful.

Definition 3.2 can be used to give a network between different flavors of $\mathsf{Q}$-nets. By applying ${(-)}\mathchar 45\relax\mathsf{Net}$ to the above diagram we get the diagram of categories

{{\mathsf{SLAT}}\mathchar 45\relax\mathsf{Net}}$${\mathsf{Petri}}$${{\mathbb{Z}}\mathchar 45\relax\mathsf{Net}}$${\mathsf{PreNet}}$${{\mathsf{GRP}}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{{b}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{{a}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{{c}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{{d}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{{e}\mathchar 45\relax\mathsf{Net}}

The functors in this diagram are described as follows:

[TABLE]

is often called abelianization because it sends a pre-net to the Petri net which forgets about the ordering on the input and output of each transition. The authors of [7] use ${c}\mathchar 45\relax\mathsf{Net}$ to explore the relationship between pre-nets and Petri nets. The functor ${e}\mathchar 45\relax\mathsf{Net}\colon{\mathsf{GRP}}\mathchar 45\relax\mathsf{Net}\to{\mathbb{Z}}\mathchar 45\relax\mathsf{Net}$ gives the analogous relationship for integer nets.

[TABLE]

is the functor which does not change the source and target of a given place. The only difference is that the markings of a $\mathbb{Z}$-net coming from a Petri net are thought of as elements of a free abelian group rather than a free abelian monoid. ${d}\mathchar 45\relax\mathsf{Net}$ is the analogous functor for pre-nets.

[TABLE]

is the functor which sends a Petri net to the $\mathsf{SLAT}$-net which forgets about the multiplicity of the edges between a given source and transition.

Before moving on to the semantics of $\mathsf{Q}$-nets, we discuss a property of the category ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$.

Proposition 3.11**.**

${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$* is cocomplete.*

Proof.

We can construct ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$ as the comma category.

[TABLE]

where $M_{\mathsf{Q}}\colon\mathsf{Set}\to\mathsf{Set}$ is the monad corresponding to the Lawvere theory $\mathsf{Q}$, $\Delta\colon\mathsf{Set}\to\mathsf{Set}\times\mathsf{Set}$ is the diagonal, and $\times\colon\mathsf{Set}\times\mathsf{Set}\to\mathsf{Set}$ is the cartesian product in $\mathsf{Set}$. An object in this category is a map

[TABLE]

which corresponds to a pair of maps $s,t\colon T\to M_{\mathsf{Q}}S$ which become the source and target maps of a $\mathsf{Q}$-net. Morphisms in this comma category are commutative squares

[TABLE]

giving a map of $\mathsf{Q}$-nets $(f\colon T\to T^{\prime},g\colon S\to S^{\prime})$. The commutativity of the above square ensures that this map of $\mathsf{Q}$-nets is well-defined.

Theorem 3, Section 5.2 of Computational Category Theory [24] says that given $S\colon A\to C$ and $T\colon B\to C$ then the comma category $(S\downarrow T)$ is cocomplete if

• •

$S$ is cocontinuous and,

• •

$A$ and $B$ are cocomplete,

Because $\mathsf{Set}$ is cocomplete and the identity functor $1_{\mathsf{Set}}\colon\mathsf{Set}\to\mathsf{Set}$ preserves all colimits, we have that $\mathsf{Set}\downarrow(\times\circ\Delta\circ M_{\mathsf{Q}})$ is cocomplete. Because ${\mathsf{Q}}\mathchar 45\relax\mathsf{Net}$ is equivalent to this category, it is cocomplete as well. ∎

4 Generating Free Commutative Monoidal Categories From Petri Nets

In this section we examine in detail the motivating example for the main result of this paper, an adjunction generating the semantics of $\mathsf{Q}$-nets for every Lawvere theory $\mathsf{Q}$. This result can feel abstract on its own and the example of Petri nets provides invaluable intuition. A confident reader may skip this section, as it is not strictly necessary for the rest of this paper.

The operational semantics for Petri nets will take the form of an adjunction

[TABLE]

For a given Petri net $P$, this adjunction will be constructed in two steps: first the transitions of $P$ will be freely closed under a commutative monoidal sum and then freely closed under composition. This will take the form of factoring the adjunction into the composite

[TABLE]

Here a left adjoint is indicated by a bullet on the left and a right adjoint is indicated by a bullet on the right. $\mathsf{Grph}(\mathsf{CMon})$ is the category of graphs internal to $\mathsf{CMon}$.

Definition 4.1**.**

A commutative monoidal graph is a graph

[TABLE]

where $E$ and $V$ are commutative monoids and $s$ and $t$ are commutative monoid homomorphisms. A morphism of commutative monoidal graphs is a tuple of commutative monoid homomorphisms $(f\colon E\to E^{\prime},g\colon V\to V^{\prime})$ making the diagrams

[TABLE]

commute. This defines a category $\mathsf{Grph}(\mathsf{CMon})$ where objects are commutative monoidal graphs and morphisms are as above. In short, $\mathsf{Grph}(\mathsf{CMon})$ is the category of graphs internal to $\mathsf{CMon}$.

We will now define these adjunctions but omit the proofs that they are indeed well-defined adjunctions, as this follows from the more general results of Section 5. The left adjoint ${}^{\bullet}\mathrm{A}\colon\mathsf{Petri}\to\mathsf{Grph}(\mathsf{CMon})$ is defined as follows:

Definition 4.2**.**

Let

[TABLE]

be the functor which sends a Petri net

[TABLE]

to the commutative monoidal graph

[TABLE]

where $L$ is the left adjoint of the adjunction in Definition 2.1 and $\phi\colon\mathrm{Hom}(LT,LS)\xrightarrow{\sim}\mathrm{Hom}(T,RLS)$ is the natural isomorphism of that adjunction. ${}^{\bullet}\mathrm{A}$ sends a morphism of Petri nets

[TABLE]

to the morphism of commutative monoidal graphs given by

[TABLE]

In words, ${}^{\bullet}\mathrm{A}$ freely generates a commutative monoidal structure on the transitions of a Petri net and ${}^{\bullet}\mathrm{A}$ uniquely extends each component of a Petri net morphism to a commutative monoid homomorphism. The right adjoint of this functor is non-trivial:

Definition 4.3**.**

Let

[TABLE]

be the functor which sends a commutative monoidal graph

[TABLE]

to the Petri net

[TABLE]

$\bar{E}$ is defined as

[TABLE]

where $\epsilon_{V}$ is the counit of the adjunction $L\dashv R$. $\bar{s}$ and $\bar{t}$ are given by the projection of $\bar{E}$ onto its first and second coordinates respectively. $\mathrm{A}^{\bullet}$ sends a morphism of commutative monoidal graphs

[TABLE]

to the morphism of Petri nets

[TABLE]

where $h$ is the function which makes the assignment

[TABLE]

Remark 4.4**.**

Petri nets must have a free commutative monoid of places, so it is necessary to regard $RV$ as the set of places for $\mathrm{A}^{\bullet}Q$ rather than having $V$ be the commutative monoid of places itself. The reader at this point may guess a simpler formula for the right adjoint $\mathrm{A}^{\bullet}$ which keeps the $RE$ as the set of transitions and uses the unit of $\mathbb{N}$ to construct the source and target maps. Unfortunately this construction is doomed to fail. For a commutative monoidal graph {E}$${V}$$\scriptstyle{s}$$\scriptstyle{t} , suppose that the right adjoint ${}^{\bullet}\mathrm{A}$ sends this graph to the Petri net

[TABLE]

A problem arises because this process unnaturally chunks the source and target of each transition. To see this consider the commutative monoidal graph

[TABLE]

The edge $\tau$ in $Q$ can be depicted as

[TABLE]

With the above (faulty) description, $\mathrm{A}^{\bullet}Q$ is given by

[TABLE]

To avoid confusion, we denote the outer sum in $\mathbb{N}[\mathbb{N}^{3}]$ by $\times$ and the sum in $\mathbb{N}^{3}$ by $+$. Then, the faulty $\mathrm{A}^{\bullet}$ would turn $\tau$ into the transition

[TABLE]

To find a counit for this adjunction we seek a morphism

[TABLE]

A morphism of this sort is defined by its assignment on generators. A natural choice of morphism sends the places $a+b$ to the sum of the places $a$ and $b$ using the counit of $L\dashv R$. However, then the assignment of $\tau\mapsto\tau$ does not respect the source of $\tau$ and is therefore not a morphism of commutative monoidal graphs. The problem is that we want the source of $\tau$ in ${}^{\bullet}\mathrm{A}\mathrm{A}^{\bullet}Q$ to be $a\times b$ and not $a+b$. To fix this we force the source of $\tau$ to be $a\times b$ by upgrading $\tau$ to the tuple $(\tau,a\times b,c)$ in $\mathbb{N}[\tau]\times\mathbb{N}[\mathbb{N}^{3}]\times\mathbb{N}[\mathbb{N}^{3}]$. Now, the natural choice for the counit which sends $a\times b$ to $a+b$ respects the source of $\tau$.

The next part of the semantics adjunction for Petri nets freely generates the structure of a category on a given commutative monoidal graph. In Section 5 this is accomplished by rephrasing this construction in terms of free monoids. Here we provide an explicit description in the case of Petri nets.

Definition 4.5**.**

Let

[TABLE]

be the forgetful functor which sends a commutative monoidal category to its underlying commutative monoidal graph and a strict monoidal functor to its underlying morphism of commutative monoidal graphs. Then $\mathrm{B}^{\bullet}$ has a left adjoint

[TABLE]

which sends a commutative monoidal graph

[TABLE]

to the commutative monoidal category ${}^{\bullet}\mathrm{B}Q$ with objects given by $V$ and morphisms generated inductively by the rules:

• •

for every edge $e\in E$ a morphism $e\colon s(e)\to t(e)$,

• •

for every pair of morphisms $e\colon x\to y$ and $d\colon y\to z$, a morphism $d\circ e\colon x\to z$,

• •

for every object $v\in V$ a morphism $1_{v}\colon v\to v$

This defines an evident composition operation $\circ$ on ${}^{\bullet}\mathrm{B}Q$. There is also a sum on the ${}^{\bullet}\mathrm{B}Q$ defined using the sum of $V$ on objects. If $e$ and $e^{\prime}$ are edges of $Q$ then the morphisms $e\colon x\to y$ and $e^{\prime}\colon x^{\prime}\to y^{\prime}$ already have a sum given by

[TABLE]

The morphisms of ${}^{\bullet}\mathrm{A}Q$ are quotiented by the axioms:

• •

for all tuples of morphisms $(f\colon a\to b,g\colon b\to c,h\colon c\to d)$

[TABLE]

• •

for all morphisms $f\colon x\to y$

[TABLE]

• •

We require that composition is a commutative monoid homomorphism. For tuples of morphisms $(e\colon x\to y,d\colon y\to z,e^{\prime}\colon x^{\prime}\to y^{\prime},d^{\prime}\colon y^{\prime}\to z^{\prime})$ we can form their sum and composite in two different ways. We quotient the morphisms of ${}^{\bullet}\mathrm{B}Q$ so that these are equal, i.e.

[TABLE]

• •

We require that the assignment of identities is a commutative monoid homomorphism. For objects $x$ and $x^{\prime}$ in $V$ we set

[TABLE]

5 Semantics Functors for Generalized Nets

In this section we construct semantics categories for $\mathsf{Q}$-nets; categories whose morphisms represent possible sequences of firings which can be performed using a given $\mathsf{Q}$-net. Let $\mathsf{Q}$ be a Lawvere theory and let

[TABLE]

be the adjunction it induces on $\mathsf{Set}$. In this section we will use this adjunction to construct an adjunction

[TABLE]

which is analogous to the adjunction in Section 4 and where $\mathsf{Mod}(\mathsf{Q},\textup{{Cat}})$ is the category of models of $\mathsf{Q}$ in Cat. This adjunction factors as

[TABLE]

where ${}^{\bullet}\mathrm{A}_{\mathsf{Q}}$ freely generates a model of $\mathsf{Q}$ on the transitions of a given $\mathsf{Q}$-Net and ${}^{\bullet}\mathrm{B}_{\mathsf{Q}}$ freely generates the structure of a category on a given $\mathsf{Q}$-graph.

These adjunctions are heavily motivated by the case when $\mathsf{Q}=\mathsf{CMON}$ as this gives Petri nets. The main result of this paper is as follows:

Theorem 5.1**.**

There is an adjunction

[TABLE]

The left adjoint can be described using inference rules. Let $P$ be the $\mathsf{Q}$-net

[TABLE]

The objects of $F_{\mathsf{Q}}$ are given by $L_{\mathsf{Q}}S$. That is, for every morphism $o\colon n\to m$ in $\mathsf{Q}$ and every tuple of places $x_{1},x_{2},\ldots,x_{n}$ there is an object $\mathbf{o}(x_{1},x_{2},x_{3},\ldots,x_{n})$. For an equation of morphisms in $\mathsf{Q}$

{n}$${m}$${k}$$\scriptstyle{f}$$\scriptstyle{h}$$\scriptstyle{g}

the objects generated by each path must be equal. This means that there are $k$ equations of objects

[TABLE]

where the unlabeled index runs over the components of $f$ and the index $j$ runs over the components of $g$ and $h$. The morphisms of $F_{Q}P$ are generated inductively by the rules

[TABLE]

[TABLE]

and is quotiented to satisfy the following:

• •

The morphisms must satisfy the same equations that the objects satisfy. That is, for an equation of morphisms in $\mathsf{Q}$, the objects generated by each path must again be equal.

• •

$\mathrm{Mor}\,F_{\mathsf{Q}}P$ is quotiented to satisfy the axioms of a category including the associative and unital laws

[TABLE]

for all morphisms $f$, $g$ and $h$ in $\mathrm{Mor}\,F_{\mathsf{Q}}P$.

• •

$\mathrm{Mor}\,F_{\mathsf{Q}}P$ is quotiented so that the structure maps of a category (source, target, identity and composition) are $\mathsf{Q}$-model homomorphisms.

For a morphism of $\mathsf{Q}$-nets, $(f,g)\colon P\to P^{\prime}$, the $\mathsf{Q}$-functor

[TABLE]

is the unique extension of $f$ and $g$ which respects composition, unitality, and the operations of $\mathsf{Q}$. The proof will require several lemmas.

The first step is to construct an adjunction which freely closes the transitions of a $\mathsf{Q}$-net under the operations of $\mathsf{Q}$. In this adjunction we will write the monad $M_{\mathsf{Q}}$ as $RL$ and make use of the natural isomorphism

[TABLE]

for all sets $X$ and objects $Y$ in $\mathsf{Mod}(\mathsf{Q})$.

Definition 5.2**.**

Let

[TABLE]

be the functor which makes the assignment

[TABLE]

on objects and morphisms.

Lemma 5.3**.**

${}^{\bullet}\mathrm{A}_{\mathsf{Q}}$* is well-defined.*

The next few proofs will make heavy use of the naturality equations for $\phi$ and its inverse:

[TABLE]

and

[TABLE]

Proof.

First we show that $Le$ commutes with the source of ${}^{\bullet}\mathrm{A}_{\mathsf{Q}}P$. This follows from the chain of equalities:

[TABLE]

A similar equation holds for the target maps. ∎

Let $G$ be the $\mathsf{Q}$-graph

[TABLE]

Because $V$ is not a free model of $\mathsf{Q}$, there is no obvious forgetful way to turn this into a $\mathsf{Q}$-net. A first guess for the $\mathsf{Q}$-net $\mathrm{A}^{\bullet}_{\mathsf{Q}}(G)$ might be the $\mathsf{Q}$-net

[TABLE]

where $\eta_{RV}$ is the unit of the monad $M_{\mathsf{Q}}$ applied to the set $RV$. However, as explained in Remark 4.4, this fails to be a right adjoint. An alternative approach was suggested by Mike Shulman in the comments of an nCafé blog post [20]. This solution was inspired by the construction of the free category on a tensor scheme introduced in The Geometry of Tensor Calculus I [16]. Instead of using $RE$ as the set of transitions, we use

[TABLE]

where $\epsilon_{V}$ is the $V$ component of the counit for $M_{\mathsf{Q}}$. Here and in what follows we are using $s$ to denote $Rs$ and $t$ to denote $Rt$ for notational simplicity. The source and target maps of the resulting $\mathsf{Q}$-net are given by the projections of $\bar{E}$ onto its second and third coordinates. The set $\bar{E}$ can be described formally using pullbacks.

Definition 5.4**.**

Let

[TABLE]

be the functor which makes the assignment on objects and morphisms

[TABLE]

where

• •

$\bar{E}$ is the pullback of sets

[TABLE]

where $(s,t)$ denotes the pairing of $s$ and $t$, and $\epsilon_{RV}\times\epsilon_{RV}$ denotes the cartesian product of the counits.

• •

$\bar{s}\colon\bar{E}\to M_{\mathsf{Q}}RV$ is the composite

[TABLE]

and $\bar{t}\colon\bar{E}\to M_{\mathsf{Q}}RV$ is the composite

[TABLE]

that is the maps which send an element $(e,x,y)$ of $\bar{E}$ to its second and third coordinates.

• •

$\bar{f}\colon\bar{E}\to\bar{E^{\prime}}$ is induced by the universal property of $\bar{E}$ as shown below

[TABLE]

More simply, $\bar{f}$ makes the assignment

[TABLE]

Lemma 5.5**.**

$\mathrm{A}^{\bullet}_{\mathsf{Q}}$* is well-defined.*

Proof.

We must show that $(\bar{f},Rg)$ is a well-defined morphism of $\mathsf{Q}$-nets. $\bar{f}$ and $Rg$ commute with the source and target maps. Indeed, using the elementary descriptions we get that

[TABLE]

A similar equation holds for the target maps. $(\bar{f},Rg)$ commutes with the identity maps:

[TABLE]

where the last two steps follow from naturality of $\eta$ and $(f,g)$ being a morphism of $\mathsf{Q}$-graphs. ∎

Lemma 5.6**.**

$\mathrm{A}^{\bullet}_{\mathsf{Q}}$* is a right adjoint to ${}^{\bullet}\mathrm{A}_{\mathsf{Q}}$.*

Proof.

Let $P$ be the $\mathsf{Q}$-net

[TABLE]

and $Q$ be the $\mathsf{Q}$-graph

[TABLE]

We define a natural isomorphism

[TABLE]

by the rule

[TABLE]

$h$ is defined by the universal property induced by $\bar{E}$ and the diagram

[TABLE]

This diagram is well defined because $T$ is a competitor to the pullback $\bar{E}$ i.e. it makes the lowest triangle commute. Checking this amounts to showing that the bottom square commutes and this can be verified componentwise:

[TABLE]

and similar equations hold for the target maps. Therefore, $h$ is well defined. Explicitly $h$ is the map which makes the assignment on transitions in $T$

[TABLE]

$(h,\phi(g))$ is a well-defined morphism of $\mathsf{Q}$-graphs by construction. The source and target functions map elements to their second and third coordinates so the equation

[TABLE]

is true.

An inverse to $\Phi$,

[TABLE]

is defined as follows

[TABLE]

$a$ is defined by the universal property of $\bar{E}$ and the diagram

[TABLE]

To show that $(\phi^{-1}(a),\phi^{-1}(g))$ is a well defined morphism of $\mathsf{Q}$-graphs we perform the computation:

[TABLE]

where $\pi_{1}\colon RLRV\times RLRV\to RLRV$ is the projection and the last two steps follow from the definition of $\bar{s^{\prime}}$ and commutativity of the above diagram. This can be reduced using the fact that $h$ commutes with the source and target of $P$ and $\mathrm{B}^{\bullet}_{\mathsf{Q}}Q$ and naturality of $\phi^{-1}$. Indeed,

[TABLE]

A similar equation holds for target so this is a well-defined morphism of $\mathsf{Q}$-graphs. $\Phi$ is a natural isomorphism if it is a natural and a bijection in the places component and the transitions component. The places component is only an application of $\phi$ so it is both natural and a bijection. For the transition component let $D\colon C\to\mathsf{Set}$ be the diagram

[TABLE]

where $C$ is the walking cospan. Let $\Delta_{T}\colon C\to\mathsf{Set}$ be the constant diagram which sends every object to $T$ and every morphism to $1_{T}$. Then the universal property of $\bar{E}$ can be expressed as the natural isomorphism

[TABLE]

where $\mathrm{Nat}(\Delta_{T},D)$ denotes the set of natural transformations from $\Delta_{T}$ to $D$. With this description, the transition component of $\Phi$ can be described as follows

[TABLE]

where the angle brackets encase the components of a natural transformation. Similarly, the transition component of $\Phi^{-1}$ can be described as

[TABLE]

where the subscript $RE$ indicates that we take the $RE$ component of the natural transformation. With this description, we can verify that they are inverses on the transition component.

[TABLE]

and the other direction

[TABLE]

The transition component of $\Phi$ and $\Phi^{-1}$ are natural because they are made up of components which are individually natural transformations. ∎

The next step in the proof of Theorem 5.1, is to construct an adjunction between $\mathsf{Grph}(\mathsf{Mod}(\mathsf{Q}))$ and $\mathsf{Mod}(\mathsf{Q},\textup{{Cat}})$. A general property of algebraic theories $\mathsf{P}$ and $\mathsf{Q}$ is the property that models of $\mathsf{P}$ in the category of models of $\mathsf{Q}$ are the same as models of $\mathsf{Q}$ in the category of models of $\mathsf{P}$. In particular for a Lawvere theory $\mathsf{Q}$, a model of $\mathsf{Q}$ in Cat is the same as a category internal to $\mathsf{Mod}(\mathsf{Q})$ and this extends to an equivalence of categories

[TABLE]

Therefore, the adjunction we seek is between the categories $\mathsf{Grph}(\mathsf{Mod}(\mathsf{Q}))$ and $\textup{{Cat}}(\mathsf{Mod}(\mathsf{Q}))$ i.e. a construction of free categories internal to $\mathsf{Mod}(\mathsf{Q})$. The free category construction in this generality was first given in [5]. However, to build this adjunction we use a Theorem of Lack [17].

Theorem 5.7**.**

[Lack]* Let $(C,\otimes)$ be a monoidal category with*

• •

finite limits,

• •

countable colimits and,

• •

the functors $-\otimes A$ and $A\otimes-$ preserve reflexive coequalizers and colimits of countable chains.

Then $C$ admits a free monoid construction, that is, a left adjoint to the forgetful functor

[TABLE]

which sends every monoid to its underlying object of $C$.

By choosing an appropriate monoidal category we can use this construction to get free categories in $\mathsf{Mod}(\mathsf{Q})$. A span of $\mathsf{Q}$-models of the form

[TABLE]

is a graph in $\mathsf{Mod}(\mathsf{Q})$. This description can be used to describe a monoidal category of graphs over $V$.

Definition 5.8**.**

Let $\mathsf{Span}(V)$ be the monoidal category where

• •

objects are given by spans $s,t\colon E\to V$ in $\mathsf{Mod}(\mathsf{Q})$,

• •

morphisms are given by maps $f\colon E\to E^{\prime}$ making the diagram

[TABLE]

commute.

• •

monoidal product is given by chosen pullbacks. That is, for spans

[TABLE]

their monoidal product is the chosen pullback

[TABLE]

On morphisms $f\colon E\to E^{\prime}$ and $g\colon F\to F^{\prime}$ is the unique map

[TABLE]

induced by the universal property of $E^{\prime}\times_{V}F^{\prime}$.

A monoid in this monoidal category is a span $s,t\colon E\to V$ along with multiplication and unit maps

[TABLE]

satisfying associativity and unitality. Interpreting $\circ$ as composition and $e$ as the map assigning identity morphisms, this gives a category internal to $\mathsf{Mod}(\mathsf{Q})$. Indeed, a category with object model $V$ is exactly a monoid in the category $\mathsf{Span}(V)$ [4]. Therefore, if $\mathsf{Span}(V)$ satisfies the hypotheses of Theorem 5.7, it gives a construction of free categories in $\mathsf{Mod}(\mathsf{Q})$. The hypotheses of Theorem 5.7 require that the following conditions hold:

• •

$\mathsf{Span}(V)$ has finite limits and countable colimits. $\mathsf{Mod}(\mathsf{Q})$ has these limits and colimits as shown in Theorem 3.4.5 of [8]. The corresponding limits and colimits in $\mathsf{Span}(V)$ are computed on the apex of each span.

• •

The monoidal product of $\mathsf{Span}(V)$ preserves colimits of countable chains. This is true if pullbacks in $\mathsf{Mod}(\mathsf{Q})$ preserve these colimits.

• •

The monoidal product of $\mathsf{Span}(V)$ preserves reflexive coequalizers. This is true if pullbacks in $\mathsf{Mod}(\mathsf{Q})$ preserve reflexive coequalizers.

Corollary 3.4.3 of [8] states that finite limits commute with filtered colimits. In particular this means that pullbacks commute with colimits of countable chains and reflexive coequalizers. Therefore, Theorem 5.7 gives an adjunction

[TABLE]

However, we would like an adjunction between the category of all graphs and categories in $\mathsf{Mod}(\mathsf{Q})$. To accomplish this, we use the Grothendieck construction [8].

Definition 5.9**.**

Let

[TABLE]

be the functor which sends an object $V$ to the category $\mathsf{Span}(V)$ of spans over $V$. For a morphism $f\colon V\to W$ in $\mathsf{Mod}(\mathsf{Q})$, let

[TABLE]

be the functor which makes the assignment

[TABLE]

on objects and morphisms. Let

[TABLE]

be the functor which sends an object $V$ to the category of small categories internal to $\mathsf{Mod}(\mathsf{Q})$ with object model of $\mathsf{Q}$ given by $V$. For a morphism $f\colon V\to W$, let

[TABLE]

be the functor which which makes the assignment

[TABLE]

on the underlying graphs of objects and morphisms.

The adjunction derived from Theorem 5.7 can be reframed in this context.

Proposition 5.10**.**

The family of adjunctions

[TABLE]

form components of natural transformations

[TABLE]

Furthermore, $C$ and $\mathrm{B}^{\bullet}$ form an adjoint pair in the 2-category $[\mathsf{Mod}(\mathsf{Q}),\textup{{Cat}}]$ where

• •

objects are functors $F\colon\mathsf{Mod}(\mathsf{Q})\to\textup{{Cat}}$,

• •

morphisms are natural transformations $\alpha\colon F\Rightarrow G$ whose components $\alpha_{c}\colon F(c)\to G(c)$ are functors and,

• •

2-morphisms are modifications $\gamma\colon\alpha\to\beta$. That is, for every object $c$ in $\mathsf{Mod}(\mathsf{Q})$ a natural transformation of the type

[TABLE]

Proof.

For naturality, it suffices to show that the squares

[TABLE]

commute. This is verified by direct computation. To show that ${}^{\bullet}\mathrm{B}$ and $\mathrm{B}^{\bullet}$ are an adjoint pair we need the following fact: ${}^{\bullet}\mathrm{B}$ is a left adjoint to $\mathrm{B}^{\bullet}$ in $[\mathsf{Mod}(\mathsf{Q}),\textup{{Cat}}]$ if and only if the components

[TABLE]

form an adjoint pair in Cat. The counit-unit definition of adjunction requires that we have modifications $\epsilon\colon^{\bullet}\mathrm{B}\circ\mathrm{B}^{\bullet}\to 1_{\textup{{Cat}}(-)}$ and $\eta\colon 1_{\mathsf{Span}(-)}\to\mathrm{B}^{\bullet}\circ^{\bullet}\mathrm{B}$ satisfying the snake equations. Unpacking this gives components $\epsilon_{V}\colon^{\bullet}\mathrm{B}_{V}\circ\mathrm{B}^{\bullet}_{V}\Rightarrow 1_{\textup{{Cat}}(V)}$ and $\eta_{V}\colon\mathrm{B}^{\bullet}_{V}\circ^{\bullet}\mathrm{B}_{V}\Rightarrow 1_{\mathsf{Span}(V)}$ satisfying the snake equations. This is equivalent to each component being an adjunction. However, Theorem 5.7 says that each component is an adjunction so the claim is shown. ∎

So far we have the diagram

[TABLE]

of adjoint 1-cells in $[\mathsf{Mod}(\mathsf{Q}),\textup{{Cat}}]$. We apply the Grothendieck construction to this diagram to get

[TABLE]

The Grothendieck construction is a 2-functor $\int\colon[\mathsf{Mod}(\mathsf{Q}),\mathsf{CAT}]\to\mathsf{CAT}/\mathsf{Mod}(\mathsf{Q})$ where $\mathsf{CAT}$ denotes the 2-category of large categories, functors, and natural transformations. When composed with the forgetful 2-functor $\mathsf{CAT}/\mathsf{Mod}(\mathsf{Q})\to\mathsf{CAT}$ which remembers only the domain of each functor, we obtain the composite

[TABLE]

which we denote as $\int$ in an abuse of notation.

A fundamental fact is that every 2-functor preserves adjunctions. Therefore the above diagram is an adjunction. Moreover, the following proposition shows that it is the adjunction we are looking for.

Proposition 5.11**.**

The category $\int\mathsf{Span}(-)$ is equivalent to $\mathsf{Grph}(\mathsf{Mod}(\mathsf{Q}))$ and the category $\int\textup{{Cat}}(-)$ is equivalent to $\mathsf{Mod}(\mathsf{Q},\textup{{Cat}})$.

Proof.

$\int\mathsf{Span}(-)$ has

• •

pairs $(V,V\leftarrow E\to V)$ as objects and,

• •

pairs $(f\colon V\to V^{\prime},g\colon E\to E^{\prime})$ such that the diagram

[TABLE]

in $\mathsf{Mod}(\mathsf{Q})$ commutes as morphisms.

An equivalence $\int\mathsf{Span}(-)\xrightarrow{\sim}\mathsf{Grph}(\mathsf{Mod}(\mathsf{Q}))$ sends $(V,V\leftarrow E\to V)$ to the graph {E}$${V}

and a morphism $(f,g)$ to the evident morphism of graphs $(f\colon E\to E^{\prime},g\colon V\to V^{\prime})$.

$\int\textup{{Cat}}(-)$ has

• •

pairs $(V,C)$ where $C$ is a category over $V$ as objects and,

• •

pairs $(f\colon V\to V^{\prime},g\colon C\to C^{\prime})$ where $g$ is an object fixing functor from $\textup{{Cat}}(f)(C)$ to $C^{\prime}$ as morphisms.

An equivalence $\int\textup{{Cat}}(-)\xrightarrow{\sim}\textup{{Cat}}(\mathsf{Mod}(\mathsf{Q})$ is given by sending objects $(V,C)$ to their second component and morphisms $(f,g)$ to the functor whose object component is $f$ and whose morphism component is the morphism component of $g$. ∎

We denote the compositions of $\int^{\bullet}\mathrm{B}$ and $\int\mathrm{B}^{\bullet}$ with the above equivalences by ${}^{\bullet}\mathrm{B}_{\mathsf{Q}}$ and $\mathrm{B}^{\bullet}_{\mathsf{Q}}$ respectively.

Proof of Theorem 5.1. The composite adjunction $F_{\mathsf{Q}}\dashv U_{\mathsf{Q}}$ is constructed by setting $F_{\mathsf{Q}}=^{\bullet}\mathrm{B}_{\mathsf{Q}}\circ^{\bullet}\mathrm{A}_{\mathsf{Q}}$ and $U_{\mathsf{Q}}=\mathrm{B}^{\bullet}_{\mathsf{Q}}\circ\mathrm{A}^{\bullet}_{\mathsf{Q}}$. ∎

6 Applications

Theorem 5.1 has many applications: it can be used to help understand existing constructions of semantics for various $\mathsf{Q}$-nets from a categorical perspective.

6.1 Semantics for Pre-nets

In [7] the authors construct an adjunction for pre-nets which highlights the individual token semantics. In this subsection we characterize a variation of this adjunction using Theorem 5.1. Theorem 5.1 gives the following adjunction for pre-nets:

Proposition 6.1**.**

Let $R_{\mathsf{MON}}\colon\mathsf{Mod}(\mathsf{MON})\to\mathsf{Set}$ be the underlying set functor and let $L_{\mathsf{MON}}\colon\mathsf{Set}\to\mathsf{Mod}(\mathsf{MON})$ be its left adjoint. Recall that the composite $R_{\mathsf{MON}}\circ L_{\mathsf{MON}}$ is denoted by $(-)^{*}$. Let $\mathsf{MC}$ be the category of strict monoidal categories and strict monoidal functors. Let

[TABLE]

be the functor which makes the assignment on objects and morphisms

[TABLE]

where $\overline{\mathrm{Mor}\,C}$ and the source and target maps are as defined in Definition 5.4. Then, $U_{\mathsf{MON}}$ has a left adjoint

[TABLE]

which sends a pre-net

[TABLE]

to the strict monoidal category where

• •

the objects are given by the free monoid $L_{\mathsf{MON}}S$ and,

• •

morphisms are defined inductively as the closure of $T$ under composition $\circ$, and monoidal product $\otimes$. This is quotiented by the axioms

• –

$(f\otimes g)\otimes h=f\otimes(g\otimes h)$* (the associative law)*

• –

$1\otimes f=f\otimes 1=f$* (the left and right unit laws)*

• –

$(f_{1}\circ g_{1})\otimes(f_{2}\circ g_{2})=(f_{1}\otimes f_{2})\circ(g_{1}\otimes g_{2})$* whenever all composites are defined (the interchange law).*

For a morphism of pre-nets $(f,g)$, $F(f,g)$ has object component given by $L_{\mathsf{MON}}g$ and a morphism component given by the unique composition preserving monoid homomorphism extending $f$.

Under the individual token philosophy, monoidal categories are not yet a sufficient semantics for pre-nets. This is because in the individual token philosophy, the order of tokens going in and out of a Petri net must be accounted for. To represent this ordering, we can freely add a swapping morphism

[TABLE]

for every pair of objects $a$ and $b$ in $F_{\mathsf{MON}}(P)$. Every morphism in this new category, can now be regarded as having some permutation of the multisets in its inputs and outputs composed on either side. After choosing an initial ordering on your tokens, these permutations give an order in which tokens flow in and out of each process. Strict monoidal categories equipped with coherent swapping morphisms are called strict symmetric monoidal categories and there is a category where they are objects.

Definition 6.2**.**

Let $\mathsf{SMC}$ be the category where

• •

objects are strict symmetric monoidal categories and,

• •

morphisms are strict symmetric monoidal functors.

Symmetries can be freely added to the category $F_{\mathsf{MON}}(P)$ and this process is a left adjoint.

Definition 6.3**.**

Let

[TABLE]

be the forgetful functor which regards every symmetric strict monoidal category as a strict monoidal category and every strict symmetric monoidal functor as a strict monoidal functor.

Proposition 6.4**.**

$M$* has a left adjoint.*

Proof.

Note that because everything here is strict, the construction of the adjunction between $\mathsf{MC}$ and $\mathsf{SMC}$ is a simpler task than constructing an adjunction between their non-strict counterparts. To find a left adjoint to the forgetful functor from symmetric monoidal categories to monoidal categories, the tools of 2-dimensional category theory must be used. On the other hand, due to their strictness, the categories $\mathsf{MC}$ and $\mathsf{SMC}$ can be characterized as the category of models for a finite limits theory [2, §3D]. To construct these finite limit theories, we start with $\mathsf{Th(Cat)}$: the well-known finite limit theory for categories. $\mathsf{Th(Cat)}$ has two sorts: $M$ for morphisms and $O$ for objects. The generating operations of $\mathsf{Th(Cat)}$ are

[TABLE]

which represent source, target, identity, and composition. These operations are quotiented to satisfy the operations of a category. To get $\mathsf{Th(SMC)}$, the theory of strict monoidal categories, we add the operations constituting the structure of a monoid on both the objects and the morphisms. These operations have types $M\times M\to M$, $O\times O\to O$, $1\to M$, and $1\to O$ representing the identity and multiplications of each monoid. These operations are quotiented to satisfy equations expressing the monoid axioms and compatibility with the operations already in $\mathsf{Th(Cat)}$.

$\mathsf{Th(SMC)}$ can be further upgraded to obtain $\mathsf{Th(SSMC)}$, the finite limit theory for strict symmetric monoidal categories. $\mathsf{Th(SSMC)}$ contains all the generating objects and morphisms of $\mathsf{Th(SMC)}$ in addition to a braiding operation with type $O\times O\to M$. This braiding is required to satisfy the typical axioms of a symmetric monoidal category. Furthermore, there is an inclusion $i\colon\mathsf{Th(SMC)}\to\mathsf{Th(SSMC)}$ which sends every sort and operation of $\mathsf{Th(SMC)}$ to the sort and operation in $\mathsf{Th(SSMC)}$ which plays the same role. In summary, there is a morphism of finite limit theories

[TABLE]

Gabriel–Ulmer duality [15, 1] establishes an equivalence between this sort of morphism and filtered colimit preserving right adjoints

[TABLE]

This right adjoint is the functor in Definition 6.3. ∎

To get the individual token semantics for pre-nets, first we freely close the transitions under composition and monoidal product using Theorem 5.1 then we freely add symmetries as shown above.

{\mathsf{PreNet}}$${\mathsf{MC}}$${\mathsf{SMC}}$$\scriptstyle{F_{\mathsf{MON}}}$$\scriptstyle{U_{\mathsf{MON}}}$$\scriptstyle{N}$$\scriptstyle{M}

This composite adjunction is the adjunction $Z\dashv K$ mentioned in Example 3.5. This doesn’t yet represent the standard individual token semantics for pre-nets. Let

[TABLE]

be a morphism in $Z(P)$ for a pre-net $P$. Then, composing $f$ with a permutation

[TABLE]

should only represent a new process if $a=a^{\prime}$. This point could be argued, but the idea is that permuting different places has no functional difference because it requires the same inputs and outputs. Therefore, to get a category which is equivalent to the category of strongly concatenable processes introduced in [26] we must quotient $Z(P)$ by requiring that

[TABLE]

commutes for every transition $\tau\colon x\to y$ and permutations $a\colon x\to x$ and $b\colon y\to y$. The key point here is that the permutations are from an element to itself. This only occurs when the permutation switches objects which are the same.

The difference between the adjunction $Z\dashv K$ and the adjunction introduced in Functorial Models for Petri Nets has to do with a change in definition of the morphisms in the category $\mathsf{PreNet}$. We require that the places component come from a function between the sets of places whereas the authors of [7] do not. This change is made so that the category $\mathsf{PreNet}$ admits a smoother description of its semantics.

For practical purposes, it useful to construct semantics for Petri nets rather than pre-nets which have the individual token philosophy. For this we use the functor

[TABLE]

introduced in Section 3 which sends every pre-net to the Petri net which forgets about the ordering on the input and output of each transtion.

In [7] the authors suggest that an individual token semantics for a Petri net $P$ can computed by choosing a linearization of $P$; a pre-net $R$ in the preimage ${c}\mathchar 45\relax\mathsf{Net}^{-1}(P)$. Then, the semantics category $N\circ F_{\mathsf{MON}}R$ is defined to be the individual token semantics of $P$. Note that this process depends on a choice of linearization only up to isomorphism. Let $R$ and $R^{\prime}$ be linearizations of $P$, then Theorem 2.5 of [7] proves that $Z(R)\cong Z(R^{\prime})$.

Choosing a linearization and then applying $Z$ gives an individual token semantics for Petri nets but it is unclear about how to extend this to morphisms of Petri nets. For a functorial construction, we can try to reverse the functor ${c}\mathchar 45\relax\mathsf{Net}$ in the diagram:

{\mathsf{Petri}}$${\mathsf{PreNet}}$${\mathsf{MC}}$${\mathsf{SMC}}$$\scriptstyle{{c}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{F_{\mathsf{MON}}}$$\scriptstyle{N}

An inverse to ${c}\mathchar 45\relax\mathsf{Net}$ cannot be single valued because there are many linearizations of a given Petri net. For given transition of a Petri net, there are many possible orderings of is source and target. To avoid making a choice, you can make them all. Let $P$ be a Petri net and let $\{(s_{i},t_{i}\colon T\to S^{*})\}_{i=1}^{n}$ be the set of linearizations of $P$, that is the set ${c}\mathchar 45\relax\mathsf{Net}^{-1}(P)$. Let $Q$ be the pre-net given by

[TABLE]

where $\Sigma s_{i}$ and $\Sigma t_{i}$ denote the copairing of the functions $s_{i}$ and $t_{i}$ respectively. Then, the mapping

[TABLE]

characterizes the category $\mathcal{Q}(P)$ introduced by Sassone in On the Category of Petri Net Computations [26]. Unfortunately, Sassone showed that this at first only gives a pseudofunctor [26]. This is because there is no obvious way to turn a morphism of Petri nets into a functor between the fibers of their source and target. However Sassone showed that after performing the appropriate quotient on the target category this mapping can be turned into a functor and a left adjoint [26].

6.2 Semantics for Integer Nets

In Executions in (Semi-)Integer Petri Nets are Compact Closed Categories, Genovese and Herold show how compact closed symmetric monoidal categories give a categorical semantics for integer nets [14]. Note that these categories are strictly compact closed but not strictly symmetric, i.e., the braidings are not given by the identity. To get an operational semantics for integer nets where the braidings are given by the identity we can use Theorem 5.1. This adjunction gives for each integer net a description of its semantics under the collective token philosophy; the morphisms represent the possible executions of an integer net but do not keep track of the identities of the individual tokens.

Proposition 6.5**.**

Let

[TABLE]

be the adjunction making up the free abelian group monad $\mathbb{Z}$ in Definition 3.4. Then there is a left adjoint

[TABLE]

which sends a $\mathbb{Z}$-net

[TABLE]

to the $\mathsf{ABGRP}$-category $F_{\mathsf{ABGRP}}(P)$ which has

• •

$LS$* as its free abelian group of objects and,*

• •

morphisms are given by the free closure of T under composition and identity, modulo the axioms of a category, and under monoidal product and inverses, modulo the axioms of an abelian group. We also require that the structure maps are abelian group homomorphisms.

For a morphism of $\mathbb{Z}$-nets $(f,g)\colon P\to P^{\prime}$, $F_{\mathsf{ABGRP}}(f,g)$ is a morphism of $\mathsf{ABGRP}$-categories which is

• •

given by $Lg$ on objects and,

• •

and morphisms it is given by the unique extension of $f$ which respects the abelian group operation and composition.

If we wish to construct semantics for integer nets under the individual token philosophy we need our semantics categories to have braidings which are not given by identities. This can accomplished using a similar construction as the previous subsection. Indeed we have a diagram of categories as follows:

{{\mathbb{Z}}\mathchar 45\relax\mathsf{Net}}$${{\mathsf{GRP}}\mathchar 45\relax\mathsf{Net}}$${\mathsf{Mod}(\mathsf{GRP},\textup{{Cat}})}SCCC\scriptstyle{{e}\mathchar 45\relax\mathsf{Net}}$$\scriptstyle{F_{\mathsf{GRP}}}$$\scriptstyle{W}

The features of this diagram are as follows.

• •

${e}\mathchar 45\relax\mathsf{Net}\colon{\mathsf{GRP}}\mathchar 45\relax\mathsf{Net}\to{\mathbb{Z}}\mathchar 45\relax\mathsf{Net}$ is abelianization. It sends a $\mathsf{GRP}$-net to the integer net which forgets about the ordering on the input and output of each transition. ${e}\mathchar 45\relax\mathsf{Net}$ sends morphisms of ${\mathsf{GRP}}\mathchar 45\relax\mathsf{Net}$-nets to themselves.

• •

The functor $F_{\mathsf{GRP}}\colon{\mathsf{GRP}}\mathchar 45\relax\mathsf{Net}\to\mathsf{Mod}(\mathsf{Q},\textup{{Cat}})$ is constructed using Theorem 5.1. This functor freely closes the transitions of a $\mathsf{GRP}$-net under the group operation, composition, and freely adds inverses and identites. These semantics categories are required to satisfy the axioms of a group and a category. The structure maps of these are categories are required to be group homomorphisms. This functor will not be explicitly described in this paper but it can be constructed using Theorem 5.1.

• •

SCCC is the category where

• –

An object $C$ is a strictly monoidal strictly compact closed category. This means that for every object $x$ in $C$ and $f$ in $\mathrm{Mor}\,C$ there are inverses with

[TABLE]

In addition, every pair of objects is equipped with a symmetry $\gamma_{x,y}\colon x\otimes y\to y\otimes x$ satisfying the axioms of a symmetric monoidal category.

• –

Morphisms in SCCC are strict symmetric monoidal functors. Preservation of inverses follows from being a strict monoidal functor.

• •

$W\colon{\mathsf{GRP}}\mathchar 45\relax\mathsf{Cat}\to\textup{{SCCC}}$ is a left adjoint of an adjunction which freely adds a symmetric braiding for every pair of objects. This adjunction is described as follows. The proof of this proposition follows the same argument as Proposition 6.4.

Proposition 6.6**.**

Let $X\colon\textup{{SCCC}}\to\mathsf{Mod}(\mathsf{GRP},\textup{{Cat}})$ be the forgetful functor which sends objects and morphisms of SCCC to their underlying $\mathsf{GRP}$-categories and $\mathsf{GRP}$-functors. Then $X$ has a left adjoint

[TABLE]

which is specified by the following:

• •

for a $\mathsf{GRP}$-category $C$, $WC$ is a symmetric monoidal category such that for every pair of objects $x$, $y$ in $C$ there is an isomorphism $\gamma_{x,y}\colon x\otimes y\to y\otimes x$ satisfiying the axioms of a symmetry in a symmetric monoidal category.

• •

for a $\mathsf{GRP}$-functor $F\colon C\to D$, $WF$ is a the unique extension of $F$ which sends symmetries to symmetries.

In order to get individual token semantics for an integer net $P$ we can start with a $\mathsf{GRP}$-net $K$ which abelianizes to $P$. This is also called a linearization of $P$. The individual token semantics of $P$ can be defined as $W\circ F_{\mathsf{GRP}}(K)$. To get a systematic mapping from integer nets to their individual token semantics we can combine all the linearizations of a given integer net. Let $\{(s_{i},t_{i}\colon T_{i}\to M_{\mathsf{GRP}}(S))\}_{i=1}^{n}$ be the set of linearizations of $P$, that is the set ${e}\mathchar 45\relax\mathsf{Net}^{-1}(P)$. Let $N$ be the $\mathsf{GRP}$-net given by

[TABLE]

where $\Sigma s_{i}$ and $\Sigma t_{i}$ denote the copairing of the functions $s_{i}$ and $t_{i}$ respectively. The mapping

[TABLE]

characterizes the category $\mathfrak{F}(P)$ introduced in [14]. Like before, this assignment extends to a pseudofunctor rather than a functor. Analogously to the situation for Petri nets, Genovese and Herold prove that after performing some quotients on the target category this turns into a functor and a left adjoint [14].

6.3 Semantics for Elementary Net Systems

Theorem 5.1 can be used to construct a functorial description of the semantics of elementary net systems. This semantics matches the standard description which has not yet been made categorical. For an elementary net system $P$, $F_{\mathsf{SLAT}}(P)$ is a category where the objects are possible markings of $P$ and the morphisms are finite sequences of firings.

Proposition 6.7**.**

Let

[TABLE]

*be the adjunction whose associated monad is $2^{(-)}\colon\mathsf{Set}\to\mathsf{Set}$. Then there is a left adjoint *

[TABLE]

which sends an elementary net system

[TABLE]

to the $\mathsf{SLAT}$-category $F_{\mathsf{SLAT}}(P)$ with objects given by $2^{S}$ and with morphisms generated inductively by the rules:

• •

for every transition $\tau\in T$, a morphism $\tau\colon s(\tau)\to t(\tau)$ is included,

• •

for every pair of morphisms $f\colon x\to y$ and $g\colon x^{\prime}\to y^{\prime}$, their sum $f+g\colon x+x^{\prime}\to y+y^{\prime}$ is included,

• •

for every pair of morphisms, $f\colon x\to y$ and $g\colon y\to z$, their composite $g\circ f\colon x\to z$ is included,

• •

these morphisms are quotiented to satisfy the axioms of an idempotent commutative monoid and of a category

• •

these morphisms are quotiented to make composition and the assignment of identities to be monoid homomorphisms.

For a morphism of $\mathsf{SLAT}$-nets $(f\colon T\to T^{\prime},g\colon S\to S^{\prime})$,

[TABLE]

is the functor given by $2^{g}$ on objects and by the unique monoidal and functorial extension of $f$ on morphisms.

Acknowledgements

I would like to thank my advisor John Baez for his constant help and guidance. I would like to thank Christina Vasilokopoulou in particular for the slick proof of Proposition 3.11. I would like to thank Clemens Berger and Mike Schulman for helping me understand how morphisms of Lawvere theories turn into morphisms of monads. I would also like to thank Mike Shulman and Todd Trimble who found a mistake in an earlier draft and helped me fix it in a way which improved the paper. I thank Joe Moeller, Daniel Cicala, Kenny Courser, and Joshua Meyers for their feedback and support. Lastly, I would like to thank my friends and family for their love and support, I would not be where I am without them.

Appendix A Lawvere Theories

Introduced by Lawvere in his landmark thesis [18], Lawvere theories are a general framework for reasoning about algebraic structures [10, 9].

Definition A.1**.**

A Lawvere theory $\mathsf{Q}$ is a small category with finite products such that every object is isomorphic to the iterated finite product $x^{n}=x\times\ldots\times x$ for a generic object $x$ and natural number $n$. Equivalently, Lawvere theories can be thought of as categories whose objects are given by natural numbers $n\in\mathbb{N}$ and with cartesian product given by $+$. The morphisms in a Lawvere theory are called operations.

The idea is that a Lawvere theory represents the platonic embodiment of an algebraic gadget.

Example A.2**.**

A canonical example is the Lawvere theory $\mathsf{MON}$ of monoids. Like all Lawvere theories, the objects of $\mathsf{MON}$ are given by natural numbers. In addition $\mathsf{MON}$ contains the morphisms

[TABLE]

For a monoid $M$, this represents the multiplication map

[TABLE]

and the map

[TABLE]

which picks out the identity element of $M$. These maps are required to satisfy the associative law

[TABLE]

and the unital laws for monoids.

[TABLE]

$\mathsf{MON}$ also contains all composites, tensor products, and maps necessary to make $n$ into the product $x^{n}$ induced by the maps $m$ and $e$.

Like all good things, Lawvere theories form a category.

Definition A.3**.**

Let Law be the category where objects are Lawvere theories and morphisms are product preserving functors.

Note that because morphisms of Lawvere theories preserve products, they must send the generic object of their source to the generic object of their target. Therefore to specify a morphism of Lawvere theories, it suffices to make an assignment of the morphisms which are not part of the product structure.

Let $\mathsf{Q}$ be a Lawvere theory and $C$ a category with finite products. We can impose the axioms and operations of $\mathsf{Q}$ onto an object in $C$ via a product preserving functor $F\colon\mathsf{Q}\to C$. The image $F(1)$ of the generating object $1$ gives the underlying object of $F$ and for an operation $o\colon n\to k$ in $\mathsf{Q}$, $F(o)\colon F(x)^{n}\to F(x)^{k}$ gives a specific instance of the algebraic operation represented by $o$. There is a natural way to make a category of these functors.

Definition A.4**.**

Let $\mathsf{Q}$ be a Lawvere theory and $C$ a category with finite products. Then there is a category $\mathsf{Mod}(\mathsf{Q},C)$ where

• •

objects are product preserving functors $F\colon\mathsf{Q}\to C$ and,

• •

morphisms are natural transformations between these functors.

When $\mathsf{Mod}(\mathsf{Q})$ is written without the second argument, it is assumed to be $\mathsf{Set}$. We will refer to objects in $\mathsf{Mod}(\mathsf{Q})$ as $\mathsf{Q}$-models and morphisms in $\mathsf{Mod}(\mathsf{Q})$ as $\mathsf{Q}$-model homomorphisms. When $C=\textup{{Cat}}$, we will refer to these objects as $\mathsf{Q}$-categories.

When the category of models is $\mathsf{Set}$ then there is a forgetful functor

[TABLE]

which sends a product preserving functor $F\colon\mathsf{Q}\to\mathsf{Set}$ to image on the generating object $F(1)$ and a natural transformation to component on the object $1$. A classical result says that $R_{\mathsf{Q}}$ always has a left adjoint

[TABLE]

which for a set $X$, $L_{\mathsf{Q}}X$ is referred to as the free model of $\mathsf{Q}$ on $X$. In fact, this construction extends to fully faithful functor

[TABLE]

which sends a Lawvere theory $\mathsf{Q}$ to the monad $R_{\mathsf{Q}}\circ L_{\mathsf{Q}}\colon\mathsf{Set}\to\mathsf{Set}$ and where $\mathsf{Mnd}$ is the category of monads on $\mathsf{Set}$ [19]. For a Lawvere theory $\mathsf{Q}$ we will denote the monad it induces via this functor by $M_{\mathsf{Q}}\colon\mathsf{Set}\to\mathsf{Set}$.

For $\mathsf{Q}=\mathsf{MON}$, $\mathsf{Mod}(\mathsf{MON},\mathsf{Set})$ is equivalent to the category Mon of monoids and monoid homomorphisms. In this case the functor $R_{\mathsf{MON}}\colon\textup{{Mon}}\to\mathsf{Set}$ turns monoids and monoid homomorphisms into their underlying sets and functions. $R_{\mathsf{MON}}$ has a left adjoint

[TABLE]

which sends a set $X$ to the free monoid $L_{\mathsf{MON}}X$. For a function $f\colon X\to Y$, $L_{\mathsf{MON}}f$ is the unique multiplication preserving extension of $f$ to $L_{\mathsf{MON}}X$.