1: %%% Préambule %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2: \documentclass[a4paper,twoside,11pt,english,fleqn]{article}
3:
4: %% Extensions
5: \usepackage[all]{xy}
6: \usepackage[intlimits]{amsmath}
7: \usepackage{amssymb,amsthm,graphicx}
8: \usepackage[dvips,dvipdf,pdftex]{epsfig}
9: \usepackage{babel}
10: \usepackage[T1]{fontenc}
11: \usepackage{fancyhdr,stmaryrd,color,times,euler,euscript,eufrak}
12:
13: %% Options
14: \DeclareGraphicsExtensions{.png}
15: \DeclareMathAlphabet{\mathscr}{T1}{pzc}{m}{it}
16:
17: %% Styles de théorèmes
18: \newtheorem{thm}{Theorem}[section]
19: \newtheorem{cor}[thm]{Corollary}
20: \newtheorem{lem}[thm]{Lemma}
21: \newtheorem{prop}[thm]{Proposition}
22: \theoremstyle{definition}
23: \newtheorem{defn}[thm]{Definition}
24: \newtheorem{ex}[thm]{Example}
25: \newtheorem{rem}[thm]{Remark}
26: \newtheorem{ntt}[thm]{Notation}
27: \newtheorem*{dem}{Proof}
28:
29: %% Caractères
30: \newcommand{\Cr}{\EuScript{C}}
31: \newcommand{\Gr}{\EuScript{G}}
32: \newcommand{\Mr}{\EuScript{M}}
33: \newcommand{\Nr}{\EuScript{N}}
34: \newcommand{\Nb}{\mathbb{N}}
35: \newcommand{\Sk}{\EuFrak{S}}
36: \renewcommand{\phi}{\varphi}
37: \renewcommand{\epsilon}{\varepsilon}
38: \newcommand{\findem}{\hfill $\diamondsuit$}
39: \newcommand{\da}{\downarrow}
40: \newcommand{\ua}{\uparrow}
41: \newcommand{\ca}{\leadsto}
42:
43: %% Relations
44: \newcommand{\fl}{\rightarrow}
45: \newcommand{\lfl}{\longrightarrow}
46: \newcommand{\mfl}{\twoheadrightarrow}
47: \renewcommand{\iff}{\Leftrightarrow}
48: \newcommand{\red}[1]{\rightarrow\!\!_{{\scriptscriptstyle #1}}}
49: \newcommand{\mred}[1]{\twoheadrightarrow\!\!_{{\scriptscriptstyle #1}}}
50: \newcommand{\equi}[1]{\equiv\!\!_{{\scriptscriptstyle #1}}}
51:
52: %% Opérations
53: \newcommand{\tens}{\otimes}
54: \newcommand{\mon}[1]{\langle #1 \rangle}
55: \newcommand{\ens}[1]{\{#1\}}
56: \newcommand{\dens}[2]{\{#1,\dots,#2\}}
57: \newcommand{\ol}[1]{\overline{#1}}
58: \newcommand{\ul}[1]{\underline{#1}}
59: \newcommand{\et}{\quad\text{and}\quad}
60:
61: %% Nouveaux opérateurs
62: \DeclareMathOperator{\id}{id}
63:
64: %% Mise en page
65: \pagestyle{fancy}
66: \setlength{\oddsidemargin}{0cm}
67: \setlength{\evensidemargin}{0cm}
68: \setlength{\topmargin}{0cm}
69: \setlength{\headheight}{1cm}
70: \setlength{\headsep}{1cm}
71: \setlength{\textwidth}{16cm}
72: \setlength{\marginparwidth}{0cm}
73: \setlength{\footskip}{2cm}
74: \setlength{\headwidth}{16cm}
75: \newcommand{\headrulelength}{16cm}
76: \renewcommand{\headrulewidth}{1pt}
77: \renewcommand{\footrulewidth}{0pt}
78:
79: \newcommand{\emptysectionmark}[1]
80: {\markboth{\textbf{#1}}{\textbf{#1}}}
81: \newcommand{\emptysubsectionmark}[1]
82: {\markright{\textbf{#1}}}
83: \renewcommand{\sectionmark}[1]
84: {\markboth{\textbf{\thesection. #1}}{\textbf{\thesection. #1}}}
85: \renewcommand{\subsectionmark}[1]
86: {\markright{\textbf{\thesubsection. #1}}}
87:
88: \fancyhead{}\fancyfoot[LC,RC]{}
89: \fancyhead[LE]{\leftmark}
90: \fancyhead[RO]{\rightmark}
91: \fancyfoot[LE,RO]{\textbf{\thepage}}
92:
93: \fancypagestyle{plain}
94: {
95: \fancyhf{}
96: \fancyfoot[LC,RC]{}
97: \fancyfoot[LE,RO]{\textbf{\thepage}}
98: \renewcommand{\headrulewidth}{0pt}
99: \renewcommand{\footrulewidth}{0pt}
100: }
101:
102: %% Titre
103: \begin{document}
104: \thispagestyle{plain}
105:
106: \hfill {\large \textbf{1st July 2005 - Modified: 6th January 2006}}
107:
108: \vspace{3mm}
109: \hrule height 1.5pt
110:
111: \vspace{4mm}
112: {\LARGE \textbf{TWO POLYGRAPHIC PRESENTATIONS}}
113:
114: \vspace{1mm}
115: {\LARGE \textbf{OF PETRI NETS}}
116:
117: \vspace{3mm}
118: \indent{\LARGE \textbf{Yves Guiraud}\footnote{Institut de mathématiques de Luminy, Marseille, France - \texttt{guiraud@iml.univ-mrs.fr}} }
119:
120: \vspace{3mm}
121: \hrule height 1.5pt
122:
123: \vspace{8mm}
124:
125: %%% résumé %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
126: \begin{minipage}{150mm}
127: \textbf{Abstract:} This document gives an algebraic and two polygraphic translations of Petri nets, all three providing an easier way to describe reductions and to identify some of them. The first one sees places as generators of a commutative monoid and transitions as rewriting rules on it: this setting is totally equivalent to Petri nets, but lacks any graphical intuition. The second one considers places as $1$-dimensional cells and transitions as $2$-dimensional ones: this translation recovers a graphical meaning but raises many difficulties since it uses explicit permutations. Finally, the third translation sees places as degenerated $2$-dimensional cells and transitions as $3$-dimensional ones: this is a setting equivalent to Petri nets, equipped with a graphical interpretation.
128: \end{minipage}
129:
130: %%% présentation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
131: \section*{Outline}
132: \emptysectionmark{Outline}
133:
134: In this document, we study Petri nets in order to give two possible polygraphic presentations for them. This work follows Albert Burroni's intuitions: many computer science and proof theory objects have natural translations into polygraphs. These are topology-flavoured objects consisting of collections of directed cells of various dimensions, equipped with a rich algebraic structure.
135:
136: In section~\ref{sec:reseaux_de_petri}, we recall some basic facts about Petri nets, describe their representations and associate them reduction graphs, equipped with a relation that identifies paths that intuitively represent the same sequence of operations.
137:
138: In section~\ref{sec:mots_commutatifs}, we recall a known algebraic account of Petri nets: they correspond to commutative word rewriting systems (or presentations of commutative monoids) and both objects generate the same reduction graph. Furthermore, in the latter, reductions have a name, which makes easier the definition of a relation between similar paths. We prove a new result concerning stating that this relation is the same as the one defined for Petri nets. All these facts are detailed in theorem~\ref{th:comm}.
139:
140: In section~\ref{sec:2d}, we craft a $2$-dimensional object, a $2$-polygraph, in which reductions of a Petri net can be translated. This result is due to Albert Burroni and is formulated as theorem~\ref{th:2d}. We go beyond and study the links between the relation on Petri nets paths and two relations on $2$-arrows of the $2$-polygraph: the first one corresponds to the relation on the Petri net, while the second one tries to solve the difficulties raised by the presence of explicit permutations in the $2$-polygraph. The study of these properties is only started here: much more work will be necessary to totally solve the encountered problems.
141:
142: Finally, in section~\ref{sec:3d}, we give a new, more natural polygraphic way to faithfully describe Petri nets. We prove that they correspond to $3$-polygraphs with one cell in dimension~$0$ and no cell in dimension~$1$. Furthermore, both objects generate the same reduction graph, with the same equivalence relation on paths. This is the main result, theorem~\ref{th:3d}.
143:
144: %%% section : Réseaux de Petri %%%%%%%%%%%%%%%%%%
145: \section{Basic notions on Petri nets}
146: \label{sec:reseaux_de_petri}
147:
148: \noindent This section briefly recalls the basic notions about Petri nets: the definitions of a net, of its markings and the usual associated graphical representations. It should be noted that there exist many possible definitions of Petri nets, but a simple one has been chosen for this study. More of them can be found in [Murata 1989] for example.
149:
150: \begin{defn}\label{def:reseau_de_petri}
151: A \emph{Petri net} is a quadruple $N=(X,T,w,w')$ made of two finite sets, $X$ and $T$, and two maps, $w:X\times T\fl\Nb$ and $w':T\times X\fl\Nb$. The elements of $X$ and $T$ are respectively called \emph{places} and \emph{transitions}, while the maps $w$ and $w'$ are the \emph{weights}. Beside this set-theoretic definition, Petri nets are usually encountered as graphical objects. A decorated graph is associated to a given net $N=(X,T,w,w')$ as follows:
152: \begin{enumerate}
153: \item[0.] Its objects are the places and the transitions. Places are pictured as circles, while transitions are represented by double bars.
154: \item[1.] If $x$ is a place and $\alpha$ a transition, there is an arrow from $x$ to $\alpha$ whenever $w(x,\alpha)>0$ and one from $\alpha$ to $x$ whenever $w'(\alpha,x)>0$. Such arrows are decorated with the corresponding weight, either $w(x,\alpha)$ or $w'(\alpha,x)$.
155: \end{enumerate}
156: \end{defn}
157:
158: \begin{ex}\label{ex:reseau_de_petri}
159: Let us condider the Petri net $N=(X,T,w,w')$ where $X=\ens{x,y,z}$, $T=\ens{\alpha,\beta}$ and the non-zero values of $w$ and $w'$ are given by:
160: $$
161: w(x,\alpha) \:=\: 1, \quad w(y,\beta) \:=\: 2, \quad w'(\alpha,y) \:=\: w'(\alpha,z) \:=\: w'(\beta,z)\: =\: 1.
162: $$
163:
164: \noindent Following the given graph construction recipe, this representation is built for $N$:
165: \begin{center}
166: \begin{picture}(0,0)%
167: \includegraphics{reseau_de_petri.eps}%
168: \end{picture}%
169: \setlength{\unitlength}{4144sp}%
170: %
171: \begingroup\makeatletter\ifx\SetFigFont\undefined%
172: \gdef\SetFigFont#1#2#3#4#5{%
173: \reset@font\fontsize{#1}{#2pt}%
174: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
175: \selectfont}%
176: \fi\endgroup%
177: \begin{picture}(2078,1179)(173,-518)
178: \put(1891,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$1$}%
179: }}}}
180: \put(361, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
181: }}}}
182: \put(1486,434){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
183: }}}}
184: \put(1486,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
185: }}}}
186: \put(901,-331){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
187: }}}}
188: \put(2251, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
189: }}}}
190: \put(721,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$1$}%
191: }}}}
192: \put(1081,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$1$}%
193: }}}}
194: \put(1171,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$1$}%
195: }}}}
196: \put(1846,344){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
197: }}}}
198: \end{picture}%
199: \end{center}
200: \end{ex}
201:
202: \noindent So far, only the hardware part of a Petri net has been represented. On top of this one, the states of the automaton are described:
203:
204: \begin{defn}\label{def:marquage}
205: Let $N=(X,T,w,w')$ be a Petri net. A \emph{marking} of $N$ is a map from the set $X$ of places to the set $\Nb$ of natural numbers. The set of all markings of $N$ is denoted by $\Mr(N)$. A given marking $\mu:X\fl\Nb$ on a Petri net $N=(X,T,w,w')$ is represented as an extra decoration on the corresponding graph: inside each place $x$, one puts $\mu(x)$ token(s), pictured as black dots.
206: \end{defn}
207:
208: \begin{ex}\label{ex:marquage}
209: With the same Petri net as in example \ref{ex:reseau_de_petri}, the marking $\mu$ defined by $\mu(x)=\mu(y)=2$ and $\mu(z)=0$ is represented as follows (thereafter, the weights equal to $1$ are removed, together with places labels, in order to make the representations clearer):
210: \begin{center}
211: \begin{picture}(0,0)%
212: \includegraphics{marquage.eps}%
213: \end{picture}%
214: \setlength{\unitlength}{4144sp}%
215: %
216: \begingroup\makeatletter\ifx\SetFigFont\undefined%
217: \gdef\SetFigFont#1#2#3#4#5{%
218: \reset@font\fontsize{#1}{#2pt}%
219: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
220: \selectfont}%
221: \fi\endgroup%
222: \begin{picture}(2078,1179)(173,-518)
223: \put(1846,344){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
224: }}}}
225: \put(901,-331){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
226: }}}}
227: \put(2251, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
228: }}}}
229: \end{picture}%
230: \end{center}
231: \end{ex}
232:
233: \noindent Now, the whole static part of Petri nets has been introduced. Their evolutions are described as follows:
234:
235: \begin{defn}\label{def:transition}
236: Let $N=(X,T,w,w')$ be a Petri net and let $\alpha$ be a transition in $T$. The \emph{reduction relation associated to $\alpha$} is the binary relation $\red{\alpha}$ on markings of $N$, defined by $\mu\red{\alpha}\nu$ if, for every place $x$ in~$X$, both following conditions hold:
237: $$
238: \begin{cases}
239: \mu(x)\geq w(x,\alpha), \\
240: \nu(x)=\mu(x)-w(x,\alpha)+w'(\alpha,x).
241: \end{cases}
242: $$
243:
244: \noindent The union of all the relations $\red{\alpha}$, for all the transitions $\alpha$, is denoted by $\red{T}$. The reflexive and transitive closure of $\red{T}$ is denoted by $\mred{T}$ and called the \emph{reachability relation}.
245:
246: The relation $\red{\alpha}$ associated to a transition $\alpha$ has a graphical interpretation. The first condition checks if the marking $\mu$ has at least $w(x,\alpha)$ tokens in each place $x$. In that case, the second condition tells that~$\nu$ is entirely determined this way: in each place $x$, $w(x,\alpha)$ tokens are removed, then $w'(\alpha,x)$ tokens are added.
247: \end{defn}
248:
249: \begin{ex}\label{ex:graphe_de_reduction}
250: Let $N$ be the Petri net of example \ref{ex:reseau_de_petri} and $\mu$ the marking of example \ref{ex:marquage}. The graph pictured thereafter displays all the markings of $N$ that can be reached from $\mu$.
251: \begin{center}
252: \begin{picture}(0,0)%
253: \includegraphics{graphe_de_reduction_petit.eps}%
254: \end{picture}%
255: \setlength{\unitlength}{4144sp}%
256: %
257: \begingroup\makeatletter\ifx\SetFigFont\undefined%
258: \gdef\SetFigFont#1#2#3#4#5{%
259: \reset@font\fontsize{#1}{#2pt}%
260: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
261: \selectfont}%
262: \fi\endgroup%
263: \begin{picture}(6494,4071)(212,-3717)
264: \put(6694,-3365){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
265: }}}}
266: \put(1675, 83){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
267: }}}}
268: \put(4089, 83){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
269: }}}}
270: \put(1675,-1450){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
271: }}}}
272: \put(4089,-1450){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
273: }}}}
274: \put(1675,-2982){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
275: }}}}
276: \put(4089,-2982){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
277: }}}}
278: \put(6503,-2982){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$2$}%
279: }}}}
280: \put(832,-454){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
281: }}}}
282: \put(832,-1986){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
283: }}}}
284: \put(832,-3518){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
285: }}}}
286: \put(3246,-454){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
287: }}}}
288: \put(3246,-1986){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
289: }}}}
290: \put(3246,-3518){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
291: }}}}
292: \put(5660,-3518){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
293: }}}}
294: \put(3361,-952){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
295: }}}}
296: \put(871,-2484){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
297: }}}}
298: \put(3361,-2484){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
299: }}}}
300: \put(832,-952){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
301: }}}}
302: \put(2250,-71){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
303: }}}}
304: \put(2250,-1603){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
305: }}}}
306: \put(2250,-3135){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
307: }}}}
308: \put(4664,-3135){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
309: }}}}
310: \put(1867,-300){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
311: }}}}
312: \put(4281,-300){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
313: }}}}
314: \put(4281,-1833){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
315: }}}}
316: \put(1867,-1833){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
317: }}}}
318: \put(1867,-3365){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
319: }}}}
320: \put(4281,-3365){\makebox(0,0)[b]{\smash{{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
321: }}}}
322: \end{picture}%
323: \end{center}
324: \end{ex}
325:
326: \vfill\pagebreak
327: \noindent In order to compare Petri nets with the rewriting-flavoured objects to be introduced in the next three sections, the notion of reduction graph appearing in example \ref{ex:graphe_de_reduction} is formalized:
328:
329: \begin{defn}\label{def:graphe}
330: Let $N=(X,T,w,w')$ be a Petri net. Its \emph{associated reduction graph} is the graph $G(N)$ defined by:
331: \begin{enumerate}
332: \item[0.] The set of objects of $G(N)$ is the set $\Mr(N)$ of markings of $N$.
333: \item[1.] In $G(N)$, there is an arrow from a marking $\mu$ to a marking $\nu$ for each transition $\alpha$ such that $\mu\red{\alpha}\nu$.
334: \end{enumerate}
335: \end{defn}
336:
337: \noindent In example \ref{ex:graphe_de_reduction}, we have pictured a subgraph of the reduction graph $G(N)$, where $N$ is the Petri net of example \ref{ex:reseau_de_petri}. Let us consider the top-most square. We can see that the two vertical arrows, both labelled by $\alpha$ are "intuitively" the same reduction: indeed, they consume the same tokens and produce the same ones. This is also the case for the two vertical $\beta$-labelled arrows. Furthermore, the horizontal and vertical reductions apply on different tokens: there should be some relation between the two sequences $\alpha$-then-$\beta$ and $\beta$-then-$\alpha$. Let us define a congruence relation on such reduction paths:
338:
339: \begin{ntt}
340: Let $N=(X,T,w,w')$ be a Petri net. We denote by $\equi{N}$ the congruence relation on paths of $G(N)$ generated by the identification of subpaths
341: $$
342: \mu_1\red{\alpha}\nu_1\red{\beta}\mu_2 \et \mu_1\red{\beta}\nu_2\red{\alpha}\mu_2,
343: $$
344:
345: \noindent such that the following equalities hold for a given marking $\rho$ in $\Mr(N)$ and for every place $x$ in $X$:
346: $$
347: \begin{array}{l c l c l c l}
348: \mu_1(x) &=&\rho(x)+w(x,\alpha)+w(x,\beta),
349: &\qquad &\nu_1(x) &=& \rho(x)+w'(\alpha,x)+w(x,\beta), \\
350: \nu_2(x) &=&\rho(x)+w(x,\alpha)+w'(\beta,x),
351: &\qquad &\mu_2(x) &=& \rho(x)+w'(\alpha,x)+w'(\beta,x).
352: \end{array}
353: $$
354: \end{ntt}
355:
356: \noindent One can check that, in the reduction graph of the Petri net of example \ref{ex:reseau_de_petri}, the relation $\equi{N}$ identifies any two paths with same source and same target one can form in the diagram of example \ref{ex:graphe_de_reduction}. In each one of the next three sections, we introduce a translation for Petri nets and study how it behaves with respect to this congruence relation.
357:
358: %%% section : réseaux de Petri = mots commutatifs %%%
359: \section{Petri nets and commutative word rewriting systems}\label{sec:mots_commutatifs}
360:
361: \noindent In this section, an equivalence between Petri nets and \emph{commutative word rewriting systems} is proved. The underlying idea of the translation is already present in [Caprotti Ferscha Hong 1995] and [Chandler Heyworth 2001] and comes from the following remarks :
362: \begin{enumerate}
363: \item[-] The markings of a Petri net have a commutative monoid structure: the sum is given by addition of the tokens in each place and the empty marking is a neutral element for this operation.
364: \item[-] If $\alpha$ is a transition, then $\red{\alpha}$ is compatible with the commutative monoid structure on markings: if~$\mu\red{\alpha}\mu'$, then $\mu+\nu\red{\alpha}\mu'+\nu$ holds for every marking $\nu$.
365: \end{enumerate}
366:
367: \begin{defn}\label{def:reecriture_commutative}
368: Let $X$ be a set. The \emph{free commutative monoid generated by $X$} is the set $[X]$ of all finite formal sums of elements of $X$:
369: $$
370: a=\sum_{x\in X} a_x.x,
371: $$
372:
373: \noindent where the $a_x$ are natural numbers that entirely define $a$. The set $[X]$ is a commutative monoid for the following operation, which admits the empty sum as a neutral element:
374: $$
375: \sum_{x\in X} a_x.x \:+\: \sum_{x\in X} b_x.x \:=\: \sum_{x\in X} (a_x+b_x).x.
376: $$
377:
378: \noindent A \emph{(finite) commutative word rewriting system} is a pair $(X,R)$, where $X$ is a (finite) set, called the \emph{alphabet}, and $R$ is a (finite) family of pairs of elements of $[X]$, called the \emph{rules}. If $\alpha=(s(\alpha),t(\alpha))$ is in $R$, the \emph{reduction relation} $\red{\alpha}$ it generates is defined by $a\red{\alpha}b$ if there exists some formal sum $c$ such that $a=c+s(\alpha)$ and $b=c+t(\alpha)$. To any commutative word rewriting system $(X,R)$, one associates a \emph{reduction graph} $G(X,R)$, defined by:
379: \begin{enumerate}
380: \item[0.] The objects of $G(X,R)$ are the elements of $[X]$.
381: \item[1.] The arrows of $G(X,R)$ are the pairs $(c,\alpha)$ made of an element $c$ of $[X]$ and a rule $\alpha=(s(\alpha),t(\alpha))$ in $R$. Such an arrow has source $c+s(\alpha)$ and target $c+t(\alpha)$; it can be written $c+\alpha$.
382: \end{enumerate}
383: \end{defn}
384:
385: \begin{rem}
386: The arrows of $G(X,R)$ are contextual applications of rules: indeed, there is an arrow $(c,\alpha)$ in $G(X,R)$ from $a$ to $b$ if and only if $a\red{\alpha}b$. Furthermore, in this case, $c$ is the context of the application of $\alpha$ at $a$: this is the part that remains unchanged after action of the rule.
387: \end{rem}
388:
389: \begin{rem}
390: In [Guiraud 2004(T)], commutative word rewriting systems are seen as presentations by generators and relations of commutative monoids: indeed, such an object defines a commutative monoid which elements are the connected components of its reduction graph. Conversely, every commutative monoid admits a commutative word rewriting system as a presentation: the generators are the elements of the monoid and the relations are given by the "multiplication" table of the sum.
391: \end{rem}
392:
393: \noindent Following the same idea as in section \ref{sec:reseaux_de_petri}, let us define a congruence relation between paths of the reduction graph of a commutative word rewriting system:
394:
395: \begin{ntt}
396: Let $(X,R)$ be a commutative word rewriting system. The relation $\equi{(X,R)}$ is the congruence relation on paths of $G(X,R)$ generated by the identification of squares of the following shape, with $\alpha$ and $\beta$ in $R$ and $c$ in $[X]$:
397: $$
398: \xymatrix
399: {
400: c + s(\alpha) + s(\beta) \ar[rr]^-{(c+s(\beta))+\alpha} \ar[dd]_-{(c+s(\alpha))+\beta}
401: &&
402: c + t(\alpha) + s(\beta) \ar[dd]^-{(c+t(\alpha))+\beta}
403: \\ \\
404: c + s(\alpha) + t(\beta) \ar[rr]_-{(c+t(\beta))+\alpha}
405: &&
406: c + t(\alpha) + t(\beta).
407: }
408: $$
409: \end{ntt}
410:
411: \noindent Translations between Petri nets and finite commutative word rewriting systems are defined as follows:
412:
413: \begin{defn}
414: Let $N=(X,T,w,w')$ be a Petri net. Its \emph{associated finite commutative word rewriting system} is denoted by $\Phi(N)$ and defined by:
415: \begin{enumerate}
416: \item[-] The alphabet of $\Phi(N)$ is the set $X$ of places of $N$.
417: \item[-] The rules of $\Phi(N)$ are the transitions of $N$, seen as pairs $\alpha=(s(\alpha),t(\alpha))$ with:
418: $$
419: s(\alpha) \:=\: \sum_{x\in X} w(x,\alpha).x \et t(\alpha) \:=\: \sum_{x\in X} w'(\alpha,x).x.
420: $$
421: \end{enumerate}
422:
423: \noindent Conversely, let $(X,R)$ be a finite commutative word rewriting system. Its \emph{associated Petri net} is denoted by~$\Psi(X,R)$ and defined by:
424: \begin{enumerate}
425: \item[-] The places of $\Psi(X,R)$ are the elements of $X$.
426: \item[-] There is one transition in $\Psi(X,R)$ for each rule in $R$.
427: \item[-] The weights $w$ and $w'$ are given, on a place $x$ and a transition $\alpha=(s(\alpha),t(\alpha))$, by:
428: $$
429: w(x,\alpha) \:=\: s(\alpha)_x \et w'(\alpha,x) \:=\: t(\alpha)_x.
430: $$
431: \end{enumerate}
432: \end{defn}
433:
434: \begin{ex}\label{ex:mots_commutatifs}
435: Let us consider the Petri net from example \ref{ex:reseau_de_petri}. The corresponding commutative word rewriting system is the pair $(X,R)$, where $X=\ens{x,y,z}$ and $R$ consists of the two following rewriting rules $\alpha:x\fl y+z$ and $\beta\::\:2y\fl z$. The marking from example \ref{ex:marquage} corresponds to the formal sum $2x+2y$. The reduction graph from example \ref{ex:graphe_de_reduction} becomes:
436: $$
437: \xymatrix{ 2x+2y \ar[dd]_-{x+2y+\alpha} \ar[rr]^-{2x+\beta} && 2x+z \ar[dd]^-{x+z+\alpha} \\ \\ x+3y+z \ar[dd]_-{3y+z+\alpha} \ar[rr]^-{x+y+z+\beta} && x+y+2z \ar[dd]^-{y+2z+\alpha} \\ \\ 4y+2z \ar[rr]_-{2y+2z+\beta} && 2y+3z \ar[rr]_-{3z+\beta} && 4z.}
438: $$
439:
440: \noindent One can check that, in this diagram, any two paths with same source and same target are identified by the congruence $\equi{(X,R)}$: the translation from Petri nets to commutative word rewriting systems seems to preserve the congruence relation we have defined on Petri nets reduction paths.
441: \end{ex}
442:
443: \noindent The following result proves that, in essence, Petri nets and finite commutative word rewriting systems are the same objects and generate the same reduction graphs:
444:
445: \begin{thm}\label{th:comm}
446: For every Petri net $N$, the equality $\Psi\circ\Phi(N)=N$ holds and the reduction graphs~$G(N)$ and $G(\Phi(N))$ are isomorphic. Furthermore, this isomorphism identifies the congruences $\equi{N}$ and $\equi{\Phi(N)}$. Conversely, for every finite commutative word rewriting system $(X,R)$, the equality $\Phi\circ\Psi(X,R)=(X,R)$ holds and the reduction graphs $G(X,R)$ and $G(\Psi(X,R))$ are isomorphic. Furthermore, this isomorphism identifies the congruences $\equi{(X,R)}$ and $\equi{\Psi(X,R)}$.
447: \end{thm}
448:
449: \begin{dem}
450: Let us fix $N=(X,T,w,w')$ and prove the equality $\Psi\circ\Phi(N)=N$. The places of $\Psi\circ\Phi(N)$ are the elements of the alphabet of $\Phi(N)$: these are the places of $N$. The transitions of $\Psi\circ\Phi(N)$ are the rules of $\Phi(N)$: these are the transitions of $N$. Let us fix a place $x$ in $X$ and a transition $\alpha$ in $T$. Let us denote by $\ol{w}$ and $\ol{w}'$ the weighting functions of $\Psi\circ\Phi(N)$ and compare them with $w$ and $w'$. By definition of $\Psi\circ\Phi(N)$:
451: $$
452: \ol{w}(x,\alpha) \:=\: s(\alpha)_x \et \ol{w}'(\alpha,x) \:=\: t(\alpha)_x.
453: $$
454:
455: \noindent And by definition of $\Phi(N)$:
456: $$
457: s(\alpha) \:=\: \sum_{y\in X} w(y,\alpha).y \et t(\alpha) \:=\: \sum_{y\in X} w'(\alpha,y).y.
458: $$
459:
460: \noindent Invoking the fact that $[X]$ is free, one gets:
461: $$
462: s(\alpha)_x \:=\: w(x,\alpha) \et t(\alpha)_x \:=\: w'(x,\alpha).
463: $$
464:
465: \noindent Hence $w=\ol{w}$ and $w'=\ol{w}'$. Now, let us prove that $G(N)$ and $G(\Phi(N))$ are isomorphic graphs. We define a graph morphism $\phi$ from the former to the latter. Let $\mu$ be a marking of $N$ and let us define an element $\phi(\mu)$ in $[X]$ this way:
466: $$
467: \phi(\mu) \:=\: \sum_{x\in X} \mu(x).x.
468: $$
469:
470: \noindent Now, let us consider an arrow $f:\mu\fl\nu$ in $G(N)$. By definition of $G(N)$, this arrow corresponds to a transition $\alpha$ such that $\mu\red{\alpha}\nu$. By definition of the relation $\red{\alpha}$ on markings, this means that:
471: $$
472: \mu(x)\geq w(x,\alpha) \et \nu(x)=\mu(x)-w(x,\alpha)+w'(\alpha,x).
473: $$
474:
475: \noindent Let us prove that $\phi(\mu)\red{\alpha}\phi(\nu)$ is a reduction generated by $(X,R)$. By definition of $\phi$ on markings:
476: $$
477: \Phi(\mu)=\sum_{x\in X} \mu(x).x \et \Phi(\nu)=\sum_{x\in X} \nu(x).x.
478: $$
479:
480: \noindent Hence, proving $\phi(\mu)\red{\alpha}\phi(\nu)$ is equivalent to prove that there exists a $c$ in $[X]$ such that:
481: $$
482: \sum_{x\in X}\mu(x).x=c+s(\alpha) \et \sum_{x\in X}\nu(x).x=c+t(\alpha),
483: $$
484:
485: \noindent Since $\mu(x)\geq w(x,\alpha)$ for every place $x$, the following $c$ is well-defined in $[X]$:
486: $$
487: c=\sum_{x\in X}(\mu(x)-w(x,\alpha)).x.
488: $$
489:
490: \noindent Then:
491: $$
492: c+s(\alpha) \:=\: \sum_{x\in X}(\mu(x)-w(x,\alpha)).x \:+\: \sum_{x\in X} w(x,\alpha).x \:=\: \sum_{x\in X} \mu(x).x.
493: $$
494:
495: \noindent Furthermore, using the fact that $\nu(x)=\mu(x)-w(x,\alpha)+w'(\alpha,x)$ holds for every $x$, one gets:
496: $$
497: c+t(\alpha) \:=\: \sum_{x\in X}(\mu(x)-w(x,\alpha)).x \:+\: \sum_{x\in X}w'(\alpha,x).x \:=\: \sum_{x\in X}\nu(x).x.
498: $$
499:
500: \noindent Hence $\phi(\mu)\red{\alpha}\phi(\nu)$ holds in $[X]$. By definition of $G(\Phi(N))$, this reduction corresponds to an arrow of the form $c+\alpha$, with $c$ in $[X]$, going from $\phi(\mu)$ to $\phi(\nu)$ in $G(\Phi(N))$. Let us define $\phi(f)$ to be this arrow.
501:
502: Let us define a graph morphism $\psi$ from~$G(\Phi(N))$ to~$G(N)$ and prove that it is inverse of $\phi$. Let $a$ be an element of $[X]$. Then $\psi(a)$ is defined as the marking $\psi(a)(x)=a_x$ for every place $x$. Now, let us consider an arrow $c+\alpha$ in $G(\Phi(N))$, which starts at $a=c+s(\alpha)$ and ends at~$b=c+t(\alpha)$. Then, for every place $x$:
503: $$
504: \psi(a)(x) \:=\: a_x \:=\: c_x+s(\alpha)_x \:=\: c_x+w(x,\alpha).
505: $$
506:
507: \noindent Thus $\psi(a)(x)\geq w(x,\alpha)$. Furthermore:
508: $$
509: \psi(b)(x) \:=\: b_x \:=\: c_x+t(\alpha)_x \:=\: \psi(a)(x) - w(x,\alpha)+w'(\alpha,x).
510: $$
511:
512: \noindent Hence $\psi(a)\red{\alpha}\psi(b)$ holds in $\Mr(N)$. This reduction corresponds to an arrow in $G(N)$, which we take as $\psi(c+\alpha)$. Checking that $\psi$ is a left and right inverse for $\phi$ is straightforward.
513:
514: In order to prove that $\phi(\equi{N})$ is $\equi{\Phi(N)}$, we prove that $\phi(\equi{N})$ is included into $\equi{\Phi(N)}$ and that $\psi(\equi{\Phi(N)})$ is included into $\equi{N}$. Furthermore, since $\phi$ and $\psi$ are graph morphisms, it is sufficient to prove these inclusions on paths of minimal lenghts, such as given in the definitions of both congruences.
515:
516: Hence, let us consider two paths $\mu_1\red{\alpha}\nu_1\red{\beta}\mu_2$ and $\mu_1\red{\beta}\nu_2\red{\alpha}\mu_2$ in $G(N)$ such that there exists a marking $\rho$ of $N$ that satisfies the following four equalities for every place $x$:
517: $$
518: \begin{array}{l l l c l l l}
519: \mu_1(x) &=& \rho(x)+w(x,\alpha)+w(x,\beta),
520: &\qquad &\nu_1(x) &=& \rho(x)+w'(\alpha,x)+w(x,\beta), \\
521: \nu_2(x) &=& \rho(x)+w(x,\alpha)+w'(\beta,x),
522: &\qquad &\mu_2(x) &=& \rho(x)+w'(\alpha,x)+w'(\beta,x).
523: \end{array}
524: $$
525:
526: \noindent Let us denote by $c$ the element $\phi(\rho)$ of $[X]$. Then $\phi$ sends both paths onto the following ones, which are identified by $\equi{\Phi(N)}$:
527: $$
528: \xymatrix
529: {
530: c + s(\alpha) + s(\beta) \ar[rr]^-{(c+s(\beta))+\alpha}
531: &&
532: c + t(\alpha) + s(\beta) \ar[rr]^-{(c+t(\alpha))+\beta}
533: &&
534: c + t(\alpha) + t(\beta)
535: }
536: $$
537:
538: \noindent and:
539: $$
540: \xymatrix
541: {
542: c + s(\alpha) + s(\beta) \ar[rr]^-{(c+s(\alpha))+\beta}
543: &&
544: c + s(\alpha) + t(\beta) \ar[rr]^-{(c+t(\beta))+\alpha}
545: &&
546: c + t(\alpha) + t(\beta).
547: }
548: $$
549:
550: \noindent Then, let us consider two paths in $G(\Phi(N))$ written as above, for a given $c$ in $[X]$. Let us denote by $\rho$ the marking $\psi(c)$. Then, if the four markings $\mu_1$, $\mu_2$, $\nu_1$ and $\nu_2$ are defined as above, the graph morphism $\psi$ sends both paths of $G(\Phi(N))$ onto $\mu_1\red{\alpha}\nu_1\red{\beta}\mu_2$ and $\mu_1\red{\beta}\nu_2\red{\alpha}\mu_2$: these two paths are identified by~$\equi{N}$.
551:
552: Conversely, let us consider a finite commutative word rewriting system $(X,R)$ and prove that the equality $\Phi\circ\Psi(X,R)=(X,R)$ holds. By definition of the rewriting system $\Phi\circ\Psi(X,R)$, its alphabet is the set of places of $\Psi(X,R)$: this is the alphabet of $(X,R)$. The rules in $\Phi\circ\Psi(X,R)$ are the pairs $(\ol{s}(\alpha),\ol{t}(\alpha))$ for each transition $\alpha$ in $\Psi(X,R)$, where:
553: $$
554: \ol{s}(\alpha) \:=\: \sum_{x\in X} w(x,\alpha).x \et \ol{t}(\alpha) \:=\: \sum_{x\in X}w'(\alpha,x).x.
555: $$
556:
557: \noindent Furthermore, each transition $\alpha$ in $\Psi(X,R)$ comes from a rule $(s(\alpha),t(\alpha))$ in $R$ and:
558: $$
559: w(x,\alpha) \:=\: s(\alpha)_x \et w'(\alpha,x) \:=\: t(\alpha)_x.
560: $$
561:
562: \noindent Thus, $\ol{s}(\alpha)=s(\alpha)$ and $\ol{t}(\alpha)=t(\alpha)$, so that the set of rules of $\Phi\circ\Psi(X,R)$ is $R$. Hence, the two commutative word rewriting systems $(X,R)$ and $\Phi\circ\Psi(X,R)$ are the same.
563:
564: Let us prove that the two graphs $G(X,R)$ and $G(\Psi(X,R))$ are isomorphic. Since $\Psi(X,R)$ is a Petri net, we already know that $G(\Psi(X,R))$ is isomorphic to $G(\Phi\circ\Psi(X,R))$: this graph is $G(X,R)$ since the equality $\Phi\circ\Psi(X,R)=(X,R)$ holds. Furthermore, this graph isomorphism is defined the same way as $\phi$ and $\psi$ in the first part of the proof. Hence $\phi(\equi{\Psi(X,R)})$ is equal to $\equi{(X,R)}$. If one applies $\psi$, one gets the equality of both congruences $\equi{\Psi(X,R)}$ and $\psi(\equi{(X,R)})$.
565:
566: \findem\end{dem}
567:
568: \begin{rem}
569: This equivalence between Petri nets and finite commutative word rewriting systems highlights the underlying algebraic structure of the formers: one immediate usage is that every arrow in the reduction graph has an explicit name, such as $x+2y+\alpha$, giving the context of application of the rule~$\alpha$.
570: \end{rem}
571:
572: \begin{rem}
573: Another more concrete concrete usage of the translation was developped in the aforementioned [Caprotti Ferscha Hong 1995] and [Chandler Heyworth 2001]: there, it was decribed how Gr\"obner bases can be used to partially solve the reachability problem for Petri nets, when they are seen as commutative word rewriting systems.
574: \end{rem}
575:
576: \begin{rem}
577: If $N$ is a Petri net, the definition of $\equi{N}$ is technical but intuitively simple. The unveiling of the intrinsic algebraic structure of Petri nets makes this definition much simpler. Indeed, let us consider a commutative word rewriting system $(X,R)$ and denote by $\circ$ the composition of paths in the graph $G(X,R)$. Note that this amounts at considering the category $\mon{G(X,R)}$ freely generated by $G(X,R)$, as it is defined in section \ref{sec:2d}. Then, the relation $\equi{(X,R)}$ can be defined as the congruence on $\mon{G(X,R)}$ generated by the following identifications, for any $c$ in $[X]$:
578: $$
579: (c+t(\alpha)+\beta)\circ(c+s(\beta)+\alpha) \:\equiv\: (c+t(\beta)+\alpha)\circ(c+s(\alpha)+\beta).
580: $$
581:
582: \noindent Let us also note that such equations allow the sum of $[X]$ to be naturally extended to reductions: $\alpha+\beta$ will be any side of the given equation for $c=0$. This is also the idea developped with polygraphs in sections~\ref{sec:2d} and~\ref{sec:3d}.
583: \end{rem}
584:
585: \noindent From now on, theorem \ref{th:comm} grants us the right to consider that a Petri net \emph{is} a finite commutative word rewriting system. In fact, the results to be proved are not limited to the finite case. Hence, thereafter, the name Petri net stands for a commutative word rewriting system. Let us use this new equivalent definition to give a different graphical account of Petri nets.
586:
587: %%% section : interprétation bidimensionelle %%%
588: \section{Petri nets as $\mathbf{2}$-dimensional objects}\label{sec:2d}
589:
590: \noindent The goal of this section is to prove that Petri nets have strong links with a certain class of \emph{two-dimensional polygraphs}. The first result presented here, theorem~\ref{th:2d}, is essentially due to Albert Burroni, who gived the idea of the translation. The behaviour of this translation with respect to the congruence on Petri nets reduction paths is new and described in proposition~\ref{prop:2d-equiv}. A discussion follows on many issues to be studied in future work.
591:
592: In order to translate Petri nets into polygraphs, we start by the interpretation of the markings of a Petri net (the formal sums of its places) into $1$-dimensional objects. Let us recall the some classical notions about graphs, free categories and monoids.
593:
594: \begin{ntt}
595: If $G$ is a graph, its set of objects is denoted by $G_0$ and its set of arrows going from an object~$x$ to another object $y$ is denoted by $G(x,y)$; for such an arrow $f$, $s_0(f)$ is the source $x$ of $f$ and~$t_0(f)$ its target $y$. The set of all arrows of $G$ is denoted by $G_1$ and $G$ itself is often abusively denoted by~$(G_0,G_1)$ only, assuming that the source and target mappings are given with $G_1$.
596: \end{ntt}
597:
598: \begin{defn}
599: Let $G=(G_0,G_1)$ be a graph. The \emph{free category generated by $G$}, denoted by $\mon{G}$, is the following (small) category:
600: \begin{enumerate}
601: \item[0.] The objects of $\mon{G}$ are the objects of $G$.
602: \item[1.] The arrows of $\mon{G}$, from $x$ to $y$, are all the finite paths in $G$ going from $x$ to $y$. Their composition, denoted by $\circ$, is the concatenation of paths. The empty paths are local identities for this operation.
603: \end{enumerate}
604:
605: \noindent Such a category is often denoted by $\mon{G}=(\mon{G}_0,\mon{G}_1)$ or just by $(G_0,\mon{G}_1)$, assuming that the source and target mappings are given with the data in $\mon{G}_1$, together with the identities and composition operations.
606: \end{defn}
607:
608: \begin{ex}
609: Let $G=(\ast,X)$ be a graph with only one object ($\ast$ denotes any single-element set); the set of arrows can be any set $X$, with source and target being the only possible map from $X$ to $\ast$. Then the free category $\mon{G}$ is the free monoid $\mon{X}$ generated by $X$: more precisely, the set $\mon{G}(\ast,\ast)$, containing all the arrows of $\mon{G}$, equipped with the composition and the identity of $\ast$, is isomorphic to the free monoid~$\mon{X}$. A proof can be found in [MacLane 1998], for example.
610: \end{ex}
611:
612: \begin{defn}
613: Let $\Cr$ be a category. Two arrows in $\Cr$ are \emph{parallel} when they have same source and same target. A \emph{relation} in $\Cr$ is a pair of parallel arrows of $\Cr$. If $R$ is a family of relations in $\Cr$, the \emph{quotient of~$\Cr$ by $R$} is the category denoted by $\Cr/R$ built this way:
614: \begin{enumerate}
615: \item[0.] The objects of $\Cr/R$ are the objects of $\Cr$.
616: \item[1.] The arrows from $x$ to $y$ in $\Cr/R$ are the elements of $\Cr(x,y)$, \emph{modulo} the reflexive-symmetric-transitive closure $\equi{R}$ of the relation $\red{R}$ defined by: $f\red{R}g$ if there exist a relation $(u,v)$ in $R$ and two arrows $h$ and $k$ in $\Cr$ such that $f=k\circ u\circ h$ and $g=k\circ v\circ h$. The identities of $\Cr/R$ are the equivalence classes of the identity of $\Cr$. The composition of $\Cr/R$ is induced by the one in $\Cr$.
617: \end{enumerate}
618: \end{defn}
619:
620: \begin{rem}
621: The defined object $\Cr/R$ is only a graph. One must check, through easy computations, that the composition of $\Cr$ is compatible with $\equi{R}$: the result of the composition is independent of any choice of representatives. Furthermore, it must be checked that induced composition satisfies the axioms of associativity and left and right units of the category structure.
622: \end{rem}
623:
624: \begin{ex}
625: Let $G=(\ast,X)$ be a graph with one object. On $\mon{G}$, one defines $R$ to be the family of all relations $(x\circ y,y\circ x)$, for $x$ and $y$ in $X$. Then $\mon{G}/R$ is the free commutative monoid $[X]$ generated by the set $X$.
626: \end{ex}
627:
628: \noindent Hence, we have a graphical description of $[X]$. However, the main idea behind higher-dimensional rewriting is to replace any equation between $n$-dimensional objects by a $(n+1)$-dimensional object: equalities are replaced by their proofs - this point of view was developped in both [Burroni 1993] and [Baez Dolan 1998]. Following this leading idea, equalities of the form $x\circ y=y\circ x$ are replaced by $2$-dimensional cells, pasted between parallel paths in the graph $(\ast,X)$, such as the following one:
629: $$
630: \xymatrix{& \ast \ar[dr]^y \ar@{=>}-<0cm,0.5cm>;[dd]+<0cm,0.5cm>^{\tau_{x,y}} \\ \ast \ar[ur]^x \ar[dr]_y && \ast \\ & \ast \ar[ur]_x}
631: $$
632:
633: \begin{rem}
634: In order to achieve commutativity, one may ask that $\tau_{x,y}$ is an isomorphism, with $\tau_{y,x}$ as inverse: in this case, one gets a \emph{categorified} version of the free commutative monoid. Another point of view would be to replace the equalities $\tau_{y,x}\circ\tau_{x,y}=\id_{x\tens y}$ and $\tau_{x,y}\circ\tau_{y,x}=\id_{y\tens x}$ by their proofs: these would be $3$-dimensional cells. This issue is discussed at the end of this section.
635: \end{rem}
636:
637: \noindent So far, we have described an object with one $0$-cell, as many $1$-cells as there are in our set $X$, together with one $2$-cell $\tau_{x,y}$ for each pair $(x,y)$ of distinct elements in $X$. Now, let us consider the rule $\alpha:x\fl y+z$ from example \ref{ex:mots_commutatifs}. Such a rule is also translated as a $2$-dimensional cell:
638: $$
639: \xymatrix{\ast \ar[rr]^x_{}="1" \ar@{=>}"1"-<0cm,0.15cm>;"2,2"+<0cm,0.3cm>^{\alpha} \ar[dr]_y && \ast \\ & \ast \ar[ur]_z }
640: $$
641:
642: \noindent A choice has been made in order to represent the rule $\alpha$. Indeed, it could have been seen as transforming~$x$ into $z+y$, which is equal to $y+z$ in the commutative monoid $[X]$. This is the arbitrary part of the presented $2$-polygraphic interpretation of Petri nets: it assumes that, for every element $a$ in $[X]$, a representative has been chosen in $\mon{X}$.
643:
644: Since we must use the axiom of choice, let us apply the equivalent Zermelo theorem and assume, until the end of this section, that, for every Petri net $(X,R)$, the set $X$ comes equipped with a total order. Then, every element $a$ of $[X]$ has a unique decomposition $a=n_1.x_1+\dots+n_k.x_k$, where the $n_i$ are non-zero natural numbers and the $x_i$ are elements of $X$ such that $x_1<\dots<x_k$.
645:
646: \begin{ntt}
647: Let $X$ be a set and $a$ an element of $[X]$. Let us denote by $n_1.x_1+\dots+n_k.x_k$ the unique decomposition of $a$. Then $\ol{a}$ denotes the representative $x_1^{n_1}\dots x_k^{n_k}$ of $a$ in $\mon{X}$, where $x^n$ is the product in $\mon{X}$ of $n$ copies of $x$.
648: \end{ntt}
649:
650: \noindent Until now, we have constructed a composite object $\Sigma=(\Sigma_0,\Sigma_1,\Sigma_2)$, made of sets $\Sigma_i$ of $i$-dimensional cells. On top of these three sets, $\Sigma$ also contains boundaries informations: for example, the cell~$\tau_{x,y}$ has source~$x\circ y$ and target $y\circ x$, while $\alpha$ has source $x$ and target $y\circ z$.
651:
652: Such an object is called a \emph{polygraph}: it is the central structure studied in \emph{higher-dimensional rewriting}. Here, the object $\Sigma$ is a $2$-dimensional polygraph or $2$-polygraph for short. Its definition is recalled from [Burroni 1993].
653:
654: \begin{defn}\label{def:2-polygraphe}
655: A \emph{$\mathit{2}$-polygraph} $\Sigma$ is given by:
656: \begin{enumerate}
657: \item[0.] A set $\Sigma_0$ of \emph{$\mathit{0}$-cells}.
658: \item[1.] A set $\Sigma_1$ of \emph{$\mathit{1}$-cells}, together with two maps $s_0,t_0:\Sigma_1\fl\Sigma_0$, called \emph{$\mathit{0}$-source} and \emph{$\mathit{0}$-target}. The arrows of the free category $(\Sigma_0,\mon{\Sigma}_1)$ are called \emph{$\mathit{1}$-arrows}. The composition of $f$ followed by $g$ is denoted by $f\star_0g$ or $g\circ_0f$ in the general case and $f\tens g$ when $\Sigma_0$ has only one element.
659: \item[2.] A set $\Sigma_2$ of \emph{$\mathit{2}$-cells}, together with two maps $s_1,t_1:\Sigma_2\fl\mon{\Sigma}_1$, called \emph{$\mathit{1}$-source} and \emph{$\mathit{1}$-target}, and such that $s_0\circ s_1=s_0\circ t_1$ and $t_0\circ s_1 = t_0\circ t_1$. The first equality gives a map $s_0:\Sigma_2\fl\Sigma_0$ and the second one yields $t_0:\Sigma_2\fl\Sigma_0$.
660: \end{enumerate}
661: \end{defn}
662:
663: \begin{defn}
664: Let $(X,R)$ be a Petri net, such that $X$ is equipped with a total order. The \emph{$\mathit{2}$-polygraph associated with $(X,R)$} is $\Sigma^2(X,R)$ defined this way:
665: \begin{enumerate}
666: \item[0.] There is one $0$-cell in $\Sigma^2(X,R)$, denoted by $\ast$.
667: \item[1.] The $1$-cells of $\Sigma^2(X,R)$ are the elements of $X$, with the only possible $0$-source and $0$-target maps.
668: \item[2.] The $2$-cells of $\Sigma^2(X,R)$ consist of all the $\tau_{x,y}$, for $x\neq y$ in $X$, together with one $2$-cell $\alpha$ for each rule in $R$. The $1$-source and $1$-target maps are given by:
669: $$
670: s_1(\tau_{x,y})\:=\: x\tens y, \quad t_1(\tau_{x,y})\:=\: y\tens x, \quad s_1(\alpha)\:=\: \ol{s(\alpha)}, \quad t_1(\alpha)\:=\: \ol{t(\alpha)}.
671: $$
672: \end{enumerate}
673: \end{defn}
674:
675: \noindent In order to compare a Petri net to its associated $2$-polygraph, we define a notion of reduction graph for these objects. The idea is to see every $2$-cell of a $2$-polygraph as a rewriting rule on $1$-arrow, that can be applied in any context: a $2$-cell $\alpha$ can be applied on any $1$-arrow of the shape $u\tens s_1(\phi)\tens v$, in order to produce the $1$-arrow $u\tens t_1(\phi)\tens v$. Let us formalize this idea.
676:
677: \begin{defn}
678: Let $\Sigma=(\Sigma_0,\Sigma_1,\Sigma_2)$ be a $2$-polygraph. The \emph{reduction graph associated to $\Sigma$}, denoted by $G(\Sigma)$, is defined this way:
679: \begin{enumerate}
680: \item[0.] The objects of $G(\Sigma)$ are the $1$-arrows of $\Sigma$.
681: \item[1.] The arrows from $f$ to $g$ in $G(\Sigma)$ are the triples $(h,\phi,k)$ where $h$ and $k$ are $1$-arrows in $\mon{\Sigma}_1$ and~$\phi$ is a $2$-cell in $\Sigma_2$ such that the following equalities hold:
682: $$
683: f \:=\: h\star_0 s_1(\phi)\star_0 k \et g \:=\: h\star_0 t_1(\phi)\star_0 k.
684: $$
685:
686: \noindent A triple $(h,\phi,k)$ is denoted $h\star_0\phi\star_0 k$, and $h\star_0$ (resp. $\star_0 k$) is dropped when $h$ (resp. $k$) is an identity (an empty path).
687: \end{enumerate}
688: \end{defn}
689:
690: \noindent We want to prove that the two graphs $G(X,R)$ and $G(\Sigma^2(X,R))$ have strong links. To begin with, let us note that the objects of the graph $G(\Sigma^2(X,R))$ are the elements of the free monoid $\mon{X}$, while the objects of the graph $G(X,R)$ are the ones of the free commutative monoid $[X]$. We define $\pi:\mon{X}\mfl[X]$ to be the canonical projection.
691:
692: \begin{lem}\label{lem:relevement}
693: Let $u$ and $v$ be two elements in $\mon{X}$ such that $\pi(u)=\pi(v)$. Then, there exists an arrow $f$ in $G(\Sigma^2(X,R))$ with source $u$ and target $v$, such that $f$ has a decomposition of the form:
694: $$
695: f \:=\: (u_n\tens\tau_{x_n,y_n}\tens v_n)\circ\dots\circ(u_1\tens\tau_{x_1,y_1}\tens v_1).
696: $$
697: \end{lem}
698:
699: \begin{dem}
700: Since $\mon{X}$ is freely generated by $X$, the elements $u$ and $v$ uniquely decompose as:
701: $$
702: u \:=\: z_1\tens\dots\tens z_p \et v \:=\: z'_1\tens\dots\tens z'_{p'},
703: $$
704:
705: \noindent with the $z_i$ and $z'_i$ in $X$. Since $\pi(u)=\pi(v)$, the following equality holds in $[X]$:
706: $$
707: z_1+\dots+z_p \:=\: z'_1+\dots+z'_{p'}.
708: $$
709:
710: \noindent Hence, since $[X]$ is freely generated by $X$, we get that $p=p'$ and that there exists a permutation $\sigma$ in $\Sk_p$ such that, for every $i\in\dens{1}{p}$, $z'_{\sigma(i)}=z_i$. Let us consider a decomposition of the permutation $\sigma$ in~$n$ transpositions:
711: $$
712: \sigma \:=\: \tau_{i_n}\circ\dots\circ\tau_{i_1},
713: $$
714:
715: \noindent where each $i_j$ is in $\dens{1}{p-1}$ and $\tau_{i_j}$ is the transposition that exchanges $i_j$ and $i_{j+1}$. Let us fix the following notations:
716: $$
717: u_1 \:=\: z_1\tens\dots\tens z_{i_1-1}, \quad x_1 \:=\: z_{i_1}, \quad y_1 \:=\: z_{i_1+1}, \quad v_1 \:=\: z_{i_1+2}\tens\dots\tens z_p.
718: $$
719:
720: \noindent Then, the arrow $f_1=u_1\tens\tau_{x_1,y_1}\tens v_1$ of $G(\Sigma^2(X,R))$ has source $u$ and target:
721: $$
722: z_1\tens\dots\tens z_{i_1-1}\tens z_{i_1+1}\tens z_{i_1}\tens z_{i_1+2}\tens\dots\tens z_p.
723: $$
724:
725: \noindent But this element of $\mon{X}$ can also be written as $z_{\tau_{i_1}(1)}\tens\dots\tens z_{\tau_{i_1}(p)}$. Hence, if we repeat this construction for each $\tau_{i_j}$, we prove, by induction on the length of the decomposition of $\sigma$, that the target of the last arrow $f_n=u_n\tens\tau_{x_n,y_n}\tens v_n$, associated with $\tau_{i_n}$, is:
726: $$
727: v \:=\: z_{\sigma(1)}\tens\dots\tens z_{\sigma(p)}.
728: $$
729:
730: \noindent In conclusion, $f=f_n\circ\dots\circ f_1$ satisfies the required hypotheses.
731:
732: \findem\end{dem}
733:
734: \noindent Now, the main result of this section can be proved. As mentioned earlier, this result formalizes a construction due to Albert Burroni:
735:
736: \begin{thm}\label{th:2d}
737: Let $(X,R)$ be a Petri net. The following equalities extend the canonical map $\pi$ into a surjective functor from the free category~$\mon{G(\Sigma^2(X,R))}$ to the free category $\mon{G(X,R)}:$
738: $$
739: \pi(u\tens\tau_{x,y}\tens v) \:=\: \id_{\pi(u)+x+y+\pi(v)} \et \pi(u\tens\alpha\tens v) \:=\: \pi(u)+\pi(v)+\alpha.
740: $$
741: \end{thm}
742:
743: \begin{dem}
744: The equalities extend $\pi$ so that it is now defined on every object and arrow of the reduction graph~$G(\Sigma^2(X,R))$ and takes its values into the free category $\mon{G(X,R)}$. Hence, a classical categorical argument tells us that $\pi$ uniquely extends into a functor, still denoted by $\pi$, from the free category~$\mon{G(\Sigma^2(X,R))}$ to the free category $\mon{G(X,R)}$. Now, let us prove that $\pi$ is surjective, which means that both its restrictions on objects and on arrows are surjective. On objects, $\pi$ is the canonical morphism from the free monoid $\mon{X}$ to the free commutative monoid $[X]$, which is surjective.
745:
746: Let us consider two objects $a$ and $b$ in $\mon{G(X,R)}$: they are elements of the free commutative monoid~$[X]$. Let $f$ be an arrow in $\mon{G(X,R)}$ from $a$ to $b$. By definition of $G(X,R)$ and of the free category it generates, this means that $f$ uniquely decomposes as:
747: $$
748: f=(c_k+\alpha_k)\circ\dots\circ(c_1+\alpha_1),
749: $$
750:
751: \noindent with the $c_i$ in $[X]$ and the $\alpha_i$ in $R$, such that the following relations hold in $[X]$:
752: $$
753: c_1+s(\alpha_1)\:=\: a, \quad c_i+t(\alpha_i)\:=\: c_{i+1}+s(\alpha_{i+1}), \quad c_k+t(\alpha_k)\:=\:b.
754: $$
755:
756: \noindent Let us denote by $f_i$ the arrow $\ol{c_i}\tens\alpha_i$ in $G(\Sigma^2(X,R))$: it has source $\ol{c_i}\tens\ol{s(\alpha_i)}$ and target $\ol{c_i}\tens\ol{t(\alpha_i)}$. Hence, the equalities $\pi(s(f_1))=a$ and $\pi(t(f_n))=b$ hold. There remains to link all the $f_i$ in order to conclude. Indeed, the relation $t(f_i)=s(f_{i+1})$ does not necessarily hold for every $i$, so that $f_i$ and $f_{i+1}$ are not composable in general.
757:
758: However, the relation $\pi(t(f_i))=\pi(s(f_{i+1}))$ holds, by assumption, for every $i$. By application of lemma~\ref{lem:relevement}, we know that there exist arrows $g_1$, $\dots$, $g_{k-1}$ in $\mon{G(\Sigma^2(X,R))}$ such that each one is a composition of arrows of the form $(u\tens\tau_{x,y}\tens v)$ and such that the following diagram is an arrow of~$\mon{G(\Sigma^2(X,R))}$:
759: $$
760: \xymatrix{ \ol{a} \ar[r]^-{f_1} & \ol{c_1}\tens\ol{t(f_1)} \ar[r]^-{g_1} & \ol{c_2}\tens\ol{s(f_2)} \ar[r]^-{f_2} & \dots \ar[r]^-{g_{k-1}} & \ol{c_k}\tens\ol{s(f_k)} \ar[r]^-{f_k} & \ol{b}.}
761: $$
762:
763: \noindent Finally, from the definition of the functor $\pi$, we conclude that:
764: $$
765: \pi(g_i)=\id_{c_i+t(f_i)} \:=\: \id_{c_{i+1}+s(f_{i+1})} \et \pi(f_i) \:=\: c_i+\alpha_i.
766: $$
767:
768: \noindent Hence $\pi(f_k\circ g_k\circ\dots\circ g_1\circ f_1)=f$, so that $\pi$ is a surjective functor.
769:
770: \findem\end{dem}
771:
772: \noindent So far, we have built a new graphical object $G(\Sigma^2(X,R))$ in which every path represents a possible evolution of the Petri net $(X,R)$ and in which every possible evolution has a representative.
773:
774: But $G(\Sigma^2(X,R))$ is not the natural object one would build from the $2$-polygraph $\Sigma^2(X,R)$: indeed, such a polygraph is a presentation of a $2$-category, which is a quotient of $\mon{G(\Sigma^2(X,R))}$ by some topology-flavoured relations. Furthermore, we will see that these relations are the ones that identify the intuitively equal paths from examples \ref{ex:graphe_de_reduction} and \ref{ex:mots_commutatifs}.
775:
776: Here we only define the notion of \emph{free $2$-category} generated by a $2$-polygraph with one $0$-cell, while the complete construction is in [Burroni 1993] and [Métayer 2003]. After the formal algebraic definition, we give the topological intuition that underlies it.
777:
778: \begin{defn}
779: Let $\Sigma=(\ast,\Sigma_1,\Sigma_2)$ be a $2$-polygraph with one $0$-cell. The \emph{free $\mathit{2}$-category} generated by $\Sigma$, denoted by $\mon{\Sigma}$, is the following $2$-polygraph:
780: \begin{enumerate}
781: \item[0.] It has one $0$-cell.
782: \item[1.] Its $1$-cells are the $1$-arrows of $\Sigma$, which are the elements of $\mon{\Sigma}_1$.
783: \item[2.] Its $2$-cells, called \emph{$\mathit{2}$-arrows}, from $u$ to $v$ are the paths in the reduction graph $G(\Sigma)$, \emph{modulo} the congruence $\equi{01}$ generated by the following \emph{exchange relations} (where $g\circ f$ is written with $f$ on top of $g$ in order to match the graphical representations to be introduced):
784: $$
785: \begin{array}{c c c}
786: u\tens\phi\tens(v\tens s_1(\psi)\tens w)
787: && (u\tens s_1(\phi)\tens v)\tens\psi\tens w \\
788: \circ & \qquad\equiv\qquad & \circ \\
789: (u\tens t_1(\phi)\tens v)\tens\psi\tens w
790: && u\tens\phi\tens(v\tens t_1(\psi)\tens w)
791: \end{array}
792: $$
793:
794: \noindent for every $2$-cells $\phi$ and $\psi$, every $1$-arrows $u$, $v$ and $w$ and where $\circ$ denotes the composition of paths in $G(\Sigma)$.
795: \end{enumerate}
796:
797: \noindent The $2$-arrows, collectively denoted by $\mon{\Sigma}_2$, are equipped with two compositions: the first one is $\circ$, the operation yielded by the composition of paths in $G(\Sigma)$; the second one is an extension of $\tens$, allowed by the exchange relations, which is defined by functorial extension of:
798: $$
799: \begin{array}{c c c}
800: && (u\tens s_1(\phi)\tens v\tens u')\tens\phi'\tens v' \\
801: (u\tens\phi\tens v)\tens(u'\tens\phi'\tens v') &
802: \quad=\quad & \circ \\
803: && u\tens\phi\tens(v\tens u'\tens t_1(\phi')\tens v')
804: \end{array}
805: $$
806:
807: \end{defn}
808:
809: \begin{rem}
810: This definition can be quite obscure and the $2$-arrows of the free $2$-category are hard to represent with the traditional cellular graphical representation. However, they become really easy to handle when using a dual representation, making the $2$-dimensional arrows appear as circuits. Let us explain how this representation is built in the case of a $2$-polygraph $\Sigma=(\ast,\Sigma_1,\Sigma_2)$ with one $0$-cell.
811:
812: Each $1$-cell $x$ is drawn as a vertical wire, labelled with $x$ (or with any symbol or color associated to the $1$-cell~$x$). A $1$-arrow is drawn as the horizontal juxtaposition of the wires representing the $1$-cells it is made of. Hence, the empty path $\id_{\ast}$ is pictured as an empty diagram and the $1$-arrow $x_1\tens\dots\tens x_n$ as:
813: \begin{center}
814: \begin{picture}(0,0)%
815: \includegraphics{1_fleche.eps}%
816: \end{picture}%
817: \setlength{\unitlength}{4144sp}%
818: %
819: \begingroup\makeatletter\ifx\SetFigFont\undefined%
820: \gdef\SetFigFont#1#2#3#4#5{%
821: \reset@font\fontsize{#1}{#2pt}%
822: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
823: \selectfont}%
824: \fi\endgroup%
825: \begin{picture}(2350,798)(-409,107)
826: \put(-179,749){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x_1$}%
827: }}}}
828: \put(1711,749){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x_n$}%
829: }}}}
830: \put(1261,749){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x_{n-1}$}%
831: }}}}
832: \put(271,749){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x_2$}%
833: }}}}
834: \end{picture}%
835: \end{center}
836:
837: \noindent A $2$-cell $\phi:u\fl v$ is pictured as a circuit component, with the wires corresponding to $u$ on top, the ones for $v$ at the bottom, such as:
838: \begin{center}
839: \begin{picture}(0,0)%
840: \includegraphics{2_cellule.eps}%
841: \end{picture}%
842: \setlength{\unitlength}{4144sp}%
843: %
844: \begingroup\makeatletter\ifx\SetFigFont\undefined%
845: \gdef\SetFigFont#1#2#3#4#5{%
846: \reset@font\fontsize{#1}{#2pt}%
847: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
848: \selectfont}%
849: \fi\endgroup%
850: \begin{picture}(744,1081)(439,-335)
851: \put(811,-286){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v$}%
852: }}}}
853: \put(811,164){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
854: }}}}
855: \put(811,614){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u$}%
856: }}}}
857: \end{picture}%
858: \end{center}
859:
860: \noindent A $2$-arrow is pictured as a circuit built from the circuit components corresponding to the $2$-cells it is made of. The two compositions $\tens$ and $\circ$ are respectively represented as horizontal juxtaposition and vertical branching:
861: \begin{center}
862: \begin{picture}(0,0)%
863: \includegraphics{compositions.eps}%
864: \end{picture}%
865: \setlength{\unitlength}{4144sp}%
866: %
867: \begingroup\makeatletter\ifx\SetFigFont\undefined%
868: \gdef\SetFigFont#1#2#3#4#5{%
869: \reset@font\fontsize{#1}{#2pt}%
870: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
871: \selectfont}%
872: \fi\endgroup%
873: \begin{picture}(5604,1138)(79,-236)
874: \put(5446,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u$}%
875: }}}}
876: \put(676,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tens$}%
877: }}}}
878: \put(316,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
879: }}}}
880: \put(1036,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi'$}%
881: }}}}
882: \put(316,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u$}%
883: }}}}
884: \put(316,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v$}%
885: }}}}
886: \put(1036,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u'$}%
887: }}}}
888: \put(1036,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v'$}%
889: }}}}
890: \put(1486,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
891: }}}}
892: \put(2206,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u\tens u'$}%
893: }}}}
894: \put(2206,-16){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v\tens v'$}%
895: }}}}
896: \put(1936,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
897: }}}}
898: \put(2431,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi'$}%
899: }}}}
900: \put(5446,479){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
901: }}}}
902: \put(5446,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\psi$}%
903: }}}}
904: \put(4546,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
905: }}}}
906: \put(3826,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\psi$}%
907: }}}}
908: \put(4996,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
909: }}}}
910: \put(4186,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\circ$}%
911: }}}}
912: \put(4546,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u$}%
913: }}}}
914: \put(4546,-16){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v$}%
915: }}}}
916: \put(3826,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v$}%
917: }}}}
918: \put(3826,-16){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$w$}%
919: }}}}
920: \put(5446,-196){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$w$}%
921: }}}}
922: \end{picture}%
923: \end{center}
924:
925: \noindent The circuits are identified \emph{modulo} homeomorphic deformation, which exactly corresponds to the equations of the $2$-category structure. For example, the exchange relations are pictured this way:
926: \begin{center}
927: \begin{picture}(0,0)%
928: \includegraphics{echange.eps}%
929: \end{picture}%
930: \setlength{\unitlength}{4144sp}%
931: %
932: \begingroup\makeatletter\ifx\SetFigFont\undefined%
933: \gdef\SetFigFont#1#2#3#4#5{%
934: \reset@font\fontsize{#1}{#2pt}%
935: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
936: \selectfont}%
937: \fi\endgroup%
938: \begin{picture}(4074,834)(79,-253)
939: \put(1351,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equiv$}%
940: }}}}
941: \put(856,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi'$}%
942: }}}}
943: \put(316,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
944: }}}}
945: \put(1846,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
946: }}}}
947: \put(2386,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi'$}%
948: }}}}
949: \put(3916,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi'$}%
950: }}}}
951: \put(3376,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\phi$}%
952: }}}}
953: \put(2881,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equiv$}%
954: }}}}
955: \end{picture}%
956: \end{center}
957: \end{rem}
958:
959: \begin{ex}\label{ex:circuits}
960: Let us consider the Petri net $(X,R)$ from example \ref{ex:reseau_de_petri}. Its associated $2$-polygraph is made of one $0$-cell $\ast$, three $1$-cells $x$, $y$ and $z$ and eight $2$-cells pictured as:
961: \begin{center}
962: \begin{picture}(0,0)%
963: \includegraphics{cellules_exemple.eps}%
964: \end{picture}%
965: \setlength{\unitlength}{4144sp}%
966: %
967: \begingroup\makeatletter\ifx\SetFigFont\undefined%
968: \gdef\SetFigFont#1#2#3#4#5{%
969: \reset@font\fontsize{#1}{#2pt}%
970: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
971: \selectfont}%
972: \fi\endgroup%
973: \begin{picture}(4191,754)(1685,-20)
974: \put(1981,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
975: }}}}
976: \put(2341,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
977: }}}}
978: \put(2521,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
979: }}}}
980: \put(2431,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
981: }}}}
982: \put(3061,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
983: }}}}
984: \put(3061,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
985: }}}}
986: \put(2881,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
987: }}}}
988: \put(2881,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
989: }}}}
990: \put(3421,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
991: }}}}
992: \put(3601,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
993: }}}}
994: \put(3421,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
995: }}}}
996: \put(3601,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
997: }}}}
998: \put(3961,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
999: }}}}
1000: \put(4141,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1001: }}}}
1002: \put(3961,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1003: }}}}
1004: \put(4141,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1005: }}}}
1006: \put(5041,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1007: }}}}
1008: \put(5221,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1009: }}}}
1010: \put(5041,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1011: }}}}
1012: \put(5221,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1013: }}}}
1014: \put(5581,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1015: }}}}
1016: \put(5761,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1017: }}}}
1018: \put(5581,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1019: }}}}
1020: \put(5761,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1021: }}}}
1022: \put(4681,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1023: }}}}
1024: \put(4501,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1025: }}}}
1026: \put(4501,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1027: }}}}
1028: \put(4681,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1029: }}}}
1030: \put(1891, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1031: }}}}
1032: \put(2431, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
1033: }}}}
1034: \put(2971, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tau_{x,y}$}%
1035: }}}}
1036: \put(3511, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tau_{y,x}$}%
1037: }}}}
1038: \put(4051, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tau_{x,z}$}%
1039: }}}}
1040: \put(4591, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tau_{z,x}$}%
1041: }}}}
1042: \put(5131, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tau_{y,z}$}%
1043: }}}}
1044: \put(5671, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\tau_{z,y}$}%
1045: }}}}
1046: \put(1891,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1047: }}}}
1048: \put(1801,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1049: }}}}
1050: \end{picture}%
1051: \end{center}
1052:
1053: \noindent Then one considers the reduction graph from examples \ref{ex:graphe_de_reduction} and \ref{ex:mots_commutatifs}. As we have seen, all the paths in this diagram can be lifted to representatives in the free category $\mon{G(\Sigma^2(X,R)}$. These representatives are organized in a diagram such as the following one:
1054: $$
1055: \xymatrix
1056: {
1057: x^2\tens y^2
1058: \ar[rrr]^-{x^2\tens\beta}
1059: \ar[d]_-{\alpha\tens x\tens y^2}
1060: &&&
1061: x^2\tens z
1062: \ar[d]^-{\alpha\tens x\tens z}
1063: \\
1064: y\tens z\tens x\tens y^2
1065: \ar[rrr]^-{y\tens z\tens x\tens\beta}
1066: \ar[d]_-{y\tens z\tens\alpha\tens y^2}
1067: &&&
1068: y\tens z\tens x\tens z
1069: \ar[d]^-{y\tens z\tens\alpha\tens z}
1070: \\
1071: y\tens z\tens y\tens z\tens y^2
1072: \ar[rrr]^-{y\tens z\tens y\tens z\tens\beta}
1073: \ar[d]_-{y\tens\tau_{z,y}\tens z\tens y^2}
1074: &&&
1075: y\tens z\tens y\tens z^2
1076: \ar[d]^-{y\tens\tau_{z,y}\tens z^2}
1077: \\
1078: y^2\tens z^2\tens y^2
1079: \ar[rrr]^-{y^2\tens z^2\tens\beta}
1080: \ar[d]_-{\beta\tens z^2\tens y^2}
1081: &&&
1082: y^2\tens z^3
1083: \ar[d]^-{\beta\tens z^2\tens y^2}
1084: \\
1085: z^3\tens y^2
1086: \ar[rrr]^-{z^3\tens\beta}
1087: &&&
1088: z^4.
1089: }
1090: $$
1091:
1092: \noindent In this diagram, all parallel paths only differ by the order of application of the same $2$-cells in different parts of the same $1$-arrows: hence they are identified by the exchange relations, which means that they become equal in the free $2$-category generated by $\Sigma^2(X,R)$. For example, the $2$-arrow corresponding to any composite from $x^2\tens y^2$ to $z^4$ is written as $(\beta\tens z^3)\circ(y\tens\tau_{z,y}\tens z^2)\circ(\alpha\tens\alpha\tens\beta)$ and is pictured as the following more-readable circuit:
1093: \begin{center}
1094: \begin{picture}(0,0)%
1095: \includegraphics{reduction_exemple.eps}%
1096: \end{picture}%
1097: \setlength{\unitlength}{4144sp}%
1098: %
1099: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1100: \gdef\SetFigFont#1#2#3#4#5{%
1101: \reset@font\fontsize{#1}{#2pt}%
1102: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1103: \selectfont}%
1104: \fi\endgroup%
1105: \begin{picture}(1049,970)(1317,-1001)
1106: \put(1801,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1107: }}}}
1108: \put(1441,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1109: }}}}
1110: \put(2071,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1111: }}}}
1112: \put(2251,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1113: }}}}
1114: \put(1441,-961){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1115: }}}}
1116: \put(1711,-961){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1117: }}}}
1118: \put(1891,-961){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1119: }}}}
1120: \put(2161,-961){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1121: }}}}
1122: \end{picture}%
1123: \end{center}
1124: \end{ex}
1125:
1126: \noindent From this example, it seems that the congruences $\equi{(X,R)}$ in $\mon{G(X,R)}$ and $\equi{01}$ in $\mon{G(\Sigma^2(X,R))}$ are linked in some way. For that, we denote by $\Gr(X,R)$ the quotient category $\mon{G(X,R)}/\equi{(X,R)}$.
1127:
1128: \begin{prop}\label{prop:2d-equiv}
1129: Let $(X,R)$ be a Petri net. The functor $\pi:\mon{G(\Sigma^2(\Sigma,R))}\fl\mon{G(X,R)}$ induces a functor $\ol{\pi}:\mon{\Sigma^2(X,R)}\fl\Gr(X,R)$.
1130: \end{prop}
1131:
1132: \begin{dem}
1133: We have to check that, whenever $f$ and $g$ are parallel arrows in $G(\Sigma^2(X,R))$ such that $f\equi{01} g$, we have $\pi(f)\equi{(X,R)}\pi(g)$. Let $u$, $v$, $w$ be $1$-arrows and $\alpha$, $\beta$ be $2$-cells in $\Sigma^2(X,R)$. Then, by definition of the functor~$\pi$, the following four equalities hold:
1134: $$
1135: \left\{
1136: \begin{array}{r c l}
1137: \pi(u\tens\alpha\tens v\tens s_1(\beta)\tens w) &\:=\: &(u+v+w+s_1(\beta))+\alpha, \\
1138: \pi(u\tens\alpha\tens v\tens t_1(\beta)\tens w) &\:=\: &(u+v+w+t_1(\beta))+\alpha, \\
1139: \pi(u\tens s_1(\alpha)\tens v\tens\beta\tens w) &\:=\: &(u+v+w+s_1(\alpha))+\beta, \\
1140: \pi(u\tens t_1(\alpha)\tens v\tens\beta\tens w) &\:=\: &(u+v+w+t_1(\alpha))+\beta.
1141: \end{array}
1142: \right.
1143: $$
1144:
1145: \noindent Thus, the functor $\pi$ satisfies:
1146: $$
1147: \pi\left(
1148: \begin{array}{c}
1149: u\tens\phi\tens(v\tens s_1(\psi)\tens w) \\
1150: \circ \\
1151: (u\tens t_1(\phi)\tens v)\tens\psi\tens w
1152: \end{array}
1153: \right)
1154: \qquad\equi{(X,R)}\qquad
1155: \pi\left(
1156: \begin{array}{c}
1157: (u\tens s_1(\phi)\tens v)\tens\psi\tens w \\
1158: \circ \\
1159: u\tens\phi\tens(v\tens t_1(\psi)\tens w)
1160: \end{array}
1161: \right).
1162: $$
1163:
1164: \noindent Since $\pi$ is a functor, we get that $\pi(f)\equi{(X,R)}\pi(g)$ for any two parallel $f$ and $g$ such that $f\equi{01}g$.
1165:
1166: \findem\end{dem}
1167:
1168: \noindent For the moment, we have seen that Petri nets can be translated as $2$-polygraphs $\Sigma=(\ast,\Sigma_1,\Sigma_2\amalg S_{\Sigma_1})$ where $\Sigma_1$ and $\Sigma_2$ are finite sets and where $S_X$ denotes the set of all $2$-cells $\tau_{x,y}$, with $x$ and $y$ distinct elements in~$X$.
1169:
1170: Conversely, given any $2$-polygraph of the form $\Sigma=(\ast,\Sigma_1,\Sigma_2\amalg S_{\Sigma_1})$ with $\Sigma_1$ and $\Sigma_2$ finite, one can build a Petri net with alphabet $\Sigma_1$ and rules given by the projection through $\pi:\mon{\Sigma_1}\fl[\Sigma_1]$ of the $2$-cells of $\Sigma_2$. Furthermore, it can be proved that the two transformations between Petri nets and $2$-polygraphs of this form are inverse to each other.
1171:
1172: Hence, we could state that Petri nets \emph{are} $2$-polygraphs of the form $\Sigma=(\ast,\Sigma_1,\Sigma_2\amalg S_{\Sigma_1})$. However, this would be quite excessive since there are much more $2$-arrows in $\mon{\Sigma}$ than rewriting paths in the corresponding Petri net.
1173:
1174: \begin{ex}
1175: Once again, let us consider the Petri net from example \ref{ex:reseau_de_petri} and the path in $\Gr(X,R)$ given in examples \ref{ex:graphe_de_reduction} and \ref{ex:mots_commutatifs}. In example \ref{ex:circuits}, we have already seen a $2$-arrow of $\mon{\Sigma^2(X,R)}$ representing this reduction path. The following parallel $2$-arrows are also possible representatives for this path:
1176: \begin{center}
1177: \begin{picture}(0,0)%
1178: \includegraphics{representants.eps}%
1179: \end{picture}%
1180: \setlength{\unitlength}{4144sp}%
1181: %
1182: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1183: \gdef\SetFigFont#1#2#3#4#5{%
1184: \reset@font\fontsize{#1}{#2pt}%
1185: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1186: \selectfont}%
1187: \fi\endgroup%
1188: \begin{picture}(4288,1150)(-122,-281)
1189: \put(2341,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1190: }}}}
1191: \put(3241,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1192: }}}}
1193: \put(3601,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1194: }}}}
1195: \put(3871,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1196: }}}}
1197: \put(4051,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1198: }}}}
1199: \put(3151,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1200: }}}}
1201: \put(3331,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1202: }}}}
1203: \put(3601,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1204: }}}}
1205: \put(3961,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1206: }}}}
1207: \put( 1,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1208: }}}}
1209: \put(631,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1210: }}}}
1211: \put(811,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1212: }}}}
1213: \put( 1,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1214: }}}}
1215: \put(271,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1216: }}}}
1217: \put(451,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1218: }}}}
1219: \put(721,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1220: }}}}
1221: \put(361,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1222: }}}}
1223: \put(1666,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1224: }}}}
1225: \put(2071,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1226: }}}}
1227: \put(2251,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1228: }}}}
1229: \put(2431,749){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1230: }}}}
1231: \put(1621,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1232: }}}}
1233: \put(1891,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1234: }}}}
1235: \put(2071,-241){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1236: }}}}
1237: \end{picture}%
1238: \end{center}
1239: \end{ex}
1240:
1241: \noindent Hence, even if there is a correspondance between Petri nets and $2$-polygraphs $\Sigma=(\ast,\Sigma_1,\Sigma_2\amalg S_{\Sigma_1})$, both objects do not naturally generate the same reduction graphs since $\mon{\Sigma^2(X,R)}$ is bigger than $\Gr(X,R)$. There are many possible solutions to this problem. One possibility is to add relations between parallel $2$-arrows of $\Sigma$ that represent the same path in the Petri net reduction graph: we are going to sketch such a study in the rest of this section. Another really different solution is studied in section~\ref{sec:3d}, where we use the fact that commutative monoids correspond to a special class of $2$-polygraphs.
1242:
1243: For the moment, let us consider a $2$-polygraph $\Sigma=(\ast,\Sigma_1,\Sigma_2\amalg S_{\Sigma_1})$, but where $S_{\Sigma_1}$ now also contains explicit permutations $\tau_{x,x}$ for every $1$-cell~$x$ in~$\Sigma_1$. This extension does not change the properties studied so far if we extend the functor $\pi$ with $\pi(\tau_{x,x})=\id_{x+x}$. We denote by $(\Sigma_1,\Sigma_2)$ the corresponding Petri net. The following result gives a family of relations for some parallel $2$-arrows corresponding to the same Petri net reduction. Its proof is straightforward and uses the facts that $\ol{\pi}$ is a functor and maps each $\tau_{x,y}$ onto an identity.
1244:
1245: \begin{lem}\label{lem:relations}
1246: The functor $\ol{\pi}$ is compatible with the congruence $\equiv$ generated by the following relations, given for all $1$-cells~$x$,~$y$ and~$z$ and every $2$-cell $\alpha$:
1247: \begin{center}
1248: \begin{picture}(0,0)%
1249: \includegraphics{relations.eps}%
1250: \end{picture}%
1251: \setlength{\unitlength}{4144sp}%
1252: %
1253: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1254: \gdef\SetFigFont#1#2#3#4#5{%
1255: \reset@font\fontsize{#1}{#2pt}%
1256: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1257: \selectfont}%
1258: \fi\endgroup%
1259: \begin{picture}(4815,795)(-1022,152)
1260: \put(-584,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equiv$}%
1261: }}}}
1262: \put(2836,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1263: }}}}
1264: \put(3646,569){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1265: }}}}
1266: \put(181,704){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1267: }}}}
1268: \put(361,704){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1269: }}}}
1270: \put(631,704){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1271: }}}}
1272: \put(811,704){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1273: }}}}
1274: \put(1261,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1275: }}}}
1276: \put(1441,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1277: }}}}
1278: \put(1621,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1279: }}}}
1280: \put(1891,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1281: }}}}
1282: \put(2071,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1283: }}}}
1284: \put(2251,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1285: }}}}
1286: \put(2746,839){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1287: }}}}
1288: \put(3376,839){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1289: }}}}
1290: \put(496,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equiv$}%
1291: }}}}
1292: \put(1756,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equiv$}%
1293: }}}}
1294: \put(3241,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equiv$}%
1295: }}}}
1296: \put(-899,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1297: }}}}
1298: \put(-719,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1299: }}}}
1300: \put(-449,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1301: }}}}
1302: \put(-269,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1303: }}}}
1304: \end{picture}%
1305: \end{center}
1306:
1307: \noindent where the generalized explicit permutations used in the third relation are defined inductively from the permutation $2$-cells in a graphically intuitive way.
1308: \end{lem}
1309:
1310: \begin{rem}
1311: The first relation states that, in a given marking of a Petri net, two tokens in the same place are totally indiscernible: for example, one cannot tell if a given transition has consumed one given token or another one in the same place.
1312: \end{rem}
1313:
1314: \begin{rem}
1315: We conjecture that the congruence $\equiv$ also satisfies the converse property: if $f$ and $g$ are two parallel $2$-arrows in $\mon{\Sigma}$ such that $\ol{\pi}(f)=\ol{\pi}(g)$, then $f\equiv g$. However, we do not yet have a proof of this fact.
1316: \end{rem}
1317:
1318: \noindent So far, we have a set of equations relating $2$-arrows we wish to identify. However this raises a $2$-\emph{dimensional word problem} [Burroni 1993]: given two parallel $2$-arrows in $\mon{\Sigma}$, are they equal \emph{modulo} the congruence $\equiv$ or not? One way to build a decision procedure for such a problem is to follow the methodology developped in [Lafont 2003] and [Guiraud 2004] and build a convergent $3$-\emph{polygraph} equivalent to the given equational presentation.
1319:
1320: \begin{rem}
1321: Here, we do not recall basic notions about rewriting: they can be found in [Baader Nipkow 1998] for example. Let us say that, for this section, a $3$-polygraph is specified by a $2$-polygraph equipped with rewriting rules between parallel $2$-arrows. These rules are in fact $3$-cells, but we postpone all definitions until section~\ref{sec:3d} since we only need the intuition of it being a "circuit rewriting system" here.
1322: \end{rem}
1323:
1324: \noindent We would like to craft a convergent $3$-polygraph for the congruence $\equiv$ on the $2$-category $\mon{\Sigma}$. However, the fact that $2$-cells may have several inputs \emph{and} several outputs at the same time makes the rewriting study much different than in the already-encountered cases. We give here a possible starting point for future work.
1325:
1326: \begin{rem}
1327: For this introduction, we limit ourselves on several points:
1328: \begin{enumerate}
1329: \item[-] First of all, we only consider the congruence $\equi{0}$ generated by the last third families: we remove the relations $\tau_{x,x}\equiv\id_{x\tens x}$ since we still do not know how to handle them. This must be seen as a first step towards the study of $\equiv$.
1330: \item[-] The second limitation is that we assume that $\Sigma_2$ does not contain any $2$-cell with an empty output: the corresponding Petri net cannot have any transition that do not produce any token.
1331: \item[-] Finally, we suppose that every $2$-cell in $\Sigma_2$ with an empty input has only one output. This is not a real limitation since, in a Petri net, we can replace a transition $\alpha:\ast\fl y_1+\dots+y_n$ by two transitions $\ast\fl z$ and $z\fl y_1+\dots+y_n$, with $z$ a new place. The Petri net one gets fully simulates the original one.
1332: \end{enumerate}
1333: \end{rem}
1334:
1335: \noindent The idea is the following one: instead of giving an answer to the question $f\equiv g$ directly in $\mon{\Sigma}$, we translate $2$-arrows of $\Sigma$ into a $3$-polygraph in which we know a decision procedure and such that the translation preserves the congruence $\equiv$.
1336:
1337: \begin{ntt}
1338: We denote by $\ol{\Sigma}$ the $2$-polygraph with one cell in dimension $0$, with $\Sigma_1$ as its set of $1$-cells and with the following families of $2$-cells:
1339: \begin{center}
1340: \begin{picture}(0,0)%
1341: \includegraphics{deux-cellules-sigma-barre.eps}%
1342: \end{picture}%
1343: \setlength{\unitlength}{4144sp}%
1344: %
1345: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1346: \gdef\SetFigFont#1#2#3#4#5{%
1347: \reset@font\fontsize{#1}{#2pt}%
1348: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1349: \selectfont}%
1350: \fi\endgroup%
1351: \begin{picture}(2033,721)(-32,295)
1352: \put(1666,344){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y_i$}%
1353: }}}}
1354: \put( 91,839){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1355: }}}}
1356: \put(271,839){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1357: }}}}
1358: \put( 91,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1359: }}}}
1360: \put(271,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1361: }}}}
1362: \put(901,839){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1363: }}}}
1364: \put(811,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1365: }}}}
1366: \put(991,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1367: }}}}
1368: \put(1531,884){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x_1$}%
1369: }}}}
1370: \put(1801,884){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x_n$}%
1371: }}}}
1372: \end{picture}%
1373: \end{center}
1374:
1375: \noindent The first family $(\tau_{x,y})$ is indexed by every possible $1$-cells $x$ and $y$; the second family $(\delta_x)$ by every $1$-cell $x$; the last one $(\alpha_i)$ by every $2$-cell $\alpha:x_1\dots x_m\fl y_1\dots y_n$ and every $i$ in $\dens{1}{n}$.
1376:
1377: On top of the $2$-category $\mon{\ol{\Sigma}}$, we denote by $R$ the family made of the following $3$-cells, given for all possible coloration of the wires by $1$-cells:
1378: \begin{center}
1379: \begin{picture}(0,0)%
1380: \includegraphics{reductions-sigma-barre.eps}%
1381: \end{picture}%
1382: \setlength{\unitlength}{4144sp}%
1383: %
1384: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1385: \gdef\SetFigFont#1#2#3#4#5{%
1386: \reset@font\fontsize{#1}{#2pt}%
1387: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1388: \selectfont}%
1389: \fi\endgroup%
1390: \begin{picture}(6312,2004)(79,-1243)
1391: \put(6391,-1141){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1392: }}}}
1393: \put(5761,-511){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1394: }}}}
1395: \put(5266,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1396: }}}}
1397: \put(5491,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1398: }}}}
1399: \put(3961,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1400: }}}}
1401: \put(4771,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1402: }}}}
1403: \put(4681,-916){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_i$}%
1404: }}}}
1405: \end{picture}%
1406: \end{center}
1407:
1408: \noindent The generalized duplication in the topmost-rightmost family is inductively built from local duplications and local permutations in a inductive way described in [Guiraud 2004] for example. We denote by $\equi{R}$ the congruence relation generated by $R$ on parallel $2$-arrows of $\mon{\ol{\Sigma}}$.
1409: \end{ntt}
1410:
1411: \noindent Following the same method as the one presented in [Guiraud 2004] and using the coloration technique sketched in [Guiraud 2005], one proves that the $3$-polygraph $\ol{\Sigma}$ is convergent. Hence, given parallel $2$-arrows $f$ and $g$ in $\mon{\ol{\Sigma}}$, one can decide whether $f\equi{R}g$ holds or not.
1412:
1413: Furthermore, we conjecture here that it is possible to define a $2$-functor $\Phi:\mon{\Sigma}\fl\mon{\ol{\Sigma}}$ such that $f\equi{0}g$ holds if and only if $\Phi(f)\equi{R}\Phi(g)$ holds. Here we define a $2$-functor $\Phi$ which is a good candidate for this rôle and check the easy part of the claim.
1414:
1415: \begin{ntt}
1416: We define a $2$-functor $\Phi:\mon{\Sigma}\fl\mon{\ol{\Sigma}}$ by giving its values on the cells of $\Sigma$:
1417: \begin{enumerate}
1418: \item[0.] It sends the only $0$-cell of $\Sigma$ onto itself.
1419: \item[1.] It sends each $1$-cell $x$ of $\Sigma$ onto itself.
1420: \item[2.] It sends each $\tau_{x,y}$ onto itself and, for every $2$-cell $\alpha:x_1\dots x_m\fl y_1\dots y_n$ in $\Sigma_2$ with $n\geq 2$, we define:
1421: $$
1422: \Phi(\alpha) \:=\: (\alpha_1\tens\dots\tens\alpha_n)\circ\delta^n_{x_1\dots x_m}
1423: $$
1424:
1425: \noindent where $\delta^n_{x_1\dots x_m}$ is the only generalized duplication from $x_1\dots x_m$ to $(x_1\dots x_m)^n$ that is in normal form with respect to~$R$.
1426: \end{enumerate}
1427: \end{ntt}
1428:
1429: \noindent Then we have:
1430:
1431: \begin{prop}
1432: The congruence $\Phi(\equi{0})$ is included into $\equi{R}$.
1433: \end{prop}
1434:
1435: \begin{dem}
1436: We check that, for every relation $f\equiv g$ defining $\equi{0}$, we have $\Phi(f)\equi{R}\Phi(g)$. This is immediate for the two relations that only involve local permutations. And for the third family of equations:
1437: \begin{center}
1438: \begin{picture}(0,0)%
1439: \includegraphics{equivalence-preservee.eps}%
1440: \end{picture}%
1441: \setlength{\unitlength}{4144sp}%
1442: %
1443: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1444: \gdef\SetFigFont#1#2#3#4#5{%
1445: \reset@font\fontsize{#1}{#2pt}%
1446: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1447: \selectfont}%
1448: \fi\endgroup%
1449: \begin{picture}(5867,885)(721,-118)
1450: \put(6481,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$)$}%
1451: }}}}
1452: \put(1171,344){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1453: }}}}
1454: \put(1441,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1455: }}}}
1456: \put(6211, 74){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1457: }}}}
1458: \put(6301,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1459: }}}}
1460: \put(2701,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1461: }}}}
1462: \put(3961,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1463: }}}}
1464: \put(5041,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1465: }}}}
1466: \put(1801,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1467: }}}}
1468: \put(1621,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$)$}%
1469: }}}}
1470: \put(901,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$($}%
1471: }}}}
1472: \put(721,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\Phi$}%
1473: }}}}
1474: \put(5401,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1475: }}}}
1476: \put(5581,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\Phi$}%
1477: }}}}
1478: \put(5761,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$($}%
1479: }}}}
1480: \end{picture}%
1481: \end{center}
1482: \findem\end{dem}
1483:
1484: \begin{ex}
1485: Let us consider the Petri net from example \ref{ex:reseau_de_petri}. Its associated $2$-polygraph $\ol{\Sigma}$ has the following $2$-cells, beside the nine explicit permutations $(\tau_{\xi,\xi'})_{\xi,\xi'\in\ens{x,y,z}}$:
1486: \begin{center}
1487: \begin{picture}(0,0)%
1488: \includegraphics{exemple-sigma-barre.eps}%
1489: \end{picture}%
1490: \setlength{\unitlength}{4144sp}%
1491: %
1492: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1493: \gdef\SetFigFont#1#2#3#4#5{%
1494: \reset@font\fontsize{#1}{#2pt}%
1495: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1496: \selectfont}%
1497: \fi\endgroup%
1498: \begin{picture}(2669,754)(1407,-20)
1499: \put(3871, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\delta_z$}%
1500: }}}}
1501: \put(2341,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1502: }}}}
1503: \put(2521,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1504: }}}}
1505: \put(2431,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1506: }}}}
1507: \put(2431, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\beta$}%
1508: }}}}
1509: \put(1981,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1510: }}}}
1511: \put(1531,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1512: }}}}
1513: \put(1531,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1514: }}}}
1515: \put(1981,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1516: }}}}
1517: \put(1531, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_1$}%
1518: }}}}
1519: \put(1981, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha_2$}%
1520: }}}}
1521: \put(2971,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1522: }}}}
1523: \put(3421,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1524: }}}}
1525: \put(3871,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1526: }}}}
1527: \put(2881,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1528: }}}}
1529: \put(3061,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$x$}%
1530: }}}}
1531: \put(3331,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1532: }}}}
1533: \put(3511,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$y$}%
1534: }}}}
1535: \put(3781,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1536: }}}}
1537: \put(3961,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$z$}%
1538: }}}}
1539: \put(2971, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\delta_x$}%
1540: }}}}
1541: \put(3421, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\delta_y$}%
1542: }}}}
1543: \end{picture}%
1544: \end{center}
1545:
1546: \noindent Once translated into $\ol{\Sigma}$, the four representative we have seen of the Petri net reduction of example~\ref{ex:graphe_de_reduction} have the following respective normal forms:
1547: \begin{center}
1548: \begin{picture}(0,0)%
1549: \includegraphics{formes-normales.eps}%
1550: \end{picture}%
1551: \setlength{\unitlength}{4144sp}%
1552: %
1553: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1554: \gdef\SetFigFont#1#2#3#4#5{%
1555: \reset@font\fontsize{#1}{#2pt}%
1556: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1557: \selectfont}%
1558: \fi\endgroup%
1559: \begin{picture}(5829,744)(34,17)
1560: \end{picture}%
1561: \end{center}
1562:
1563: \noindent If the announced conjecture is true, then this will prove that the first and the third representatives are identified by $\equi{0}$ and hence by $\equiv$.
1564: \end{ex}
1565:
1566: \noindent The $2$-polygraphic translation of Petri nets we have built in this section has the advantage of having graphical representations that are easy to draw and interpret. However, as we have seen, the explicit way in which it handles the intrinsic commutativity of the net raises many issues we have only started to study here. The non distinction of tokens might be even worse since relations $\tau_{x,x}\equiv\id_{x\tens x}$ will create many nasty critical pairs when added to a rewriting system. However, future work will be devoted to a thorough study of these polygraphs.
1567:
1568: The next section is devoted to a much more natural translation of Petri nets that unveils their intrinsic $3$-dimensional nature.
1569:
1570: %%% section : 3d %%%
1571: \section{Petri nets as $\mathbf{3}$-dimensional objects}\label{sec:3d}
1572:
1573: \noindent In this section, we prove that Petri nets are exactly $3$-dimensional polygraphs with one cell of dimension~$0$ and no cell of dimension~$1$. The $2$-cells are the places of the net, while the $3$-cells are its transitions: there is no need of extra explicit permutation cells. This is due to a topological properties of this class of polygraphs which comes from the folkloric result of algebra, attributed to Hilton:
1574:
1575: \begin{lem}\label{lem:algebre}
1576: Let $M$ be a set equipped with two monoid structures $(\bullet,e)$ and $(\star,1)$ such that, for every elements~$x$, $y$, $z$ and $t$ in $M$, the relation $(x\bullet y)\star(z\bullet t)=(x\star z)\bullet(y\star t)$ holds. Then the two monoid structures are equal and commutative, which means that $e=1$ and that $x\bullet y=x\star y=y\bullet x=y\star x$.
1577: \end{lem}
1578:
1579: \begin{dem}
1580: Let us start by proving the equality $e=1$. Let us apply the hypothesis with $x=t=e$ and $y=z=1$, which gives $(e\bullet 1)\star(1\bullet e)=(e\star 1)\bullet(1\star e)$. On one hand, we have $(e\bullet 1)\star(1\bullet e)=1\star 1=1$, since $e$ is a bilateral unit for $\bullet$ and since $1$ is a left (or right) unit for $\star$. But, on the other hand, $(e\star 1)\bullet(1\star e)=e\bullet e=e$, since $1$ is a bilateral unit for $\star$ and since $e$ is a left (or right) unit for $\bullet$. Hence $e=1$.
1581:
1582: In order to prove that both operations $\bullet$ and $\star$ are the same, let us fix two elements $x$ and $y$ in $M$. We have the following chain of equalities, using the hypothesis together with the facts that $1$ is a bilateral unit for $\star$ and for $\bullet$:
1583: $$
1584: x\bullet y \:=\: (x\star 1)\bullet(1\star y) \:=\: (x\bullet 1)\star(1\bullet y) \:=\: x\star y.
1585: $$
1586:
1587: \noindent Finally, we prove that the operation $\star$ is commutative, using the same arguments:
1588: $$
1589: x\star y \:=\: (1\bullet x)\star(y\bullet 1) \:=\: (1\star y)\bullet(x\star 1) \:=\: y\bullet x \:=\: y\star x.
1590: $$
1591: \findem\end{dem}
1592:
1593: \begin{rem}
1594: The proof does not use the associativity of $\bullet$ nor $\star$. It works with a set with two binary relations such that each one admits a bilateral unit.
1595: \end{rem}
1596:
1597: \noindent Let us translate the lemma \ref{lem:algebre} in our setting:
1598:
1599: \begin{cor}\label{cor:algebre}
1600: Let $\Sigma=(\ast,\Sigma_1,\Sigma_2)$ be a $2$-polygraph with one $0$-cell. Then the two compositions $\tens$ and~$\circ$ are equal and commutative on the set $\mon{\Sigma}_2(\id_{\ast},\id_{\ast})$, which is the set of all the $2$-arrows $\id_{\ast}\fl\id_{\ast}$ of the free $2$-category $\mon{\Sigma}$.
1601: \end{cor}
1602:
1603: \begin{dem}
1604: On $\mon{\Sigma}_2(\id_{\ast},\id_{\ast})$ both compositions $\tens$ and $\circ$ induce a monoid structure. We already know that both structures have the same neutral element, $\id_{\id_{\ast}}$. Furthermore, the exchange relation gives, for any four $f$, $g$, $h$ and $k$ in $\mon{\Sigma}_2(\id_{\ast},\id_{\ast})$:
1605: $$
1606: (f\tens g)\circ(h\tens k) \:=\: (f\circ h)\tens(g\circ k).
1607: $$
1608:
1609: \noindent Then, one applies lemma \ref{lem:algebre} to conclude.
1610: \findem\end{dem}
1611:
1612: \medskip
1613: \begin{ntt}
1614: Let $\Sigma=(\ast,\Sigma_1,\Sigma_2)$ be a $2$-polygraph with one $0$-cell. The $1$-arrow $\id_{\ast}$ is denoted by $0$ and, by a slight abuse, so is the $2$-arrow $\id_{\id_{\ast}}$. The common restriction of $\circ$ and $\tens$ to $\mon{\Sigma}_2(0,0)$ is denoted by $+$.
1615: \end{ntt}
1616:
1617: \begin{rem}
1618: A $2$-arrow with source and target equal to $0$ is represented as a circuit with no input wire and no output wire. The proof that both compositions are equal and commutative on this kind of $2$-arrows corresponds to the following moves:
1619: \begin{center}
1620: \begin{picture}(0,0)%
1621: \includegraphics{mouvements.eps}%
1622: \end{picture}%
1623: \setlength{\unitlength}{4144sp}%
1624: %
1625: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1626: \gdef\SetFigFont#1#2#3#4#5{%
1627: \reset@font\fontsize{#1}{#2pt}%
1628: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1629: \selectfont}%
1630: \fi\endgroup%
1631: \begin{picture}(6414,474)(169,242)
1632: \put(6391,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1633: }}}}
1634: \put(1126,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1635: }}}}
1636: \put(2206,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1637: }}}}
1638: \put(2836,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1639: }}}}
1640: \put(3916,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1641: }}}}
1642: \put(4996,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1643: }}}}
1644: \put(6076,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1645: }}}}
1646: \put(361,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1647: }}}}
1648: \put(811,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1649: }}}}
1650: \put(1441,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1651: }}}}
1652: \put(2521,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1653: }}}}
1654: \put(3601,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1655: }}}}
1656: \put(4681,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1657: }}}}
1658: \put(5761,569){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1659: }}}}
1660: \put(6391,569){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1661: }}}}
1662: \put(1891,569){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1663: }}}}
1664: \put(2521,569){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1665: }}}}
1666: \put(3151,569){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1667: }}}}
1668: \put(4231,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1669: }}}}
1670: \put(5311,299){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1671: }}}}
1672: \end{picture}%
1673: \end{center}
1674:
1675: \noindent Explicitely:
1676: $$
1677: f\tens g \:=\: (f\tens 0)\circ(0\tens g) \:=\: f\circ g \:=\: (0\tens f)\circ(g\tens 0) \:=\: g\tens f \:=\: (g\tens 0)\circ(0\tens f) \:=\: g\circ f.
1678: $$
1679:
1680: \noindent This means that such a special $2$-arrow can turn around another one: there is no wire, hence no limitation to their homeomorphic movement.
1681: \end{rem}
1682:
1683: \noindent Using corollary \ref{prop:comm}, we give a polygraphic description of the free commutative monoid generated by a given set:
1684:
1685: \begin{prop}\label{prop:comm}
1686: Let $\Sigma$ be a $2$-polygraph of the form $(\ast,\emptyset,\Sigma_2)$. Then the set $\mon{\Sigma}_2(0,0)$ contains all the~$2$-arrows of $\mon{\Sigma}$ and, equipped with the structure $(+,0)$, is isomorphic to the free commutative monoid~$[\Sigma_2]$ generated by $\Sigma_2$.
1687: \end{prop}
1688:
1689: \begin{dem}
1690: Since there is one $0$-cell and no $1$-cell in the $2$-polygraph $\Sigma$, the only $1$-arrow of the free $2$-category~$\mon{\Sigma}$ is $\id_{\ast}=0$: indeed, there is only one path in the graph $(\ast,\emptyset)$ with one object and no arrow, the empty one. Hence, every $2$-arrow of $\mon{\Sigma}$ starts and ends at $0$.
1691:
1692: By application of corollary \ref{cor:algebre}, we know that both compositions $\circ$ and $\tens$ are equal and commutative, so that $(\mon{\Sigma}_2,+,0)$ is a commutative monoid. Furthermore, each element of $\Sigma_2$ is represented in $\mon{\Sigma}_2$: this inclusion induces a unique monoid morphism from $[\Sigma_2]$ to $\mon{\Sigma}_2$. This morphism is surjective, since every $2$-arrow of $\mon{\Sigma}$ is built from $2$-cells (elements of $\Sigma_2$) using only the operations $\tens$ and $\circ$, both equal to $+$. Hence, every $2$-arrow $f$ of $\mon{\Sigma}$ admits a decomposition:
1693: $$
1694: f \:=\: \sum_{x\in\Sigma_2} f(x).x,
1695: $$
1696:
1697: \noindent where the $f(x)$ are natural numbers. In order to conclude the proof, one must prove that this decomposition is unique. Let us assume that $f$ has another decomposition:
1698: $$
1699: f \:=\: \sum_{x\in\Sigma_2} f'(x).x.
1700: $$
1701:
1702: \noindent Let us fix a $2$-cell $x\in\Sigma_2$ and assume that $f(x)=f'(x)+k$, with $k$ a natural number. Then:
1703: $$
1704: f-f'(x).x \:=\: \sum_{y\neq x} f(y).y + k.x \:=\: \sum_{y\neq x} f'(y).y.
1705: $$
1706:
1707: \noindent Hence, in the first decomposition of $f-f'(x).x$, there are $k$ copies of the $2$-cell $x$, but there are no in the other. However, in a free $2$-category, two arrows are equal if and only if they differ only by a limited number of applications of the rules of associativity, units and exchange for $\circ$ and $\tens$: all these operations leave the number of generating $2$-cells $x$ unchanged. Hence $k=0$ and $f(x)=f'(x)$. Finally, there are only a finite number of $x$ such that $f(x)\neq 0$: an induction on this number conludes the proof.
1708:
1709: \findem\end{dem}
1710:
1711: \noindent Now, we have a correspondance between the elements of $[X]$ and the $2$-arrows of the free $2$-category generated by $(\ast,\emptyset,X)$. Then, transitions of a Petri net, through their rewriting representation, are translated as $\mathit{3}$-\emph{cells} in a $\mathit{3}$-\emph{polygraph}.
1712:
1713: \begin{defn}
1714: A \emph{$\mathit{3}$-polygraph} is a family $\Sigma=(\Sigma_0,\Sigma_1,\Sigma_2,\Sigma_3)$ of sets, equipped with an additional structure of $2$-polygraph on $(\Sigma_0,\Sigma_1,\Sigma_2)$ and with a graph structure $s_2,t_2:\Sigma_3\fl\mon{\Sigma}_2$ such that:
1715: $$
1716: s_1\circ s_2 \:=\: s_1\circ t_2 \et t_1\circ s_2 \:=\: t_1\circ t_2.
1717: $$
1718: \end{defn}
1719:
1720: \begin{rem}
1721: Usually, the $3$-cells are seen as \emph{directed volumes} between parallel circuits (circuits with the same $1$-source and the same $1$-target).
1722: \end{rem}
1723:
1724: \noindent Let us formalize the translation from Petri nets into $3$-polygraphs:
1725:
1726: \begin{defn}
1727: Let $(X,R)$ be a Petri net. The \emph{$\mathit{3}$-polygraph associated to $(X,R)$}, denoted by $\Sigma^3(X,R)$, is the $3$-polygraph $(\ast,\emptyset,X,R)$, where each rewriting rule $\alpha=(a,b)$ is seen as a $3$-cell with $2$-source the circuit representing $a$ and $2$-target the circuit representing $b$.
1728:
1729: Conversely, let $\Sigma=(\ast,\emptyset,\Sigma_2,\Sigma_3)$ be a $3$-polygraph with one $0$-cell and no $1$-cell. Its associated Petri net is the pair $\Nr(\Sigma)=(\Sigma_2,\Sigma_3)$.
1730: \end{defn}
1731:
1732: \noindent In order to compare a Petri net and its associated $3$-polygraph, a notion of reduction graph is defined, which conveys the idea of reduction under a context - see [Guiraud 2004(T)] for a study of contexts for circuits:
1733:
1734: \begin{defn}
1735: Let $\Sigma=(\ast,\Sigma_1,\Sigma_2,\Sigma_3)$ be a $3$-polygraph with one $0$-cell. Its \emph{associated reduction graph} is the graph $G(\Sigma)$ defined this way:
1736: \begin{enumerate}
1737: \item[0.] The objects of $G(\Sigma)$ are the $2$-arrows of $\mon{\Sigma}_2$.
1738: \item[1.] The arrows of $G(\Sigma)$ from $u$ to $v$ are all the triples $(f,\alpha,g)$, made of two $2$-arrows $f$ and $g$ of $\mon{\Sigma}_2$ and one $3$-cell $\alpha$ of $\Sigma_3$, such that the two following equalities are defined and hold:
1739: \begin{center}
1740: \begin{picture}(0,0)%
1741: \includegraphics{definition_contextes.eps}%
1742: \end{picture}%
1743: \setlength{\unitlength}{4144sp}%
1744: %
1745: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1746: \gdef\SetFigFont#1#2#3#4#5{%
1747: \reset@font\fontsize{#1}{#2pt}%
1748: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1749: \selectfont}%
1750: \fi\endgroup%
1751: \begin{picture}(4447,1014)(79,-253)
1752: \put(4411,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$v$}%
1753: }}}}
1754: \put(586,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1755: }}}}
1756: \put(3376,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1757: }}}}
1758: \put(586,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1759: }}}}
1760: \put(3376,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1761: }}}}
1762: \put(586,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$s_2\alpha$}%
1763: }}}}
1764: \put(3376,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$t_2\alpha$}%
1765: }}}}
1766: \put(1351,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1767: }}}}
1768: \put(1621,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$u$}%
1769: }}}}
1770: \put(4141,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1771: }}}}
1772: \end{picture}%
1773: \end{center}
1774: \noindent These triples are considered \emph{modulo} the following \emph{deformation} equations, given for every possible $2$-arrows~$f$,~$g$ and~$h$ and $3$-cell $\alpha$:
1775: \begin{center}
1776: \begin{picture}(0,0)%
1777: \includegraphics{egalites_contextes.eps}%
1778: \end{picture}%
1779: \setlength{\unitlength}{4144sp}%
1780: %
1781: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1782: \gdef\SetFigFont#1#2#3#4#5{%
1783: \reset@font\fontsize{#1}{#2pt}%
1784: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1785: \selectfont}%
1786: \fi\endgroup%
1787: \begin{picture}(6324,1284)(79,-253)
1788: \put(5896,479){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1789: }}}}
1790: \put(1351,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1791: }}}}
1792: \put(5131,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
1793: }}}}
1794: \put(586,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1795: }}}}
1796: \put(2116,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1797: }}}}
1798: \put(4366,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1799: }}}}
1800: \put(5896,794){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1801: }}}}
1802: \put(586,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1803: }}}}
1804: \put(2116,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1805: }}}}
1806: \put(4681,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$h$}%
1807: }}}}
1808: \put(6211,164){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$h$}%
1809: }}}}
1810: \put(271,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$h$}%
1811: }}}}
1812: \put(1801,164){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$h$}%
1813: }}}}
1814: \put(4366,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1815: }}}}
1816: \put(5896,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1817: }}}}
1818: \put(586,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1819: }}}}
1820: \put(2116,479){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1821: }}}}
1822: \put(4366,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
1823: }}}}
1824: \end{picture}%
1825: \end{center}
1826: \end{enumerate}
1827:
1828: \noindent A triple $(f,\alpha,g)$ is denoted by $g\circ\alpha\circ f$, with $(\circ f)$ and/or $(g\circ)$ dropped when $f$ and/or $g$ is an identity. We denote by $\star$ the composition of the free category $\mon{G(\Sigma)}$, with $A\star B$ standing $A$ followed by $B$.
1829: \end{defn}
1830:
1831: \noindent Once again, the reduction graph is not the natural object one associates to a $3$-polygraph: we prefer the $3$-category it generates. We give a formal definition and, then, its underlying graphical intuition.
1832:
1833: \begin{defn}
1834: Let $\Sigma=(\ast,\Sigma_1,\Sigma_2,\Sigma_3)$ be a $3$-polygraph with one $0$-cell. The \emph{free $\mathit{3}$-category generated by $\Sigma$} is denoted by $\mon{\Sigma}$ and is made of the $0$, $1$ and $2$-arrows of $\Sigma$, together with a family of \emph{$\mathit{3}$-arrows} which are the paths of the reduction graph $G(\Sigma)$ \emph{modulo} the congruence $\equi{\Sigma}$ generated by the following exchange relations:
1835: $$
1836: \begin{array}{c c c}
1837: (A\tens s_2(B))\star(t_2(A)\tens B)
1838: &\quad\equi{02}\quad&
1839: (s_2(A)\tens B)\star(A\tens t_2(B)), \\
1840: (B\circ s_2(A))\star(t_2(B)\circ A)
1841: &\quad\equi{12}\quad&
1842: (s_2(B)\circ A)\star(B\circ t_2(A)).
1843: \end{array}
1844: $$
1845:
1846: \noindent These equations allow one to extend the two compositions $\tens$ and $\circ$ on equivalence classes of paths in the graph $G(\Sigma)$, with $A\tens B$ being given by either side of the relation $\equi{02}$ and $B\circ A$ by either side of $\equi{12}$.
1847: \end{defn}
1848:
1849: \begin{rem}
1850: Let us give a more graphical account of the free $3$-category $\mon{\Sigma}$ generated by a $3$-polygraph $\Sigma$. Its $3$-arrows are generated by the $3$-cells of $\Sigma$ seen as blocks:
1851: \begin{center}
1852: \begin{picture}(0,0)%
1853: \includegraphics{bloc_et_2d.eps}%
1854: \end{picture}%
1855: \setlength{\unitlength}{4144sp}%
1856: %
1857: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1858: \gdef\SetFigFont#1#2#3#4#5{%
1859: \reset@font\fontsize{#1}{#2pt}%
1860: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1861: \selectfont}%
1862: \fi\endgroup%
1863: \begin{picture}(3225,868)(118,-146)
1864: \put(1126, 29){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
1865: }}}}
1866: \put(676,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$m$}%
1867: }}}}
1868: \put(676,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$n$}%
1869: }}}}
1870: \put(2206,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$f$}}}}
1871: \put(3196,434){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$g$}}}}
1872: \put(2656,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$A$}}}}
1873: \put(226,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
1874: }}}}
1875: \end{picture}%
1876: \end{center}
1877:
1878: \noindent On these generators, one can use the three following constructors, called compositions:
1879: \begin{center}
1880: \begin{picture}(0,0)%
1881: \includegraphics{trois_compositions.eps}%
1882: \end{picture}%
1883: \setlength{\unitlength}{4144sp}%
1884: %
1885: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1886: \gdef\SetFigFont#1#2#3#4#5{%
1887: \reset@font\fontsize{#1}{#2pt}%
1888: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1889: \selectfont}%
1890: \fi\endgroup%
1891: \begin{picture}(2904,1249)(169,-470)
1892: \put(2701,-421){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$A\star B$}%
1893: }}}}
1894: \put(766,614){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$B$}%
1895: }}}}
1896: \put(226,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$A$}%
1897: }}}}
1898: \put(1396,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$B$}%
1899: }}}}
1900: \put(2386,-16){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$A$}%
1901: }}}}
1902: \put(2656,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$B$}%
1903: }}}}
1904: \put(1756,659){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$A$}%
1905: }}}}
1906: \put(496,-421){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$A\tens B$}%
1907: }}}}
1908: \put(1576,-421){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$B\circ A$}%
1909: }}}}
1910: \end{picture}%
1911: \end{center}
1912:
1913: \noindent If they are sliced, these compositions appear this way:
1914: \begin{center}
1915: \begin{picture}(0,0)%
1916: \includegraphics{coupe_trois_compositions.eps}%
1917: \end{picture}%
1918: \setlength{\unitlength}{4144sp}%
1919: %
1920: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1921: \gdef\SetFigFont#1#2#3#4#5{%
1922: \reset@font\fontsize{#1}{#2pt}%
1923: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1924: \selectfont}%
1925: \fi\endgroup%
1926: \begin{picture}(6414,1599)(79,-838)
1927: \put(2656,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$g$}}}}
1928: \put(4006,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$f'$}}}}
1929: \put(4006,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$g'$}}}}
1930: \put(4366,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$f$}}}}
1931: \put(5356,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$g$}}}}
1932: \put(6346,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$h$}}}}
1933: \put(1036,-646){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$A$}}}}
1934: \put(1396,-646){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$B$}}}}
1935: \put(3286,119){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$A$}}}}
1936: \put(3286,-151){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$B$}}}}
1937: \put(4816,-691){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$A$}}}}
1938: \put(5851,-691){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$B$}}}}
1939: \put(226,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$f$}}}}
1940: \put(586,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$g$}}}}
1941: \put(1936,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$f'$}}}}
1942: \put(2296,-376){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$g'$}}}}
1943: \put(2656,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$f$}}}}
1944: \end{picture}%
1945: \end{center}
1946:
1947: \vfill\pagebreak
1948: \noindent All the constructions are identified modulo the following moves:
1949: \begin{center}
1950: \begin{picture}(0,0)%
1951: \includegraphics{echanges_blocs.eps}%
1952: \end{picture}%
1953: \setlength{\unitlength}{4144sp}%
1954: %
1955: \begingroup\makeatletter\ifx\SetFigFont\undefined%
1956: \gdef\SetFigFont#1#2#3#4#5{%
1957: \reset@font\fontsize{#1}{#2pt}%
1958: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
1959: \selectfont}%
1960: \fi\endgroup%
1961: \begin{picture}(5244,2319)(169,-1513)
1962: \put(2791,-466){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equi{02}$}%
1963: }}}}
1964: \put(2161,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equi{01}$}%
1965: }}}}
1966: \put(2161,-826){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equi{01}$}%
1967: }}}}
1968: \put(4951,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equi{12}$}%
1969: }}}}
1970: \put(4951,-916){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equi{12}$}%
1971: }}}}
1972: \put(1531,-466){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\equi{02}$}%
1973: }}}}
1974: \end{picture}%
1975: \end{center}
1976:
1977: \noindent This picture contains three families of moves, one for each exchange relation $\equi{02}$, $\equi{12}$ and $\equi{01}$, where the relation $\equi{01}$ is induced by the deformation relations and the other two exchange relations.
1978: \end{rem}
1979:
1980: \begin{rem}
1981: In the case of a $3$-polygraph $\Sigma$ with one $0$-cell and no $1$-cell, there are only two ways to compose $3$-arrows, namely $+$ and $\star$, since $\circ$ and $\tens$ are the same and denoted by $+$. As a consequence, there is only one family of exchange relations:
1982: $$
1983: (A+s_2(B))\star(t_2(A)+B) \quad\equi{\Sigma}\quad (s_2(A)+B)\star(A+t_2(B)).
1984: $$
1985:
1986: \end{rem}
1987:
1988: \noindent We prove that the reduction graphs of a Petri net and of its associated $3$-polygraph are the same. Moreover, the $3$-arrows of the $3$-category generated by the latter are exactly the equivalence classes of Petri net reductions \emph{modulo} the congruence relation we have defined on them.
1989:
1990: \begin{thm}\label{th:3d}
1991: Let $(X,R)$ be a commutative word rewriting system. Then $\Nr(\Sigma^3(X,R))=(X,R)$ and the graphs $G(\Sigma^3(X,R))$ and $G(X,R)$ are isomorphic. Furthermore, this isomorphism identifies the congruences $\equi{(X,R)}$ and $\equi{\Sigma^3(X,R)}$. Conversely, given any $3$-polygraph $\Sigma=(\ast,\emptyset,\Sigma_2,\Sigma_3)$, the equality $\Sigma^3(\Nr(\Sigma))=\Sigma$ holds and the graphs $G(\Sigma)$ and $G(\Sigma^3(\Nr(\Sigma)))$ are isomorphic. Furthermore, this isomorphism identifies the congruences $\equi{\Sigma}$ and $\equi{\Nr(\Sigma)}$.
1992: \end{thm}
1993:
1994: \begin{dem}
1995: Let us fix a Petri net $(X,R)$. The equality $\Nr(\Sigma^3(X,R))=(X,R)$ is immediate. The objects of both graphs $G(X,R)$ and of $G(\Sigma^3(X,R))$ are the same: the elements of the free commutative monoid~$[X]$.
1996:
1997: Then, the arrows from $u$ to $v$ in $G(X,R)$ are the $c+\alpha$, made of an element $c$ of $[X]$ and a rule $\alpha$ in $R$, such that $u=c+s(\alpha)$ and $v=c+t(\alpha)$. To such an arrow $c+\alpha$, we associate the arrow $\phi(c+\alpha)=(c,\alpha,0)$ in $G(\Sigma^3(X,R))$.
1998:
1999: Conversely, let us consider an arrow $(f,\alpha,g)$ in $G(\Sigma^3(X,R))$. Let us prove graphically that $(f,\alpha,g)=(f+g,\alpha,0)$, using the fact that all the $2$-arrows of $\mon{\Sigma^3(X,R)}_2$ have source and target $0$:
2000: \begin{center}
2001: \begin{picture}(0,0)%
2002: \includegraphics{preuve_graphique.eps}%
2003: \end{picture}%
2004: \setlength{\unitlength}{4144sp}%
2005: %
2006: \begingroup\makeatletter\ifx\SetFigFont\undefined%
2007: \gdef\SetFigFont#1#2#3#4#5{%
2008: \reset@font\fontsize{#1}{#2pt}%
2009: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
2010: \selectfont}%
2011: \fi\endgroup%
2012: \begin{picture}(6414,834)(79,-163)
2013: \put(4366,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
2014: }}}}
2015: \put(586,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
2016: }}}}
2017: \put(586,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
2018: }}}}
2019: \put(586,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
2020: }}}}
2021: \put(1936,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
2022: }}}}
2023: \put(3286,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
2024: }}}}
2025: \put(4636, 74){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
2026: }}}}
2027: \put(5986,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f+g$}%
2028: }}}}
2029: \put(5986, 74){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\alpha$}%
2030: }}}}
2031: \put(1261,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
2032: }}}}
2033: \put(2611,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
2034: }}}}
2035: \put(3961,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
2036: }}}}
2037: \put(5311,209){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$=$}%
2038: }}}}
2039: \put(1936,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
2040: }}}}
2041: \put(2296,-106){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
2042: }}}}
2043: \put(3286,524){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$f$}%
2044: }}}}
2045: \put(3646,254){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
2046: }}}}
2047: \put(4906,389){\makebox(0,0)[b]{\smash{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$g$}%
2048: }}}}
2049: \end{picture}%
2050: \end{center}
2051:
2052: \noindent Let us denote by $\psi$ the map that sends each $(f,\alpha,g)$ onto $f+g+\alpha$ and let us check that $\psi$ is an inverse for $\phi$:
2053: $$
2054: \psi\circ\phi(c+\alpha) \:=\: \psi(c,\alpha,0) \:=\: c+0+\alpha \:=\: c+\alpha.
2055: $$
2056:
2057: \noindent And:
2058: $$
2059: \phi\circ\psi(f,\alpha,g) \:=\: \phi(f+g+\alpha) \:=\: (f+g,\alpha,0) \:=\: (f,\alpha,g).
2060: $$
2061:
2062: \noindent Let us prove that $\phi(\equi{(X,R)})$ is included into $\equi{\Sigma^3(X,R)}$. For that, we fix $c$ in $[X]$ and $\alpha$, $\beta$ in $\Sigma_3$. Then $\phi$ sends the following square of $G(X,R)$
2063: $$
2064: \xymatrix
2065: {
2066: c + s(\alpha) + s(\beta) \ar[rr]^-{(c+s(\beta))+\alpha} \ar[dd]_-{(c+s(\alpha))+\beta}
2067: &&
2068: c + t(\alpha) + s(\beta) \ar[dd]^-{(c+t(\alpha))+\beta}
2069: \\ \\
2070: c + s(\alpha) + t(\beta) \ar[rr]_-{(c+t(\beta))+\alpha}
2071: &&
2072: c + t(\alpha) + t(\beta)
2073: }
2074: $$
2075:
2076: \noindent onto the following square of $G(\Sigma^3(X,R))$:
2077: $$
2078: \xymatrix
2079: {
2080: c + s(\alpha) + s(\beta) \ar[rr]^-{(c+s(\beta),\alpha,0)} \ar[dd]_-{(c+s(\alpha),\beta,0)}
2081: &&
2082: c + t(\alpha) + s(\beta) \ar[dd]^-{(c+t(\alpha),\beta,0)}
2083: \\ \\
2084: c + s(\alpha) + t(\beta) \ar[rr]_-{(c+t(\beta),\alpha,0)}
2085: &&
2086: c + t(\alpha) + t(\beta).
2087: }
2088: $$
2089:
2090: \noindent Using the already-known properties of $G(\Sigma^3(X,R))$, we get the following two equations:
2091: $$
2092: \left\{
2093: \begin{array}{c c c}
2094: (c+s(\beta),\alpha,0)\star(c+t(\alpha),\beta,0) &\:=\:&
2095: c+\big((\alpha+s(\beta))\star(t(\alpha)+\beta)\big), \\
2096: (c+s(\alpha),\beta,0)\star(c+t(\beta),\alpha,0) &\:=\:&
2097: c+\big((s(\alpha)+\beta)\star(\alpha+t(\beta))\big).
2098: \end{array}\right.
2099: $$
2100:
2101: \noindent Thus, two paths in $G(X,R)$ identified by $\equi{(X,R)}$ are sent by $\phi$ on two paths in $G(\Sigma^3(X,R))$ identified by $\equi{\Sigma^3(X,R)}$. The inclusion of $\psi(\equi{\Sigma^3(X,R)})$ into $\equi{(X,R)}$ is proved similarly, starting from the last two equations, in the case $c=0$, and moving upwards to a square whose paths are identified by $\equi{(X,R)}$.
2102:
2103: Now, let us fix a $3$-polygraph $\Sigma=(\star,\emptyset,\Sigma_2,\Sigma_3)$. The equality $\Sigma^3(\Nr(\Sigma))=\Sigma$ is once again immediate. Since $\Nr(\Sigma)$ is a Petri net, we know that $G(\Nr(\Sigma))$ is isomorphic to $G(\Sigma^3(\Nr(\Sigma)))$, which is the same as $G(\Sigma)$. Furthermore, this graph isomorphism is defined the same way as $\phi$ and $\psi$ in the first part of the proof. Hence $\phi(\equi{\Nr(\Sigma)})$ is equal to $\equi{\Sigma}$. We apply $\psi$ to get the equality between $\equi{\Nr(\Sigma)}$ and $\psi(\equi{\Sigma})$.
2104:
2105: \findem\end{dem}
2106:
2107: \noindent This result allows the informal statement "Petri nets \emph{are exactly} the $3$-polygraphs with one $0$-cell and no $1$-cell" for the following reasons:
2108: \begin{enumerate}
2109: \item[-] There is a correspondance between the presentations, given by the interpretation of places as $2$-cells and of transitions as $3$-cells.
2110: \item[-] Both presentations generate the same reduction graph, so that each one can simulate the evolutions of the other one.
2111: \item[-] There is a correspondance between the congruences that identify, in each graph, the paths that only differ by the order of application of the same transitions/3-cells.
2112: \end{enumerate}
2113:
2114: \noindent Another, more categorical way to formulate this correspondance is to say that the category $\Gr(X,R)$ generated by a Petri net is isomorphic to the category whose objects and arrows are respectively the $2$-arrows and $3$-arrows of $\mon{\Sigma^3(X,R)}$.
2115:
2116: %%% conclusion
2117: \section*{Comments and future directions}
2118: \emptysectionmark{Comments and future directions}
2119:
2120: We have proved that Petri nets have two natural interpretations in terms of polygraphs. Let us informally compare them.
2121:
2122: The first one, using a $2$-polygraph, is really convenient to use, since the circuit-like representation is now well-understood and user-friendly. The only difficulty comes with the explicit permutations: one has to choose a way to identify two paths that only differ by permutations. We have discussed possible starting points in order to reach a solution for this issue. And, as we have seen, this is non trivial and is postponed to further work. Nonetheless, this is an important new challenge for $3$-dimensional rewriting, since the polygraphs involved provide a new class of rather different examples.
2123:
2124: The second polygraphic interpretation we have studied, using a $3$-dimensional polygraph, provides, at least theoretically, a better description of the intrinsic algebraic structure of Petri nets: they do not require any extra cell, apart from the ones given with the Petri nets. However, these objects are hard to handle for the moment and this mainly comes from the lack of graphical representations: indeed, the first ones have been constructed in [Guiraud 2005] to represent classical proofs, but they remain hard to produce and handle in a convenient way. For that reason, part of the future work will concern these $3$-dimensional representations: the goals are to improve the ones already known, to automatize their production and, maybe, to search for other ones. In the case of Petri nets, the representations should be really interesting since their shape will strangely be close to diagrams used in superstring theory to represent interactions between superstrings.
2125:
2126: Let us finish by a more general comment on polygraphs. The results presented here constitute another clue of the expressive power of polygraphs in theoretical computer science, proof theory and universal algebra. Indeed, it is already known that polygraphs generalize word and term rewriting systems, equational presentations of algebraic structures, Reidemeister moves on knots and tangles, formal proofs of classical logic. The interested reader can find more information about the translations of all these objects into polygraphs in the following documents: [Burroni 1993], [Lafont 2003], [Métayer 2003], [Guiraud 2004(T), 2004, 2005].
2127:
2128: \vfill
2129: \begin{flushright}
2130: \begin{minipage}{100mm}
2131: \emph{I wish to thank Albert Burroni and Yves Lafont for many discussions and advices and the referees for their comments that have helped to improve this document.}
2132: \end{minipage}
2133: \end{flushright}
2134:
2135: %%% références %%%
2136: \section*{References}
2137: \emptysectionmark{References}
2138:
2139: \noindent\textsc{Franz Baader}, \textsc{Tobias Nipkow} \\
2140: \indent\emph{Term rewriting and all that}, Cambridge University Press, 1998.
2141:
2142: \bigskip
2143: \noindent\textsc{John Carlos Baez}, \textsc{James Dolan} \\
2144: \indent\emph{Categorification}, ArXiv preprint, 1998.
2145:
2146: \bigskip
2147: \noindent\textsc{Albert Burroni} \\
2148: \indent\emph{Higher-dimensional word problems with applications to equational logic}, \\
2149: \indent\indent Theoretical Computer Science 115(1), 1993.
2150:
2151: \bigskip
2152: \noindent\textsc{Olga Caprotti, Alois Ferscha, Hoon Hong} \\
2153: \indent\emph{Reachability test in Petri nets by Gröbner bases}, RISC report series 95(03), 1995.
2154:
2155: \bigskip
2156: \noindent\textsc{Angie Chandler, Anne Heyworth} \\
2157: \indent\emph{Gröbner bases as a tool for Petri net analysis}, Proceedings SCI 2001.
2158:
2159: \bigskip
2160: \noindent\textsc{Yves Guiraud} \\
2161: \indent\emph{Présentations d'opérades et systèmes de réécriture}, Thèse de doctorat, 2004(T). \\
2162: \indent\emph{Termination orders for $3$-dimensional rewriting}, \\
2163: \indent\indent To appear in Journal of Pure and Applied Algebra (2004). \\
2164: \indent\emph{The three dimensions of proofs}, To appear in Annals of Pure and Applied Logic (2005).
2165:
2166: \bigskip
2167: \noindent\textsc{Yves Lafont} \\
2168: \indent\emph{Towards an algebraic theory of boolean circuits}, Journal of Pure and Applied Algebra 184, 2003.
2169:
2170: \bigskip
2171: \noindent\textsc{Saunders MacLane} \\
2172: \indent\emph{Categories for the working mathematician}, Springer, second edition 1998.
2173:
2174: \bigskip
2175: \noindent\textsc{François Métayer} \\
2176: \indent\emph{Resolutions by polygraphs}, Theory and Applications of Categories 11(7), 2003.
2177:
2178: \bigskip
2179: \noindent\textsc{Tadao Murata} \\
2180: \indent\emph{Petri nets: properties, analysis and applications}, Proceedings IEEE 77(4), 1989.
2181:
2182: \end{document}