Presheaves for Processes and Unfoldings ∗Clovis Eberhart1 and Tom Hirschowitz2
12

Université Savoie Mont-Blanc
CNRS, Université Savoie Mont-Blanc

1Introduction

Baldan et al. [? ] give a general framework for rewriting systems based on adhesive categories. They give a definition of process in their setting, which is a sequence of rewriting
steps considered up to permutation of independent steps, and they build the unfolding of
any object. Here, we propose a different approach to model rewriting, processes, and unfoldings, which is based on a formalism inherited from playgrounds [? ]. The main contributionof our work is a direct, combinatorial description of processes and unfoldings in terms ofpresheaves. Just like in Bladan et al.’s work, the unfolding of an object has a universal
property (slightly different from theirs, though very close in spirit). This framework canadequately model executions of Petri nets, term graphs, or interaction nets, as well as processes in simple concurrent languages such as CCS [? ], the π-calculus, or the join-calculus.
It can also model some form of graph rewriting, which has yet to be compared to existing
frameworks, such as SPO and DPO.
The main difficulty in Baldan et al.’s work is that a process is more than the sequenceof its successive positions: it also records all the different occurrences of the rules that wereapplied. In our framework, this is dealt with by describing the whole process as a single
presheaf that describes a combinatorial object of higher dimension. Given a signature Σthat describes a set of objects (which are the presheaves over a category C) and rewriting
rules on these objects (given as a set R of spans of such objects), we build a bicategory
B that models rewriting on this set of objects according to the given rewriting rules. Thisbicategory will have as objects the set of objects described by Σ, and as morphisms from anobject Y to an object X all the processes (also called execution traces or rewriting traces)that correspond to rewriting X into Y according to the rules given by Σ. Processes arê (the category of presheaves over some category C[R]defined as particular cospans in C[R]constructed from C and R). Such a cospan Y → U ← X describes an execution trace whosestarting position is X and whose final position is Y . We build C[R] from C by adding
an object r for each rewriting rule in R and some meaningful morphisms from objects of
C to r. We then define seeds, which are the local shape of a rewriting step, by equipping
each representable presheaf yr with its initial and final positions X and Y (as given by therewriting rule), thus forming a cospan Y → yr ← X. Rewriting steps are then defined byembedding seeds into larger positions (thus allowing rewriting steps to occur in context).
Finally, rewriting traces are defined to be compositions of rewriting steps in the bicategorŷ We then derive the unfolding UX of any object X as the colimit of allof cospans in C[R].
the rewriting traces whose starting position is X.
Under some assumptions on the category C, the presheaves over C[R] have a graphicalnotation that is both close in spirit to string diagrams, and also inspired by that of graphs(but with multiple types of edges and higher-dimensional edges). For this reason, we usuallycall them higher-dimensional graphs or string diagrams (though none of these terms are
actually very accurate).

∗The authors acknowledge support from French ANR projets blanc Récré ANR-11-BS02-0010.

© Clovis Eberhart and Tom Hirschowitz;
licensed under Creative Commons License CC-BY
6th Conference on Algebra and Coalgebra in Computer Science.
Editors: Larry Moss and Pawel Sobociński; pp. 1–9
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

2Presheaves for Processes and Unfoldings

Figure 1 Our running example.

2

From Signatures to Bicategories and Unfoldings▸ Definition 1 (Signature). A signature Σ is given by:
a “base category” C that describes positions (more precisely, positions are presheavesover C),wu
̂ of presheaves over C, called “rules”,
a finite set R of spans Y ←ÐI Ð→ X in the category C
which describe the possibility to rewrite X into Y ,̂and a “starting position” S in C.
▸ Example 2. We give here two motivating examples our techniques apply to.
In the case of Petri nets, the Petri net ⟨P, T, δ, M ⟩, where P and T are the sets of its places
and transitions, δ ∶ T → (NP ) × (NP ) its transition function (where the first component
encodes consumed tokens and the second one created tokens), and M ∶ P → N its initial
marking, is modeled by:
the base category C = P , where P is viewed as the discrete category with ∣P ∣ elements
and only identity morphisms (note that presheaves on C indeed model markings ofthe Petri net),
if δ = ⟨δcons , δcrea ⟩, R contains a rule Yt ← ∅ → Xt for each transition t ∈ T , where Ytand Xt are resp. the multisets δcrea (t) and δcons (t), seen as presheaves,the starting position is S = M , seen as a presheaf.
In the case of graph rewriting, rewriting a graph G according to a given set of rewriting
rules RGph given as spans r = Lr ← Ir → Rr , describing the possibility to rewrite Lr into
Rr , is modeled by:
the base category is the category with two objects e, v and two non-trivial arrowss, t ∶ v → e (again, note that presheaves over C are indeed graphs),
R contains a rule Rr ← Ir → Lr for each r ∈ RGph , where Lr and Rr are seen aspresheaves over C,
the starting position is S = G, where G is seen as a presheaf over C.
▸ Remark. In the case of Petri nets, we could also model “read arcs” by changing the middle
component of the span (and therefore Yt and Xt as well) to include the place the transition
reads from.
▸ Example 3. We further specialize the example of Petri net rewriting to the particularPetri net and marking shown in Figure 1. In our setting, this is modeled by:
the set {a, b} as its base category, where a represents the top-left place and b the bottomleft one,

