# Drag Rewriting

Nachum Dershowitz, Jean-Pierre Jouannaud, Fernando Orejas

► To cite this version:

Nachum Dershowitz, Jean-Pierre Jouannaud, Fernando Orejas. Drag Rewriting. 2023. [hal-04143346v6](https://hal HAL Id:)

https://inria.hal.science/hal-04143346v6

Preprint submitted on 27 Jun 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
DRAG REWRITING

NACHUM DERSHOWITZ, JEAN-PIERRE JOUANNAUD, AND FERNANDO OREJAS

School of Computer Science, Tel Aviv University, Ramat Aviv, Israel

École Normale Supérieure de Paris-Saclay, France

Universitat Politècnica de Catalunya, Barcelona, Spain

**ABSTRACT.** We present a new and powerful algebraic framework for graph rewriting, based on *drags*, a class of graphs enjoying a novel composition operator. Graphs are embellished with roots and sprouts, which can be wired together to form edges. Drags enjoy a rich algebraic structure with sums and products. Drag rewriting naturally extends graph rewriting, dag rewriting, and term rewriting models.

**Keywords:** Graph rewriting, drags, composition

<figure><img src="image_2.png" /></figure>

Ring-a-ring o' roses,
A pocket full of posies,
A-tishoo! A-tishoo!
We all fall down.

—From: Kate Greenaway,
*Mother Goose or*
*The Old Nursery Rhymes* (1881);
illustration from
*Harper's Young People* (1881)

<footnote>Received by the editors Draft of June 27, 2024.</footnote>
CONTENTS

<table><tr><td>1. Introduction</td><td>3</td></tr><tr><td>2. The Drag Model</td><td>4</td></tr><tr><td>3. Contexts and Subdrags</td><td>7</td></tr><tr><td>4. An Example</td><td>8</td></tr><tr><td>5. Drag Morphisms</td><td>11</td></tr><tr><td>5.1. Morphisms, monomorphisms, isomorphisms and equimorphisms</td><td>11</td></tr><tr><td>5.2. The Category of Drags</td><td>13</td></tr><tr><td>5.3. Notations</td><td>15</td></tr><tr><td>6. Drag Operations</td><td>15</td></tr><tr><td>6.1. Compatibility</td><td>15</td></tr><tr><td>6.2. Sum</td><td>16</td></tr><tr><td>6.3. Wiring</td><td>17</td></tr><tr><td>6.4. Coherence</td><td>20</td></tr><tr><td>6.5. Product</td><td>22</td></tr><tr><td>7. Decomposition of Drags</td><td>24</td></tr><tr><td>8. Algebra of Drags</td><td>29</td></tr><tr><td>9. Sharing Equivalence</td><td>30</td></tr><tr><td>10. Rewriting</td><td>33</td></tr><tr><td>10.1. Congruences</td><td>33</td></tr><tr><td>10.2. Rewrite rules</td><td>35</td></tr><tr><td>10.3. Rewriting relations</td><td>35</td></tr><tr><td>10.4. Congruences joinable by rewriting</td><td>40</td></tr><tr><td>11. Drag Rewriting versus Term Rewriting</td><td>42</td></tr><tr><td>12. Categorical Interpretation of Drag Rewriting</td><td>45</td></tr><tr><td>12.1. Rules</td><td>45</td></tr><tr><td>12.2. Matching</td><td>45</td></tr><tr><td>12.3. Rewriting</td><td>48</td></tr><tr><td>13. Discussion</td><td>50</td></tr><tr><td>13.1. Coherent sets of wires</td><td>51</td></tr><tr><td>13.2. Varyadic labels</td><td>51</td></tr><tr><td>14. Related Work</td><td>51</td></tr><tr><td>14.1. DPO</td><td>51</td></tr><tr><td>14.2. Algebraic approaches</td><td>52</td></tr><tr><td>14.3. Term graphs</td><td>52</td></tr><tr><td>14.4. Patches</td><td>53</td></tr><tr><td>14.5. Graphs with interfaces</td><td>53</td></tr><tr><td>14.6. String diagrams</td><td>54</td></tr><tr><td>15. Conclusion</td><td>54</td></tr><tr><td>References</td><td>55</td></tr></table>
# 1. INTRODUCTION

Rewriting with graphs has a long history in computer science, graphs being used to represent data structures, as well as program structures and even concurrent and distributed computational models. They therefore play a key rôle in program evaluation, transformation, and optimization, and more generally in program analysis; see, for example, [CS18].

As rewriting graphs is very similar to rewriting algebraic terms, the same questions arise for both: What rewriting relation do we need? Is there an efficient pattern-matching algorithm? How can one determine if a particular rewriting system is confluent and/or terminating? Does graph rewriting encompass term rewriting?

These questions have—for these reasons—been addressed by the rewriting community since the mid-seventies with two different research trends: (1) in research initiated by Hartmut Ehrig and his collaborators, either in the context of general graphs equipped with pushouts [EPS73] or for particular classes of graphs—specifically those that do not contain cycles [PH94]; and (2) in research initiated by Henk Barendregt and his collaborators [BvEG$^+$87] in the context of term graphs, a generic terminology capturing various generalizations of terms. Over the years, some effort was devoted to uniting these two trends (e.g. [Plu99, CG99b]), aiming at answering the question to what extent term rewriting is covered. As part of these efforts, termination and confluence techniques have been elaborated for various generalizations of trees, such as rational trees, directed acyclic graphs, jungles, term-graphs, lambda-terms, and lambda-graphs, as well as for graphs in general. See [Cou90, Cou93] for detailed accounts of these techniques and [HT18] for a survey of implementations of various forms of graph rewriting and of available analysis tools.

One important practical objective of many of these works is to make modeling of sharing within graph structures possible so as to enable formal proofs of sharing techniques used in programming languages, whether by means of terms or graphs. In this context, it becomes crucial to faithfully encode term rewriting as a form of graph rewriting. This question was first addressed in [BvEG$^+$87], and solved in the particular case of term graphs (directed graphs whose all vertices are accessible from one of them, and equipped with a function symbol whose arity dictates the number of their successors) and left-linear rewrite rules whose all critical pairs are trivial. This question has returned again and again in the literature on term-graphs, by extending the term-graph framework to more general graphs and rewrite rules [CG99b], by restricting the general graph framework to acyclic graphs, or by accepting cyclic graphs while restricting one to acyclic left-hand sides of rules to better capture term rewrites [HKP91]. One reason, among several, for the multiplicity of efforts is the difficulty of integrating non-linear rewrite rules within graph frameworks, a problem pointed out already in [BvEG$^+$87], but—as they argue—one that cannot be solved positively without substantial modifications to their framework. Nor has it been solved in the categorical framework, where its importance has also been stressed [PEM86].

Drags, the alternative model considered here, are arbitrary directed graphs equipped with roots and sprouts that facilitate composition. Internal vertices, as in term graphs, are labeled by function symbols having a fixed arity. Sprouts are non-internal vertices without successors, labeled by variables. Our framework is able to faithfully encode term rewriting without restriction, hence finally solving this old question positively. An earlier version of drags paved the way for the present work [DJ19]. The current, substantially revised version has the potential to provide an interesting alternative to the double pushout (DPO)
framework for graph rewriting. In addition to its conceptual simplicity, one advantage of drags over DPO is the absence of dangling edges caused by rewriting.

Intuitively, drags can be viewed as networks of processing units that accept a given (finite) number of data as inputs and deliver data as outputs that can be sent over an arbitrary (finite) number of one-way channels. Channels can of course be duplicated, allowing thereby for arbitrary sharing. There is an order among the input channels of a processing unit so as to appropriately discriminate among the inputs. Inputs enter a drag at its sprouts, which are vertices without successors, labeled by variables. Outputs exit the drag at its roots, which are incoming edges with no source. Duplication is modeled by multiplicity of a given root vertex and of a given variable labeling several sprouts. Thus, drags differ from ordinary directed labeled graphs in their distinguishing of roots and sprouts.

The generality of this graph model requires that these one-way channels connect the processing units in an arbitrary way via their respective roots and sprouts. Connecting two drags defines a composition operator so that matching a left-hand side of rule *L* in a drag *D* amounts to writing *D* as the composition of a context graph *C* with *L*, and rewriting *D* with the rule *L* → *R* amounts to replacing *L* with *R* in that composition. In the case of drags, composition plays therefore the rôle of both context grafting and substitution in the case of trees. The same applies to equations, allowing us to define the notion of a congruence generated by a set of drag equations in the usual way, with rewriting providing, as for terms, a way to decide whether two drags are congruent. In sharp contrast with term rewriting, on the other hand, drag rewriting takes advantage of the underlying graph model: subdrags shared by *L* and *R* need not be removed before being (re-) generated. This holds for sprouts as well. This is similar to the DPO approach to rewriting, which specifies which vertices are to be removed, which are to be (re-) generated, and for which variables are absent. The DPO formalism applies to many different categories of graphs. In our model, such specifications follow the determination of the user that left-hand and right-hand sides of a rule do or do not share specific subgraphs.

## 2. THE DRAG MODEL

Drags were introduced in [DJ19, DJ18] and developed further in [JO23]. Retaining the moniker, we introduce here a completely new version, which is much better behaved and allows for easier generalization, while at the same time is more simply defined.

Drags are finite *d*irected *r*ooted *l*abeled ordered multi-*g*raphs. Some vertices with no outgoing edges are designated *sprouts*. Other vertices are *internal*. We presuppose the following: a set of function symbols $\Sigma$, whose elements—equipped with a fixed arity—serve as labels for internal vertices; and a set of nullary variable symbols $\Xi$, disjoint from $\Sigma$, used to label sprouts.

We make considerable use of multisets. A *finite multiset* is a function from a finite base set *E* to the set $\mathbb{N}$ of natural numbers. Finite multisets are often enumerated as in {$a, a, b, a, b, c$}. *Finite sets* are finite multisets all of whose elements occur precisely once as in {$a, b, c$}. A *sub-multiset* $N$ of a multiset $M$, written $N \subseteq M$, gives a number of elements $N(e) \le M(e)$ for each element $e$ of the base $E$. Given two finite multisets $M$ over $E$ and $N$ over $F$, a (total) *multi-map* $f: M \to N$ is some (dependent) function $f^+: (a, m) \mapsto (b, n)$, $0 < m \le M(a)$, $0 < n \le N(b)$, so that $f(e)$ will denote the multiset of elements $\{f^+(e, 1), \dots, f^+(e, M(a))\}$. (The second arguments $m, n$ of the function description $f^+$ serve as indices of the multiple $M(a), N(b)$ occurrences of the first arguments $a, b$). The
multiset *M* is the *domain* of *f*, also denoted *Dom*(*f*), while the multiset *N* is its *codomain*
or *image*, denoted *Ima*(*f*). A multi-map *f*: *M* → *N* is *partial* if the associated map *f*<sup>+</sup> is
partial, and *multi-injective* (*multi-equjective*) if the associated map *f*<sup>+</sup> is *injective* (bijective,
respectively). Note that a partial multi-injective multi-map becomes multi-equjective as a
multi-map from its domain to its image. If *M*, *N* are finite sets, then *f* is a classical injective
(bijective) map from *M* to *N*. Finally, a map *f*: *E* → *F* extends to a finite multiset {*a*<sub>*i*</sub>}<sub>*i*</sub>
over *E* as the multi-map returning the finite multiset {*f*(*a*<sub>*i*</sub>)}<sub>*i*</sub> over *F*.

To ameliorate notational burden, we use vertical bars `|` to denote various quantities,
such as length of lists, size of expressions, of sets or multisets, and even the arity of function
symbols. We use `Ø` for an empty list, set, or multiset, `∪` for both set and multiset union
(which takes the maximum of multiplicities for multisets), `∩` for set and multiset intersection
(minimum for multisets), `∩\cup` for set and multiset difference (natural subtraction for multisets),
`∪\cup` for disjoint union (which adds multiplicities), and `∈` for membership (`a ∈ M` iff `M(a) > 0`
for multiset `M`). We will identify a singleton set or multiset with its single element to avoid
unnecessary clutter. So, for example, `a₀ ∪ {aᵢ}i=n = {aᵢ}i=0`.

**Definition 2.1** (Drag). A drag *D* is a tuple *⟨V, R, L, X, S⟩*, where

(1) *V* is a finite set of *vertices* (vertices have a *name*);

(2) $R: V \to \mathbb{N}$ is a finite, possibly empty, multiset of vertices, called *roots*; when $R(v) > 0$, vertex $v$ is *rooted*; when $R(v) = 0$ it's *rootless*; sprouts can be rooted;

(3) *S* ⊆ *V* is a set of *sprouts*, leaving *I* = *V* `\` *S* to be the *internal* vertices;

(4) $L: V \rightarrow \Sigma \cup \Xi$ is the *labeling function*, mapping internal vertices $I$ to labels from vocabulary $\Sigma$ and sprouts $S$ to labels from vocabulary $\Xi$ (vertices have a *label*);

(5) $X: V \rightarrow V^*$ is the *successor function*, mapping each vertex $v \in V$ to a list of vertices in $V$ whose length equals the arity of its label, that is, $|X(v)| = |L(v)|$. Sprouts have no successors.

The pair $(R, S)$ of *roots* and *sprouts* is the *interface* of drag *D*.

Drags are accordingly based on ordered multigraphs with *roots*.

**Definition 2.2** (Linear; bare; ground; empty; disjoint). A drag *D* is *linear* if no two sprouts in *S*(*D*) have the same label, *closed* if it has no sprout (*S*(*D*) = *Ø*), *bare* if it has no roots, *ground* if it has neither root (*R*(*D*) = *Ø*) nor sprout, and *empty* (denoted by *Ø*) if it has no vertices at all (*V*(*D*) = *Ø*). We denote by *D̂* the bare drag obtained from *D* by removing all its roots. Two drags are *disjoint* if they share neither vertex nor variable.

Here is an example of a linear drag with three internal vertices (blue and yellow), one
(red) root and two (green) sprouts:

<figure><img src="image_3.png" /></figure>

**Definition 2.3** (Accessibility). Drags are directed: If *b* is the *k*th vertex in the list *X*(*a*) of successors of vertex *a* of drag *D* = ⟨*V*, *R*, *L*, *X*, *S*⟩, then *a* →*k* *b* is a directed *edge* with *tail*
a and head b, k being usually omitted. The reflexive-transitive closure $X^*$ of the successor relation X is called accessibility. We also write $aXb$, $a \to b \in X$, or just $a \to b$, as well as $aX^*b$, $a \to b \in X^*$, or $a \to^{*} b$.

(1) A vertex $v$ is said to be accessible from vertex $u$, and likewise that $u$ accesses $v$, if $uX^*v$.

(2) Two vertices are unrelated if neither is accessible from the other.

(3) Accessibility extends to sets as expected, denoting the set of vertices of $D$ that are accessible from any vertex in $W \subseteq V$ by $X^*(W)$.

(4) A vertex $v$ is accessible (without qualification) if it is accessible from some root, that is if $v \in X^*(r)$ for some rooted vertex $r$.

(5) A path of length $n$ is a sequence $u_0, \dots, u_n$ of vertices such that $\forall i \in [0..n-1] : u_i \to u_{i+1} \in X$. The path is trivial if $n=0$.

(6) A cycle is a (non-trivial) path such that $s_n = s_0$. A loop is a cycle of length one.

**Definition 2.4 (Connected component).** Given a drag $D$ with successor relation $X$, a connected component is a subdrag of $D$ generated by a set $W$ of vertices closed under predecessor, ancestor, and equal labeling of sprouts: $\forall u\forall v : uXv$ we have $u \in W$ iff $v \in W$, and $\forall s : x\forall t : x$ we have $s \in W$ iff $t \in W$.

**Definition 2.5 (Predecessor; indegree).** We denote by $pred(v, D)$, or simply $pred(v)$, the number of incoming edges to $v$ in drag $D$, and by $in(v, D)$, or simply $in(v)$, called the indegree of $v$, the number of its incoming edges plus the number of times $v$ is a root of $D$: $in(v, D) = pred(v, D) + R(v)$.

A vertex is a *source* of a drag if it has no predecessor, is a *sink* if it has no successor, and is *isolated* if it has neither predecessor nor successor, hence is both a source and a sink.

A *tree* is a ground drag all vertices of which have one predecessor, except for a lone vertex with none. A *forest* is a ground drag with no cycle, all vertices of which have zero or one predecessor. A *dag* is a ground drag sans cycles.

Here is a ground drag that is not a dag:

<figure><img src="image_4.png" /></figure>

**Remark 2.6.** Two other natural data structures are possible for the roots of drags: lists with repetitions and sets. Sets imply that arbitrarily many output channels can be given access to a given root. Multisets put a precise bound on that number and have slightly better algebraic behavior compared to lists with repetitions, which were used in [DJ19]. Completing the set of natural numbers with an infinite value allows one to easily encode set-like behavior by a multiset, another reason for our choice here.

**Remark 2.7.** Another important difference vis-à-vis [DJ19] is that we now also consider drags with inaccessible vertices, such as ground drags all of whose vertices are inaccessible.

**Notations:**

* When convenient, a drag $D = (V, R, L, X, S)$ will be denoted

$$ \langle \mathcal{V}(D), \mathcal{R}(D), \mathcal{S}(D), \mathcal{L}(D), X(D) \rangle $$
<figure><img src="image_5.png" /><figcaption>Figure 1: Two drags with the same subdrag but different context drags.</figcaption></figure>

with $Int(D)$ being its internal vertices, $Acc(D)$ its set of accessible vertices, $Var(D)$ the set of variables labeling its sprouts, and $Dom(R)$ the domain of the partial function $R$.

* We write $r^{[n]} \in R$ to indicate that there are $n$ copies of the rooted vertex $r$ in the multiset $R$, that is, $R(r) = n$, but also $r \in R$, considering $R$ as the set of rooted vertices. A root may also be seen as an edge without designated tail; so we will sometimes, in particular in figures, use the notation $\rightarrow r$ to indicate that vertex $r$ is rooted.

* We write $u : f$ when the vertex $u$ (possibly a sprout) has label $f$ (possibly a variable). The labeling function extends to lists, sets, and multisets of vertices as expected.

* In examples, we will often name vertices by their label, when the intention is clear. In case of ambiguity, we will index the label by a positive number, so that $f(x, x)$ has vertices $f$, $x_1$, and $x_2$. Combining these notations, $f^{[2]}(x, x^{[1]})$ has now two roots at vertex $f$ and one root at vertex $x_2$. In that case, we will alternatively write $f^{[2]}(x_1, x_2^{[1]})$.

* In pictures, roots will be illustrated by incoming arrows, possibly indexed by a natural number indicating their multiplicity.

### 3. CONTEXTS AND SUBDRAGS

**Definition 3.1** (Subdrag; context). Let $D$ be the drag $\langle V, R, L, X, S \rangle$, and let $W \subseteq V$. We define the following notions:

(1) The restriction $D|_W$ of drag $D$ to vertices $W$ is the drag

$$D' = \langle W \cup S', R', L', X', (W \cap S) \cup S' \rangle$$

where

(a) $S' = \{s_v : v \in V \setminus W, \exists w \in W : wXv\}$ are new sprouts, the $s_v$ being new vertices;

(b) $R'(w) = R(w) + \sum_{v \to w} \sum_{w \to v} k$, for each $w \in W$ (hence $in(w, D') = in(w, D)$);

(c) $L'$ coincides with $L$ on $W$, while $L'(s_v) = x_v$ for each $s_v \in S'$, where $x_v$ is a fresh variable;

(d) $X'$ coincides with $X$ on $W$, and for each $s_v \in S'$, $u \to s_v$ iff $u \to v \in X$.

(2) The subdrag $D|_W$ of $D$ generated by $W$ is the restriction of $D$ to the set of all vertices accessible from $W$. That is, $D|_W = D|_{X^*(W)}$. The subdrag is *void* when $W = \emptyset$, *trivial* when $X^*(W) = V$ (as for $D|_R$ because all vertices of $D$ are accessible from $R$), and *strict* when not trivial.

(3) The context $D|_W$ of $W$ in $D$ is the restriction of $D$ to the set of vertices that are inaccessible from $W$, viz. $D|_{V \setminus X^*(W)}$.

Let $D$ a drag reduced to a single internal vertex $v$ and edge $v \to v$. Then, the restriction of $D$ to $v$ is $D$ itself. Examples of drags, subdrags, and context drags are shown in Figure 1.
Subdrags need no new sprouts since their vertices are closed under succession, but context drags do. On the other hand, a (nontrivial, non-void) subdrag always has new roots. In particular, a nontrivial subdrag of a term at some position in the term has a root at its head, while the subterm has none. These new roots play an important rôle in the reconstruction of $D$ from $D|_W$ and $D \upharpoonright_W$.

**Lemma 3.2.** *The strict subdrag relation is a well-founded order.*

*Proof.* Because strict subdrags have fewer vertices. ☐

## 4. AN EXAMPLE

To motivate the development of drag rewriting, consider an example. The goal is to take a ring of blue vertices (a ground drag) like this:

<figure><img src="image_6.png" /></figure>

and create instead a ring consisting of red vertices, in the same quantity as the blue but going in the opposite direction, like this:

<figure><img src="image_7.png" /></figure>

To make what's happening clearer, we will be using red for original edges, blue for new, and green for temporary ones.

We seek a rewriting algorithm that can apply at the same time—in parallel—to many vertices along the ring.

The left-hand and right-hand sides are drags; see [DJ19]. Left roots map to right roots, and the two share variables.

There are two rules. The first creates the red vertex and introduces a gray vertex to keep track of connections.

<figure><img src="image_8.png" /></figure>

The two new vertices, red $c$ and gray $o$, are added with edges connecting them in both directions. The edge from $a$ to whatever $x$ may be is replaced by an edge from $o$. Instead of the root $a$ on the left, it is $o$ that becomes the new root. Vertex $a$ becomes detached as its incident edges are removed by the rule.
Applying this rule thrice to

<figure><img src="image_9.png" /></figure>

starting at the lower left and proceeding counterclockwise, we get the following sequence of drags:

<figure><img src="image_10.png" /></figure>

The orphaned *a* vertices are left shaded.

The next rule connects the added red vertices in the opposite direction:

<figure><img src="image_11.png" /></figure>

The red *c* vertex on the left is dotted and the one on the right is dashed to indicate that they are actually distinct vertices. The edge from it is redirected (in blue) to the other vertex pointed to by the gray *o* that points to the original head of the edge from *c*. A new, yellow double-rooted vertex *e* is created to replace the deleted, double-rooted *o*, and serves to preserve incoming edges. The two edges to the vertex signified by variable *x* have been cut, so are now just roots.
Applying this rule to

<figure><img src="image_12.png" /></figure>

three times, we get

<figure><img src="image_13.png" /></figure>

This rule cannot be applied before a red vertex is created by the previous rule. Later on, we will consider garbage collection for vertices like *e* that have served out their purpose. Actually, the old *c* vertex also sticks around and can be recycled.

An alternative is to allow the left-hand and right-hand drags to share internal vertices— not just sprouts, but to have separate sets of edges for the two sides. The two rules are the same as before, except that now the red vertex *c* in the second rule is shared by both sides:

<figure><img src="image_14.png" /></figure>

The red *c* vertex on the two sides has a solid border to make it clear that it is the same vertex on the two sides. The edge from *c* to *x* is redirected to *y*, as before. As in the previous version, the gray *o* vertex is only in the left drag, while the yellow *e* is only in the right one. The application of this rule would look the same as the above, except that the red vertices are preserved by the rule. Later, in Example 10.16, we will recast this example by using a more general rewrite rule format, with sharing of subdrags between left- and right-hand sides.
## 5. DRAG MORPHISMS

A vertex of a drag has both a name (an element in $V$) and a label, taken from $\Sigma$ or $\Xi$. In particular, the sprouts of a drag are vertices labeled by variables from $\Xi$. The vertices of ordinary terms, on the other hand, are usually left nameless, with their positions (in a Dewey-decimal-like notation) standing in for names. In the term tradition, sprouts are variables: the difference between a sprout and its label does not matter because the term framework does not distinguish between two terms that correspond to distinct isomorphic graphs. Drags being graphs, two drags may be identical or they may be isomorphic as graphs. This distinction becomes crucial when it comes to sharing, which is why it is not relevant for terms, where there is no sharing. Of course, terms can be seen as a particular kind of drag, but, as just stressed, it is important to understand that term equality for trees corresponds to isomorphism of drags, not identity.

To define precisely the kinds of equalities on drags in which we are interested, notions of drag morphism, drag monomorphism, and drag isomorphism are required. These must of course reduce to the corresponding notions on graphs for ground drags. The possibility that drags share vertices will require special care. Another important matter is categoricity.

### 5.1. Morphisms, monomorphisms, isomorphisms and equimorphisms.
As usual, morphisms will be maps from the set of edges of the input drag to the set of edges of the target drag that are the identity on shared vertices. What differs from the usual graph morphisms is that we need to take care of variables, regarding which we encounter three problems. First, internal vertices need be mapped to internal vertices, as is already the case with terms. Second, the drag may be nonlinear, two or more sprouts being labeled the same; such sprouts cannot be mapped independently of each other. Third, two vertices of the input drag may be mapped to the same vertex of the target drag in case the mapping is not injective. This is a standard situation for morphisms, but this has to happen for monomorphisms as well, if only for two sprouts sharing the same label. But monomorphisms may also have to map a sprout and an internal vertex of the input drag to the same vertex of the target drag: Monomorphisms will be injective on internal vertices only. We address these questions in turn in the sequel.

**Definition 5.1 (Equimorphism).** Given two drags $D = (V, R, L, X, S)$ and $D' = (V', R', L', X', S')$, an *equimorphism* is a bijective map $o: V \to V'$ that preserves labels and *root quantity* at all vertices $[\forall u \in V: L'(o(s)) = L(u) \text{ and } R'(o(u)) = R(u)]$ as well as the successor function $[u \to^i v \in X \text{ iff } o(u) \to^i o(v) \in X']$.

Equimorphic drags are just copies of one another, possibly sharing some vertices, and therefore, the inverse of an equimorphism is itself an equimorphism.

**Definition 5.2 (Morphism).** Given two drags $D = (V, R, L, X, S)$ and $D' = (V', R', L', X', S')$, $I$ and $I'$ their respective sets of internal vertices, a *morphism* from $D$ to $D'$ is a map $o: V \to V'$, called a *vertex map*, which

(1) restricts to mappings from internal vertices $I$ to $I'$ and preserves their labels;

(2) restricts to mappings from isolated sprouts of $D$ to isolated sprouts of $D'$;

(3) preserves indegrees at all vertices of $o(I)$ [$\forall v \in o(I): \sum_{u \in I: o(u)=v} in(u, D) = in(v, D')$];

(4) maps edges of $D$ to corresponding edges of $D'$ [$\forall u \to^i v \in X: o(u) \to^i o(v) \in X'$];

(5) preserves equimorphic subdrags, that is, maps equimorphic subdrags of the source drag to equimorphic subdrags of the target drag.
We denote by $o_I$ the restriction of $o$ to the internal vertices of $D$, and define the *edge map* of the morphism $o$ as $o_X(u \to^i v) = o(u) \to^i o(v)$.

If $D$ and $D'$ are ground drags, morphisms are just ordinary graph morphisms.

An important aspect of our definition is that morphisms may map a non-isolated sprout to any vertex of the same indegree, while isolated sprout must be mapped to an isolated sprout of the same indegree. In the literature of term graphs, isolated sprouts are rarely considered when defining morphisms. Likewise, condition (5) is either omitted in the absence of non-linear sprouts, or strengthened by mapping non-linear sprouts to the same vertex.

**Definition 5.3 (Monomorphism, isomorphism).** A *monomorphism* is a morphism whose vertex map restricts injectively to internal vertices and isolated sprouts. An *injection* is a monomorphism whose vertex map is the identity on internal vertices and isolated sprouts. A *isomorphism* is a morphism whose vertex map is bijective.

We will see later that finding a monomorphism mapping a drag $D$ to a drag $D'$ is nothing but matching $D$ against $D'$, an operation that will rely on indegree preservation. Note that indegree preservation becomes indeed a true preservation property for monomorphisms.

Since an edge $o(u) \to^i o(v)$ is characterized by the pair $(o(u), i)$, which is unique when $o$ is injective, the edge map $o_X$ of a monomorphism $o$ is injective on all edges. That's why we do not need to state it, even though $o$ is not injective on all vertices. This would not be the case were an edge simply a pair $u \to v$ instead of a triple $u \to^i v$.

Because isomorphisms are bijective and preserve equimorphic subdrags, they must map two sprouts of the same label $x$ to two sprouts of the same label $y$ possibly different from $x$, implying that the inverse of an isomorphism is an isomorphism. It therefore appears that equimorphisms are those isomorphisms that preserve labels at all sprouts.

Given a morphism $o: D \to D'$, edges of $D'$ may be mapped from edges between internal vertices of $D$, they will appear in black on the figures. Some others may be mapped for an edge of $D'$ whose target is a sprout, they will appear in red. Other edges of $D'$ are *context edges*. They appear in green if their target is not a vertex in the image of $o$, otherwise in blue. This categorization of edges will be made formal later and play an important rôle. For all examples, checking the requirements for being morphisms is left to the reader.

**Example 5.4 (Morphism).** Consider drags $D = f^{[1]}(f^{[2]}(x, x), x)$, with vertices $f_1$ (above) and $f_2$ (below) labeled by the binary symbol $f$ and three other vertices $x_1, x_2$, and $x_3$ (in depth-first order), and $D' = f(\text{SELF}, \text{SELF})$, a drag with a single vertex $f_3$ labeled $f$, two edges $f_3 \to^1 f_3$ and $f_3 \to^2 f_3$, and no root. Observe that the mapping $o: D \to D'$ such that $o(f_1) = o(f_2) = o(x_1) = o(x_2) = o(x_3) = f_3$ is a morphism. In particular, the indegree of $f_3$ (= 4) is the sum of the indegrees of $f_1$ (= 3) and $f_2$ (= 1). This example is represented on the right of Figure 2. $\square$

**Example 5.5 (Monomorphism).** The same Figure 2 shows on its left a monomorphism that maps the internal vertex $f_1$ to vertex $f_2$ of the same indegree 3, and both sprouts $x_1$ and $x_2$ to the internal vertex $f_2$. See how the two (red) edges of $D$ become edges of $D'$ between internal vertices.

**Example 5.6.** Figure 3 (left) is an example of a monomorphism $[o(f_1) = f_2, o(a_1) = a_2, o(x) = a_2]$ with various kinds of edges. Note that the left vertex labeled $a$ has lost its roots. One has actually been “used” by the edges $f_1 \to^1 x$ to create the edge $f_2 \to^1 a_2$; The other has been “absorbed” by the edge $h \to^1 a_2$ of the target drag.
<figure><img src="image_15.png" /><figcaption>Figure 2: A monomorphism (↔) on the left and a morphism (→) on the right. Incoming arrows at some vertex annotated with numbers stand for multiple roots.</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>Figure 3: Additional examples of monomorphisms.</figcaption></figure>

**Example 5.7 (Isomorphism).** We now show that the two drags $D = f(x, y^{[1]})$ and $D' = f(x, z^{[1]})$, sharing the sprout labeled $x$, where $y$ and $z$ are different, are isomorphic. Using the map $o: D \to D'$ such that $o(f_1) = f_2$, $o(x) = x$ and $o(y) = z$, $o$ being the identity for the shared vertex $x$, implying that $o_X(f_1 \to^1 x) = f_2 \to^1 x$ and $o_X(f_1 \to^2 x) = f_2 \to^2 z$, we get $o(D) = D'$. The map $o$ is a monomorphism that is bijective, hence is an isomorphism. Were the vertex $z$ in $v$ replaced by a vertex $w$ labeled $y$, both drags would be equimorphic, regardless of whether $w$ is shared with the vertex $y$ in $u$. □

**5.2. The Category of Drags.** We have already pointed out the strong preservation condition of equimorphic drags by morphisms: The weaker condition that identically labeled sprouts be related by isomorphism, as suggested in [DJ19], would not ensure the following key properties:

**Lemma 5.8.** *Morphisms, monomorphisms, injections, isomorphisms, and equimorphisms are closed under composition.*

*Proof.* Consider $o: D \to D'$ and $o': D' \to D''$, and let $o'' = o' \circ o: D \to D''$ be their composition.
Equimorphisms compose since bijections do, and preservation of variable labels and edges is transitive.

Morphisms compose because restrictions to internal vertices and isolated sprouts compose, preservation of indegrees does because addition is associative, edge maps compose because vertex maps do, and preservation of equimorphic subdrags is satisfied because equimorphisms compose.

Monomorphisms compose because injectivity on internal vertices and isolated sprouts is preserved by composition.

Being monomorphisms whose vertex map is the identity, injections compose.

Being monomorphisms whose vertex map is bijective, isomorphisms compose. □

Classically, graphs and their morphisms form a category but have no roots at their internal vertices nor variables at their leaves that can be redirected to the roots. Their presence in drags and the associated preservation properties that morphisms must satisfy make nontrivial two properties that are usually obtained naturally.

Drag morphisms are indeed defined on equivalence classes of drags modulo isomorphisms because, given any input drag, an isomorphism preserves its roots at all vertices and maps its equimorphic subdrags to equimorphic subdrags of the output drag.

Monomorphisms on graphs are just injective morphisms between their sets of vertices and between their sets of edges. Here, monomorphisms are more complex maps, being injective on internal vertices only, as are substitutions on terms, which actually implies that $o_X$ is injective on all edges thanks to the natural number component of an edge. These properties imply that our monomorphisms are indeed monomorphisms in the categorical sense, that is, are the left-cancellative morphisms:

**Lemma 5.9 (Categoricity).** Let $D', D''$ be drags. A morphism $\kappa$ from $D'$ to $D''$ is a monomorphism iff for it is left cancellative, that is, for all drags $D$ and morphisms $o, o'$: $D \to D'$ such that

$$ \kappa \circ o = \kappa \circ o' \quad (*) $$

it is the case that $o = o'$.

*Proof.* Claim: Let $I$ and $I'$ be the sets of internal vertices and isolated sprouts of $D$ and $D'$, respectively. Property (*) implies $\kappa_{I'} \circ o_I = \kappa_{I'} \circ o'_I$. Since categoricity reduces to injectivity for functions on sets, it follows that $o_I = o'_I$ iff $\kappa_{I'}$ is injective.

Assume now that $\kappa$ is a monomorphism, hence that $\kappa_{I'}$ is injective and $o_I = o'_I$ by the above Claim. Therefore, $o_X = o'_X$ by definition of an edge map, which implies in turn that $o_V = o'_V$ for non-isolated sprouts. Altogether, we get $o = o'$.

Conversely, assume that $o = o'$ for all morphisms $\kappa$ satisfying (*). By the same token as previously, the restriction $\kappa_{I'}$ of the morphism $\kappa$ is therefore injective, hence $\kappa$ is a monomorphism. □

The proof shows that injectivity of monomorphisms for internal vertices and isolated sprouts ensures categoricity. The definition of morphisms for sprouts is therefore unimportant, provided transitivity is satisfied. The precise definition we gave has therefore a single objective: to ensure that matching behaves as desired. We will show in Section 12 that this is indeed the case.

We can now conclude:

**Theorem 5.10.** Drags equipped with their morphisms, monomorphisms, and isomorphisms form a category, of which the category of terms is a particular case.
**5.3. Notations.** We end this section by introducing notations for the various kinds of morphisms and related equalities that are relevant for drags.

We write $o: D \to D'$ for a morphism $o$; $o: D \to D'$ if $o$ is a monomorphism; $D \cong_o D'$ when $o$ is an isomorphism; $D \cong_o D'$ if $o$ is an equimorphism; and $D = D'$ when $o$ is identity. The subscript $o$ will often be omitted. Monomorphisms may be abbreviated “monos”.

We may need more precise notations $D \cong_o D'$ in case of an isomorphism $o$, where $\sigma$ is a bijection between the variables of corresponding sprouts. $D'$ is sometimes called a renaming of $D$. The renaming preserves variables if $\sigma$ is the identity, in which case $D$ and $D'$ are equimorphic, implying that $D \cong_o^id D'$ and $D \cong_o D'$ are indeed the same. The notation $D = D'$ (not to be confused with definitional equality) is reserved for the case where $D$ and $D'$ are the very same drag.

Two drags $D$ and $D'$ are disjoint if they share no vertices nor variables. Renaming apart two drags $D$ and $D'$ amounts to renaming bijectively the shared vertices and variables of $D$ so that the result $D''$ is isomorphic to $D$ while $D'$ and $D''$ are disjoint.

## 6. DRAG OPERATIONS

There are two main operations on drags, sum and product, that are reminiscent of similar operations used in the literature, although in restricted settings compared to here. The third operation, wiring, is in some sense more fundamental than product, which amounts to a particular case of wiring a sum. Sum and product operate on compatible drags.

**6.1. Compatibility.** Operations on drags that are not disjoint requires an assumption:

**Definition 6.1 (Compatible drags).** Two drags $D = (V, R, L, X, S)$ and $D' = (V', R', L', X', S')$ are compatible if

* $V \cap V'$ is closed under $X$ and $X'$;

* $L$ and $L'$ coincide on $V \cap V'$;

* $D$ and $D'$ have the same indegree at each shared vertex $v$, at least equal to the total number of shared and non-shared edges heading at $v$.

In words, compatible drags that share a vertex must also share the whole subdrag generated by that vertex. Also, they must have enough roots at their shared vertices so as to have the same indegree after replacing the roots of each graph at a shared vertex by the incoming non-shared edges of the other graph at that vertex.

**Example 6.2.** The following two graphs $D, D'$ are compatible:

$$D = (\{v_1, v_2, v_3\}, (R(v_1) = R(v_3) = 0, R(v_2) = 1), (L(v_1) = f, L(v_2) = g, L(v_3) = a), (X(v_1) = v_2, X(v_2) = v_3, X(v_3) = v_2), \emptyset),$$

$$D' = (\{v'_1, v_2, v_3\}, (R(v'_1) = R(v_3) = 0, R(v'_2) = 1), (L(v'_1) = h, L(v_2) = g, L(v_3) = a), (X(v'_1) = v_2, X(v_2) = v_3, X(v_3) = v_2), \emptyset).$$
On the other hand, the following graphs are not compatible (closure condition violated):

$$D = (\{v_1, v_2, v_3\}, (R(v_1) = R(v_3) = 0, R(v_2) = 1), (L(v_1) = f, L(v_2) = g, L(v_3) = a), \\ (X(v_1) = v_2, X(v_2) = v_3, X(v_3) = v_1), \emptyset),$$

$$D' = (\{v'_1, v_2, v_3\}, (R(v'_1) = R(v_3) = 0, R(v_2) = 1), (L(v'_1) = h, L(v_2) = g, L(v_3) = a), \\ (X(v'_1) = v_2, X(v_2) = v_3, X(v_3) = v_2), \emptyset).$$

The following two graphs are also incompatible (lack of roots at $v_2$):

$$D = (\{v_1, v_2, v_3\}, (R(v_1) = R(v_2) = R(v_3) = 0), (L(v_1) = f, L(v_2) = g, L(v_3) = a), \\ (X(v_1) = v_2, X(v_2) = v_3, X(v_3) = v_1), \emptyset),$$

$$D' = (\{v'_1, v_2, v_3\}, (R(v'_1) = R(v_2) = R(v_3) = 0), (L(v'_1) = h, L(v_2) = g, L(v_3) = a), \\ (X(v'_1) = v_2, X(v_2) = v_3, X(v_3) = v_2), \emptyset).$$

One difficulty is that compatibility is not preserved by equimorphisms: $D = f(a_1)$ is compatible with itself, and $D$ is equimorphic with $D' = f(a_2)$, but $D$ and $D'$ are incompatible since $f$ is shared in $D$ and $D'$ but its successors $a_1$ in $D$ and $a_2$ in $D'$ are not.

**6.2. Sum.** Our first operation on compatible drags is both very simple and familiar when both drags are disjoint: it consists of placing two drags side by side to form a new drag.

**Definition 6.3 (Sum).** The parallel composition or sum $D \oplus D'$ of two compatible drags $D = (V, R, L, X, S)$ and $D' = (V', R', L', X', S')$ is the drag $\langle V \cup V', R \rangle, L \cup L', X \cup X', S \cup S'$, where, $\forall x \in V \cup V' : R''(v) = R(v) - |\{u \to^i v \in X' \setminus X\}| = R'(v) - |\{u \to^i v \in X \setminus X'\}|$.

Note that the equality statement when defining the number of roots at all vertices in the union of two drags follows from the definition of compatibility. Note also that $R''(v) = R(v)$ if $v \in V \cup V'$ and $R''(v) = R'(v)$ if $v \in V' \cup V$, implying that the union of disjoint drags is their juxtaposition.

The following straightforward properties of parallel composition are important:

**Lemma 6.4.** Given two compatible drags $D = (V, R, L, X, S)$ and $D' = (V', R', L', X', S')$,
(1) $D \oplus D'$ preserves indegrees of $D$ and $D'$ at all vertices;

(2) the injections from $V$ and $V'$ to $V \cup V'$ are monomorphisms from $D$ and $D'$ to $D \oplus D'$.

*Proof.* Preservation of indegrees at all vertices follows from the definitions of compatibility and sum. Being identities, these injections are injective morphisms that protect equimorphic subdrags and indegrees, hence are monomorphisms. $\square$

Parallel composition allows to define the intersection of two compatible drags:

**Definition 6.5 (Intersection).** The intersection of two compatible drags $D$ and $D'$ with vertices $V$ and $V'$ respectively is the subdrag of $D \oplus D'$, denoted $D \cap D'$, generated by $V \cap V'$.

Once more, we remark that indegrees are preserved at all vertices of the intersection.
**6.3. Wiring.** The purpose of wiring a drag *D* is to add new edges to a drag by *connecting* sprouts to roots. Informally, a set of wires will be a set of pairs made out of a sprout and a root, written as *s* ↦ *r*. Wiring *D* will be the action of redirecting all edges *u* → *s* in *D*, including the roots of *s*, so that they become edges *u* → *r* or roots of *r* in a new drag *D*'. Wiring may use a succession of wires like *s* ↦ *t* and *t* ↦ *r* that generate chains of wirings.

**Definition 6.6 (Wire, origin, target).** Given a drag $D = (V, R, L, X, S)$, a *wire* is a pair $s \rightsquigarrow r$ of vertices of $D$, whose *origin* $s$ is a sprout and *target* $r$ a vertex different from $s$.

**Definition 6.7 (Wiring chain).** Given a set of wires $W$ of a drag $D = (V, R, L, X, S)$, we define $s >_W r$ for $s \in S$ and $r \in R$, if $s \rightsquigarrow r \in W$ or if there is a vertex $t$ such that $s \rightsquigarrow t \in W$ and $t >_W r$.

In a wiring chain $s_0 \rightsquigarrow s_1 \rightsquigarrow \dots \rightsquigarrow s_n \rightsquigarrow r$, all but possibly the final element $r$ are sprouts, and the final element $r$ is a root—and possibly also a sprout.

**Definition 6.8 (Well-behaved set of wires).** A finite set $W$ of wires of $D$ is *well-behaved* if:

(1) functionality: $\forall s \rightsquigarrow r, s \rightsquigarrow r' \in W : r = r'$;

(2) injectivity: $\forall r \in R : \Sigma_{s>W} \mathrm{pred}(s) \leq R(r)$;

(3) well-foundedness: $W$ does not induce a cycle among the sprouts of $D$, that is, the restriction of $>_W$ to $S \times S$ is acyclic.

The domain $\mathrm{Dom}(W)$ of $W$ is the set of sprouts that are origins of a wire.

Condition (1) implies that $W$ is a partial function from $S$ to $V$. We will therefore be able to consider the *restriction* of that function to a subset of its domain. If $V' \subseteq V$, we will say that $W$ *restricts* to $V'$ if $\forall s \rightsquigarrow r \in W : r \in V'$ if $s \in V'$.

Condition (2) means that vertex $r$ is a root with a multiplicity large enough so that rewiring edges from $s_1, \dots, s_n$ to $r$ does not require more roots of $r$ than are available, which is yet another manifestation of multi-injectivity.

Condition (3) allows us to compare sprouts. Well-foundedness of this order aims at defining wiring by induction.

It also implies the following:

**Proposition 6.9.** The relation $\geq_W$ is a partial order for any well-behaved set of wires $W$.

An empty set of wires is trivially well-behaved. A wire $s \rightsquigarrow t$, considered as a singleton set, is well-behaved iff it satisfies injectivity, that is, if the indegree of $s$ is no larger than the number of roots of $r$.

We now define the drag obtained by adding wires to an existing drag, starting with the case of a single wire $s \rightsquigarrow r$. The idea is that sprout $s$ is removed, all edges ending up in $s$ (but not its roots) are moved to $r$ using its roots in the same number:

**Definition 6.10 (Elementary wiring).** Given a drag $D = (V, R, L, X, S)$ and a wire $s \rightsquigarrow r$, we define the drag $D_{s \rightsquigarrow r}$, after *wiring*, as the drag $\langle V', R', L', X', S' \rangle$ such that:

(1) $V' = V \setminus s$;

(2) $R' = R \setminus (R(s) \cup R(r)) \cup r^{R(r)-\mathrm{pred}(s)}$;

(3) $L' = L \upharpoonright V'$, the restriction of labels $L$ to vertices in $V'$;

(4) $X' = X \setminus \{v \to s : v \in X\} \cup \{v \to r : v \in X\}$;

(5) $S' = S \setminus s$.
The condition that the origin of a wire is distinct from its target ensures that the sprout origin of the wire has disappeared from the resulting drag. The calculation of the new multiset of roots in item (2) expresses the fact that each edge redirected from the origin to the target of the wire consumes a root of the target. In contrast with [DJ19], sprouts at the origin of a wire disappear with their roots, which are therefore lost if there were any. In the particular case where $s:x$ and $r:y$ are both rootless isolated sprouts, wiring allows one to rename the sprout labeled $x$ by the sprout labeled $y$.

**Lemma 6.11.** *Wiring preserves indegrees at all remaining vertices.*

To define wiring for an arbitrary set of well-behaved wires, we write a non-empty well-behaved set of wires $W$ as the union $s \rightsquigarrow r \cup W'$, where sprout $s$ is maximal in $>W$. Well-foundedness of $>W$ allows us to wire $s \rightsquigarrow r$ first, and then recur on $W'$, which can be easily shown well-behaved:

**Lemma 6.12.** *Let $W = s \rightsquigarrow r \cup W'$ be a well-behaved set of wires of $D$ such that $s$ is maximal in $>W$. Then, $W'$ is a well-behaved set of wires of $D' = D_{s \rightsquigarrow r}$.*

*Proof.* By maximality assumption, $s$ does not occur in $W'$ which is therefore a set of wires of $D'$. Functionality and membership follow straightforwardly from well-behavedness of $W$, as well as well-foundedness, since it restricts to subsets. Injectivity holds at all vertices since $\Sigma_{t>W} pred(t) = \Sigma_{t>W'} pred(t) + pred(s)$. $\square$

It follows that all subsets of a well-behaved set of wires are well-behaved.

We can now define recursively wiring with an arbitrary well-behaved set $W$ of wires. Not only do we define the new drag $D_W$, but also trace the vertices of the original drag along the recursive computation, with or without their root multiplicity.

**Definition 6.13 (Wiring, resolution, natural injection).** Given a well-behaved set of wires $W$ of a drag $D$, we define the drag $D_W$, after wiring, by induction on the size of $W$, where for a non-empty set of wires $W$, we write $s \rightsquigarrow r \cup W'$ for $W = \{s \rightsquigarrow r\} \cup W'$,

$$D_{\emptyset} = D \\ D_{s \rightsquigarrow r \cup W'} = (D_{s \rightsquigarrow r})_{W'}$$

The resolution $W(t)$ of sprout $t$ of $D$ in the domain of $W$ is the (unique) root $r$ in $D$ that is the minimal one such that $t \geq_W r$, together with its root multiplicity in $D_W$ after wiring. (There is a unique minimum on account of functionality of well-behaved sets of wires.) Also, the natural injection of $D$ into $D_W$ is the map $W_0(t)$ which returns the same vertex as $W(t)$ without its root multiplicity.

Since $W'$ is a well-behaved set of wires for the drag $D_W$ by Lemma 6.12, the recursive call $(D_{s \rightsquigarrow r})_{W'}$ makes sense. The functions, resolution and natural injection, could also be defined by induction in the same way that the post-wiring drag was. Note that in case $t$ is an internal vertex, the vertex itself is not changed by wiring, but its multiplicity might be.

Note also that a cycle is generated in a wired drag in case a sprout $s$ is accessible in the original drag from its resolution, implying that a loop (a cycle of length 1) can only be generated on an internal vertex.

**Example 6.14.** Figure 4 displays two examples of wiring, illustrating the recursive calculation of the result. We start with a drag union of two drags, and a well-behaved set $W$ of two wires written underneath. The number of times a vertex is a root is indicated next
<figure><img src="image_17.png" /><figcaption>Figure 4: Formation of cycles via composition, two versions.</figcaption></figure>

to the root arrow's origin; the number 1 is often omitted. Labels can serve here as vertex names since no two vertices have the same label. The middle drag is the result of the first step of the calculation, with the remaining set of one wire written again underneath.

For the first calculation, both edges that ended up in sprout $x$, which has disappeared, are now redirected to sprout $y$, which has a single root left, since two roots have been utilized by redirecting the edges $f \to x$ and $h \to x$. The rightmost drag is the final result, there is no set of wires left. 3 roots out of 4 in $h$ have been used by redirecting the 3 edges ending up in $y$ to $h$, while the root of $y$ is lost.

Starting with 2 roots instead of 3 for $y$ would yield the same result. Note also that starting with the wire $y \to h$ in which $y$ is not maximal would not make sense, since $x \to y$ would not be a wire anymore after the first step of the calculation. The tracing of $W(x)$ is indicated in red, $x$ moving to $y$ and then to $h$.

The second calculation is similar. We note that it yields the same result. This is no coincidence, as we shall see. □

For the recursive calculation of Definition 6.13 to make sense, we need to show that the resulting drag does not depend upon the choice of a maximal wire $s \rightsquigarrow r$:

**Lemma 6.15.** Given a drag $D = \langle V, R, L, X, S \rangle$ and a well-behaved set of wires $W$, $D_W$ and $W(v)$, for each vertex $v \in V$, are well-defined.

*Proof.* By induction on the size of $W$. We give the proof for the wiring definition.

If $W$ is empty, the result is straightforward. If it contains a single maximal wire, the induction hypothesis applies. Otherwise, let $W = s \rightsquigarrow r \cup s' \rightsquigarrow r' \cup W'$ where $s \rightsquigarrow r$ and $s' \rightsquigarrow r'$ are distinct wires, maximal for $>W$. Let $D' = (D_{s \rightsquigarrow r})_{s' \rightsquigarrow r'}$ and $D'' = (D_{s' \rightsquigarrow r'})_{s \rightsquigarrow r}$. Note that $W'$ is well-behaved for both $D'$ and $D''$, even if $r = r'$. By functionality, $s \neq s'$, and by maximality, $s' \neq r$ and $s \neq r'$; hence, redirecting the edges ending up in $s$ to $r$ and those ending up in $s'$ to $r'$ can be done in any order, showing that $D' = D''$.

Using Definition 6.13 twice for each calculation, $D_W = D'_{W'}$ if $s \rightsquigarrow r$ is chosen first, and $D_W = D''_{W'}$ if $s' \rightsquigarrow r'$ is chosen first. Since $D' = D''$, we conclude by the induction hypothesis that $D_W$ is well-defined. □

Wiring has three important properties illustrated at Figure 4:

**Lemma 6.16.** Let $D$ be a drag and $W$ a well-behaved set of wires of $D$. Then,
(1) $D_W$ and $D$ have the same internal vertices and total number of edges—not counting roots as edges;

(2) all vertices of $D_W$ have the same indegree in $D$ and $D_W$;

(3) whenever $W'$ is a well-behaved set of wires such that $\forall t \in V(D) : W(t) = W'(t)$, then $D_W = D_{W'}$.

The fact that wiring preserves indegrees, just like monomorphisms must, will turn out to be a key observation (Lemma 12.4 below).

*Proof.* The third property follows from the other two, which hold because internal vertices, total number of edges, and indegree of vertices are all preserved by an elementary wiring step—thanks to Lemma 6.11 for indegree. $\square$

**6.4. Coherence.** We haven't yet required that different wires sharing the same label satisfy an assumption implying that the corresponding sprouts are related. More precisely, given a drag $D$ and a set of wires $W$, we want two sprouts $s : x$ and $t : x$ of $D$, with the same label $x$, to become equivalent after wiring. Ideally, we would like to check the property without computing $D_W$, that is, read it on $D$ and $W$. In [DJ19], we required that $r = r'$ for any two wires $s : x \rightsquigarrow r$ and $s' : x \rightsquigarrow r'$ belonging to $W$, a model called *forced sharing*, and suggested that a more general equivalence should be drag isomorphism.

It turns out, however, that drag isomorphism is too weak. Take for example the drag $D = f(x, x, y, z, a, b)$ and the set of wires $W = \{x_1 \rightsquigarrow y, x_2 \rightsquigarrow z, y \rightsquigarrow a, z \rightsquigarrow b\}$. The sprouts $x_1$ and $x_2$ are replaced by equivalent drags, but won't remain equivalent in $D_W$ since $x_1$ will be eventually replaced by $a$ and $x_2$ by $b$. We could then expect that equimorphism, which is weaker than equality but stronger than isomorphism, could do.

And indeed, equimorphism in $D$ of the subdrags generated by $r$ and $r'$ is one possible answer, although not the most general one. There is however a difficulty: Equimorphism is not preserved along the wiring process, although it is finally restored. For an example, consider the drag $D$ made of three copies of $f(x)$, numbered 1,2,3. Let $W = x_3 \rightsquigarrow f_1 \cup W'$, with $W' = \{x_1 \rightsquigarrow f_2, x_2 \rightsquigarrow f_3\}$, be a set of wires that satisfies this equivalence condition. Wiring the sole wire $x_3 \rightsquigarrow f_1$ yields the drag $D'$ made of three subdrags, the first two are still the same as before while the last has become $f_3(f_1(x_1))$. Wires $W'$ no longer satisfy the property, since $x_1$ maps to $f_2$, which generates the subdrag $f_2(x_2)$, while $x_2$ maps to $f_3$, which generates now the subdrag $f_3(f_2(x_2))$, two non-isomorphic subdrags. On the other hand, applying all wires at once yields the drag which has three vertices $f_1, f_2, f_3$ and three edges $f_1 \to f_2, f_2 \to f_3, f_3 \to f_1$. Obviously, the subdrags generated by $f_1, f_2, f_3$ are still equimorphic. This is the reason why we did not include coherence into the definition of a well-behaved set of wires: recurring on $W$ would have become impossible. Wiring, hopefully, makes sense even when $W$ is not coherent, hence our choice. The question however remains, whether we need a property weaker that equimorphism. To illustrate the need, let us consider the drag $D = f(x, x, y, a)$ and the set of wires $W = \{x_1 \rightsquigarrow y, x_2 \rightsquigarrow a, y \rightsquigarrow a\}$. Obviously, $y$ and $a$ do not generate equimorphic drags in $D$, but they do in $D_W$. This tells us that the condition should be checked on the result of wiring $W$ in $D$. We now give the formal definition of a coherent set of wires:

**Definition 6.17 (Coherence).** Let $D$ be a drag and $W$ a well-behaved set of wires of $D$. We say that $W$ is *coherent* (*strongly coherent*, respectively) if it satisfies the two following properties:
(1) Fullness: All sprouts with the same label are the origin of a wire as soon as one is.

(2) Equimorphism: For any two wires $s: x \rightsquigarrow r$ and $s': x \rightsquigarrow r'$ of $W$, $W_0(r)$ and $W_0(r')$ ($r$ and $r'$, respectively) generate equimorphic subdrags of $D_W$ (of $D$, respectively).

Note that forced sharing is a simple, particular case of strong coherence.

Like for the sum operation, wiring relates to the existence of certain morphisms between the wired drag and the original drag that will play a key rôle when it comes to rewriting drags.

**Lemma 6.18.** Let $D$ be a drag having no isolated sprout and $W$ a well-behaved, coherent set of wires of $D$. Then the natural injection from $D$ to $D_W$ defines a monomorphism.

*Proof.* The natural injection $\iota$ from $D$ to $D_W$ is a map $\iota$ that is the identity on the internal vertices of $D$, hence preserves their labels, is injective and indegree preserving by Lemma 6.16 (2), and maps every sprout to its resolution;

Since every vertex of $D_W$ is a vertex of $D$, the set of entering edges is empty. Edges of $D$ of the form $u \to^i s_i$, where $s_i$ is a sprout such that $v' = o(s_i)$, create the edge $o(u) \to^i v'$ of $D_W$. This edge takes the place of a root at $v$ in $D$ if the inverse image of $\iota$ contains an internal vertex or is a sprout $s = o(s)$ shared between $D$ and $D_W$, a root that has therefore disappeared in $D_W$, hence ensuring root preservation. The case where $v'$ is a sprout whose inverse image is a set of sprouts all different from $s$ is simply impossible here since a resolution vertex must be a vertex of $D$. We are left with showing that $\iota$ preserves equimorphic subdrags of $D_W$, which follows from coherence of $W$. $\square$

Coherence can actually be checked without requiring the full computation of $D_W$: any property implying coherence and preserved by wiring would do. This is of course the case of forced sharing, but we can do better.

**Lemma 6.19.** Given a drag $D$, a well-behaved set of wires $W$ of $D$ is coherent iff $W = W' \cup W''$ for some coherent $W'$ and strongly coherent $W''$.

In words, coherence is achieved in the drag resulting from the whole computation as soon as, for every variable $x$, the various wires $s: x \rightsquigarrow r$ generate equimorphic subdrags in the drag computed so far. Note that only nonlinear variables of $D$ need be checked for strong coherence.

*Proof.* The only-if direction follows directly from the definition of coherence by taking $W'' = \emptyset$. The converse is by induction on the size of $W''$, the base case being obtained for $W'' = \emptyset$, which yields coherence of $W = W'$ by assumption.

If $W''$ is non-empty, let $x$ be a variable maximal in $>W''$ and $W'' = W^x \cup W'''$, where $W^x = \{s_i : x \rightsquigarrow r_i\}$ is the set of wires in $W''$ whose origins are labeled $x$. The origins of wires in $W''$ are therefore labeled by variables other than $x$. We will first show that (i) $W' \cup W^x$ is coherent, then that (ii) $W''$ is strongly coherent with respect to $D_{W' \cup W^x}$, before concluding that $W$ is coherent via the induction hypothesis.

(i) Since $x$ is maximal, the subdrags generated by the $r_i$'s are identical in $D_{W'}$ and $(D_{W'})_{W^x}$, establishing property (i).

(ii) Since replacing sprouts labeled $x$ in equimorphic subdrags of $D_{W'}$ by equimorphic subdrags of $D_{W'}$ yields equimorphic subdrags of $(D_{W'})_{W^x}$, property (ii) follows. $\square$
**6.5. Product.** While wiring operates on a single drag, product operates on a pair of drags via a connecting device we call a *switchboard*:

**Definition 6.20 (Switchboard).** Given two disjoint drags $D, D'$, a *switchboard* $\xi$ for $D, D'$ is a pair of partial functions $\langle \xi_D : S(D) \to \mathcal{R}(D'), \xi_{D'} : S(D') \to \mathcal{R}(D) \rangle$, called *switchboard components*, such that $\xi_D \cup \xi_{D'}$ is a coherent well-behaved set of wires for $D \oplus D'$. We also say that $\langle D', \xi \rangle$ is an *extension* of $D$ and $D'$ its *context extension*. Switchboard $\xi$ is *one-way* if either one of $\xi_D$ and $\xi_{D'}$ has an empty domain.

Drags $D$ and $D'$ being disjoint, $\xi_D \cup \xi_{D'}$ is well defined. Therefore, $\xi$ can be identified with $\xi_D \cup \xi_{D'}$. Note further that $\xi_D$ and $\xi_{D'}$ need not be true injective functions as in [DJ19], where roots were lists with repetitions: Injectivity has been adapted to multisets of roots in our definition of a well-behaved set of wires.

Composition can now be defined as a wiring operation on $D \oplus D'$:

**Definition 6.21 (Composition).** Let $D = \langle V, R, L, X, S \rangle$ and $D' = \langle V', R', L', X', S' \rangle$ be disjoint drags, and $\xi$ a switchboard for $D, D'$. Their *cyclic composition* or *product* is the drag $D \otimes_{\xi} D' = (D \oplus D')_{\xi}$.

**Example 6.22.** In Example 6.14, the first drag is the union of two drags that share no vertices, and the set of wires is just their switchboard. The result is therefore the composition of these two drags with respect to that switchboard. $\square$

Lemma 6.16(1) applies to composition: The total number of edges of $D \otimes_{\xi} D'$ is the sum of the number of edges of $D$ and $D'$, a property already noted in [DJ19]. The indegree is preserved at all vertices of $D \otimes_{\xi} D'$ since indegrees are preserved by the sum of disjoint drags and by wiring. Finally, the injection of $D$ into $D \otimes_{\xi} D'$ is a monomorphism by Lemmas 6.4(2) and 6.18(2).

When restricted to one-way switchboards, cyclic composition is indeed a substitution, and is dubbed “sequential” in [Gad07] and one-way in [DJ19]. Many other names coexist that target other classes of graphs and particular cases of composition.

A direct definition of a switchboard and of composition of two disjoint drags connected by a switchboard was given in [DJ19]. Our definition here assumes (a) that roots are multisets, instead of the lists there, (b) that resolution vertices have enough roots for transferring the edges of its corresponding origins, instead of edges and roots there, and (c) that coherence is ensured via equimorphism instead of sharing. These two models therefore have different behaviors.

Apart from these differences, both definitions are similar: our goal now is to give a definition of composition via wiring in the style of the direct definition used in [DJ19]. In the context of composition of two drags $D, D'$ with respect to switchboard $\xi$, we define:

**Definition 6.23 (Resolution).** Let $D = \langle V, R, L, X, S \rangle$ and $D' = \langle V', R', L', X', S' \rangle$ be disjoint drags, and $\xi$ a switchboard for $D, D'$. The *resolution* of a sprout $s \in S \cup S'$ is the vertex $\xi^!(s) = \xi_0(s)$, viewing the switchboard $\xi$ as the set of wires $W$ in Definition 6.13.

The direct definition of composition has now become a simple property of the wiring definition:

**Lemma 6.24 (Composition).** Let $D = \langle V, R, L, X, S \rangle$ and $D' = \langle V', R', L', X', S' \rangle$ be compatible drags, and $\xi$ be a switchboard for $D, D'$. Then $D \otimes_{\xi} D' = \langle V'', R'', L'', X'', S'' \rangle$, where
$$ (1) \ V'' = (V \cup V') \setminus \text{Dom}(\xi); $$
$$ (2) S'' = (S \cup S') \setminus \mathrm{Dom}(\xi); $$

$$ (3) R''(v) = \begin{cases} R(v) - \sum_{\xi!(w)=v \land w \neq v} \mathrm{pred}(w, D) & \text{if } v \in R \setminus \mathrm{Dom}(\xi) \\ R'(v) - \sum_{\xi!(w)=v \land w \neq v} \mathrm{pred}(w, D') & \text{if } v \in R' \setminus \mathrm{Dom}(\xi); \end{cases} $$

$$ (4) L''(v) = \begin{cases} L(v) & \text{if } v \in V \cap V'' \\ L'(v) & \text{if } v \in V' \cap V''; \end{cases} $$

$$ (5) X''(v) = \begin{cases} \xi'(X(v)) & \text{if } v \in V \setminus S \\ \xi'(X'(v)) & \text{if } v \in V' \setminus S'. \end{cases} $$

The calculation of the multiset of roots of the composition is based on the preservation of indegrees by wiring, making it very simple: Edges accumulate along the computation until the very end, at which point they must be compensated for by the roots of the resolution.

*Proof.* By Definition 6.21, $D \otimes_{\xi} D' = (D \oplus D')_{\xi}$. We therefore show that $(D \oplus D')_{\xi}$ is the drag obtained from $D \oplus D'$ by (i) removing from the set of vertices all sprouts in $\mathrm{Dom}(\xi)$, (ii) redirecting all edges ending up in a removed sprout to its associated resolution, and (iii) keeping the indegree unchanged for all vertices in $(V \cup V') \setminus \mathrm{Dom}(\xi)$, which determines their number of roots as stated. The proof is by induction on the size of $\xi$ considered as a set of wires. There are two cases:

- In the empty case, $D \otimes_{\emptyset} D' = D \oplus D'$. Properties (i), (ii), and (iii) hold trivially.

- Otherwise, by Lemma 6.15, we can choose any wire $s \leadsto r$ such that $\xi = W \cup s \leadsto r$, where $s$ is maximal in $\xi$; hence $D \otimes_{\xi} D' = ((D \oplus D')_{s \leadsto r})_W$. We then conclude by the induction hypothesis, since $W$ has one wire fewer than does $\xi$, that $D \otimes_{\xi} D'$ is obtained from $(D \oplus D')_{s \leadsto r}$ as claimed. Since $s$ is maximal, it follows from the definitions of resolutions $\xi_0(x)$ and $\xi^1(x)$ that $(D \oplus D')_{\xi}$ is obtained from $D \oplus D'$ as claimed. $\square$

Not all vertices of the composition $D \otimes_{\xi} D'$ may be reached via $\xi$ from the sprouts of one of them. We denote by $\xi(D)$ the subdrag of $D'$ generated by the vertices in $\xi_D(\mathrm{Dom}(\xi_D))$, which contains all vertices of $D'$ reached from sprouts of $D$.

There are important particular cases of switchboards that impose additional, hence stronger, coherence conditions:

* Equality switchboard: $\forall s \neq t \in S \cup S'$ such that $L(s) = L(t)$, we have $\xi(s) = \xi(t)$.

* Inequality switchboard: $\forall s \neq t \in S \cup S'$ such that $L(s) = L(t)$, we have $(D \oplus D')|_{\xi(s)}$ and $(D \oplus D')|_{\xi(t)}$ have no vertex in common.

Composition is said to *force sharing* if $\xi$ is a switchboard with equality, and to *force cloning* if $\xi$ is a switchboard with inequality. Term rewriting is based on cloning switchboards while dag rewriting is based on equality switchboards. Our notion of composition can potentially do both, and can also achieve partial sharing by having $(D \oplus D')|_{\xi(s)}$ and $(D \oplus D')|_{\xi(t)}$ sharing subdrags, in particular sprouts, when possible. These question will be studied in more detail in Section 11.

**Notations:** Given two drags $D$ and $D'$ and a switchboard $\xi = \{s_i \leadsto r_i\}_i$ for $(D, D')$, we will sometimes need to restrict the switchboard $\xi$ to some subsets of vertices $V$ of $\mathcal{V}(D)$ and $V'$ of $\mathcal{V}(D')$. We will therefore denote by $\xi_{V \to V'}$ the restriction of switchboard $\xi$ to the set of wires $\{s_i \leadsto r_i : s_i \in V, r_i \in V'\}_i$. We will use $\xi_{V, V'}$ for the switchboard $\xi_{V \to V'} \cup \xi_{V' \to V}$, $\xi_{V \to}$ for the switchboard $\xi_{V \to \mathcal{V}(D')}$, and $\xi_{V' \to}$ for the switchboard $\xi_{\mathcal{V}(D) \to V'}$.
## 7. DECOMPOSITION OF DRAGS

We now investigate to what extent a drag can be expressed in terms of simpler drags by means of sum and product so as to obtain a *drag expression*:

**Definition 7.1 (Drag expression).** By a *drag expression*, we mean any expression built from a given set of *drag components* {$D_i$}$_i$ such that $D_i$ and $D_j$ share no vertex nor variable if $i \neq j$, by means of sum and product of drags. Drags occurring in a drag expression are its *drag components*. A drag $D$ is a *trivial* drag expression whose drag $D$ is its only drag component.

Note that product alone would suffice to build drag expressions, writing a sum $D \oplus D'$ as the product $D \otimes_D D'$.

An initial, straightforward answer is that we can decompose a drag according to some subset of its internal vertices by using the corresponding subdrag and associated context:

**Lemma 7.2 (Reconstruction).** Given a drag $D$ and a subset $W$ of its vertices, then $D = D|_W \otimes_{\xi} D|_W$ for some *switchboard* $\xi$.

*Proof.* Using the notations of Definition 3.1, it suffices to define $\xi$, which maps every new sprout $s_v$ of the restriction (of the context, respectively) to the vertex $v$ of the context (of the restriction, respectively). The equality claim then follows easily using preservation of indegrees by wiring. □

We will indeed use the restriction of $D$ to some carefully-chosen single internal vertex, give a specific definition for that case, and treat some special cases separately.

First, we need to define what are “atomic” drags, the kind we like to have in a full decomposition, and the non-atomic ones that we want to eliminate:

**Definition 7.3 (Connected drag).** (1) A *connected* drag is any drag $\langle V, R, L, X, S \rangle$ whose set of vertices is generated by successor and equal labeling of sprouts, that is, any subset $W$ of $V$ closed under these two operations must be $V$ itself:

$$ \forall W \subseteq V (\forall u \forall v \in V (uXv : u \in W \text{ iff } v \in W) \text{ and } \forall s : x \forall t : x \in V (s \in W \text{ iff } t \in W)) \Rightarrow W = V $$

(2) A *flat* drag is a connected drag with no non-trivial path between internal vertices.

(3) An *atomic vertex* is a drag with only a single internal vertex and any number of roots and different sprouts as successors, all with different labels.

(4) A nonempty set of pairwise distinct sprouts is *atomic* if they all share the same variable, each with any number of roots.

(5) An *atomic drag* is an atomic vertex or an atomic set of sprouts.

For example, the drag with two internal vertices sharing one sprout is flat, while the drag made of a single loop on an internal vertex is not. Note also that the drag made of two drags $f(s:x)$ and $g(t:x)$ is connected by our definition, as if $s$ and $t$ where the same shared sprout.

A major property of non-flat connected drags is that they all have non-necessarily distinct internal vertices $u, v$ such that $u$ is a predecessor of $v$.

Atomic drags are of course flat, but there are also flat non-atomic drags. On the other hand, non-connected drags can always be written as a sum of connected drags. We therefore consider the decomposition of non-flat connected drags first, before addressing the case of flat non-atomic connected drags.
In what follows, we give a sequence of four transformation rules in the form of as many lemmas. These transformations take as input a drag expression $E$ containing a drag component $D$ that is not yet atomic, but instead: (i) comprises pairwise distinct connected components; or (ii) is a non-flat connected component with an edge $u \to v$ between two distinct internal vertices; or (iii) is a non-flat connected component with a loop $u \to u$ on some internal vertex $u$; or else (v) is a flat connected component with sprouts $s_i : x$ that are either shared or sharing the variable label $x$, or both. Clearly, any non-atomic drag belongs to one of these four categories. Therefore, applying these transformations repeatedly to a not-yet atomic drag component $D$ of $E$ will eventually transform $E$ into a drag expression $E'$ of whose components are atomic drags. This is so because the drag expressions $E'$ obtained from $E$ are simpler than $E$, in some well-founded order, hence implying that any sequence of transformation is finite.

Before specifying the transformation rules, we define the order used to compare drag expressions:

**Definition 7.4.** To a given drag $D$, we associate the triple $(\#I, In, M)$, where

(1) $\#I$ is the number of its internal vertices plus the edges between them;

(2) $In$ is the multiset of its sprouts' indegrees;

(3) $M$ is the multiset counting, for each variable $x \in Var(D)$, the number of its sprouts that are labeled $x$.

Denoting by $>_{\mathbb{N}}$ the usual order on natural numbers, triples—hence drags—are compared in the well-founded order $\gg = (>_{\mathbb{N}}, >_{\mathbb{N}}^{mul}, >_{\mathbb{N}}^{mul})^{lex}$, where $lex$ and $mul$ denote lexicographic and multiset extensions of an order, respectively. Drag expressions, interpreted as the multiset of interpretations of their drag components, are compared in the well-founded order $\gg^{mul}$.

**Lemma 7.5.** Let $D$ be a drag made of pairwise distinct connected drags $D_1, \dots, D_n$, with $n > 1$. Then, $D = D_1 \oplus \dots \oplus D_n$ is a drag expression such that $\forall i : D \gg D_i$.

*Proof.* The only difficulty is the ordering statement. If there are two or more $D_i$'s with internal vertices, the result is clear. If all $D_i$'s are made of sprouts, their first component is 0, as for $D$, but the second has fewer 0's than in $D$, hence decreases strictly. If, say, $D_1$ has at least one internal vertex but all other $D_i$'s do not, then $D$ has strictly more internal vertices than the $D_i$'s, while $D_1$ has the same number of them as does $D$. But its multiset of sprout indegrees must have decreased strictly. $\square$

**Lemma 7.6 (Decomposition).** Given a non-flat connected drag $D = (V, R, L, X, S)$, let $v$ be an internal vertex of $D$ of indegree $p$, labeled $f$ of arity $n$, having at least one predecessor $u \neq v$, and whose successors in $D$ are the vertices $v_1, \dots, v_n$. Then—denoting $v$ by $f$:

$$D = D_f \otimes_{\xi} D' \text{ with } \xi = \{s \rightsquigarrow v, s_1 \rightsquigarrow w_1, \dots, s_n \rightsquigarrow w_n\}$$

is a drag expression such that $D \gg D_f$ and $D \gg D'$, where:

(1) $D_f = f^{[p]}(s_1 : x_1, \dots, s_n : x_n)$;

(2) $D' = \langle V', R', L', X', S' \rangle$;

(3) $V' = (V \setminus v) \cup s$, where $s$ is a fresh sprout;

(4) $\forall u \in V \setminus \{v \cup \{v_i\}\} : R'(u) = R(u); \forall u \in \{v_i\}_i : R'(u) = R(u) + 1; R'(s) = 0$;

(5) $\forall u \in V \setminus v : L'(u) = L(u); L'(s) = x$, where $x$ is a fresh variable;

(6) $\forall u, w \in V \setminus s : uX'w \text{ iff } uXw; \forall u \in V \setminus s : uX's \text{ iff } uXv$;

(7) $S' = S \cup s$;

(8) $w_i = s$ if $v_i = v$, and otherwise it is $v_i$.
**Proof.** Note that $D$ is a non-flat connected drag, since $u \to v$. The switchboard is designed so that it is trivially coherent and well-behaved, and $D$ is reconstructed from two drag components sharing no vertex or variable. We do not and need not assert that $D'$ itself is a connected drag; it may not be if the subdrag generated by some $v_i$ has no shared vertex with its associated context drag.

The equality claim follows from preservation of indegrees by composition.

Drag $D'$ is smaller than $D$ since an internal vertex has been removed, and the edges between the remaining internal vertices are those of $D$.

For the last claim, notice that the drag $f^{[p]}(s_1 : x_1, \dots, s_n : x_n)$ has a single internal vertex $v$ and no edge $v \to v$. $\square$

**Example 7.7.** Consider a drag $D$, reduced to two internal vertices labeled $g$ and $a$, of arities 1 and 0, respectively, plus a single edge $g \to a$. We get $D = a^{[1]} \otimes_{s \to a} g(s^{[0]})$. $\square$

**Lemma 7.8 (Loop decomposition).** Let $D$ be a drag with an internal vertex $v$ of indegree $p$, labeled $f$ of arity $n$, whose successors in $D$ are the vertices $v_1, \dots, v_n$, with $v_i = v$ for some $i$. Then,

$$D = D' \otimes_{\xi} t^{[1]} : y \text{ with } \xi = \{s \rightsquigarrow t, t \rightsquigarrow v\}$$

is a drag expression such that $D \gg D'$ and $D \gg t^{[1]}$, where:

(1) $D' = \langle V', R', L', X', S' \rangle$;

(2) $V' = V \cup s$, where $s$ is a fresh sprout;

(3) $\forall u \in V \setminus v : R'(u) = R(u); R'(v) = R(v) + 1; R'(s) = 0$;

(4) $\forall u \in V : L'(u) = L(u); L'(s) = x$, where $x$ is a fresh variable;

(5) $\forall u, w \in V : uX'w \text{ iff } uXw \text{ except for the edge } v \to^i v \text{ of } D \text{ replaced by } v \to^i s \text{ in } D'$;

(6) $S' = S \cup s$.

This lemma allows us to eliminate one loop at a time. When there are several loops on the internal vertex $v$, they have to be eliminated one by one. We could of course give a more general statement eliminating them all at once, at the price of a slightly more complicated statement and proof.

**Proof.** Similar to the proof of Lemma 7.6, except for the ordering statements.

Here $D'$ has the same total number of internal vertices but strictly fewer edges between them since some edge $v \to v$ of $D$ has been replaced by an edge $v \to s$ in $D'$, which does not count because $s$ is a sprout. As for the other drag, it has no internal vertices, while $D$ has at least one. $\square$

**Example 7.9.** Consider a drag $D$ reduced to a single internal vertex $v$ labeled $f$ of arity 1, and a single looping edge $f \to f$. Then, we have $D = f^{[1]}(s : x) \otimes_{s \to t, t \to f} t^{[1]}$. $\square$

We next consider the case of non-atomic connected flat drags. They are made of one or more internal vertices connected via their successor sprouts, some of them being shared, or sharing the same variable label, or both. We will eliminate at once all connections related to a given variable label. If there are several variable labels involved in the connections, they will have to be eliminated one by one.

**Lemma 7.10 (Unsharing decomposition).** Let $D$ be a connected flat drag whose nonempty set $\{s_i : x\}_{i=1}^n$ ($n \ge 1$) of distinct sprouts sharing variable label $x$, having $q_i$ predecessors and indegree $p_i \ge q_i$, respectively, contains at least two sprouts, or one shared sprout, or both. Then

$$D = D' \otimes_{\xi} \left( s_1^{[p_1]} \dots s_n^{[p_n]} \right)$$
is a drag expression such that $D \gg D'$ and $D \gg s_1^{[p_1]} \dots s_n^{[p_n]}$, where:

(1) $D'$ is obtained from $D$ by replacing each vertex $s_i$ by fresh rootless sprouts $t_{i,1} : y_{i,1}, \dots, t_{i,q_i} : y_{i,q_i}$ and every edge $v \to s_i$, if any, by edges $v \to t_{i,j}$, with $1 \le j \le q_i$;

(2) $\xi = \{t_{i,k} \to s_i\}_i$.

Note that the drag $s_1^{[p_1]} \dots s_n^{[p_n]}$, all of whose sprouts share the same variable, is an atomic variable drag that cannot be decomposed any further without violating our notion of drag expression, since all these sprouts share label $x$.

*Proof.* In case $p_i = 0$, the switchboard $\xi$ maps a rootless sprout $t_{i,1}$ to a rootless sprout $s_i$. Since all sprouts labeled $x$, whether shared or nor, are renamed with the appropriate number of fresh sprouts, the resultant product is a drag expression. The equality statement is again a straightforward consequence of indegree preservation.

Finally, $D'$ has the same number of internal vertices as $D$. If $n > 1$, the number of sprouts labeled $x$ decreases strictly while the multiset of sprout indegrees does not increase. Or else $p_1 > 1$ and the multiset of sprouts indegrees decreases strictly. We are left with the case of a flat drag with no internal vertices but several sprouts labeled $x$. In that case, $D$ and $D'$ have the same first two components, but the third decreases strictly. The other ordering statement is straightforward. $\square$

Here are two examples of flat non-atomic drags decomposed into atomic drags:

$$f(s^{[0]} : x, t^{[0]} : x) = f(s'^{[0]} : y_1, t'^{[0]} : y_2) \otimes_{s'^{\leftarrow} s, t'^{\leftarrow} t} (s^{[1]} : x \quad t^{[1]} : x)$$

$$f(s^{[0]} : x, s^{[0]} : x) = f(s' : y_1, t' : y_2) \otimes_{s' \leftarrow s, t' \leftarrow t} s^{[2]}$$

—assuming now that $s^{[0]}$ is shared.

Note the difficulty in representing the drag of the second example faithfully by means of the expression $f(s^{[0]} : x, s^{[0]} : x)$. We have to make explicit that $s^{[0]}$ is shared. On the other hand, our product-based representation is faithful; sharing is attained by calculating the drag expression. Note that this representation avoids the kind of unary binding notation usual in programming languages: The annotated product operation is a binder for its arguments.

The decomposition properties can be used to decompose a given drag $D$ into atomic drags, so as to obtain a drag expression built from atomic drags by means of sum and product. Initially, we are given a drag $D$, considered as a (trivial) drag expression. We get the following:

**Theorem 7.11.** For every drag $D$, there exists a drag expression made of atomic drags whose evaluation yields $D$.

*Proof.* By its definition, the order on drag expressions is monotonic: replacing in $E$ a drag component $D$ by a drag expression $D'$ all of whose components are strictly smaller than $D$ yields a strictly smaller drag expression $E'$.

Since every non-atomic dag is either made of several distinct connected components, or is a non-flat connected component, or is a flat connected component that is not yet atomic, all cases have been taken care of. Therefore, by applying Lemmas 7.5, 7.6, 7.8, and 7.10 for as long as possible—termination being ensured by the well-founded order on drag expressions, we get a drag decomposition into atomic components. $\square$
A drag can therefore be defined by induction from atomic pieces glued together by appropriate compositions, which gives rise to an (non-unique) algebraic notation for drags.

**Example 7.12.** Let $f$ be of arity 2 and $h$ of arity 1. The connected drag $D$ with vertices $f_1, f_2$ labeled $f$, vertices $h_1, h_2, h_3$ labeled $h$, and edges $f_1 \to^1 f_2, f_1 \to^2 h_2, f_2 \to^1 h_1, f_2 \to^2 h_2, h_1 \to^1 h_1, h_2 \to^1 h_3, h_3 \to^1 f_2$ has as its drag expression

$$f_2^{[2]}(x_1, x_2) \otimes_{x_1 \to h_1, x_2 \to h_2, x_3 \to f_2} (f_1(x_3, h_2^{[1]}(h_3(x_3)))) \oplus h_1^{[1]}(\text{SELF})$$

where $x_3$ denotes a shared sprout, obtained by applying successively Lemma 7.6 to the vertex $f_2$ and then Lemma 7.5 to the resultant drag. We continue now with the right-hand side argument of $\otimes$. Applying first Lemma 7.6 at vertex $h_2$, we get:

$$(h_2^{[2]}(x_4) \otimes_{x_4 \to h_3, x_5 \to h_2} (f_1(x_3, x_5) h_3^{[1]}(x_3))) \oplus h_1^{[1]}(\text{SELF})$$

Then applying Lemma 7.10 to the flat sub-expression sharing sprout $s_3$, which is the right-hand side argument of $\otimes$, yields the drag expression:

$$(h_2^{[2]}(x_4) \otimes_{x_4 \to h_3, x_5 \to h_2} ((f_1(x_6, x_5) \otimes_{x_6 \to x_3, x_7 \to x_3} h_3^{[1]}(x_7)))) \oplus h_1^{[1]}(\text{SELF})$$

And now applying Lemma 7.8 to the rightmost subdrag, being a loop, gives

$$(h_2^{[2]}(x_4) \otimes_{x_4 \to h_3, x_5 \to h_2} ((f_1(x_6, x_5) \otimes_{x_6 \to x_3, x_7 \to x_3} h_3^{[1]}(x_7)))) \oplus (h_1^{[2]}(x_6) \otimes_{x_6 \to x_8, x_8 \to h_1} x_8^{[1]})$$

a decomposition with no non-atomic components left. Putting the pieces together, we get the following drag decomposition of the starting drag:

$$f_2^{[2]}(x_1, x_2) \otimes_{x_1 \to h_1, x_2 \to h_2, x_3 \to f_2} (h_2^{[2]}(x_4) \otimes_{x_4 \to h_3, x_5 \to h_2} ((f_1(x_6, x_5) \otimes_{x_6 \to x_3, x_7 \to x_3} h_3^{[1]}(x_7)))) \oplus (h_1^{[2]}(x_6) \otimes_{x_6 \to x_8, x_8 \to h_1} x_8^{[1]})$$

The following decomposition of the same drag

$$f_1(x_1, x_2) \otimes_{x_1 \to f_2, x_2 \to h_2} (f_2^{[2]}(x_3, x_4) \otimes_{x_3 \to h_1, x_4 \to h_2, x_6 \to f_2} (h_2^{[2]}(x_5) \otimes_{x_5 \to h_3} h_3^{[1]}(x_6)) \oplus (h_1^{[1]}(x_7) \otimes_{x_7 \to x_8, x_8 \to h_1} (x_8)^{[1]}))$$

cannot be obtained by using our lemmas, since we are missing an analog of Lemma 7.6 applying to a vertex without ancestors of a non-flat drag. This additional decomposition lemma can be surmised by the reader; it would be needed in case we were interested in all possible decompositions of a given drag. Note that we end up here with a decomposition using again 8 fresh sprouts. This is no surprise: one sprout is needed for each incoming edge in the original drag, plus one for each loop, since a loop decomposition requires two wires. The reader can verify that all switchboards used in these decompositions are well behaved and that the result is indeed the drag $D$ in both cases. $\square$
8. ALGEBRA OF DRAGS

Once equipped with sum and product, drags enjoy a very rich algebraic structure which is
known to be suitable for expressing distributed computations [MM90, MMS97].

**Lemma 8.1.** *Drag sum is associative, commutative, idempotent, and has the empty drag as an identity element.*

Noting that a drag is compatible with itself, all these properties are straightforward.
We proceed with product:

**Lemma 8.2.** *Drag product is associative, commutative, and has an identity element, the empty drag. Other identities are isolated sprouts provided they belong to the domain of the switchboard, and do not belong to its image.*

*Proof.* Commutativity is straightforward here, because of the root structure as a multiset. The empty drag is again an identity for any drag *D*, since ξ must be empty, and therefore *D* ⊗ ∅ = *D* ⊕ ∅ = *D*. Let now *s*^[n] be a drag reduced to a sprout which is not a vertex of *D*, and *s* ↣ *v* be a wire for (*D*, *s*). By assumption, *s* does not belong to the image of ξ_D. Then, a straightforward calculation shows that *D* ⊗_{s<v} *s*^[n] = *D*.

We are left with associativity. Consider the drag (*C* ⊗<sub>ξ</sub> *D*) ⊗<sub>ζ</sub> *E*. We prove first that ξ ∪ ζ is a well-behaved set of wires for *C* ⊕ *D* ⊕ *E*. By the definition of a switchboard, ξ and ζ are well-behaved sets of wires for *C* ⊕ *D* and (*C* ⊗<sub>ξ</sub> *D*) ⊕ *E*, respectively. Since ζ maps remaining sprouts of *C* ⊕ *D* after wiring with ξ to roots of *E*, and sprouts of *E* to remaining roots of *C* ⊕ *D* after wiring with ξ, ξ ⊕ ζ is well-defined and satisfies functionality, coherence and injectivity. It is also well-founded, since chains of sprouts for ξ ∪ ζ are either chains of sprouts for ξ or for ζ which both satisfy well-foundedness.

We construct now two new sets of wires, $\zeta'$ for $D \oplus E$, and $\xi'$ for $C \oplus (D \otimes \zeta' E)$ such that
$\xi' \cup \zeta' = \xi \cup \zeta$, showing that $\xi' \cup \zeta'$ is a well-behaved set of wires for $C \oplus D \oplus E$, which implies
that $\xi'$ and $\zeta'$ are well-behaved sets of wires for $C \oplus (D \otimes \zeta' E)$ and $D \oplus E$, respectively. We
now classify each wire $s \rightsquigarrow r \in \xi \cup \zeta$ as a wire of $\xi'$ or $\zeta'$:

(1) $s \in S(C) : s \rightsquigarrow r \in \xi'$;

(2) $r \in \mathcal{R}(C) : s \rightsquigarrow r \in \xi'$;

(3) $s \in S(D)$ and $r \in \mathcal{R}(E) : s \rightsquigarrow r \in \zeta'$;

(4) $s \in S(E)$ and $r \in \mathcal{R}(D) : s \rightsquigarrow r \in \zeta'$.

The equality between both obtained drags now follows from routine calculations. □

<figure><img src="image_18.png" /></figure>

Finally, we consider the distributivity law, which will be used later when investigating
the categorical structure of drags. Omitting switchboards, this is an identity of the form
*C* ⊗ (*D* ⊕ *E*) = (*C* ⊗ *D*) ⊕ (*C* ⊗ *E*). There are two obstacles: The first is that the sums *D* ⊕ *E*
and (*C* ⊗ *D*) ⊕ (*C* ⊗ *E*) must make sense, which requires that compatibility of drags *D* and
*E* is preserved by their product with *C*. This is not true in general, but will require that
all wires whose source sprout is in *C* satisfy some *safety condition*. The second obstacle is
that wirings between *D* and *E* going through *C* in *C* ⊗ (*D* ⊕ *E*) cannot be reproduced, in
general, in (*C* ⊗ *D*) ⊕ (*C* ⊗ *E*), unless wiring again the result, which is not expected from a
distributivity law whose rôle is to transform a product into a sum. We will therefore need
to strengthen the safety condition for that purpose.

**Definition 8.3.** Let *D*, *E* be compatible drags with shared subdrag *G*, *C* a drag disjoint from *D* ⊕ *E*, ξ a switchboard for (*D* ⊕ *E*, *C*), *H* the subgraph of *C* generated by all vertices
$v \in \mathcal{V}(C)$ such that $s \rightsquigarrow v \in \xi_G$, $C'$ the context drag of $H$ in $C$, and $D'$, $E'$ the context drags of $G$ in $D$, $E$, respectively. We say that switchboard $\xi$ is *safe* if

(1) $\forall t \rightsquigarrow v \in \xi_H : v \in \mathcal{V}(G)$;

(2) $\forall s \rightsquigarrow u \in \xi_D \forall t \rightsquigarrow u \in \xi_E$ such that $s, t \notin G : v \in \mathcal{V}(H)$

(3) $\forall s \rightsquigarrow t, t \rightsquigarrow v \in \xi$ such that $s \in \mathcal{S}(D')(s \in \mathcal{S}(E')$, respectively) : $v \notin \mathcal{V}(E')(v \notin \mathcal{V}(D'))$, respectively).

We can now show distributivity under the safety assumption:

**Lemma 8.4 (Distributivity).** Let $D, E$ be compatible drags with shared subdrag $G$, $C$ a drag disjoint from $D \oplus E$, and $\xi$ a safe switchboard for $(D \oplus E, C)$. Then, drags $D \otimes_{\xi} C$ and $E \otimes_{\xi} C$ are compatible with shared subdrag $G \otimes_{\xi} C$, and

$$ (D \oplus E) \otimes_{\xi} C = (D \otimes_{\xi} C) \oplus (E \otimes_{\xi} C). $$

*Proof.* The definition of $H$ and safety condition (1) ensure that $G \otimes_{\xi} H$ is shared by drags $D \otimes_{\xi} C$ and $E \otimes_{\xi} C$, while safety condition (2) ensures that no other vertex is shared, hence $G \otimes_{\xi} H$ is exactly their shared subgraph, implying compatibility.

Safety condition (3) ensures that no edge is created between $C'$ and $D'$ by the product $(D \oplus E) \otimes_{\xi} C$ unless it is an edge in $G$ created by the product $G \otimes_{\xi} H$. Therefore, all edges of $(D \oplus E) \otimes_{\xi} C$ will be edges of $(D \otimes_{\xi} C) \oplus (E \otimes_{\xi} C)$, the converse being trivial. $\square$

Since $\xi$ must map sprouts of $H$ to vertices of $G$ by condition (1) of Definition 8.3, then condition (3) is trivially true in case $C = H$. This remark will later allow us to use distributivity in order to characterize pushout objects by means of product and sum of drags in the proof of the important Lemma 12.7.

## 9. SHARING EQUIVALENCE

Next, we define and study the equivalence on drags defined by sharing subdrags, which will play an important rôle for defining rewriting. We will share subdrags that are equimorphic up to their roots, which do not play a rôle here.

**Definition 9.1 (Sharing).** A drag is *maximally shared* if no two distinct bare subdrags are equimorphic.

Note that a maximally shared drag must be linear.

First, we define the *maximally shared form* $D \downarrow$ of a drag $D$ by iterating the following sharing transformation as long as necessary:

(1) Assume $E_1, \dots, E_n, F$ are all pairwise distinct maximally shared subdrags of $D$ whose bare versions are equimorphic to $\tilde{F}$, called the *class* of $F$ in $D$, and let $C_F$ be the *context* of $\tilde{F} = E_1 \oplus \dots \oplus E_n \oplus F$. By Lemma 7.2, $D = C_F \otimes_{\xi} \tilde{F}$ for some $\xi$. The class of $F$ is said to be *trivial* if it consists of the single drag $F$ only ($n = 0$), and *nontrivial* otherwise ($n > 0$).

**Claim 9.2.** Given a drag $D$, assume that the bare version of some drag in a class $\overline{E}$ is equimorphic to the bare version of some strict subdrag of a drag in a class $\overline{F}$. Then, all drags in the class $\overline{F}$ contain at least one subdrag belonging to the class $\overline{E}$. This shows that the well-founded subdrag order lifts to classes of drags. As a consequence, some classes are minimal in this order.
<figure><img src="image_19.png" /><figcaption>Figure 5: Maximally shared form of a drag.</figcaption></figure>

(2) Assuming $D$ is not maximally shared, there exists at least one minimal nontrivial class $\overline{F}$ in $D$. Let, therefore, $o_i : E_i \hookrightarrow F$ be the equimorphism from $E_i$ to $F$ and $o = \cup_i o_i$. We define $\xi' = o \circ \xi$ and $D' = C_F \otimes_{\xi'} F$. In words, $D'$ is obtained from $D$ by replacing any edge of $D$ from an internal vertex $u$ of $C$ to a vertex $v$ of some $E_i$ by an edge from $u$ to $o_i(v)$, and transfer any root of a vertex $v$ of some $E_j$ to $o_j(v)$, resulting in the drag $D'$, which contains a unique element of the class of $F$, $F$ itself. Note that this step does not create any new class of drags whose bare versions are equimorphic. The choice of $F$ in its class implies that the maximally shared form of $D$ will be defined up to equimorphism.

**Lemma 9.3.** *The maximally shared form $D\downarrow$ of a drag $D$ exists and is unique up to equimorphism.*

*Proof.* A sharing step strictly decreases the number of nontrivial classes of the drag $D$. It follows that it terminates, and therefore maximally shared forms exist. We prove uniqueness by showing that any two different sharing steps commute, and then conclude by the Diamond Lemma [Hin69].

Let $\overline{G}, \overline{H}$ be two different minimal classes of equimorphic drags of $D$ that can be shared each in turn. By minimality of both classes, we can consider the context $C$ of $\overline{G} \oplus \overline{H}$ such that $D = C \otimes_{\xi} (\overline{G} \oplus \overline{H}) = C \otimes_{\xi} (\overline{G} \otimes_{\emptyset} \overline{H})$. Using associativity and commutativity of product, we get $D = (C \otimes_{\xi_{C,\overline{H}}} \overline{H}) \otimes_{\xi_{C,\overline{G}}} \overline{G} = (C \otimes_{\xi_{C,\overline{G}}} \overline{G}) \otimes_{\xi_{C,\overline{H}}} \overline{H}$, showing that $(C \otimes_{\xi_{C,\overline{H}}} \overline{H})$ and $(C \otimes_{\xi_{C,\overline{G}}} \overline{G})$ are the contexts in $D$ of $\overline{G}$ and $\overline{H}$, respectively. Let now $E = C \otimes_{\xi_{C,\overline{H}}} \overline{H}) \otimes_{\xi_{C,G}} G$ and $F = (C \otimes_{\xi_{C,\overline{G}}} \overline{G}) \otimes_{\xi_{C,H}} H$, obtained from $D$ by sharing classes $\overline{G}$ and $\overline{H}$, respectively. Using associativity and commutativity again, we can now share the classes $\overline{G}$ and $\overline{H}$ in $E$ and $F$, respectively. We get $E' = (C \otimes_{\xi_{E,H}} H) \otimes_{\xi_{C,G}} G$ and $F' = (C \otimes_{\xi_{C,G}} G) \otimes_{\xi_{C,H}} H$. Using associativity and commutativity again, we get $E' = (C \otimes_{\xi} (G \otimes_{\emptyset} H) = F'$. $\square$

**Example 9.4.** Figure 5 shows two examples of drags that have the same maximally shared form. For the left drag, the two subdrags reduced to a vertex labeled $a$ are equimorphic. The maximally shared form is obtained in one step. For the right drag, two steps will be needed, as shown on the figure. $\square$

**Definition 9.5** (Sharing-equivalence). Two drags $D, D'$ are sharing-equivalent, written $D \cong_{sh} D'$, if they have equimorphic maximally shared forms.

Simple consequences are that equimorphic drags are sharing-equivalent; and that drags that are sharing-equivalent have the same sets of variables and multiset of roots, since both are preserved by computing maximally shared forms.
**Lemma 9.6.** *Given a drag D, there exists a morphism $o: D \to D\downarrow$, such that all vertices of D sent to the same vertex by $o$ generate subdrags of D that are sharing-equivalent.*

*Proof.* Straightforward, noticing that each class of equimorphic drags in a drag has a representative (the one chosen by sharing) in normal form. □

We now show that sharing-equivalence is closed by the operations on drags that we have defined. First, obviously,

**Lemma 9.7.** *Sharing-equivalence is closed under parallel composition.*

**Definition 9.8 (Sharing-equivalence of wires).** Let $D, D'$ be two drags that are sharing-equivalent. Two well-behaved set of wires $W = \{s_i \rightsquigarrow r_i\}_i$ of $D$ and $W' = \{s'_j \rightsquigarrow r'_j\}_j$ of $D'$ are sharing-equivalent if

* the sets of variables labeling the sprouts $\{s_i\}_i$ and $\{s'_j\}_j$ are identical;

* for all sprouts $s_i, s'_j$ sharing the same label, $D \downarrow_{r_i}$ and $D' \downarrow_{r'_j}$ are sharing-equivalent.

Two rewriting extensions $(E, \xi)$ of $D$ and $(E', \xi')$ of $D'$ are sharing-equivalent if so are $E$ and $E'$, and $\xi$ and $\xi'$.

The definition of sharing-equivalence for sets of wires makes sense since the same variables label the respective sprouts of sharing-equivalent drags. It makes sense for extensions by Lemma 9.7, since $\xi$ and $\xi'$ are well-behaved sets of wires of $D \oplus E$ and $D' \oplus E'$ by definition. Sharing-equivalence is thus an equivalence on drags, sets of wires, and extensions.

**Lemma 9.9.** *Given two sharing-equivalent well-behaved sets of wires $\xi, \zeta$ of a drag $D$, $D_\xi$ and $D_\zeta$ are sharing-equivalent.*

*Proof.* By induction on the number of wires in $\xi$. If $\xi$ is empty, then $\zeta$ must be empty too since they are sharing-equivalent, and the result holds in that case. Otherwise, neither $\xi$ nor $\zeta$ can be empty. Let $s \rightsquigarrow r \in \xi$ be a maximal wire. By the definition of sharing-equivalence for sets of wires, there must exist a wire $s' \rightsquigarrow r' \in \zeta$ such that $D \downarrow_r$ and $D \downarrow_{r'}$ are sharing-equivalent, implying that neither are sprouts or both are in which case their label is the same. By coherence of a well-behaved set of wires, we can always choose $s = s'$. It follows that $s \rightsquigarrow r'$ must be maximal in $\zeta$. The drags $D_{s \rightsquigarrow r}$ and $D_{s \rightsquigarrow r'}$ are clearly sharing-equivalent. Since $\xi \setminus s \rightsquigarrow r$ and $\zeta \setminus s \rightsquigarrow r'$ are sharing-equivalent, well-behaved sets of wires, we conclude by the induction hypothesis. □

**Lemma 9.10.** *Sharing commutes with wiring: $D_{\xi\downarrow} = (D_{\downarrow\xi})\downarrow$.*

The set of wires $\xi$ for $D\downarrow$ should of course be understood as the restriction of $\xi$ to the sprouts of $D$ which are still vertices of $D\downarrow$.

*Proof.* By induction on the size of $\xi$. If $\xi$ is empty, the result is clear. Otherwise, let $\xi = \zeta \cup s \rightsquigarrow r$, where $s \rightsquigarrow r$ is maximal. By coherence of $\xi$, we can choose $s \rightsquigarrow r$ such that $s$ is still a sprout of $D\downarrow$. By Lemma 9.6, $r$ is mapped to a vertex $o(r)$ of $D$ such that $r$ and $o(r)$ generate sharing-equivalent subdrags. Now, $D_\xi = (D_{s \rightsquigarrow r})_\zeta$, and $D_{\downarrow\xi} = (D_{\downarrow s \rightsquigarrow o(r)})_\zeta$, and by the previous remark, $D_{s \rightsquigarrow r}$ and $D_{\downarrow s \rightsquigarrow r}$ are sharing-equivalent. We then conclude by the induction hypothesis. □

**Lemma 9.11.** *Sharing-equivalence is closed under wiring.*
*Proof.* We are now given two sharing-equivalent drags $D, D'$ and two sharing equivalent, well-behaved sets of wires $\xi, \zeta$ for $D, D'$, respectively. Now,

$$ 
\begin{align*}
D_{\xi} \downarrow &= (D_{\downarrow \xi}) \downarrow && \text{(by Lemma 9.10)} \\
&= (D'_{\downarrow \xi}) \downarrow && \text{(because $D$ and $D'$ are sharing-equivalent)} \\
&= (D'_{\downarrow \zeta}) \downarrow && \text{(by Lemma 9.9)} \\
&= (D'_{\zeta}) \downarrow,
\end{align*}
$$

showing that $D_{\xi}$ and $D'_{\zeta}$ are sharing-equivalent.

<figure><img src="image_20.png" /></figure>

Using now Lemmas 9.7 and 9.11, we get:

**Lemma 9.12.** Given two sharing-equivalent drags $D, D'$, let $\langle E, \xi \rangle$ and $\langle E', \xi' \rangle$ be two sharing equivalent extensions of $D$ and $D'$, respectively. Then, $D \otimes_{\xi} E$ and $D' \otimes_{\xi'} E'$ are sharing-equivalent.

The following important result summarizes the closure properties of sharing-equivalence:

**Theorem 9.13.** *Sharing-equivalence is closed under parallel and cyclic composition.*

## 10. REWRITING

Rewriting is often used as a method to decide congruences, or to describe syntactic transformations, the underlying congruence being implicit. The idea is that a congruence is an equivalence that is closed under composition with respect to extensions. This is the case for drags just like it is for terms, composition taking here the place of both context application and substitution.

As usual, rewriting is a precongruence. Symmetry is eschewed, so as to allow the unidirectional use of rewriting to decide whether two given drags are equivalent in the congruence generated by a given set of drag equations, thereby potentially reducing the nondeterminism involved in proof search.

**10.1. Congruences.** Term congruences are defined as equivalences closed under context application and substitution. Drag congruences should generalize term congruences by being closed under sum and product. The latter will require a precise correspondence between the roots of congruent terms. Besides, they should also allow for sharing, hence contain sharing equivalence.

**Definition 10.1 (Root-map).** Given drags $D, D'$, a *root-map* from $D$ to $D'$ is a multi-injective multi-map $\eta: \mathcal{R}(D) \to \mathcal{R}(D')$.

As noted in Section 2, $\eta$ is multi-equijective from its domain multiset to its image multiset. When needed, root-maps can be written as lists with repetitions $\{u_1 \mapsto v_1, \dots, u_n \mapsto v_n\}$.

**Definition 10.2 (Rewriting extension).** Given a drag $D$ and a linear drag $C$ disjoint from $D$, $\langle C, \xi \rangle$ is a *rewriting extension* of $D$ if $\xi_D$ is total and $\xi_C$ surjective.

Imposing that $\xi_C$ is surjective is not a restriction, since it is always possible to extend $C$ by isolated sprouts mapped by $\xi_C$ to the remaining roots of $D$. Imposing totality is no restriction either since we are indeed interested in congruences on closed drags.
**Definition 10.3 (Compatible extensions).** Given compatible drags $D, D'$, rewriting extensions $(C, \xi)$ of $D$ and $(C', \xi')$ of $D'$ are compatible with root-map $\eta: D \to D'$, if

(1) $C$ and $C'$ are compatible, equimorphic drags: $C \equiv_o C'$;

(2) for all sprouts $t: x$ of $D$ and $t': x$ of $D'$, the subdrags $C|_{\xi(t)}$ and $C'|_{\xi'(t')}$ are equimorphic;

(3) $\forall s \in \mathcal{D}om(\xi_C) : \xi'_C(o(s)) = \eta(\xi_C(s))$.

Note that any two sprouts of $D \oplus D'$ sharing their variable label must be mapped by $\xi_D \cup \xi'_{D'}$ to vertices generating equimorphic subdrags. Totality is the key to ban dangling edges when rewriting. It is also important to notice that $\xi_D$ need not being surjective; hence the context $C$ may contain rooted subdrags needed for $\xi'_{D'}$ that remain useless for $\xi_D$. This is in particular the case if there are more sprouts labeled by a given variable $x$ in $D'$ than in $D$.

**Definition 10.4.** A congruence over the set of drags is an equivalence over compatible drags $U, V$ equipped with a *root-map* $\eta$, written $U \equiv^\eta V$ or simply $U \equiv V$ when the *root-map* is not needed, satisfying the following closure properties:

(1) Under sharing equivalence: Let $U \equiv^\eta V$ and $V \cong_{sh} V'$, that is $V \equiv_o V'$. Then, $U \equiv^{\circ\circ\eta} V'$.

(2) Under sum: Let $U \equiv^\eta V$, $W$ compatible with both $U$ and $V$, and $\mu$ a *root-map* from $W$ to $W$ whose domain and image are disjoint from $\mathcal{R}(U, V)$, then $U \oplus W \equiv^{\eta \cup \mu} V \oplus W$.

(3) Under product: Let $U \equiv^\eta V$, $(C, \xi)$ and $(C', \xi')$ extensions of $U, V$, respectively, compatible with the *root-map* $\eta$, and $\mu$ a restriction of the equimorphism from $C$ to $C'$ whose domain and image are disjoint from $\mathcal{Ima}(\xi_U)$ and $\mathcal{Ima}(\xi'_{U'})$, respectively. Then $U \otimes_\xi C \equiv^\mu V \otimes_{\xi'} C'$.

Note that we use the same symbol $\equiv$ for both equimorphisms and congruences, the former with a lower index and the latter with an upper index.

By wiring different sprouts, possibly but not necessarily labeled the same, to the same vertex, case (3) incorporates some limited amount of sharing. Only limited, since internal vertices generating equimorphic subgraph cannot become shared when computing products.

**Example 10.5.** Let drags $D = g^{[1]}(f_1^{[1]}(x_1, x_2)) \equiv_{\{g \to k, f_1 \mapsto f_2\}} k^{[1]}(f_2^{[1]}(x_3, x_3)) = D'$, and equimorphic context drags $C = h_1^{[2]}(z_1) \oplus z_1^{[1]}$ and $C' = h_2^{[2]}(z_2) \oplus z_2^{[1]}$, where $x_1, x_2, x_3$ are different vertices labeled $x$, while $z_1, z_2$ are labeled $z$, and $z_1', z_2'$ are labeled $z'$. Then,

$$[y = f(y', y'), y' = h(y)] g(y) = g^{[1]}(f_1^{[1]}(x_1, x_2)) \otimes_{\{x_1 \to h_1, x_2 \to h_1, z_1 \to f_1, z_2 \to k\}} C \\ \equiv \emptyset$$

$$[y = f(y', y'), y' = h(y)] k(y) = k^{[1]}(f_2^{[1]}(x_3, x_3)) \otimes_{\{x_3 \to h_2, x_3 \to f_2, z_4 \to g\}} C'$$

Note that $x_1$ and $x_2$ are both mapped to $h_1$, while $x_3$ is mapped to $h_2$, $h_1$ and $h_2$ generating equimorphic subdrags of the result. Note also that $z_1$ is mapped to $f_1$ while $z_2$ is mapped to $f_2$ as dictated by the *root-map*. Similarly, $z_1'$ and $z_2'$ are mapped to $g$ and $k$, respectively.

We are of course interested in congruences generated by a set of equations:

**Definition 10.6.** An equation is a pair of compatible drags $U, V$ together with a *root-map* $\eta$, denoted $U \equiv^\eta V$. The equality over drags generated by a set $\mathcal{E}$ of equations, denoted $\equiv_\mathcal{E}$, is the least congruence that contains all pairs in $\mathcal{E}$.

**Example 10.7.** Assuming $f$ is binary, we take here for $\mathcal{E}$ the associativity equation with its trivial root-map: $f_1 \mapsto f_3 : f_1^{[1]}(f_2(x, y), z) = f_3^{[1]}(x, f_4(y, z))$. Then, closure under
product with the compatible extensions $\langle x'^{[1]} \oplus b^{[1]} \oplus c^{[1]}, \{x \rightsquigarrow x', y \rightsquigarrow b, z \rightsquigarrow c, x' \rightsquigarrow f_1\} \rangle$
and $\langle x''^{[1]} \oplus b^{[1]} \oplus c^{[1]}, \{x \rightsquigarrow x'', y \rightsquigarrow b, z \rightsquigarrow c, x'' \rightsquigarrow f_3\} \rangle$ renders equal the two ground drags
$[z = f(f(z, b), c)]z$ and $[z' = f(z', f(b, c))]z'$.

**10.2. Rewrite rules.** A rewrite rule serves to replace some drag pattern $L$ by some other drag pattern $R$ in a given drag $D$ that contains $L$ in a context defined by an extension $\langle E, \xi \rangle$ of $L$. That is, $D = E \otimes_{\xi} L$.

First, it is important to ensure that all roots and sprouts of $L$ disappear in this com-
position, yielding the previously encountered notion of a rewriting extension. Next, it is
equally important to ensure that replacing $L$ by $R$ is possible; this is what root-maps are for.
Finally, the extensions used for the left-hand and right-hand sides of a rewrite rule must
be compatible, so that sprouts with identical labels are mapped to vertices that generate
equimorphic subdrags.

**Definition 10.8 (Patterns).** A drag all of whose vertices are accessible is called a *right-pattern*. It is called a *left-pattern*, or simply *pattern*, if also all of its sprouts have predecessors.

**Definition 10.9 (Rewrite rules).** A *drag rewrite rule* is a triple written $\eta : L \to R$ (alternatively, $L \to_{\eta} R$) made of two compatible drags $L$ and $R$, such that $L$ is a pattern, $R$ is a right pattern, and $\eta$ is a multi-equijjective root-map from $\mathcal{R}(L)$ to $\mathcal{R}(R)$ (hence $|\mathcal{R}(R)| = |\mathcal{R}(L)|$).

A rule is *stringent* if $Var(L) \subseteq Var(R)$.

A renaming of a rule $\eta : L \to R$ is a rule $\eta' : L' \to R'$ such that (i) $L' \oplus R'$ is a renaming of $L \oplus R$, that is, $L \oplus R \cong_{\sigma_o} L' \oplus R'$, and (ii) $\forall r \in \mathcal{R}(L) : \eta'(\sigma(r)) = \sigma(\eta(r))$.

Since $L$ and $R$ are compatible drags, their sum $L \oplus R$ is defined and can indeed be
seen as the rule whose multiset of roots is partitioned into a left multiset $\mathcal{R}(L)$ and a right
multiset $\mathcal{R}(R)$, so that $\eta$ is a multi-equijjective map from the first to the second.

The case of term rewriting rules is then quite simple: since $L$ and $R$ have a single root
each, there is a unique possible map $\eta$. In [DJ19], $L$ and $R$ have ordered lists of roots of
the same length, making $\eta$ unique again. In both these cases, there is no need for $\eta$ to be
explicit. Having multisets of roots forces us to specify $\eta$.

**10.3. Rewriting relations.** We first consider “relational” rewriting. Given drags $D, D'$,
rewriting $D$ to $D'$ using rule $\eta : L \to R$ sharing no variable with $D, D'$ involves the following
steps:

(1) *Match*: Find a variable-preserving renaming $\eta' : L' \to R$ of $\eta : L \to R$, and rewriting extensions $\langle E, \xi \rangle$ of $L'$ and $\langle E', \xi' \rangle$ of $R'$, such that $D = E \otimes_{\xi} L'$ and $D' = E' \otimes_{\xi'} R'$.

(2) *Verify*: Establish that these two extensions are *compatible*.

In the following, we will usually confuse the rule $\eta : L \to R$ with its variable preserving renaming $\eta' : L' \to R'$.

The rewriting switchboards map sprouts of $E, E'$ to roots of $L', R'$, respectively, and
these mappings must fit with $\eta'$, hence condition (2). Note that taking $E$ and $E'$ isomorphic
would suffice: imposing that their sprouts are labeled by the same variables is possible
because we distinguish both switchboards $\xi$ for the left-hand side and $\xi'$ for the right-hand
side. Condition (3) expresses the property that the restrictions of $\xi$ and $\xi'$, to the sprouts
<figure><img src="image_21.png" /><figcaption>Figure 6: Compatible rewrite extension of a rewrite rule.</figcaption></figure>

of $L'$ and $R'$, respectively, could be made into a single well-behaved set of wires, which will
become important later.

One may worry about the complexity of deciding a rewrite step. The matching step 1 in
the “list of roots” model has a worst case complexity which is bounded by the product of the
sizes of $D \oplus D'$ and $L' \oplus R'$ [JO23]. It should not be very different for the “multiset of roots”
model since the main drag invariant checked for that purpose is indegree preservation, for
which only the number of roots matters. Checking equimorphism at step (3) has indeed a
worst case complexity bounded by the sum of the sizes of $D$ and $D'$, since the two vertices
$\xi(t)$ and $\xi'(t')$ are given, both drags are directed, and the successors of both vertices are
lists of the same length. So, the overall complexity is determined by that of the matching
process, which has a quadratic upper bound in the “list model”.

We can now define *relational rewriting*:

**Definition 10.10 (Rewriting).** A drag *D* is in a *rewriting relation* with drag *D'*—using the (renamed) rewrite rule $\eta: L \to R$ sharing no variable with *D*, if there exist two compatible rewriting extensions $\langle E, \xi \rangle$ of *L* and $\langle E', \xi' \rangle$ of *R* such that $D = E \otimes_{\xi} L$ and $D' = E' \otimes_{\xi'} R$.

Since the extension drags *E* and *E'* must be equimorphic, it is tempting to take them to
be identical. This is of course impossible in case *D* and *D'* do not share vertices, in which
case only the sprouts of *E* and *E'* can be shared, which simplifies condition (2) already
to $\xi'(s) = \eta(\xi(s))$. Usually, however, only *D* is given, and *D'* is defined by the rewriting
process, in which case the same extension *E* can do for both, and rewriting can be defined
as a computation mechanism.
**Definition 10.11** (Strong compatibility). Given a rule $\eta : L \to R$, two rewriting extensions $\langle E, \xi \rangle$ and $\langle E', \xi' \rangle$ of $L$ and $R$, respectively, are strongly compatible if

(1) $E = E'$;

(2) for all sprout $s$ of $E$, $\xi'(s) = \eta(\xi(s))$;

(3) for all sprouts $s:x$ of $L$ and $t:x$ of $R$, the subdrags $E|_{\xi(s)}$ and $E|_{\xi'(t)}$ are equimorphic.

Using the same drag $E$ for both extensions does not mean that all of $E$ is used for $L$ and all of $E$ is used for $E'$. It may be that there are more sprouts labeled $x$ (for some $x$) in $R$ than in $L$; mapping these sprouts to different subdrags of $E$ requires more of them for $R$ than for $L$. So, the same rewrite could be achieved with two more economic drags $E$ and $E'$, that would not be equimorphic anymore, but which enjoy a more complex relationship.

**Definition 10.12** (Functional rewriting). A drag $D$ rewrites to a drag $D'$ using the strin-
gent rewrite rule $\eta : L \to R$ sharing no variable with $D$, if there exist two strongly compatible
rewriting extensions $\langle E, \xi \rangle$ of $L$ and $\langle E', \xi' \rangle$ of $R$ such that $D = E \otimes_{\xi} L$ and $D' = E' \otimes_{\xi'} R$.

We say that drag $D$ rewrites to drag $D'$ with rewrite system $\mathcal{R}$, all of whose rules are
stringent, denoted $D \xrightarrow{\mathcal{R}} D'$, if $D$ rewrites to $D'$ using some rule $\eta \in \mathcal{R}$.

**Example 10.13.** Consider the two rewriting examples of Figure 7. The input drags to be rewritten and the resulting output drags are in black. The rule $h(x,x) \to k(x,x)$ is in red. Its various sprouts, all labeled $x$, are not shared; hence, we can use our naming conventions. The extension drags are in blue, and the switchboards in black.

In the upper example, the right-hand side switchboard $\xi'$ coincides roughly with the
left-hand side switchboard $\xi$. Note that the left- and right-hand sides of the rule have a
single root, the vertices $h$ and $k$, respectively. Note also that these switchboards do satisfy
strong compatibility.

In the lower example, the switchboard $\xi'$ differs from $\xi$ in that both left-hand side $x$'s
are mapped to $a_2$ (there is no other choice) while the two right-hand sides $x$'s are mapped to
$a_1$ and $a_2$, respectively, which yields a quite different result. Note that $a_1$ and $a_2$ generate
equimorphic subdrags reduced to a single vertex labeled $a$ having two roots. Here, the
right-hand side switchboard does not force sharing, that's why we can map $x_3$ and $x_4$ to
different vertices.

Using the rule $h(x,x) \to k(x,x)$ in which $x$ is shared in the left-hand side would yield
exactly the same result with the same switchboards. In this example, the switchboard forces
sharing on the left-hand side, even if the rule does not. $\square$

So, the determination of a switchboard obeys precise rules, but leaves also some room
for choosing the right-hand side switchboard among sometimes several possibilities. As a
consequence, the result of a rewrite step is not entirely determined by matching, as it seems
to be the case for terms. The very same definition is indeed used for rewriting a term with a
term rewrite rule $L \to R$: the two contexts $E$ and $E'$ are identical, condition (2) is implicit,
and condition (3) is usually ensured by taking for each occurrence of $x$ in $R$ a disjoint copy
of $E|_{\xi(s)}$ for $E|_{\xi'(t)}$, at least when $R$ is non-linear (otherwise it is possible to use $E|_{\xi(s)}$ for
$E|_{\xi'(t)}$). So, uniqueness of the result of a term rewriting step is not true in general, the
result being unique up to equimorphism only. This is hidden by the assumption that terms
are defined up to equimorphism, an assumption which pops up when terms are considered
as particular drags.

In the general case of drag rewriting, however, the two resulting drags obtained in
Example 10.13 are not even equimorphic: they are sharing-equivalent.
<figure><img src="image_22.png" /><figcaption>Figure 7: Rewriting example.</figcaption></figure>

Given now a rule $L \to R$ such that $\langle E, \xi \rangle$ and $\langle E, \zeta \rangle$ are two equimorphic extensions for $R$, the result of rewriting with that rule and these extensions will not depend upon which extension is used, up to sharing-equivalence:

**Theorem 10.14.** Let $D \to_{L \to R} G$ and $D \to_{L \to R} G'$, using compatible rewriting extensions. Then, $G$ and $G'$ are sharing-equivalent.

*Proof.* Since compatible rewriting extensions are sharing-equivalent, $R$ and $R'$ are sharing-equivalent by Theorem 9.13. $\square$

This result applies to rewriting as a computing device, but also to rewriting as a relation. Note that we have not required that variables of the right-hand side $R$ of the rule $L \to R$ all occur in $L$. The choice of $\zeta(y)$, if $y$ is such a variable, is given by matching $G$ with respect to $R$, when using rewriting as a relation. When using rewriting as a computing device, every choice of $\zeta(y)$ will give a specific $G$, but any two strongly compatible choices of $\zeta(y)$ will give sharing-equivalent $G$'s.

In practice, the choice of a particular extension for the right-hand side of a rewrite rule is important. What should be pointed out here is that relational rewriting, and to some extent functional rewriting as well, leave us entire liberty of making the choice one likes. In practice, this choice can be expressed via a strategy being a parameter of the rewriting step. For example, one could choose a maximal sharing strategy, as is often the case with term rewriting implementations (which become then dag implementations.)

**Example 10.15.** Figure 8 illustrates rewriting with a rule whose left-hand side originates from the example of wiring presented in Figure 4, and right-hand side is just a variable with 3 roots. Leftmost is the input drag, and rightmost is the result. Both are in black. The rule is written in red, the context in blue, the switchboard in black. The reader is invited to verify the result of the rewrite step by actually doing the composition calculation. $\square$

We now come back to the motivating example given in Section 4.

**Example 10.16.** In the fully shared subdrag scenario, the left- and right-hand sides are both parts of the same drag, their sum. For the first rule of the example of Section 4, we
<figure><img src="image_23.png" /><figcaption>Figure 8: Rewriting with the red rule.</figcaption></figure>

now have the following combined drag:

<figure><img src="image_24.png" /></figure>

We are using dotted arrows for edges that are in the left side of the rule only, and dashed arrows when it's only on the right; were an edge in both, we would leave it solid (like some of the roots in the second rule below). Left roots are noted by an L; right ones by R. Internal vertices are only on one side are likewise dotted or dashed. So, this rule adds gray o and red c for each blue a, erasing the latter.

The second rule looks now like this:

<figure><img src="image_25.png" /></figure>

The red c vertex is shared; a yellow e is introduced in place of the deleted gray o, with incoming edges L₁ and L₂ redirected to roots R₁ and R₂, respectively.

We show with a last example that the drag format allows more sharing that available in usual term rewriting implementations.

**Example 10.17.** Consider the rule described by the drag $f_1^{[1]}(f_2^{[1]}(x))$ with two roots, the left-hand side root pointing at the upper occurrence of $f$ (L = $f_1$), and the right-hand side root pointing at the inner occurrence of $f$ (R = $f_2$). Rewriting with this rule amounts to eliminating an $f$, the outermost one, from any drag $D$ having two consecutive symbols $f$, for example $D = f(f(a))$. The entire drag $f(a)$ which results from the computation is therefore the very subterm $f(a)$ of $f(f(a))$, which goes beyond what is usually done in term rewriting implementations, where only $a$ would derive from the original term $f(f(a))$.

Consider now the rule given by the drag $f_1^{[1]}(f_2(x)) \oplus f_3^{[1]}(x)$ made of the two terms $f(f(x))$ and $f(x)$ with no common subexpression, and two roots, L = $f_1$ and R = $f_3$.
Rewriting the term $f(f(a))$ with that rule has a completely different effect: It still eliminates the topmost $f$, but it will now generate a new vertex labeled $f$, and possibly (but not necessarily, depending whether the two sprouts labeled $x$ are shared or not) a new vertex labeled $a$, resulting in a term $f(a)$ that may be an entire, or only partial, copy of the subterm $f(a)$ of the term $f(f(a))$. $\square$

We continue our investigation of drag rewriting with an important property to be used in the coming subsection.

**Lemma 10.18 (Monotonicity).** *Given a drag rewrite rule $\eta: L \to R$, let $\langle C, \xi \rangle$ and $\langle C', \xi' \rangle$ be rewrite extensions of $L, R$, respectively, compatible with $\eta$, so that $U = C \otimes_{\xi} L \dashrightarrow C' \otimes_{\xi'} R = V$.*

• Let $W$ be a drag compatible with both $U$ and $V$. Then, $U \oplus W \dashrightarrow V \oplus W$.

• Let $\langle E, \zeta \rangle$ and $\langle E', \zeta' \rangle$ be two extensions of $U$ and $V$ compatible with a root-map from $U$ to $V$ induced by the equimorphism from $C$ to $C'$. Then, $U' = E \otimes_{\zeta} U \dashrightarrow E' \otimes_{\zeta'} V = V'$.

*Proof.* The first statement is straightforward. The second uses associativity of product (Lemma 8.2) to define the extensions of $L$ and $R$: $U' = (E \otimes_{\theta} C) \otimes_{\delta} L$ for some switchboards $\theta$ and $\delta$, and $V' = (E' \otimes_{\theta'} C') \otimes_{\delta'} R$. It follows from the closure property of equimorphisms by product that $\langle E \otimes_{\theta} C, \delta \rangle$ and $\langle E \otimes_{\theta} C, \delta' \rangle$ are indeed extensions of $L$ and $R$. These extensions are compatible because the root-map from $U$ to $V$, induced by the equimorphism from $C$ to $C'$, ensures that sprouts $s$ of $L$ and $t$ of $R$ sharing the same variable label $x$ are mapped by $\theta$ and $\delta$ to products of equimorphic subdrags $A, B$ of $E, C$, respectively, for $s$, and equimorphic subdrags $A', B'$ of $E', C'$, respectively, for $t$. An arbitrary root-map would not ensure that the subdrags $B$ and $B'$ of $C$ and $C'$ are equimorphic, but that their products $B \otimes_{\zeta} L$ and $B' \otimes_{\zeta'} R$ happen to be equimorphic, which would not imply that $B$ and $B'$ are themselves equimorphic. $\square$

A final question arises: Given a drag $D$, a rule $L \to R$, and a rewriting extension $\langle E, \xi \rangle$ for $L$, does there exist a rewriting extension $\langle E, \xi' \rangle$ for $R$? In general, yes, but there is a particular case for which this is not the case. It may indeed be that the switchboard $\xi$, which is well-behaved for $L$, is not well-behaved for $R$. This happens in the following situation: $u$ is a rooted internal vertex of $L$, $s: x$ is a sprout of $L$ accessible from $u$, $s': x$ is a rooted sprout of $R$ such that $\eta(u) = s'$, $t: y$ is a sprout of $E$, $\xi(s) = t$, and $\xi(t) = u$. Switchboard $\xi$ is well-behaved with respect to $L$ because $u$ is an internal vertex. Now, $\xi'(s') = t$ and $\xi'(t) = \eta(u) = s'$; hence, $\xi'$ is not well-behaved. This is the only situation where this may arise, but this is why we always assumed the existence of one rewriting extension for $L$ and one for $R$.

Note finally that our definition of rewriting implies that a rewrite succeeds as soon as compatible rewrite extensions exist: dangling edges can't be created in our model. The situation would be different without indegree preservation of matching. On the other hand, indegree preservation implies that rules must be duplicated with various numbers of roots at all vertices so as to fit with all possible rewriting extensions. We shall come back to these questions when investigating the categorical properties of drags in Section 12.

**10.4. Congruences joinable by rewriting.** Our goal now is to prove that congruent pairs are joinable when the congruence $\mathcal{E}$ is generated by a confluent set of drag rewrite rules $\mathcal{R}$, yet again generalizing the situation for terms. Furthermore, since a congruence contains sharing equivalence, rewriting should actually operate uniformly on sharing-equivalent drags. We will therefore assume two different properties of a rewrite system:
**Definition 10.19 (Church-Rosser).** A drag rewrite system $\mathcal{R}$ is

(1) *confluent modulo sharing* if for all drags $U, V, W$ such that $V_{\mathcal{R}} \leftarrow U \longrightarrow_{\mathcal{R}} V$, there exist drags $W, W'$ such that $V \longrightarrow_{\mathcal{R}} W \cong_{sh} \mathcal{R} \leftarrow W'$;

(2) *coherent modulo sharing* if, for all drags $U, V, W$ such that $V \cong_{sh} U \longrightarrow_{\mathcal{R}} V$, there exist $W$ such that $V \longrightarrow_{\mathcal{R}} W \cong_{sh} V$.

(3) *Church-Rosser (modulo sharing)* if it is both confluent and coherent modulo sharing.

**Theorem 10.20.** Let $\mathcal{E}$ be a set of equations and $\mathcal{R}$ a Church-Rosser set of rules that satisfy the following two assumptions:

(1) $\forall U =^{\eta} V \in \mathcal{E} : U \longrightarrow_{\mathcal{R}} \cong_{sh} \mathcal{R} \leftarrow V$ (root-map $\eta$);

(2) $\forall \eta : L \to R \in \mathcal{R} : L =^{\eta}_{\mathcal{E}} R$.

Then, $U =_{\mathcal{E}} V$ iff $U \longrightarrow_{\mathcal{R}} \cong_{sh} \mathcal{R} \leftarrow V$.

*Proof.* This will follow from the soundness and completeness lemmas (10.21 and 10.22) below. □

Hence, it is sound and complete to check a congruence by rewriting—possibly until a normal form is obtained if rewriting is confluent and coherent (with respect to sharing equivalence). The resulting terms—possibly normal forms—should be checked for equality under sharing equivalence, which is decidable.

Note that equations need not be pairs of patterns; they can be built from arbitrary drags having the same number of roots, provided rules (built from patterns) exist that satisfy (1). When equations are built from patterns, assumption (1) is usually obtained by orienting the equations in $E$ into rules, and then completing the obtained set of rules until confluence and coherence are satisfied, providing assumption (2).

**Lemma 10.21 (Soundness).** *Assuming (2), $\longrightarrow_{\mathcal{R}} \subseteq =_{\mathcal{E}}$.*

*Proof.* By induction on the length of the derivation $\longrightarrow_{\mathcal{R}}$. Since equimorphism is included in any congruence, it is enough to carry out the proof for a single step $U \longrightarrow_{\mathcal{R}}^p V$, which is a consequence of assumption (2). □

**Lemma 10.22 (Completeness).** *Assuming (1), let $U =^{\eta}_{\mathcal{E}} V$. Then, $U \longrightarrow_{\mathcal{R}} \cong_{sh} \mathcal{R} \leftarrow V$.*

*Proof.* By induction on the definition of the congruence $=_{\mathcal{E}}$. If $U =^{\eta} V \in \mathcal{E}$, the result follows by Assumption (1). Otherwise, $U \longrightarrow_{\mathcal{R}} \cong_{sh} \mathcal{R} \leftarrow V$ by induction hypothesis, and let

(1) $V \cong_{sh} W$. We then conclude by applying the coherence assumption..

(2) $W$ compatible with both $U$ and $V$. Then $U \oplus W \longrightarrow_{\mathcal{R}} \cong_{sh} \mathcal{R} \leftarrow V$, since rewriting is closed under sum with a compatible drag, as well as sharing-equivalence.

(3) $\langle C, \xi \rangle$ and $\langle C', \xi' \rangle$ rewriting extensions of $U$ and $V$ respectively, compatible with the root-map $\eta$. By repeated applications of Lemma 10.18, $C \otimes_{\xi} U \longrightarrow D \otimes_{\zeta} W$, where $\mathrm{ext}(D, \zeta)$ is an extension of $W$ compatible with the extension $\langle C, \xi \rangle$ of $U$. Likewise, $C' \otimes_{\xi'} V \longrightarrow D' \otimes_{\zeta'} W'$, where $\mathrm{ext}(D', \zeta')$ is an extension of $W'$ compatible with the extension $\langle C', \xi' \rangle$ of $V$. We are therefore left showing that these extensions are compatible, which results from the transitivity property of compatibility.

(4) $V =^{\mu}_{\mathcal{E}} W$. Then, $U \longrightarrow_{\mathcal{R}} \cong_{sh} V'_{\mathcal{R}} \leftarrow V \longrightarrow_{\mathcal{R}} V'' \cong_{sh} \mathcal{R} \leftarrow W$. By confluence assumption, $V' \longrightarrow_{\mathcal{R}} T \cong_{sh} T'_{\mathcal{R}} \leftarrow V''$ for some sharing-equivalent drags $T$ and $T'$. We then conclude by using the coherence assumption twice. □

Ensuring coherence of $\mathcal{R}$ with respect to sharing equivalence can be achieved by completing the set of rules until sharing equivalence is obtained. The problem indeed is that two
distinct subdrags of a left-hand side $L$ of rule may become equimorphic when computing the product of $L$ with respect to some rewrite extension. Then, these two subdrags may become identical by applying a sharing equivalence step, and the rule won't be applicable anymore. For example, assume $L = f(g(x), g(y)) \to f(a)$, and $D = [z = g(a)]f(z)$. Then, rewriting $D$ would require using the rule $L' = [z = g(x)]f(z) \to f(a)$. Computing these extensions requires unifying the subdrags $g(x)$ and $g(y)$, a process very similar to Knuth and Bendix completion [KB70, DJ90]. We know that drag unification is solvable for drags whose roots are organized as lists with repetitions, and that any solvable unification problem has a most general solution, which is unique up to isomorphism. We assume here (there is little doubt about that conjecture) that this is the same for our current model of drags with multisets of roots. So, making a set of rules coherent with respect to sharing-equivalence should not be difficult. Whether it could be terminating is another question.

Theorem 10.20 does not state that these equalities, generated by the equations for the first and by the rules for the second, coincide. Indeed, they do not:

**Example 10.23.** Let $\mathcal{E} = \{f^{[1]}(x) = g^{[1]}(x), f^{[1]}(x) = h^{[1]}(x, x)\}$, and $\mathcal{R} = \{f^{[1]}(x) \to h^{[1]}(x, x), g^{[1]}(x) \to h^{[1]}(x, x)\}$. Using the extension $\langle a^{[1]}, \{x \to a\} \rangle$ for both left- and right-hand sides of the equation, we get $f(a) =_\mathcal{E} g(a)$. Using now the extensions $\langle a^{[1]} \oplus a^{[1]}, \{x_1 \to a_1\} \rangle$ and $\langle a^{[1]} \oplus a^{[1]}, \{x_2 \to a_1, x_3 \to a_2\} \rangle$ for the first rule, we get $f(a) \to h(a, a)$. Finally, using the extensions $\langle a^{[1]}, \{x_1 \to a\} \rangle$ and $\langle a^{[1]}, \{x_2 \to a, x_3 \to a\} \rangle$ for the second rule, we get $g(a) \to [z = a]h(z, z)$. Therefore:

$$f(a) \to h(a, a) \cong_{sh} [x = a]h(x, x) \leftarrow g(a).$$

Could we define congruences and rewriting so that they would coincide? The answer is yes, we believe. For the former, we would simply need to include sharing-equivalence in the definition of a congruence. For the latter, we would need for rewriting to be modulo sharing, a more complex task indeed, which is yet another way to achieve coherence. Since distinct subdrags of a left-hand side of rule $L$ could become equimorphic, hence shared, by computing the product $D$ of $L$ with an appropriate rewrite extension, the injection of $L$ into $D$ would no longer be injective. This question would be worth exploring, but is beyond the scope of the present paper.

## 11. DRAG REWRITING VERSUS TERM REWRITING

In this section, we consider term rewrite rules having possibly a root at their head, and (try to) apply them to terms, including terms that possibly involve sharing.

Consider a rule $f(x, x) \to g(x, x)$ with no roots on either side. The sprouts are $x_1, x_2$ in the left-hand side and $x_3, x_4$ in the right-hand side.

Let $t_1 = f(a, a)$ with vertices $f$ (on top) and $a_1$ (shared). Let $t_2 = f(a, a)$, with vertices $f, a_1, a_2$ And let $t'_1 = g(a, a)$, with the shared vertex $a_1$ being the same as above, and $t'_2 = g(a, a)$ with vertices $a_2$ on the left and $a_1$ on the right.

* $t_1 \to t'_1$ with extension drag $E$ being the two-rooted vertex $a_1^{[2]}$ and switchboards being $\xi = \{x_1 \mapsto a_1, x_2 \mapsto a_1\}$ and $\xi' = \{x_3 \mapsto a_1, x_4 \mapsto a_1\}$.

* $t_2 \to t'_2$ with extension drag $E = a_1^{[1]} \oplus a_2^{[1]}$, and switchboards $\xi = \{x_1 \mapsto a_1, x_2 \mapsto a_2\}$ and $\xi' = \{x_3 \mapsto a_2, x_4 \mapsto a_1\}$.

* $t_1 \to t'_2$ with extension drags (two are needed here) $E = a_1^{[2]}$ and $E' = a_1^{[1]} \oplus a_2^{[1]}$ and switchboards $\xi = \{x_1 \mapsto a_1, x_2 \mapsto a_1\}$ and $\xi' = \{x_3 \mapsto a_2, x_4 \mapsto a_1\}$. Note that the vertex
$a_1$ does not have the same number of roots in $E$ and $E'$. Note also that $E'$ cannot be identical to $E$ since $t'_2$ has additional vertices that do not originate from the rewrite rule, they must therefore come from the extension drag. This rewrite is therefore relational, using the isomorphic copy (a “clone”) $a_2$ of $a_1$.

• $t_2 \to t'_1$. Take $E = a_1^{[1]} \oplus a_2^{[1]}$, $E' = a_1^{[2]}$, $\xi = \{x_1 \mapsto a_1, x_2 \mapsto a_2\}$ and $\xi' = \{x_3 \mapsto a_1, x_4 \mapsto a_1\}$. Note that the choice of $E'$ allowed us to “garbage collect” the vertex $a_2^{[1]}$ of $E$ implicitly. The other choice $E' = a_1^{[2]} \oplus a_2^{[1]}$ would yield as a result the expression $t'_1 \oplus a_2^{[1]}$, hence disabling “garbage collection”.

• $t_1 \to a_3^{[1]} \oplus t'_1$, where $a_3$ is a fresh copy of $a$, that is, a *clone* of $a$. Take $E = a_1^{[1]} \oplus a_2^{[1]}$, $E' = a_1^{[2]} \oplus a_3^{[1]}$, with $\xi$ and $\xi'$ as above. Here, we have achieved “cloning” and “garbage collection” at the same time.

Terminating computations—to which we are partial—are incompatible with “cloning”. In general, functional rewriting restricts context extensions so as to avoid “cloning” and allow one to attain termination. Relational rewriting, on the other hand, is more lax regarding “cloning” and nontermination.

We provide now a formal statement comparing term rewriting to drag rewriting. Remember that terms have positions identifying their various subterms, and that rewriting a term $s$ to a term $t$ with the rule $l \to r$ is defined as $s|_p = l\sigma$ for some position $p$ in $s$ and substitution $\sigma$, and $t = s[r\sigma]_p$, denoting by $s|_p$ the subterm of $s$ at position $p$, and by $s[u]$ the term obtained by replacing $s|_p$ by $u$ at position $p$.

Term rewriting does not really apply to terms, that is, drags whose all vertices have a single predecessor but one which has none, but to equimorphisms classes of terms (and not isomorphisms classes, variables can't be renamed in terms to be rewritten). This is so because term rewriting does not distinguish between two copies of the same term $t$, for example, two disjoint drags $f(a)$ and $f(a)$. So, term rewriting *looks* functional, but it is not, the result of a rewrite step is determined up to equimorphism only. The situation is indeed the same with functional drag rewriting, hence we can compare both.

Any strict subdrag of a term has a root at its head. We therefore denote by $\bar{t}$, for a term $t$, the vertex at the head of the ground drag $t$, and by $[[t]]$ the drag obtained by adding a root at vertex $\bar{t}$ of $t$. This encoding has three simple properties: first, a term and its encoding have exactly the same vertices, hence, in particular, the same labeled sprouts; second, positions in terms make therefore sense for their encoding; and third, taking subterms in terms commutes with their encoding. A substitution $\sigma = \{x \mapsto x\sigma : x \in \text{Var}(l)\}$ is encoded as the drag $\Sigma_{x \in \text{Var}(l)}[[x\sigma]]$, but also as the switchboard $\xi_{\sigma} = \{v \to [[x\sigma]] : (v : x) \in S([[l]]) = S(l)\}$. A term rewrite rule $l \to r$ is encoded as the drag rewrite rule $[[l]] \to [[r]]$. A set of term rewrite rules $R$ is denoted by $[[R]]$ when encoded as drag rewrite rules.

**Lemma 11.1.** Let $t$ and $l$ be terms and $p$ a position of $t$. Then, $t = t[l\sigma]_p$ for some substitution $\sigma$ of domain $\text{Var}(l)$ iff $[[t]] = ([[t[z]]_p) \oplus [[\sigma]]) \otimes \xi_{\sigma}[[l]]$ for some fresh sprout $s:z$ and switchboard $\xi = \{s \to \overline{[[l]]}\} \cup \xi_{\sigma}$.

Note first that the statement makes sense: $t$ being a term, $t[z]_p$ and $\sigma$ do not share any vertex, hence the sum of their encodings is defined, and since $z \to \bar{l}$ and $\sigma$ don't interfer, the union $s \to \bar{l} \cup \xi_{\sigma}$ is a (non-directed) switchboard.

*Proof.* First, the only if direction. Since $t = t[l\sigma]_p$, we have $[[t]] = [[t[z]]_p] \otimes_{s \to t|_p} [[t|_p]]$ by Lemma 7.2. We now apply Lemma 7.2 to $l\sigma$, which requires to linearize $l$ so as to become
the context in $l\sigma$ of the subterms associated with the substitution $\sigma$. Denoting by $lin(l)$ the linearized version of $l$, by $\sigma'$ the substitution satisfying $l\sigma = lin(l)\sigma'$, we have $[[t|_p]] = [[l\sigma]] = [[lin(l)\sigma']]] = [[lin(l)]] \otimes_{\sigma'} [[\sigma]] = [[l]] \otimes_{\sigma} [[\sigma]]$, where $\sigma$ and $\sigma'$ are now considered as switchboards by replacing an elementary substitution $x \mapsto u$ by the wire $s: x \mapsto \bar{u}$. It follows that $[[t]] = [[t[z]_p]] \otimes_{z \sim \overline{t|_p}} [[t|_p]] = [[t[z]_p]] \otimes_{z \sim \overline{t|_p}} ([[l]] \otimes_{\xi_\sigma} [[\sigma]]) = [[t[z]_p]] \otimes_{z \sim \overline{[l]}} ([[l]] \otimes_{\xi_\sigma} [[\sigma]]) = (([t[z]_p] \oplus [[\sigma])) \otimes_{z \sim \overline{[l]}, \xi_\sigma}} [[l]]$.

The converse amounts to apply the wires in $\xi_\sigma$ (which do not depend on $s \rightsquigarrow \overline{[l]}$), yielding $[[t]] = [[t[z]_p]] \otimes_{s \rightsquigarrow \overline{[l]}} [[l]]$, hence the expected result by unencoding the terms on both sides of the equality, since the switchboard reduced to the single wire $s \rightsquigarrow \overline{[l]}$ is now directed, hence acts as a substitution. $\square$

Assuming now that left-hand sides of term rewriting rules are not variables (hence are patterns), we have:

**Theorem 11.2.** Let $R$ be a set of term rewriting rules and $s, t$ be two terms such that. $s \to_R^p t$. Then, $[[s]] \to_{\llbracket R \rrbracket} [[t]]$.

*Proof.* The only if part is a direct application of the rewriting definitions and of Lemma 11.1 to $s$ and $t$. Checking functionality is straightforward. $\square$

The converse is not true in general, since drag rewriting is defined up to sharing equiv-
ality instead of equimorphism: rewriting with rule $[[l]] \to [r]$ may introduce sharing when
$r$ is non-linear, hence cannot be mimicked by term rewriting with the rule $l \to r$. Here is
the precise statement:

**Lemma 11.3.** Let $R$ be a set of term rewriting rules and $s, t$ be two terms such that. $$ [[s] \to_{\llbracket R \rrbracket} [[t]]]. \text{ Then, } s \to_R^p t' \text{ for some } t' \text{ sharing equivalent to } t. $$

*Proof.* Using this time the if direction of Lemma 11.1. The reason for obtaining a term $t'$ sharing-equivalent to $t$ rather than $t$ itself, is the use of a right-hand side switchboard possibly different from the left-hand side one. $\square$

Encoding term rewriting as drag rewriting appears to be slightly different from the
encoding of term rewriting by jungle rewriting, as described in [HKP91]. The reason is
that drag rewriting does not integrate the use of sharing equivalence (actually, sharing
normal forms) to the encoding process as they do, since we only consider here what could
be called “plain dag rewriting”. Encoding sharing equivalence would require the use of a
slightly different notion of drag rewriting, modulo sharing equivalence, which is not within
the scope of this paper.

We could of course now repeat a similar development for dags as for terms, defining
a dag rewrite rule as a pair of dags $L \to R$, whose encoding is obtained by having an
arbitrary number of roots (possibly none) at the heads of both $L$ and $R$. Of course, there
will be infinitely many rules, but using the rule schema $L^{[n]} \to R^{[n]}$ instead will do, $n$ being
calculated on the fly thanks to indegree preservation. Then, a dag $D$ to be rewritten can be
encoded by the identity: there is no need to add roots at the head of $D$ since dag rewrite
rules can have no root at their head.
## 12. CATEGORICAL INTERPRETATION OF DRAG REWRITING

Our definition of drag rewriting is concrete: Drags are specific concrete (multi-) graphs, and drag rewrite rules are pairs of drags whose roots are bijectively related, used to rewrite other drags. We found that drags and their morphisms form a category. So a natural question to ask is whether we could define drag rewriting in terms of the general DPO framework for graph transformation. We will see that this is in general impossible, there being several reasons for that failure.

**12.1. Rules.** In DPO graph transformation, rules are spans $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$, where $l, r$ are monomorphisms (sometimes a specific kind of monomorphisms), and $K$ is assumed to be the shared subgraph of $L$ and $R$.

Considering this definition, it seems reasonable to represent a drag rewriting rule $\eta: L \rightarrow R$ as the DPO rule $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$, where $K$ is the subgraph shared by $L$ and $R$, and $l, r$ are the natural injections $l: K \rightarrow L$ and $r: K \rightarrow R$. Unfortunately, this representation may be incorrect, as the following example shows. Suppose that $L$ is the drag $f \implies a$ ($a$ is a double successor of $f$) and $R$ is the drag $g_1 \implies a \leftarrow g_2$ (where vertex $a$ is shared with $L$). Then, the DPO representation of $K$ would be the drag $a$ with some roots, but at least one of the injections $l, r$ would fail to be a monomorphism, since they could not both preserve the indegree of $a$, which is 2 on one side and 3 on the other. This may restrict the choice of a common subdrag by DPO to a non-maximal one—the empty one in this example.

**12.2. Matching.** In the DPO approach, the operation of matching a drag $D$ against a drag $L$ is defined by means of a (mono)morphism, while in drags this done by the definition of an extension $\langle C, \xi \rangle$ such that $D = L \otimes_{\xi} C$. We will see that both forms of matching are equivalent.

**Lemma 12.1.** Given two disjoint drags $L, C$ and a switchboard $\xi$ for $L, C$, the natural injection from $L$ to $C \otimes_{\xi} L$ is a monomorphism.

*Proof.* By Lemma 6.4, the natural injection from $L$ to $L \oplus C$ is a monomorphism. By Lemma 6.18, the natural injection from $L \oplus C$ to $L \otimes_{\xi} C$ is a monomorphism. We conclude by Lemma 5.8. □

Next, we consider the converse, namely, the existence of an extension when given a monomorphism from $L$ to $D$. First, we define the categorization of edges corresponding to the colours used in the examples of monomorphisms given earlier:

**Definition 12.2 (Inside/created/entering/outside edges).** Given drags $L = \langle V, R, L, X, S \rangle$ and $D = \langle V', R', L', X', \emptyset \rangle$ with no vertex in common and a monomorphism $o: V \to V'$, we characterize an edge $u' \dashrightarrow^i v'$ of $D$ as follows:

(1) It is an *inside* edge at $v'$ if $u' = o(u)$ and $v' = o(v)$ for some internal vertices $u, v$ of $L$ such that $u \dashrightarrow^i v \in X$;

(2) it is *created* by the *creating* edge $u \dashrightarrow^i s \in X$ if $u' = o(u)$ for some internal vertex $u$ of $L$, and $s$ is a sprout such that $o(s) = v'$;

(3) it is an *entering* edge at $v'$ if $v' = o(v)$ for some internal vertex $v$ of $L$, and $u' \dashrightarrow^i v'$ is not the image of an edge in $L$ by $o_X$;

(4) it is an *outside* edge at $v'$ if $v'$ is not the image of an internal vertex of $L$ by $o$, and $u' \dashrightarrow^i v'$ is not the image of an edge of $L$ by $o_X$.
<figure><img src="image_26.png" /><figcaption>Figure 9: An injection with all four kinds of edges: black for inside, red for created, blue for entering and green for outside.</figcaption></figure>

Inside and created edges of $D$ originate from some (unique) edge in $L$, while entering and outside edges don't originate from edges in $L$. Entering edges must have their head mapped from some internal vertex of $L$, while outside edges do not. This is therefore a categorization, which is illustrated in Example 9.

**Lemma 12.3.** Let $L, D$ be drags satisfying the assumptions of Definition 12.2, and $o$ be a monomorphism from $L$ to $D$. Then each edge of $D$ is precisely one of the above four kinds.

*Proof.* We show first that these four kinds of edges are disjoint as a consequence of injectivity of $o$. The first two kinds are disjoint because two edges $u \dashrightarrow^i v$ and $u \dashrightarrow^j s$ of $L$ such that $v \neq s$ are different, hence $i \neq j$. The last two kinds are disjoint from the first two since edges in $D$ do not originate from edges in $L$. The fourth is disjoint from the third since they discriminate on $v'$ being the image of an internal vertex in $L$.

We show now that all edges in $D$ at considered. All edges in $D$ obtained from an edge $u \dashrightarrow^i v$ in $L$ by $o_X$ must have an internal vertex as tail vertex $u$, hence are either inside or created. If $u' \dashrightarrow^i v'$ is not obtained from an edge in $L$, there are two cases: either $v' = o(v)$ for some internal vertex $v$ of $L$ and it is an entering edge; or there is no such $v$ and it is an outside edge. $\square$

**Lemma 12.4.** Given a drag $D$, a drag $L$ with no rootless isolated sprout and no sprout in common with $D$, and an injection $o: L \to D$, there exists a rewriting extension $\langle C, \xi \rangle$ of $L$ such that $D = C \otimes_{\xi} L$.

*Proof.* Without loss of generality, sprouts of $D$, if any, will be considered internal vertices of $D$, since they will not belong to the domain of $\xi$. In what follows, we successively (a) construct the context extension $C$, (b) then the switchboard $\xi$, and finally (c) verify that putting them together we have $D = C \otimes_{\xi} L$. These constructions rely on Lemma 12.3, ensuring that each edge of $D$ belongs to exactly one kind.

(a) Construction of context $C$:

* Labeled internal vertices. Let $V$ be the vertices of $D$ and $I$ the internal vertices of $L$ (which are also internal vertices of $D$ by the assumption that $o$ is an injection). Then, the set of internal vertices of $C$ will be $W = V \setminus I$, each one equipped with its label in $D$.

* Labeled sprouts. The set $S$ of sprouts of $C$ consists of fresh sprouts $t_{u,i} : x_{u,i}$, bijectively associated with the pair $(u, i)$ for each entering edge $u \dashrightarrow^i v$ in $D$—with $u \in W$ and $v \in I$, plus sprouts $t_{u,i} : y_{u,i}$ for each creating edge $u \dashrightarrow^i v$ in $D$, such that $u, v \in I$, but $u \dashrightarrow^i v$ is not an edge of $L$, $u \dashrightarrow^i s$ is an edge in $L$ and $o(s) = v$. Notice that the edge $u \dashrightarrow^i s$, with $o(s) = v$, must exist by the definition of morphism. Notice also that, by definition,
the variables of any two sprouts in $C$ must be different, implying that the context $C$ will be linear.

* Edges. The set of edges of $C$ consists of all outside edges $u \to^i v$ in $D$, such that $u, v \in W$, plus edges $u \to^i t_{u,i}$, for each entering edge $u \to^i v$ in $D$ with $u \in W$ and $v \in I$. These sprouts are not isolated.

* Roots. Finally, each vertex $v$ in $W$ is equipped with roots so that $v$ has the same indegree in $C$ and $D$. Sprouts $t_{u,i}$, $t_{u,i} : y_{u,i} \in C$, associated to the creating edge $u \to^i v$ in $D$, are equipped with a single root, hence will be rooted, isolated sprouts.

(b) Construction of switchboard $\xi$:

* For each creating edge $u \to^i s$ of $L$, $\xi_L(s) = t_{u,i} : y_{u,i}$.

* For any other sprout $s \in L$, $\xi_L(s) = o(s)$.

* For each sprout $t_{u,i} : x_{u,i} \in C$, associated to entering edge $u \to^i v$ in $D$, $\xi_C(t_{u,i} : x_{u,i}) = v$.

* For each sprout $t_{u,i} : y_{u,i} \in C$, associated to creating edge $u \to^i v$ in $D$, $\xi_C(t_{u,i} : y_{u,i}) = v$.

We are left with showing that $\xi$ is a switchboard. The union $\xi_L \cup \xi_C$ is coherent and well-behaved: It is coherent since $o$ is a morphism and $C$ is linear; by definition $\xi_L \cup \xi_C$ is functional and well-founded. Finally, $\xi_L \cup \xi_C$ is injective, since $o$ is a morphism and, hence, root preserving. Therefore, $\langle C, \xi \rangle$ is a rewriting extension.

(c) Verification that $D = C \otimes_{\xi} L$:

Internal vertices of $D$ and $C \otimes_{\xi} L$ coincide, and so too their labeling, hence implying that they have the same number of edges. To show that their edges coincide, it is therefore enough to show that every edge of $D$ is an edge of $C \otimes_{\xi} L$, which we do by inspecting the four categories of an edge $u \to^i v$ of $D$:

* Outside edges: $u, v \in W$. By construction of $C$, $u \to^i v$ is an edge of $C$ and therefore of $C \otimes_{\xi} L$.

* Inside edges: $u, v \in I$ and $u \to^i v$ is an edge of $L$. Then $o(u) \to^i o(v)$ is an edge in $C \otimes_{\xi} L$.

* Created edges: $u, v \in I$, but $u \to^i v$ is not an edge of $L$. Then, there must exist a creating edge $u \to^i s$ in $L$. By construction, $\xi_L(s) = t_{u,i}$ and $\xi_C(t_{u,i}) = v$; hence $u \to^i v$ is an edge in $C \otimes_{\xi} L$. This case shows the need for bouncing from $L$ to $C$ and back from $C$ to $L$.

* Entering edge: $u \in W$, $v \in I$. By construction, $C$ includes a sprout $t_{u,i} : x_{u,i}$ and an edge $u \to^i t_{u,i}$, with $\xi_C(t_{u,i}) = v$; hence $u \to^i v$ is an edge in $C \otimes_{\xi} L$.

It follows that all vertices have the same incoming edges in $D$ and $C \otimes_{\xi} L$, hence the same number of them. Since they have identical indegree by construction, they must have the same number of roots, which terminates verification and proof. □

In case $L$ is a rooted isolated sprout, the constructed context $C$ is identical to $D$, and the switchboard $\xi$ contains the single wire $s \rightsquigarrow o(s)$. Then, all edges of $D$ are outside edges. Note that verification is straightforward in that case since isolated sprouts are then identities for product by Lemma 8.2.

**Example 12.5.** Let $D$ be a drag with two internal vertices labeled $h^{[1]}$ and $f^{[1]}$, both of ar- ity 3, and edges $h \to^1 f, h \to^2 f, h \to^3 h$, and $f \to^1 h, f \to^2 f, f \to^3 h$. Now consider the drag $L = f^{[4]}(x_1^{[1]}, x_2^{[1]}, x_3)$ with the injection $o$ mapping its four vertices $f, x_1, x_2, x_3$ to $f, h, f, h$, respectively, and $o_R(x_1^{[1]}) = h \to^3 h$, $o_R(f^{[3]}) = \{h \to^1 f, h \to^2 f, f \to^3 f\}$.

Let now $C$ be the drag $h^{[4]}(y_1, \text{SELF}, y_3) \oplus z^{[2]}$. We construct the expected extension by processing all missing edges in turn:
(1) $f \xrightarrow{2} f$: add $z^{[2]}$ to $C$, define $\xi_L(x_2) = z$ and $\xi_C(z) = f$; remove a root from $f$ and $f \xrightarrow{2} f$ from $o_R(f)$;

(2) $f \xrightarrow{1} h$: define $\xi_L(x_1) = h$ and remove $f \xrightarrow{1} h$ from $o_R(h)$;

(3) $f \xrightarrow{3} h$: define $\xi_L(x_3) = h$ and remove $f \xrightarrow{3} h$ from $o_R(h)$;

(4) $h \xrightarrow{1} f$: define $\xi_C(y_1) = f$ and remove $h \xrightarrow{1} f$ from $o_R(f)$;

(5) $h \xrightarrow{2} f$: define $\xi_C(y_2) = f$ and remove $h \xrightarrow{2} f$ from $o_R(f)$.

We therefore obtain the extension:

$$(h^{[3]}(y_1, y_2, \text{SELF}) \oplus z^{[2]}, \{x_1 \rightsquigarrow h, x_2 \rightsquigarrow z, z \rightsquigarrow f, x_3 \rightsquigarrow h, y_1 \rightsquigarrow f, y_2 \rightsquigarrow f, y_3 \rightsquigarrow x_1, z \rightsquigarrow h\}).$$

We observe that mapping $x_2$ to $z$ and then $z$ to $f$ produces the edge $f \to f$, while other edges are produced more directly, as pointed out above, not being created edges of $L$ in $D$. $\square$

The previous lemmas imply that matching based on composition and matching based on the existence of an injection coincide:

**Theorem 12.6.** Given a drag $D$, a drag $L$ with no rootless isolated sprout and no sprout in common with $D$, there exists an injection $o: L \to D$ iff there exists a rewriting extension $\langle C, \xi \rangle$ of $L$ such that $D = C \otimes_{\xi} L$.

We have not claimed uniqueness of the rewriting extension $\langle C, \xi \rangle$ when given $D, L$, and $\iota$, and there are indeed many rewriting extensions satisfying Lemma 12.4, hence Theorem 12.6. The relevance of uniqueness lies in the fact that given $D, L, o$, the result of rewriting $D$ with $L \to R$ at $o$ would then be deterministic, as is usually expected from a functional rewriting mechanism. Uniqueness could indeed be achieved by introducing the definition of a *reduced extension*, imposing two requirements: The switchboard $\xi$ should not bounce between $L$ and $C$ more than necessary. And isolated sprouts of the extension context $C$ should have a single root, hence cannot be targets for two different wires of the switchboard. This question merits further investigation, and it would be interesting to have both a matching and an unification algorithm for this version of drags, in the style of [JO23].

### 12.3. Rewriting.
We now consider whether drag rewriting can be defined algebraically, in terms of a double pushout in **Drags**, the category of drags. A standard approach would be to show that the category of drags has some form of adhesivity. Unfortunately, drags are not even $\mathcal{M},\mathcal{N}$-adhesive [HP12], as shown below, because we cannot always ensure the existence of pushouts when they are needed. This is the second reason for failure of DPO.

We can see the problem with the following counterexample. Suppose that we have drags $D_0 = [v^{[1]} : a]$, $D_1 = [v_1 : f \to v : a]$, and $D_2 = [v_2 : g \to v : a]$. Let now $o_1$ and $o_2$ be the natural injections, mapping $D_0$ to $D_1$ and $D_2$, respectively. In particular $o_1$ and $o_2$ would map the root at $v$ to the edges $v_1 \to v$ and $v_2 \to v$, respectively. Then, it is easy to see that there is no pushout of $o_1$ and $o_2$ in the category of drags. The obvious candidate would be the drag $D_3 = [v_1 : f \to v : a \leftarrow v_2 : g]$. The problem is that the natural injection $o'_1 : D_1 \to D_3$, mapping vertices $v, v_1$ and edge $v_1 \to v$ of $D_1$ to vertices $v, v_1$ and edge $v_1 \to v$ in $D_3$, is not even a morphism, since the indegree of $v$ in $D_3$ is 2, while it is 1 in $D_1$, and the same happens with $o'_2 : D_2 \to D_3$.

This counterexample shows a form of dangling edge problem in drags: If $o_1$ maps $v : a$ in $D_0$ to $v : a$ in $D_1$, and the root on $v : a$ in $D_0$ to the edge $v_1 \to v$ in $D_1$, there would not exist a pushout complement to $(o_1, o'_1)$ since, after deleting $v_1 : f$ from $D_3$, the edge
$v_1 \rightarrow v$ would be dangling. However, we may notice that, while in the context of DPO transformations, dangling conditions ensure the existence of pushout complements but do not interfere with the existence of pushouts, this is no longer the case for drags.

Pushouts in **Drags**, when they exist, have the form of the diagram in Lemma 12.7. We use here the fact that if there exist a monomorphism $o_1 : D_0 \to D_1$, then $D_1$ is the product of $D_0$ by some rewriting extension $\langle C_1, \xi_1 \rangle$ by Theorem 12. Assume now that we are given two injections $o_1 : D_0 \to D_1$ and $o_1 : D_0 \to D_1$, so that $D_1$ and $D_2$ are compatible, $D_0$ being their shared subdrag. Then, the context subgraphs $C_1$ and $C_2$ must be disjoint, and disjoint from $D_0$. This explains the assumptions given below, which are exactly the assumptions needed for applying a rewrite step in the DPO model.

**Lemma 12.7.** Given monomorphisms $o_1 : D_0 \to D_0 \otimes_{\xi_1} C_1$ and $o_2 : D_0 \to D_0 \otimes_{\xi_2} C_2$, such that $D_0$, $C_1$, and $C_2$ are pairwise disjoint, $\xi_1 \cup \xi_2$ is a switchboard for $(D_0, C_1 \oplus C_2)$, and the pushout of $o_1$ and $o_2$ exists, then the pushout object must be the drag $D_0 \otimes_{\xi_1 \cup \xi_2} (C_1 \oplus C_2)$ and the monomorphisms from $D_1$ and $D_2$ to the pushout object are the natural injections $o'_1$ and $o'_2$, as depicted here:

$$ \begin{tikzcd} D_0 \arrow[r, "o_1"] \arrow[d, "o_2"'] & D_1 = D_0 \otimes_{\xi_1} C_1 \arrow[d, "o'_1"'] \\ D_2 = D_0 \otimes_{\xi_2} C_2 \arrow[r, "o'_2"'] & D_3 = D_0 \otimes_{\xi_1 \cup \xi_2} (C_1 \oplus C_2) \end{tikzcd} $$

*Proof.* Let $D'_3 = D_0 \otimes_{\xi_1 \cup \xi_2} (C_1 \oplus C_2)$, and $o'_1, o'_2$ be the natural injections of the vertices in $D_1, D_2$ to the vertices in $D'_3$. Under our assumptions, $\xi_1 \cup \xi_2$ is safe, hence $D'_3 = (D_0 \otimes_{\xi_1} C_1) \oplus (D_0 \otimes_{\xi_2} C_2)$ by distributivity (Lemma 8.4). Therefore, $o'_1$ and $o'_2$ are monomorphisms of $D_1, D_2$ to $D'_3$ by Lemma 6.4(2).

Using our assumption of existence of a pushout, let $(D_3, o'_1, o'_2)$ be a pushout of $D_1$ and $D_2$ in **Drags**. By the universal property of pushouts, there exists a unique morphism $o_3$ from $D_3$ to $D'_3$, such that $o'_1 = o'_1 \circ o_3$ and $o'_2 = o'_2 \circ o_3$, whose vertex map $o_3 : \mathcal{V}(D_3) \to \mathcal{V}(D'_3)$ is the corresponding universal morphism in **Set**. By definition of $D'_3$, we know that $\mathcal{V}(D'_3)$ is also a pushout object of the diagram depicted in Figure 10. Hence, $o_3$ is an isomorphism in **Set** and, since it is a morphism in **Drags**, it is an isomorphism in **Drags**. $\square$

We now describe a necessary condition for the existence of pushouts of monomorphisms in **Drags**:

**Lemma 12.8.** Given monomorphisms $o_1 : D_0 \to D_1 = (D_0 \otimes_{\xi_1} C_1)$ and $o_2 : D_0 \to D_2 = (D_0 \otimes_{\xi_2} C_2)$, such that $C_1$ and $C_2$ are disjoint, then $o_1$ and $o_2$ have a pushout only if for every vertex $v \in V_0$:

$$ R_0(v) \geq (\mathrm{pred}(v, D_1) - \mathrm{pred}(v, D_0)) + (\mathrm{pred}(v, D_2) - \mathrm{pred}(v, D_0)). $$

*Proof.* First, $(\mathrm{pred}(v, D_1) - \mathrm{pred}(v, D_0))((\mathrm{pred}(v, D_2) - \mathrm{pred}(v, D_0))$, respectively) is the number of edges of head $v$ added to $D_0$ by the composition $(D_0 \otimes_{\xi_1} C_1)((D_0 \otimes_{\xi_1} C_2)$, respectively) to obtain $D_1$ ($D_2$, respectively).

By Lemma 12.7, the pushout object of $o_1$ and $o_2$ is $D_0 \otimes_{\xi_1+\xi_2} (C_1 \oplus C_2)$. Suppose, contrary to the claim, that $R_0(v) < (\mathrm{pred}(v, D_1) - \mathrm{pred}(v, D_0))+(\mathrm{pred}(v, D_2) - \mathrm{pred}(v, D_0))$, for some $v \in V_0$. The composition $D_0 \otimes_{\xi_1+\xi_2} (C_1 \oplus C_2)$ would need to add to $D_0 \mathrm{pred}(v, D_1)$-
<figure><img src="image_27.png" /><figcaption>Figure 10: Pushout for sets of vertices.</figcaption></figure>

<figure><img src="image_28.png" /><figcaption>Figure 11: Pushout for drags.</figcaption></figure>

$pred(v, D_0)) + (pred(v, D_2) - pred(v, D_0))$ edges whose target is $v$. But $v$ is lacking roots for that purpose, so this is impossible. □

This implies that **Drag**s is not $\mathcal{M},\mathcal{N}$-adhesive, and hence is not $\mathcal{M}$-adhesive either. For being $\mathcal{M},\mathcal{N}$-adhesive, the category would need to have two designated classes of monomorphisms, $\mathcal{M},\mathcal{N}$, that, among other properties, should satisfy that **Drag**s has all pushouts along $\mathcal{M}$-morphisms and also along $\mathcal{N}$-morphisms, respectively. However, the above lemma shows that there is no class of monomorphisms $\mathcal{M}$ such that, if $o_1 \in \mathcal{M}$, then for any monomorphism $o_2$ with the same domain as $o_1$, $o_1$ and $o_2$ have a pushout, since the existence of this pushout depends on $o_2$. And the same happens for monomorphisms in $\mathcal{N}$. Therefore, we conclude:

**Theorem 12.9.** *The category *Drag*s* is neither *M*,*N*-adhesive nor *M*-adhesive.*

13. DISCUSSION

In the course of this study of graph rewriting, we have made a number of choices among alternatives, motivated by what seemed to us to be either more general and useful, or simpler and more convenient.

In Remark 2.6, we explained why we have chosen to consider multisets of roots, rather than lists as in [DJ19] or sets. This design choice impacted our definition of composition, for which we decided to maintain a strong invariant: the indegree of each individual vertex. We indeed tried an alternative, using root transfer as in [DJ19], which resulted in more complex technicalities that we were not able to resolve in a satisfactory manner. Root transfer considers roots as plugs waiting for a connection there, while indegree preservation considers roots as wires waiting for a connection at the other end.

Another issue is how to understand multiple instances of variables. We have already explained in Section 6.4 why we require equimorphism of the subdrags connected to different sprouts with the same label, rather than the weaker isomorphism suggested in [DJ19] or the stronger identity relation used in [DJ19]. We have also seen that this gives us the very helpful Lemmas 5.8 and 6.18. The latter is extremely important in that it allowed us to relate, in Section 12, two completely different notions of matching: the traditional one, matching as a monomorphism, and the new one, matching as a drag extension. This relationship is a major justification for the drag model. But is equimorphism the best possible answer?

In the remainder of this section, we hint at variations that may extend the capabilities of the drag model. First, we briefly discuss a more general definition of coherence of a set of wires. Second, and significantly, we consider how sharing can be improved by a definition of
rules allowing their left- and right-hand sides to share subdrags. Next, we suggest dropping
the fixed arity of labeled vertices, and consequently hint at a more flexible graph-rewriting
model for which sprouts and roots are particular cases of a more general notion of connector.

**13.1. Coherent sets of wires.** There is a slight potential for generalization here, replacing *equimorphism* by *sharing equivalence* in the definition of a coherent set of wires. This variant would require changes in the definition of monomorphisms so as to preserve Lemma 6.18, a change that should not impact Theorem 5.10 since isomorphisms preserve sharing equivalence. The computation of a product $L \otimes_{\xi} C$ can render two subterms of $L$ equimorphic, or even sharing equivalent, and they might then be shared in the resulting drag. As a consequence, matching would no longer be injective on internal vertices. Note that part of the DPO community uses non-injective matching, although in [HMP98a] it is shown that injective matching is more powerful. We won't explore that path here, but it is worth mentioning as a potential area of future investigation.

**13.2. Varyadic labels.** Drags were designed for generalizing terms and term rewriting. Accordingly, a vertex of a drag comes with a label equipped with a fixed arity that governs the number of successors of that vertex, a constraint that has not, however, been central to the theory of drags developed here. Extending the model to deal with arbitrary graphs is possible by relaxing the fixed arity constraint, allowing for bounded or even unbounded arities.

In the fixed-arity model, it is crucial that wiring does not change the number of outgoing edges at a vertex. It follows that only sprouts can be mapped to other vertices, implying that decomposing a drag into smaller pieces can only be done by cutting its edges.

This limitation disappears with varyadic arities. Thus an alternative would be to decompose drags by “slicing” apart vertices instead of cutting edges. The incident edges (regardless of direction) of the vertex are then split between the slices. Dissecting an internal vertex creates a new “snap”, along with the leftover “base” vertex. Composition (or wiring) connects then snaps with vertices, which may also be snaps. Decomposition of a drag into two is straightforward in this alternate model, as would be decomposition into single-edge atoms.

## 14. RELATED WORK

There are several competing approaches to graph rewriting, as already sketched in the introduction. Here, we list and discuss some of the more closely related proposals.

**14.1. DPO.** Introduced in the early seventies, the double-pushout (DPO) approach [EPS73] is the best studied and most popular approach to graph transformation. There are many varieties of graphs that may be of interest in different contexts. For example, one may work with directed or undirected graphs; they may be typed or untyped; they may be labeled, unlabeled, or include attributes that represent values stored in vertices or edges; they may be graphical structures like Petri nets or state-transition diagrams, or they even may be drags. It should be clear that studying graph rewriting separately for each kind of graph is a waste of time since there is almost no difference between rewriting a
directed or an undirected graph or any other kind of graphical structure. Using categor-
ical constructions allows the DPO approach to describe and study at one and the same
time rewriting for all manner of structures that satisfy some given properties. The DPO
approach is currently defined for any category of objects that is *adhesive* [EEPT06, LS06]
(or *M*-adhesive [EGH<sup>+</sup>14, EGH<sup>+</sup>12], or even *M*-*N*-adhesive [HP12]). This includes most
graph categories as well as other graphical structures, and other categories of objects, like
sets, bags, or algebraic specifications.

In Section 12, we showed that the DPO construction applies to drags as well, and can
be extended so as to be relational rather than functional. The definition of a rule $L \to R$ as
a single drag with left- and right-hand sides roots L and R as introduced at Definition 10.9
looks very much like a DPO rule, the subgraphs accessible from both L and R serving
as the interface. The only difference is that we do not force the rewriting extensions of
$L$ and $R$ to be identical, but rather to be compatible, which makes sense for concrete
graphs. A direct benefit of compatibility combined with a relational definition of rewriting
is that this extended version of DPO has a built-in ability for erasing and cloning subdrags.
Furthermore, drag rules can be nonlinear, on the left or right, while DPO rules are essentially
linear. We can therefore claim to have solved the problem of allowing nonlinear variables
in drag rewrite rules, a problem the importance of which was stressed already in [PEM86],
and which has remained unsolved since then, despite numerous attempts. Non-linearity
is permitted here by an appropriate definition of morphisms for drags with variables. We
believe that similar ideas should scale to graphs whose vertices can have varyadic labels,
along the lines suggested in Section 13.2. Making sense of nonlinear rules (and morphisms)
in the case of abstract graph categories might require additional nontrivial properties of
morphisms yet to be elaborated. This is likely to be nontrivial since we have seen that the
category of drags does not have any of the adhesivity properties that have been elaborated
along the years to make DPO work.

14.2. **Algebraic approaches.** Several other algebraic approaches, like Agree [HMP98b], PBPO [CDE<sup>+</sup>19], and PBPO<sup>+</sup> [OER21], have been defined to overcome some limitations of the DPO approach, such as the ability to erase or clone nodes. For us, cloning and erasing can be implemented by drag rewriting.

14.3. **Term graphs.** The literature on term graphs (graphs that represent terms having shared subterms) is extremely rich, as surveyed in [Plu99]. Since the presence of cycles is a distinctive feature of drags—as studied in this paper—we compare them here with term graphs admitting cycles.

The work of Barendregt et al. [BvEG<sup>+</sup>87] is essentially interested in showing that graph
rewriting faithfully implements term rewriting on finite and infinite trees. This turns out not
always to be the case, in particular because of sharing that inhibits some term derivations,
and because of infinite trees (obtained by unravelling graphs with a distinct root vertex).
The first reason holds likewise for the drags of [DJ19], as pointed out there, due to forced
sharing. It is shown in [BvEG<sup>+</sup>87], however, that faithfulness obtains for “weakly regular”
(left-linear, non-overlapping) rewrite systems. The proof uses complete developments, and
that’s where weak-regularity comes in by ensuring the absence of non-trivial critical pairs.
Left-linearity is crucial. The authors argue that it could be adapted to non-left-linear rules,
but would then require forced sharing to reflect non-left-linear rules, so, the problem would
remain for non-linear systems. They also assert that a relaxed equality (instead of identity implied by forced sharing) should also be possible, but that this would require changing their definition of a graph with variables (which is inherently linear).

Example 3.8(v) in [BvEG$^+$87] demonstrates that in their formalism rewriting the cyclic graph $G = v : I(v)$ with the rule $I(x) \to x$ yields $G$ again. In our setup, this is the case when there is no right-hand side extension (the switchboard is not well-behaved), so $G$ does not rewrite. The phenomenon is indeed the very same, since the computation of a product with a non-well-behaved switchboard would cycle if allowed; hence the computation of $G$ is non-terminating in both cases.

In the work of [CG99b], graphs are arbitrary, with a list of variables and a list without repetition of rooted vertices. Variables are ignored for defining morphisms. Composition is defined by gluing sprouts and roots (in one direction: switchboards are one-way only) of the same index, provided they are in equal number. This is a very restricted mechanism compared to ours. Feedback is the gluing of the last variable with the last root of a graph, provided they are in equal number. Rules are acyclic graphs with two roots, $l$ and $r$. The rule format is therefore more general than Barendregt's, but still quite limited with respect to drags.

So, our model is much more expressive than other term graph formalisms: non-linear possibly cyclic left-hand sides, powerful composition operator, morphisms taking care of variables, whether linear or non-linear, absence of dangling edges, and adequacy of drag rewriting for non-linear term rewriting in this strictly more powerful formalism.

### 14.4. Patches.
A framework similar to ours has been recently developed by Overbeek and Endrullis [OE20], but which is designed for graphs whose vertices have variable arity. For composition, they employ “patches”—a device similar to our switchboard, which adds connecting edges between the two components. Likewise, they have an analogue to roots cum sprouts (rather like the snaps suggested in Section 13.2), which allows one to constrain the permitted shapes of subgraphs around a match for a left-hand side, and also to specify how the subgraphs should be transformed. Transformations include rearrangement, deletion, and duplication of edges. PBPO$^+$ [OER21], which was developed in a categorical framework, can be seen as a conceptual successor to patches and has been proposed as a unifying notion.

### 14.5. Graphs with interfaces.
The idea of building graphs using some kind of composition operation, by gluing some selected nodes of the graphs involved, which are considered interfaces, is already quite old, going back to the work of Bauderon and Courcelle [BC87]. In the context of DPO, graphs with interfaces and their transformation have been studied by Bonchi, Corradini, Gadducci, and their colleagues; see, among others, [CG99a, Gad07, BGK$^+$17]. The main difference is that they only consider sequential composition; they don't consider the possibility that sprouts of one drag are connected to roots of another *and* vice versa. In our terms, this means that in this case composition is limited to *one-way switchboards* [DJ19].
**14.6. String diagrams.** String diagrams are a restricted graphical syntax for representing computational models used in various fields, including programming language semantics, circuit theory, and control theory. Mathematically, string diagrams are the terms of symmetric monoidal theories, which generalize algebraic theories in a way that makes them suitable for expressing resource-sensitive systems in which variables cannot be copied or discarded at will. String diagrams enjoy a restricted composition operator in the sense that it is based on one-way switchboards (as in [CG99b]). Rewriting of string diagrams is defined as a specific instance of DPO rewriting with interfaces (DPOI), called convex rewriting, for a category of labeled hypergraphs that correspond to string diagrams [BGK$^{+}$22a, BGK$^{+}$22b].

**15. CONCLUSION**

In this work, we have completely revamped the preliminary drag model of [DJ19]. In particular, the arrangement of roots in this work is much more useful, variables provide much more flexible sharing, the notion of rewriting rule is much more general, and we end up with a much better algebra. Repeated (nonlinear) variables are used to restrict matches to equimorphic subgraphs. Distinct drags may now share vertices, which is economical when rewriting. The proposed model encompasses term rewriting as a special case, in stark contrast to the prior work. Composition is facilitated by a new notion of step-by-step wiring of connections from sprouts to roots. We have also developed a pleasing algebra of drags with sum and product. These advances are supported by new, original notions of morphisms for drags, which allow us to precisely relate drag rewriting based on composition with drag rewriting based on DPO, and even to slightly generalize DPO when applied to drags. We observe that seemingly minor changes in the details of the formalism have had far-flung effects and have required significant effort to put all the pieces together in place. In this respect, indegree preservation happened to be the key property that made it possible.

The drag framework was conceived so as to apply to a specific category of graphs, namely drags, and to generalize the standard term rewriting and dag models to drags. As a consequence, drags are graphs equipped with specific vertices, called sprouts, labeled with variables, while the other, internal vertices are labeled by function symbols equipped with an arity that specifies the number of their outgoing edges. In addition, vertices are equipped with roots that provide them with the potential for creating new edges.

The major originality of the drag model is to base the matching of a given drag *D* with respect to a left-hand side of rule *L* on the existence of a pair made of a context drag *C* and a switchboard $\xi$ such that *D* is the product of *L* and *C* with respect to $\xi$. In this view, the switchboard $\xi$ maps a sprout *s* of each drag to a rooted vertex *r* of the other drag, provided *r* has at least as many roots as the number of incoming edges and roots of *s*. Computing the product amounts to redirecting to *r* all edges incoming to *s* and removing from *r* an equal number of roots, an operation that leaves the indegree of *r* unchanged. Rewriting amounts then to replacing *L* by *R*, that is, to computing the new drag resulting from the product of the context *C* with the right-hand side *R* with respect to the switchboard $\xi$. This assumes the existence of an injective mapping from the roots of *L* to the roots of *R*.

We have indeed succeeded, inasmuch as our new drag model appears to generalize the term and dag rewriting models very smoothly, something that our former drag model [DJ19] could not do. Furthermore, it even generalizes the term and dag rewriting models when applied to terms and dags by having two new built-in capabilities: sharing and cloning.
By this we mean that we are able to specify formally at each rewrite step which subdrags should be shared and which should be duplicated.

The most widely accepted and used graph-rewriting model is DPO. While DPO was conceived so as to apply to various categories of graph structures, namely the adhesive categories, its expressivity is limited by the absence of variables, one consequence of which is the infeasibility of cloning. Furthermore, we have seen that drags lack some categorical properties that are essential for applying DPO, properties whose absence follows from the preservation of indegrees by monomorphisms. We could of course weaken that property so that indegrees could grow along monomorphisms, but the price to pay would be heavy: The two different views of matching, by the existence of a monomorphism as for DPO and by the existence of a rewriting extension of the left-hand side of rule, as for drags, would no longer coincide.

A natural question then follows: Can graphs be equipped with variables, and can these variables be used within the DPO model? This question was actually raised long ago [PEM86], but to date no satisfactory answer has been proffered [Hof05], despite several attempts, most notably that of [HP96]. We have given here a general answer to that question for the category of drags, thanks to the drag’s notion of a variable being a one-way channel, to the notion of switchboard—which allows one to compose graphs in a very general way, and to a notion of morphism (and monomorphism) for non-ground drags. Matching a left-hand side of rule can then be defined either via composition or via the existence of a monomorphism in the obtained category, while rewriting can be defined by replacement or by a double pushout. Moreover, a slight generalization of DPO is suggested that inherits the cloning and sharing capabilities of composition based drag rewriting.

Even more interesting are the following related questions: Can composition be defined for arbitrary graphical structures, or—more precisely—for arbitrary objects belonging to some adhesive category? Is adhesivity required for that purpose? Are variables needed for that purpose?

## REFERENCES

[BC87] Michel Bauderon and Bruno Courcelle. Graph expressions and graph rewritings. *Math. Syst. Theory*, 20(2-3):83-127, 1987. doi:10.1007/BF01692060.

[BGK$^{+}$17] Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and Fabio Zanasi. Confluence of graph rewriting with interfaces. In Hongseok Yang, editor, *Proceedings of the 26th European Symposium on Programming (ESOP), Held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Uppsala, Sweden*, volume 10201 of *Lecture Notes in Computer Science*, pages 141-169. Springer, 2017. doi:10.1007/978-3-662-54434-1_6.

[BGK$^{+}$22a] Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: Rewriting with Frobenius structure. *Journal of the ACM*, 69(2):14:1-14:58, 2022. doi:10.1145/3502719.

[BGK$^{+}$22b] Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: Rewriting with symmetric monoidal structure. *Math. Struct. Comput. Sci.*, 32(4):511-541, 2022. doi:10.1017/S0960129522000317.

[BvEG$^{+}$87] Henk P. Barendregt, Marko C. J. D. van Eekelen, John R. W. Glauert, J. Richard Kennaway, Marinus J. Plasmeijer, and Michael R. Sleep. Term graph rewriting. In *Parallel Architectures and Languages Europe (PARLE)*, volume 259 of *Lecture Notes in Computer Science*, pages 141-158, Berlin, January 1987. Springer.

[CDE$^{+}$19] Andrea Corradini, Dominique Duval, Rachid Echahed, Frédéric Prost, and Leila Ribeiro. The PBPO graph transformation approach. *J. Log. Algebraic Methods Program.*, 103:213-231, 2019. doi:10.1016/j.jlamp.2018.12.003.
[CG99a] Andrea Corradini and Fabio Gadducci. An algebraic presentation of term graphs, via gs-monoidal categories. *Appl. Categorical Struct.*, 7(4):299-331, 1999.
doi:10.1023/A:1008647417502.

[CG99b] Andrea Corradini and Fabio Gadducci. Rewriting on cyclic structures: Equivalence between the operational and the categorical description. *Theoretical Informatics and Applications*, 33(4/5):467-493, 1999.

[Cou90] Bruno Courcelle. Graph rewriting: An algebraic and logic approach. In *Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics*, pages 193-242. Elsevier, 1990.

[Cou93] Bruno Courcelle. Graph rewriting: A bibliographical guide. In Hubert Comon and Jean-Pierre Jouannaud, editors, *Term Rewriting, French Spring School of Theoretical Computer Science, Font Romeux, France, May 17-21, 1993, Advanced Course, volume 909 of Lecture Notes in Computer Science*. Springer, 1993. URL: https://www.labri.fr/perso/courcell/Textes/BiblioReecritureGraphes(1995).pdf, doi:10.1007/3-540-59340-3_6.

[CS18] Horatiu Cirstea and David Sabel, editors. *Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@FSCD 2017, Oxford, UK, September 2017*, volume 265 of EPTCS, 2018. URL: http://arxiv.org/abs/1802.05862.

[DJ90] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In *Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics*, pages 243-320. Elsevier, 1990.

[DJ18] Nachum Dershowitz and Jean-Pierre Jouannaud. Graph path orderings. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, *22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-22)*, volume 57 of EPiC Series in Computing, pages 307-325. EasyChair, 2018. URL: https://easychair.org/publications/paper/8DzT, doi:10.29007/6hkk.

[DJ19] Nachum Dershowitz and Jean-Pierre Jouannaud. Drags: A compositional algebraic framework for graph rewriting. *Theoretical Computer Science*, 777:204-231, 2019. doi:10.1016/j.tcs.2019.01.029.

[EEPT06] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. *Fundamentals of Algebraic Graph Transformation*. Springer, 2006.

[EGH<sup>+</sup>12] Hartmut Ehrig, Ulrike Golas, Annegret Habel, Leen Lambers, and Fernando Orejas. *M*-adhesive transformation systems with nested application conditions. Part 2: Embedding, critical pairs and local confluence. *Fundam. Inform.*, 118(1-2):35-63, 2012. doi:10.3233/FI-2012-705.

[EGH<sup>+</sup>14] Hartmut Ehrig, Ulrike Golas, Annegret Habel, Leen Lambers, and Fernando Orejas. *M*-adhesive transformation systems with nested application conditions. Part 1: Parallelism, concurrency and amalgamation. *Math. Struct. Comput. Sci.*, 24(4):e240406, August 2014. doi:10.1017/S0960129512000357.

[EPS73] Hartmut Ehrig, Michael Pfender, and Hans Jürgen Schneider. Graph-grammars: An algebraic approach. In *14th Annual Symposium on Switching and Automata Theory, Iowa City, IA*, pages 167-180. IEEE Computer Society, October 1973. URL: http://dx.doi.org/10.1109/SWAT.1973.11, doi:10.1109/SWAT.1973.11.

[Gad07] Fabio Gadducci. Graph rewriting for the π-calculus. *Math. Struct. Comput. Sci.*, 17(3):407-437, 2007. doi:10.1017/S096012950700610X.

[Hin69] J. Roger Hindley. An abstract form of the Church-Rosser Theorem. I. *J. Symb. Log.*, 34(4):545-560, 1969. doi:10.1017/S0022481200128439.

[HKP91] Annegret Habel, Hans-Jörg Kreowski, and Detlef Plump. Jungle evaluation. *Fundam. Inform.*, 15(1):37-60, 1991.

[HMP98a] Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout approach with injective matching. In Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors, *Theory and Application of Graph Transformations, 6th International Workshop, TAGT'98, Paderborn, Germany, November 16-20, 1998, Selected Papers*, volume 1764 of Lecture Notes in Computer Science, pages 103-116. Springer, 1998. doi:10.1007/978-3-540-46464-8_8.

[HMP98b] Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout approach with injective matching. In Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors, *Selected Papers of the 6th International Workshop on Theory and Application of Graph Transformations*, 2008. doi:10.1007/978-0-3-540-46464-8_9.
*Transformations (TAGT '98), Paderborn, Germany*, volume 1764 of *Lecture Notes in Computer Science*, pages 103–116. Springer, November 1998. doi:10.1007/978-3-540-46464-8_8.

[Hof05] Berthold Hoffmann. Graph transformation with variables. In Hans-Jörg Kreowski, Ugo Montanari, Fernando Orejas, Grzegorz Rozenberg, and Gabriele Taentzer, editors, *Formal Methods in Software and Systems Modeling, Essays Dedicated to Hartmut Ehrig, on the Occasion of His 60th Birthday*, volume 3393 of *Lecture Notes in Computer Science*, pages 101–115. Springer, 2005. doi:10.1007/978-3-540-31847-7_6.

[HP96] Annegret Habel and Detlef Plump. Term graph narrowing. *Math. Struct. Comput. Sci.*, 6(6):649–676, 1996.

[HP12] Annegret Habel and Detlef Plump. *,-adhesive transformation systems. In Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors, *Proceedings of the 6th International Conference on Graph Transformations (ICGT)*, Bremen, Germany, volume 7562 of *Lecture Notes in Computer Science*, pages 218–233. Springer, 2012. doi:10.1007/978-3-642-33654-6_15.

[HT18] Reiko Heckel and Gabriele Taentzer, editors. *Graph Transformation, Specifications, and Nets – In Memory of Hartmut Ehrig*, volume 10800 of *Lecture Notes in Computer Science*. Springer, 2018. doi:10.1007/978-3-319-75396-6.

[JO23] Jean-Pierre Jouannaud and Fernando Orejas. Unification of drags and confluence of drag rewriting. *Journal of Logical and Algebraic Methods in Programming*, 131:100845, February 2023. doi:10.1016/j.jlamp.2022.100845.

[KB70] Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, *Computational Problems in Abstract Algebra*, pages 263–297. Pergamon Press, 1970.

[LS06] Stephen Lack and Paweł Sobociński. Adhesive categories. In Igor Walukiewicz, editor, *Foundations of Software Science and Computation Structures (FOSSACS'04)*, Lecture Notes in Computer Science, pages 273–288, Berlin, 2006. Springer.

[MM90] José Meseguer and Ugo Montanari. Petri nets are monoids. *Inf. Comput.*, 88(2):105–155, 1990. doi:10.1016/0890-5401(90)90013-8.

[MMS97] José Meseguer, Ugo Montanari, and Vladimiro Sassone. Representation theorems for Petri nets. In Christian Freksa, Matthias Jantzen, and Rüdiger Valk, editors, *Foundations of Computer Science: Potential – Theory – Cognition, to Wilfried Brauer on the Occasion of his Sixtieth Birthday*, volume 1337 of *Lecture Notes in Computer Science*, pages 239–249. Springer, 1997. doi:10.1007/BFb0052092.

[OE20] Roy Overbeek and Jörg Endrullis. Patch graph rewriting. In *The 13th International Conference on Graph Transformation (ICGT 2020)*, volume 12150 of *Lecture Notes in Computer Science*, pages 128–145. Springer, 2020.

[OER21] Roy Overbeek, Jörg Endrullis, and Aloïs Rosset. Graph rewriting and relabeling with PBPO+. In *Proceedings of the 14th International Conference on Graph Transformation (ICGT)*, pages 60–80, Berlin, June 2021. Springer. Held as Part of STAF 2021, Virtual Event. doi:10.1007/978-3-030-78946-6_4.

[PEM86] Francesco Parisi-Presicce, Hartmut Ehrig, and Ugo Montanari. Graph rewriting with unification and composition. In Hartmut Ehrig, Manfred Nagl, Grzegorz Rozenberg, and Azriel Rosenfeld, editors, *Proceedings of the 3rd International Workshop on Graph-Grammars and Their Application to Computer Science, Warrenton, VA*, volume 291 of *Lecture Notes in Computer Science*, pages 496–514. Springer, December 1986. doi:10.1007/3-540-18771-5_72.

[PH94] Detlef Plump and Annegret Habel. Graph unification and matching. In Janice E. Cuny, Hartmut Ehrig, Gregor Engels, and Grzegorz Rozenberg, editors, *Selected Papers of the 5th International Workshop on Graph Grammars and Their Application to Computer Science, Williamsburg, VA*, volume 1073 of *Lecture Notes in Computer Science*, pages 75–88. Springer, November 1994. doi:10.1007/3-540-61228-9_80.

[Plu99] Detlef Plump. Term graph rewriting. In H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozenberg, editors, *Handbook of Graph Grammars and Computing by Graph Transformation*, volume 2: Applications, Languages and Tools, pages 3–61. World Scientific, Singapore, 1999. URL: https://www.cs.york.ac.uk/plasma/publications/pdf/Plump.Handbook.99.pdf.