2.1 Double pushout rewriting

DPO rewriting has an established literature, so we use this section to cover the fundamentals and to establish our conventions. The interested reader can see Ehrig et al. (Reference Ehrig, Pfender and Schneider1973) to learn about graph rewriting or Lack and Sobociński (Reference Lack and Sobociński2004) for an axiomatic approach based on adhesive categories.

Rewriting starts with the notion of a rewrite rule, or simply rule. This is a span $\ell \leftarrow k \to r$ with two monic arrows. The interpretation of this rule is that $ \ell$ can be replaced by $ r$ , and $ k$ is the part of $ \ell$ that does not change. A grammar $(\mathsf{C},P)$ is defined to be an adhesive category $ \mathsf{C}$ together with a finite set of rules $ P := \{ \ell _j \leftarrow k_j \to r_j \}$ .

We can apply a rule $ \ell \leftarrow k \to r$ from $P$ to an object $ \ell '$ of $\mathsf{C}$ using any arrow $ m \colon \ell \to \ell '$ for which there exists a pushout complement, that is, an object $ k'$ fitting into a pushout diagram

A pushout complement need not exist, but if it does and the map $ k \to \ell$ is monic, then it is unique up to isomorphism (Lack and Sobociński Reference Lack and Sobociński2004, Lemma 15).

Every application of a rule begets a new rule. Applying $ \ell \leftarrow k \to r$ to $\ell '$ along $ m \colon \ell \to \ell '$ induces a derived rule $ \ell ' \leftarrow k' \to r'$ obtained as the bottom row of the DPO diagram

This diagram expresses a three-stage process whereby $ m$ selects a copy of $ \ell$ inside $ \ell '$ , this copy is replaced by $ r$ , and the resulting object $ r'$ is returned. Because pushouts preserve monos in adhesive categories, a derived rule is, in fact, a rule.

A grammar $( \mathsf{C},P )$ induces a collection $dP$ of all derived rules obtained by applying a rule in $P$ to an object in $\mathsf{C}$ . We can use $dP$ to analyze the grammar $(\mathsf{C},P)$ by constructing the rewrite relation $ \rightsquigarrow ^\ast$ . The meaning of $x \rightsquigarrow ^\ast y$ is that we can rewrite $x$ into $y$ by applying a sequence of rules in $dP$ . To precisely define the rewrite relation, we start by constructing a relation $ \rightsquigarrow$ on the objects of $ \mathsf{C}$ by setting $ \ell ' \rightsquigarrow r'$ if there exists a rule $ \ell ' \leftarrow k' \to r'$ in $ dP$ . However, $ \rightsquigarrow$ does not capture enough information about $( \mathsf{C},P )$ , which is why we define the rewrite relation $ \rightsquigarrow ^\ast$ to be the reflexive and transitive closure of $ \rightsquigarrow$ .

The rewrite relation can be encoded as arrows in a category, which we call the language of a grammar $ \mathrm{Lang} (\mathsf{C},P)$ , whose objects are those of $\mathsf{C}$ and arrows are generated by $ \rightsquigarrow$ . The language is constructed so that there is an arrow $ x \to y$ in $ \mathrm{Lang} (\mathsf{C},P)$ if and only if $ x \rightsquigarrow ^\ast y$ .

In the rewriting literature, the terms “language” and “rewrite relation” are often interchangeable. However, we give them slightly different meanings in order to help orient the reader. Namely, we use “rewrite relation” when giving a relational perspective and “language” when giving the category theoretical perspective.

Though there is more to the theory of rewriting than is provided in this section, we have developed enough of the theory to continue our goal of introducing rewriting to structured cospans.

2.2 Structured cospans

Baez and Courser (Reference Baez and Courser2020) introduced structured cospans as a framework to study open networks. A network is open when equipped with a mechanism by which it can connect to any compatible network. For example, a vacuum cleaner can connect with the electrical grid via an electrical socket. A pulley network can connect to a mechanical motor. An open network stands in contrast to a closed network that cannot interact with its outside environment.