Clovis Eberhart and Tom Hirschowitz

3rules a ← ∅ → a and b ← ∅ → a + b 1 , which represent the top-right and bottom-righttransitions respectively,
the starting position is a + b.
We will also use a more graphical notation for positions, i.e., presheaves over the set{a, b}. We could of course, as it is usually done for Petri nets, represent a position X bydrawing a circle for each place and drawing as many bullets inside the circle that corresponds
to a place p as there are elements in X(p). However, this will prove quite impractical in ourcase, so we use a different representation. We will represent tokens in the place a by bullets
and tokens in the place b by circles. For example, ● ● ○ represents a marking with twotokens in a and one token in b.
For each rule r ∈ R, we define a new category Cr that has the same objects as C, plus
an additional object r and morphisms from some objects of C to that new object.
▸ Definition 4. For any presheaf U , C[U ] is the following cocomma category:∫ UpUC!

1λ⌜u⌝iUC[U ],

where ∫ U is U ’s category of elements.
▸ Remark. In more simple terms, C[U ] has the same objects as C, plus an additional object,
say u. Between two objects of C, C[U ] has the same morphisms as C, and the only morphismfrom u to itself is the identity morphism. For c an object of C, there is a morphism f¯ ∶ c → ufor each morphism f ∶ c → U (here again, we identify c and yc ), and there are no morphisms
from u to c. Composition is defined in the obvious way.
(X) over C[U ]. In simple
For each presheaf X over C, there is a presheaf X = Laniop
Uterms, for each object c of C, X(c) is isomorphic to X(c), and X(u) is empty. Therefore,
we will often denote X instead of X when it’s obvious that the presheaf is over C[U ].
pXyiÛ]▸ Proposition 5. Each presheaf X is the colimit of ∫ X Ð→ C Ð→ C[U ] Ð→ C[UProof. We consider the squareCŷCiUC[U ]ŷ].
C[UThere are two possible ways to fill the morphism on the right and the natural transformation:either with Lany (yiU ) or with Laniop(–), but the two possible fillings are actually isomorphic:
ULaniop(X)(d) = ∫Uc∈CC[U ](iopU c, d) × X(c) ≅ ∫Lany (yiU )(X)(d) = (∫c∈Cc∈CX(c) × C[U ](iU c, d)̂C(yc,X) × yiU c) (d) ≅ ∫c∈CX(c) × C[U ](iU c, d).

Now, since
1Here, a and b are actually ya and yb , the representable presheaves on a and b, i.e., C(–, a) and C(–, b).
We will often identify an object of a category and its representable presheaf and let the context disambiguate.

C A L C O E ar l y I d e a4Presheaves for Processes and Unfoldings

!

∫ X

1

pX

⌜X⌝

C

̂
C

yis a comma square and Kan extensions are pointwise in Cat, the composition of any left
̂ → C′ with ⌜X⌝ is again a left Kan extension. In particular, sinceKan extension Lany F ∶ CLaniop(–) is isomorphic to Lany (yiU ), which is a left Kan extension, it is also a left KanUextension, and therefore, so is Laniop(–) ○ ⌜X⌝ = ⌜Laniop(X)⌝ = ⌜X⌝, so X is indeed theU
Udesired colimit.
◂pUyiÛ]. Moreover, we have theIn particular, U is the colimit of ∫ U Ð→ C Ð→ C[U ] Ð→ C[Ufollowing natural transformation:!

∫ U

1
⌜u⌝

pU

⌜u⌝

C

C[U ]iUŷ],C[Uso, by universal property of the colimit, there is a unique morphism from U to u such that!

∫ U

1iU pU

C[U ]y1⌜U ⌝⌜u⌝̂]C[Û]
C[Ugives back the natural transformation above.
▸ Definition 6. We call ∂u ∶ U → u be the morphism constructed above.
▸ Definition 7. Cr is C[Mr ], where Mr is defined as the following pushout:
Ir

wr

Yr

ur

Xr

Mr .

▸ Remark. Cr is defined as any C[U ], and, if we call r its new object, then the morphisms
from c to r are as defined below:
̂ add a morphism tf ∶ c → r in Cr ,for each f ∶ yc → Xr in C,
̂for each f ∶ yc → Yr in C, add a morphism sf ∶ c → r in Cr ,
̂ add a morphism f˜ ∶ c → r in Cr ,for each f ∶ yc → Ir in C,
quotient these morphisms by f˜ = tur f and f˜ = swr f .
▸ Remark. In fact, we have only added morphisms tf and sf , since each morphism f˜ will beidentified with tur f and swr f .
̂r , we call Yr Ð→ r ←Ð Xr the cospan obtained by composing Yr → Mr ←▸ Definition 8. In C
Xr with ∂r.
srsrtrtr▸ Proposition 9. Yr Ð→ r ←Ð Xr is such thatIrwrur

Xrcommutes.

Yrsrtrr(1)

Clovis Eberhart and Tom Hirschowitz

5◂

Proof. It is the composition of a commutative square with ∂r.

We finally define C[R], the base category our pseudo double category will be built on.
▸ Definition 10. For a signature Σ = (C, R, S), we define the base category C[R] as thei Mr

wide pushout of C ÐÐ→ Cr for all rules r in R.
▸ Remark. In more simple terms, this is the category C with all the objects r in R andcorresponding morphisms.
▸ Example 11. In our running example, if we call the first rule u and the second one v, wehave that C[u, v], the base category of the corresponding pseudo double category will have:as objects: the set {a, b, u, v},
as non-trivial morphisms: tid a ∶ a → u, sid a ∶ a → u, til ∶ a → v, tir ∶ b → v, sid b ∶ b → v,
or, up to renaming, and in more graphical terms:
utu
av
tv
asu
au
tv
b sb

ab

We now build a pseudo double category that will describe rewriting on the signature.
More precisely, the objects of this pseudo double category will be positions, horizontal morphisms will describe “spatial inclusion”, i.e., how positions are included in larger positions,and vertical morphisms will be “rewriting traces”, i.e., how a position can reach anotherposition after a finite number of rewriting steps.
First of all, we need to define how we model a rewriting step.
In order to do this, we first define “seeds”, which are the basic components of a rewritingstep.
wrur▸ Definition 12. The seed that corresponds to the rule r = Yr ←Ð Ir Ð→ Xr is the commuting
square shown in (1).
▸ Definition 13. A rewriting step is any cospan Y → M ← X obtained by taking a pushoutof a seed along some monomorphism Ir → Z:YrYrIr

MZXrX.

We say that this rewriting step rewrites X into Y .
▸ Example 14. In our running example, there are two seeds, which correspond respectively
to u and v. They are the pushouts∅ı2a∅aı1ubandı3a+b

ı1 +ı2v

C A L C O E ar l y I d e a

6Presheaves for Processes and Unfoldings

We can represent them in a more graphical way. Recall the graphical notation for positions
from Example 3. We can draw the seeds that correspond to u and v like so:and.
The initial position of each seed is drawn at the bottom, and its final position is drawn at
the top, with another element in the middle that corresponds to the action of moving fromthe initial position to the final one itself.
▸ Remark. These drawings actually correspond to drawing the category of elements of theseeds that correspond to u and v, just like drawing a graph corresponds to drawing thecategory of elements of its corresponding presheaf. Here, we have drawn the categories ofelements of the presheaves u and v, with the convention that Xu = a and Xv = a + b are
drawn at the bottom, while Yu = a and Yv = b are drawn at the top. Therefore, in all ourdrawings, “time flows upwards”.
▸ Example 15. Remember that our starting marking is a + b, so there are two possible
rewriting steps on this marking:a+babu+bubvv

and∅∅baa+b∅a+ba + b.

The first one corresponds to firing u on the marking a + b, which indeed gives back themarking a + b, while the second one corresponds to firing v on the same marking, whichindeed gives the marking b.
We can draw these rewriting steps in a graphical way, very much like we did for seeds(and again, this corresponds to drawing the category of elements of the object we represent).
Since the move that corresponds to v doesn’t differ from the seed, it is represented exactly
as in the example above; the move that corresponds to u is drawn like so:.
The top and bottom positions indeed correspond to the initial and final positions of therewriting step, and the equal sign between the two tokens in b express that they are actually
the same token, but that this token is present both in the initial and final positions (in thecategory of elements, there is of course only one object corresponding to the token in b, but
we draw it twice with an equal sign between them for increased readability).
▸ Definition 16. A rewriting trace is any cospan that is isomorphic to a finite composition̂of rewriting steps in the category of cospans on C[R].
▸ Example 17. For example, on our running example, the different rewriting traces are(isomorphic to) either:

Clovis Eberhart and Tom Hirschowitz

7Figure 2 A less sequential Petri net.

Un for some n in N, where Un is the n-fold composition of the move that corresponds
to u on the initial marking (note that they can indeed be composed because the final
position is the same as the initial one),or Vn for some n in N, where Vn is the composition of Un with the move that corresponds
to v.
They can be described in graphical terms, for example, here are the graphical descriptionsof U2 on the left and of V2 on the right:.
▸ Example 18. To see how this definition is not sequential, but retains only the minimalcausality information between rewriting steps, we have to introduce another Petri net, because the one from our running example is entirely sequential.
Let us take as example the Petri net in figure 2, which is much more parallel: indeed,
the two transitions do not interact anymore. If we still call a, b, u, and v the different placesand transitions, we have that the possible moves from the initial marking are isomorphic toone of the following two moves:a+bau+bua+bba+v

v
or∅∅baa+baba + b.

A possible execution in the Petri net consists in first firing u, then firing v. It is thecomposition of the two cospans a + b → u + b ← a + b and a + b → a + v ← a + b, which gives
a + b → u + v ← a + b, which is the same as the rewriting trace obtained by first firing v, andthen firing u, which corresponds to the fact that there is no causality relation between firingu and firing v.
This can also be seen in graphical terms: if the seeds are drawn as

C A L C O E ar l y I d e a

8Presheaves for Processes and Unfoldings

and,then the moves on the initial marking can be drawn as
and.
Therefore, the execution that fires u then v and the one that fires v then u can be drawn as
on the left and right respectively, which can also be drawn as in the middle (these drawings
are again the graphical representation of the categories of elements associated to the differentpresheaves):==.

We can now define the pseudo double category D that will describe processes:
its objects are the positions, i.e., the presheaves over C (more precisely, they’re thepresheaves over C[R] that are of the form Laniop
X for some presheaf X over C),U
its horizontal morphisms are monomorphisms of positions,its vertical morphisms are rewriting traces,
its double cells are monomorphisms of traces, i.e., commuting diagrams of the form
YlY′

UkU′

XhX ′,

where h, k, and l are mono.
▸ Remark. We can draw a parallel between rewriting and games (and indeed, the ideas usedhere to model rewriting stem from playgrounds, which are a general framework for gamesemantics):
the objects our rewriting system works on (in the case of Petri nets, markings) are akinto positions,rewriting steps (in the case of Petri nets, the firing of a transition) to moves,and rewriting traces (in the case of Petri nets, executions) to plays.
▸ Definition 19. The category E(X) is the category of rewriting traces over X:st

its objects are the lower legs of rewriting traces: for each rewriting trace Y Ð→U ←Ð X,tXÐ→ U is an object of E(X),tt′uthe morphisms from X Ð→ U to X Ð→ U ′ are monomorphisms U Ð→ U ′ such that ut = t′ .

Clovis Eberhart and Tom Hirschowitz

9▸ Remark. The morphisms in E(X) correspond to “prefix” inclusion of rewriting traces, i.e.,there is a morphism U → U ′ in E(X) if the rewriting trace U can be followed by anotherrewriting trace such that the whole rewriting trace is isomorphic to U ′ .
▸ Example 20. On our running example, E(X) is composed of all the plays isomorphic toeither Un or Vn (as defined in Example 17), plus the morphisms that correspond to prefix
inclusion, which are generated by:for each n, the only morphism Un → Un+1 that fixes X,
for each n, the only morphism Un → Vn that fixes X.
t̂ by mapping X Ð
E(X) defines a diagram in C[R]
→ U to U (with the identity action onmorphisms).

▸ Definition 21. The unfolding UX of X is the colimit of the functor defined above.
id X▸ Remark. Since X ÐÐ→ X is an object of E(X), the unfolding UX of X comes with a map
X → UX obtained by universal property of UX .
▸ Example 22. In our running example, if we draw the unfolding UX of X, we obtain:⋮⋮,and the morphism X → UX maps X to the bottom of this drawing, which is exactly what
we expect.

C A L C O E ar l y I d e a