To interpret $ La \to x \leftarrow Lb$ as an open network, take $x$ to represent the network with inputs $ La$ chosen by the arrow $ La \to x$ and outputs $ Lb$ chosen by $ x \leftarrow Lb$ . This open network can now connect to any other open network with inputs $ Lb$ , say $ Lb \to y \leftarrow Lc$ . We form the composite of the two open networks by connecting $ x$ to $ y$ along their common interface $ Lb$ . Mathematically, this amounts to taking the pushout of $ x$ and $ y$ over $ Lb$ , thus giving the composite network $ La \to x+_{Lb}y \leftarrow Lc$ . We capture this in a category $_{L} \mathsf{Csp}$ whose objects are those of $\mathsf{A}$ and arrows $a \to b$ are structured cospans $La \to x \leftarrow Lb$ with composition given by pushout.

Example 2. Structured cospans can be used to slightly generalize open graphs. Set theoretically, a graph is open when equipped with two subsets of its nodes, one set serving as inputs and the other as outputs. When the inputs of one open graph coincide with the outputs of another, they can be composed. For example, the pair of open graphs

compose by gluing the corresponding nodes together, forming the new open graph

To define an open graph as a structured cospan, consider

where $ L$ is the discrete graph functor and $ R$ forgets the graph edges. The above open graphs can be presented as the structured cospans

with composite

Note, that the functions forming the legs of the cospan need not be monic, hence calling the structured cospan version of open graphs a slight generalization of the set theoretic version of open graphs. In this example, the category $ _L\mathsf{Csp}$ has sets for objects and open graphs for arrows.

3.1 Characterizing structured cospan categories as adhesive or topoi

Every adhesive category supports a rich rewriting theory. This fact underpins our efforts to introduce rewriting to structured cospans. And so, in this section, we reintroduce the notion of structured cospans in a different context and find sufficient conditions for them to be adhesive.

Recall that, in Section 2, we saw that rewriting operates on the objects of an adhesive category, not the arrows. Therefore, we cannot hope to rewrite structured cospans inside the category $ _L\mathsf{Csp}$ . Our task, now, is to build a category where structured cospans are objects and then to show that it is adhesive.

Definition 3. Fix an adjunction $ L \dashv R \colon \mathsf{X} \to \mathsf{A}$ . Define $ _L \mathsf{StrCsp}$ to be the category whose objects are structured cospans and arrows from $ La \to x \leftarrow Lb$ to $ La' \to x' \leftarrow Lb'$ are triples of arrows $ ( f,g,h )$ fitting into the commuting diagram

Now, in order to enable the rewriting of structured cospans in the sense of Section 2, $_{L} \mathsf{StrCsp}$ must be adhesive. To achieve this, we outline two sets of conditions in order to later prove results of different strengths.

Every topos is adhesive (Lack and Sobociński Reference Lack and Sobociński2006), meaning the topos condition is strictly stronger than the adhesive condition. As shown in the next two results, when structured cospans are built with $L \dashv R$ satisfying the adhesivity condition, then $_{L} \mathsf{StrCsp}$ is adhesive. Similarly, $_{L} \mathsf{StrCsp}$ is a topos when $L \dashv R$ satisfies the topos condition.

While in this paper, we will largely work with the generality of adhesive categories, many objects of rewriting interest actually form topoi. Graphs are the primary example. Therefore, we show that under slightly stronger conditions, structured cospans form a topos and that this construction is functorial in $L$ .

Proof. By adjointness, $ _{L}\mathsf{StrCsp}$ is equivalent to the category whose objects are cospans of form $ a \to Rx \leftarrow b$ and morphisms are triples $ ( f,g,h )$ fitting into the commuting diagram

This, in turn, is equivalent to the comma category $ ( \mathsf{A} \times \mathsf{A} ) \downarrow \Delta R$ where $ \Delta \colon \mathsf{A} \to \mathsf{A} \times \mathsf{A}$ is the diagonal functor, a right adjoint. Because $ \Delta R$ is a right adjoint, $ ( \mathsf{A} \times \mathsf{A} ) \downarrow \Delta R$ is an Artin gluing (Wraith 1974), therefore a topos.

Theorem 7. Denote by $ \mathsf{Topos}$ the category of topoi and geometric morphisms. There is a contravariant functor $ _{(-)}\mathsf{StrCsp} \colon [\bullet \to \bullet , \mathsf{Topos} ] \to \mathsf{Topos}$ defined by

which is in turn given by

Proof. In light of Theorem6, it suffices to show that $ \Theta \dashv \Psi$ gives a geometric morphism. Let $ \ell$ and $\ell '$ , respectively, denote the $ L$ -structured cospan $ La \to x \leftarrow Lb$ and the $ L'$ -structured cospan $ L'a' \to x' \gets L'b'$ . Denote the unit and counit for $F \dashv G$ by $ \eta$ , $ \varepsilon$ and for $ F' \dashv G'$ by $ \eta '$ , $ \varepsilon '$ . The assignments

\begin{align*} \left ( (f,g,h)\colon \ell \to \Psi \ell ' \right ) & \mapsto \left ( (\varepsilon '\circ G'f, \varepsilon \circ Gg, \varepsilon '\circ G'h ) \colon \Theta \ell \to \ell '\right ) \\ \left ( (f',g',h')\colon \Theta \ell \to \ell '\right ) & \mapsto \left ( (Ff'\circ \eta ',F'g'\circ \eta ,F'h'\circ \eta ') \colon \ell \to \Theta '\ell '\right ) \end{align*}

give a bijection $ \hom (\Theta \ell ,\ell ') \simeq \hom (\ell ,\Psi \ell ' )$ . The naturality in $\ell$ and $\ell '$ follows from the naturality of $\eta$ , $\varepsilon$ , $\eta '$ , and $\varepsilon '$ . The left adjoint $\Theta$ preserves finite limits because they are taken pointwise and $ L'$ , $ G$ , and $ G'$ all preserve finite limits. Identity and composition are easily checked to be preserved.

For the remainder of the paper, we work with structured cospans that satisfy the adhesive condition unless otherwise stated.

3.2 Rewriting structured cospans

We now know that the category $ _L\mathsf{StrCsp}$ of structured cospans and their morphisms are adhesive and, therefore, supports a rich rewriting theory. In this section, we begin to develop this theory.

Definition 8. A rewrite rule of structured cospans is an isomorphism class of spans of structured cospans (Cicala and Courser Reference Cicala and Courser2018; Cicala Reference Cicala2018b) of the form

The marked arrows $ \rightarrowtail$ are monic.

The conceit of this rule is that the structured cospan $ La \to x' \leftarrow Lb$ along the top of the diagram is rewritten as the structured cospan $ La \to x'' \leftarrow Lb$ along the bottom. Here, we are orienting our diagrams as “top rewrites to bottom” instead of “left rewrites to right”. A nonsuperficial difference is that this diagram is not merely a span in $ _L\mathsf{StrCsp}$ with monic legs. We disallow the inputs and outputs from being rewritten.

In order to apply this rule to other graphs, we need the notions of grammars and derived rules for structured cospans.

Proof. Consider the diagram

where the top face is a rewrite rule of structured cospans, and the back left and front left faces give a matching map, with pushout complement, of structured cospans. Then the bottom face is also a rewrite rule of structured cospans because pushouts preserve monos in an adhesive category.

Now that we are certain that derivation preserves rewrite rules of structured cospans, we can construct the language. Similar to the construction in Gadducci and Heckel (Reference Gadducci and Heckel1998), we realize the language as the free 2-category on a computad whose 0-cells are interface types, 1-cells are structured cospans, and 2-cells are generated by the rewrite rules of a given grammar.

Definition 11. Given an adjunction $L \dashv R \colon X \to A$ satisfying the adhesivity condition (Definition 4) and a structured cospan grammar $(_L\mathsf{StrCsp}, P)$ , define a computad $\mathrm{Comp} (_L\mathsf{StrCsp}, P)$ with $0$ -cells the $\mathsf{A}$ -objects, $1$ -cells the arrows of $_L\mathsf{StrCsp}$ and, for each

derived from $P$ , a $2$ -cell $\gamma _p$

Apply to this computad the free 2-category functor, that is the left adjoint to the forgetful functor taking each 2-category to its underlying computad. The resulting 2-category is what we call $\mathbf{Lang}(_L\mathsf{StrCsp}, P)$ .

Note that we have two notions of language. The first, written in non-bold type, $\mathrm{Lang} (\mathsf{X},P)$ is a 1-category generated by the rewrite relation of a typical grammar. The second, written in bold type, $\mathbf{Lang} (_L\mathsf{StrCsp}, Q)$ is the 2-category generated by a computad for a structured cospan grammar.

3.3 Basic properties inherited

Thus far, we have constructed an adhesive category $_{L} \mathsf{StrCsp}$ . Therefore, it enjoys the basic properties of adhesive categories, as detailed by Lack and Sobociński (Reference Lack and Sobociński2004). Moreover, structured cospan grammars involve rewrite rules that are stronger than those for general adhesive grammars. For general adhesive categories, rewrite rules can be any span with monic legs, while structured cospan rewrite rules are certain spans with monic legs. Therefore, a structured cospan grammar is just a grammar in an adhesive category. It follows that the Local Church Rosser theorem and the Concurrency theorem hold for structured cospan grammars.

4.1 A brief history of inductive rewriting

Before graph rewriting, there were both formal language rewriting and term rewriting. In these cases, there are two ways to define the rewrite relation. The first way is called the operational method, which applies a rule by substituting a sub-term for another term. The second way is called the inductive method, which constructs the rewrite relation using generators and closure operations. In classical graph rewriting, only the operational method existed, where substitution was achieved with the DPO method. Eventually, Gadducci and Heckel introduced an inductive method to construct the rewrite relation, opening the way to analyze graph grammars through structural induction.

These authors accomplished this by defining what are now more commonly called open graphs defined using a cospan $d_1 \to g \leftarrow d_2$ where the images of discrete graphs $d_1$ and $d_2$ identified the inputs and outputs of a graph $g$ . This idea is a precursor for structured cospans. The inductively defined rewrite relation for a graph grammar used this open graph construction to encode the relation inside the hom-set of a particular 2-category. We emphasize here that the goal was not about rewriting open graphs, but to use open graphs to talk about rewriting graphs.

In this section, we adapt their ideas to give an inductive definition of the rewrite relation for a grammar $ ( \mathsf{X},P )$ such that $\mathsf{X}$ fits into an adjunction $L \dashv R \colon \mathsf{X} \to \mathsf{A}$ satisfying the adhesivity condition (Definition 4) and has a monic counit. We also require the grammar to induce the same language as the discrete grammar obtained by replacing each rule $\ell \leftarrow k \to r$ in $P$ with $\ell \gets LRk \to r$ . It is already known that the category of directed graphs satisfies these conditions (Ehrig et al. Reference Ehrig, Pfender and Schneider1973, Proposition 3.3). We show this is also true of typed graphs, different flavors of hypergraphs, and Petri nets.

Before proceeding, we reemphasize that this section is not about rewriting structured cospans. Instead, we use structured cospans as a tool to inductively construct the language for a certain class of grammars.

4.2 Discrete grammars

In general, for any rewrite rule $ \ell \leftarrow k \to r$ , there is only one constraint on the value of $ k$ : it must be a subobject of $ \ell$ and $ r$ . But requiring that $ k$ also be discrete can simplify any analysis involving that rule. This leads us question whether we can learn about a grammar $ ( \mathsf{X},P )$ by instead studying the grammar $ ( \mathsf{X}, P_\flat )$ , where $ P_\flat$ is obtained by discretizing the apexes of every rule in $ P$ . In this section we explain the $ \flat$ notation and make precise the concept of discreteness before giving the main result of this section that characterizes when $ ( \mathsf{X},P )$ and $ ( \mathsf{X}, P_\flat )$ give the same language. This result generalizes the characterization of discrete graph grammars given by Ehrig et al. (Reference Ehrig, Pfender and Schneider1973, Proposition 3.3).

As a brief aside, experts in topos theory will know that discreteness comes from the flat modality on a local topos (Johnstone Reference Johnstone2002, Ch. 3.6)). While this is not unrelated to our definition of discreteness, we are really borrowing this term to use in this paper because it evokes the primary example of discretizing open graphs (Example 13).

We can interpret a discrete comonad as returning largest interface $ \flat x$ supported by a network $ x$ . Here is an example illustrating how the discrete graph adjunction gives rise to $ \flat$ .

Example 13. Consider the geometric morphism

defined by setting $ La$ to be the discrete graph on $ a$ and $ Rx$ to be the set of nodes in $ x$ . This adjunction induces the comonad $ \flat := LR$ on $ \mathsf{Graph}$ . Applying $ \flat$ to a graph $ x$ returns the discrete graph underlying $ x$ , for instance

The counit $ \varepsilon _x \colon \flat x \to x$ is certainly monic as it includes the discrete graph $ \flat x$ into the graph $ x$ , as in

Discrete comonads provide a tool to control the form of a grammar by replacing every rule $ \ell \leftarrow k \to r$ with $ \ell \leftarrow \flat k \to r$ .

Definition 14 (Discrete grammar). Let $ \flat \colon \mathsf{X} \to \mathsf{X}$ be a discrete comonad with counit $ \varepsilon$ . Given a grammar $ ( \mathsf{X} , P )$ , define $ P_\flat$ as the set containing

\begin{equation*} \ell \leftarrow k \xleftarrow {\varepsilon } \flat k \xrightarrow {\varepsilon } k \to r \end{equation*}

for each rule $ \ell \leftarrow k \to r$ in $ P$ . We call $ ( \mathsf{X} , P_\flat )$ the discrete grammar underlying $ ( \mathsf{X}, P )$ .

4.3 Expressiveness of grammars

The following lemma uses pushout complements to characterize when $(\mathsf{X}, P)$ and $(\mathsf{X},P_\flat )$ generate the same language. We then use this characterization to show that this holds for both directed and undirected hypergraphs, Petri nets, and marked Petri nets. It also holds for certain slice categories, which allows us to extend this result to typed graphs and hypergraphs.

Lemma 15. Fix an adjunction

between adhesive categories with a monic counit and $L$ preserving pullbacks. Take a grammar $(\mathsf{X}, P)$ and its underlying discrete grammar $(\mathsf{X}, P_{\flat })$ . If for every derived rewrite rule

there is a pushout complement $d$ to the composite $\flat k \to k \to k'$ , then $(\mathsf{X},P)$ and $(\mathsf{X}, P_{\flat })$ generate the same language.

Proof. Suppose that $\ell ' \rightsquigarrow r'$ in the rewrite relation for $(\mathsf{X},P)$ . That means there is a DPO diagram

in $\mathsf{X}$ so that the top span is in $P$ . Then, $\ell ' \rightsquigarrow r'$ in $(\mathsf{X}, P_{\flat })$ as witnessed by the DPO diagram

Conversely, suppose that $\ell ' \rightsquigarrow r'$ is generated by a rule $\ell \leftarrow \flat k \to r$ in $P_\flat$ . That means there is a diagram

By the construction of $P_\flat$ , the maps $\flat k \to \ell$ and $\flat k \to r$ both factor through the counit $\flat k \to k$ and, consequently, we get

Both maps $d \to \ell '$ and $d \to r'$ factor through $k +_{\flat k} d$ which results in the diagram

whose pushouts result from the pushout pasting law. This witnesses $\ell ' \rightsquigarrow r'$ derived from $P$ .

Showing that a grammar and its underlying discrete grammar generate the same language was initially shown for directed graphs.

Example 16 Ehrig et al. (Reference Ehrig, Pfender and Schneider1973, Proposition 3.3). Returning to the discrete graph geometric morphism

any grammar $(\mathsf{Graph}, P)$ generates the same language as the discrete grammar $(\mathsf{Graph}, P_{\flat })$ .

4.3.1 Hypergraphs

We can now show for the first time that this result also holds for hypergraphs, both directed and undirected. Following (Bonchi et al. Reference Bonchi, Gadducci, Kissinger, Sobociński and Zanasi2017), we realize hypergraphs as a presheaf topos in the following way.

Definition 17. Define the category of directed hypergraphs $\mathsf{DHGraph}$ as the presheaf category $[\mathsf{DH}^{\scriptsize { \textrm {op} } }, \mathsf{Set}]$ where $\mathsf{DH}$ has objects ${\mathbb{N}} \times {\mathbb{N}} + \{N\}$ and arrows

\begin{equation*}\mathsf{DH}(N,(n,m)) := \{s_1, \dotsc , s_n\} + \{t_1, \dotsc , t_m\}.\end{equation*}

All other homsets are trivial. For such a presheaf, the image of $(n,m) \in {\mathbb{N}} \times {\mathbb{N}}$ gives the set of edges with in-degree $n$ and out-degree $m$ , the image of $N$ gives the set of nodes, the image of each $\text{source}$ map $s_j^{^{\scriptsize { \textrm {op} } }} \colon (n,m) \to N$ records the $j$ -th incidence for the source of each edge, and the image of each $\text{target}$ map $t_j^{^{\scriptsize { \textrm {op} } }} \colon (n,m) \to N$ records the $j$ -th incidence for the target of each edge.

Define the category of undirected hypergraphs $\mathsf{HGraph}$ as the category of presheaves $[\mathsf{H}^{\scriptsize { \textrm {op} } },\mathsf{Set}]$ on the category $\mathsf{H}$ with objects ${\mathbb{N}} + \{N\}$ and arrows

\begin{equation*}\mathsf{H}(N,n) := \{x_1, \dotsc , x_n\}.\end{equation*}

All other homsets are trivial. For such a presheaf, the image of $n \in {\mathbb{N}}$ gives the set of edges with degree $n$ , the image of $N$ gives the set of nodes, and the image of each map $x_j^{^{\scriptsize { \textrm {op} } }} \colon n \to N$ records the $j$ -th incidence for each edge.

Both undirected hypergraphs can be discretized via geometric morphisms

where $R$ returns the node set and $L$ returns a discrete hypergraph on a given set. It is straightforward to check that, in each case, the counit of the induced comonad is indeed monic. Therefore, for a grammar of directed hypergraphs $(\mathsf{DHGraph}, P)$ , we have the underlying discrete grammar $(\mathsf{DHGraph}, P_{\flat })$ . This holds too for undirected hypergraphs.

Proposition 18. A grammar of directed hypergraphs $(\mathsf{DHGraph}, P)$ and its underlying discrete grammar $(\mathsf{DHGraph}, P_{\flat })$ have the same language.

Proof. Consider a derived rewrite rule

By Lemma 15, it suffices to find a hypergraph $d$ that is a pushout complement to $\flat k \to k \to k'$ . Define $d$ by $d(N) := k'(N)$ and $d(n,m) := k'(n,m) - k(n,m)$ for each in-degree, out-degree pair $(n,m)$ . Recalling that the directed hypergraph $\flat k$ has no edges and the same nodes as $k$ , we have pushouts

ensuring that $d$ is the pushout complement we sought.

Proposition 19. A grammar of undirected hypergraphs $(\mathsf{HGraph}, P)$ and its underlying discrete grammar $(\mathsf{HGraph}, P_{\flat })$ have the same language.

Proof. The proof follows the same reasoning as the directed hypergraph case.

4.3.3 Typed objects

Occasionally, those working with rewriting typify their objects. For instance, instead of working with graphs, one might work with graphs whose edges and notes each come in multiple colors. This can be accomplished by working in an appropriate slice category. For example, suppose we wanted to work with graphs whose edges come in red $r$ and green $g$ colors. Add this information to a graph using a map to

so that the images of the edges and nodes of $g$ encode the typing information. In short, we may want to be rewriting in a slice category $\mathsf{X} / x$ using an adhesive category $\mathsf{X}$ and object $x$ .

This next result provides conditions for a grammar and its underlying discrete grammar in $\mathsf{X}/x$ to generate the same language. The first condition is that the “untyped grammars” $(\mathsf{X}, P)$ and $(\mathsf{X},P_\flat )$ generate the same rewrite relation. To move to a grammar in $\mathsf{X}/x$ , there would be user-driven decisions to make, namely how the rewrite rules in $P$ will be mapped to $x$ .

Proposition 24. Fix an adjunction $L \dashv R \colon \mathsf{X} \to \mathsf{A}$ between adhesive categories with a monic counit and $L$ preserving pullbacks. Fix an object $x$ in $\mathsf{X}$ . Consider both the comonad $\flat := LR$ and the induced adjunction between slice categories $L_x \dashv R_x \colon \mathsf{X}/x \to \mathsf{A}/Rx$ that also has a monic counit and $L_x$ preserving pullbacks. Let $(\mathsf{X}/x, P_x)$ be any grammar, $(\mathsf{X}/x, P_{x,\flat })$ be the underlying discrete grammar, and $(\mathsf{X}, P)$ and $(\mathsf{X}, P_{\flat })$ be their projections into $\mathsf{X}$ .

If for every derived rewrite rule

in $(\mathsf{X},P)$ there is a pushout complement $d$ to the composite $\flat k \to k \to k'$ , then $(\mathsf{X}/x,P_x)$ and $(\mathsf{X}/x, P_{x,\flat })$ generate the same rewrite relation.

Proof. Recalling that pushouts in $\mathsf{X}/x$ are computed by projecting to $\mathsf{X}$ , this result follows from a similar argument as in Lemma 15.

Corollary 25. Grammars and their underlying discrete grammars generate the same rewrite relation for typed directed graphs, typed directed hypergraphs, and typed undirected hypergraphs.

4.4 Inductive rewriting systems

In the networks perspective, a grammar $( \mathsf{X},P )$ can be thought of as comprising an adhesive category $\mathsf{X}$ of closed networks and a set of rules $P$ stating how to revise the closed networks. For example, one might revise an network of resistors by replacing a series of resistors with a single resistor. An important part of our construction involves decomposing a closed network $x$ into other networks $x_1, \dotsc , x_n$ that are somehow connected. Structured cospans provide a way to form these connections, hence we want $\mathsf{X}$ to fit into an appropriate adjunction $L \dashv R$ . Because our construction uses structured cospans, we need a way to represent a closed network with structured cospans. We turn a closed network $x$ into the structured cospan $L0 \to x \leftarrow L0$ with an empty interface. Note that here $0$ denotes an initial object in $\mathsf{A}$ , and $L0$ is an initial object in $\mathsf{X}$ because $L$ is a left adjoint.

The particular decomposition we use is determined by the grammar. That is, we start with a grammar $( \mathsf{X},P )$ where $\mathsf{X}$ can fit into an adjunction $L \dashv R \colon \mathsf{X} \to \mathsf{A}$ with a monic counit satisfying the adhesivity condition. This gives a discrete comonad $\flat := LR$ , which allows us to form the discrete grammar $(\mathsf{X},P_\flat )$ as in Definition 14.

Finally, we need to define a particular grammar used to generate our inductive viewpoint of rewriting.

Definition 26. Fix an adjunction $L \dashv R \colon \mathsf{X} \to \mathsf{A}$ and a grammar $G := (\mathsf{X}, P)$ . Define $ G' = ( _L \mathsf{StrCsp} , P'_\flat )$ to be a structured cospan grammar where $ P'_\flat$ contains the rule

for each rule $ \ell \leftarrow \flat k \to r$ of $ P_{\flat }$ .

Applying the language construction $\mathbf{Lang} (G')$ , then, encodes $\mathrm{Lang} (G)$ in its 2-cells, which are generated by the rules in $P_\flat$ . Since $\mathrm{Lang} (G)$ is generated by the rewrite relation for $G$ , this forms the inductive viewpoint of the rewrite relation.

Proof. We show sufficiency by inducting on the length of the generating arrows of $\mathrm{Lang} (G)$ , which come from the rewrite relation $ \rightsquigarrow ^\ast$ . If $ g \rightsquigarrow ^\ast h$ in a single step, meaning that there is a diagram

in $\mathsf{X}$ whose top row is a rewrite rule in $P$ , then the desired 2-cell is the horizontal composition of

where $g \cong l +_{\flat k} d$ and $h \cong r +_{\flat k} d$ . Then, the 2-cell for a derivation $ g \rightsquigarrow ^\ast h \rightsquigarrow j$ is the vertical composition of

The top square is from $ g \rightsquigarrow ^\ast h$ and the second from $ h \rightsquigarrow j$ .

Conversely, we proceed by structural induction to show that given an arrow in the hom-category $ \mathbf{Lang} (G')(L0,L0)$ , there is a corresponding derivation per the rewrite relation. The base case is the generating 2-cells, which holds by construction. Next, we show that both horizontal and vertical composition preserve $ \rightsquigarrow ^\ast$ . Vertical composition preserves $ \rightsquigarrow ^\ast$ due to the transitivity of the rewrite relation. Horizontal composition must have the form

\begin{equation*} \mathbf{Lang} (G')(L0,La) \times \mathbf{Lang} (G') (La,L0) \to \mathbf{Lang} (G')(L0,L0). \end{equation*}

So given

where $g \rightsquigarrow ^\ast h$ and $g' \rightsquigarrow ^\ast h'$ then we get $g+_{a}g' \rightsquigarrow ^\ast h+_{a} h'$ by realizing the horizontal composition as

composing horizontally, then performing this rewrite by first applying $g \rightsquigarrow ^\ast h$ to $g$ to get $g+_{La}g' \rightsquigarrow ^\ast h+_{La} g'$ and then applying $g' \rightsquigarrow ^\ast h'$ to $g'$ to get $g+_{La}g' \rightsquigarrow ^\ast h+_{La} h'$ .

As a corollary, we have that Theorem27 applies to grammars in the categories of directed hypergraphs, undirected hypergraphs, unmarked Petri nets, marked Petri nets, and their typed variants. It also applies to typed graphs so applies to the ZX-calculus (Cicala Reference Cicala, Coecke and Kissinger2018a).