### Confluence in Graph Rewriting

#### Posted by John Baez

*guest post by Anna Matsui and Innocent Ob*

In this blog post we discuss the main (‘algebraic’) ideas of term rewriting and how they can be applied to term graph and
arbitrary graph (i.e. string diagrams) rewriting. Our group was
interested in the application of critical pairs for string diagram
rewriting. We read Detlef Plump’s *Critical Pairs in Term Graph Rewriting* and given the task before us wanted to understand the following question: if Plump needed a new decision procedure for critical pairs in graph rewriting, how would we know what we might need for string diagram rewriting? In the this blog post we start at the root (pun intended) and work our way up from term rewriting to rewriting on arbitrary graphs. The goal is to understand, for example, why we can’t just apply, without modification,
the ideas in Plump’s paper to rewriting in the *λ*-calculus. This post is aimed at an audience unfamiliar with term rewriting and presents foundational ideas and results to set the stage for (old and more) recent categorical applications.

**I. Preliminaries**

**I.a On theories, signatures, and terms**

A theory can be thought as a “finite or an infinite set of formulas
characterized by common grammatical rules, allowed functions and
predicates, and a domain of values. Example of theories include propositional logic, equality, linear arithmetic, bit vectors. These are examples of first-order (FOL) theories. We can also have higher-order theories . First order logic (FOL) is based on
the following four elements: variables, logical symbols (boolean
connectives and quantifiers), non-logical symbols (functions,
predicates, constants), and syntax (rules about constructing valid
formulas in the logic). Typically, a theory defines restrictions on the
non-logical symbols. This set of **non-logical symbols** is called the
**signature**. With a signature *Σ*, A *Σ*-formula is constructed using
only non-logical symbols from *Σ*. A first-order *Σ*- theory T consists
of a set of *Σ*-sentences. In the case of rewriting systems, the only
logical symbol we care about is equality. Said differently, with
rewriting systems it makes sense to restrict not only the set of
non-logical symbols, but also logical symbols. Such a restriction exists
in the **equality logic**. It is the quantifier-free fragment of FOL
with equality as the singular logical symbol.

**Definition 1** (Signature). A *signature* *Σ* consists of non-empty set of
*function symbols* each equipped with a fixed *arity*. The arity of a
function symbol *F* is a natural number, indicating the number of
arguments it is supposed to have. Nullary functions are allowed: these
are called *constant symbols*.A term is a string of symbols from an
alphabet consisting of the signature and a countably infinite set, *Var*,
of variables. The set of terms over *Σ* is indicated as
$\mathcal{F}$(*Σ*, *Var*). All variables and functions are terms.

**I.b On abstract reduction systems**

More generally, we can view term rewriting systems as instances of an abstract reduction system.

**Definition 2** (Abstract Reduction System). An abstract reduction systems is a pair $(A, \rightarrow)$, where $\rightarrow$ is a binary relation on the set $A$, i.e $\rightarrow \subseteq A \times A$.

In an abstract reduction system, the relation → can
represent a program evaluation
(*a*_{0} → *a*_{1}⋯*a*_{n}) or
identities (*a*_{0} ← *a*_{1}⋯ → *a*_{2}⋯). The
former describes some directed computation from one element to another. The latter implies the *reflexive transitive symmetric closure* ($\xleftrightarrow{\text{\*}}$): there exists some finite path the first term to the second and vice versa. By closure we use the common description : the *P* closure of *R* is the least set with the property *P* which contains *R*. So the $\xleftrightarrow{\text{\*}}$ is the least reflexive transitive symmetric relation which contains →. Given two terms *x* and *y*, we say that *X* is **reducible** if and only if there is a *y* such that *x* → *y*. *x* is in **normal form** if it is
not **reducible**. *y* is a **normal form** of *x* if y is in normal
form and there exist some finite path from *x* to *y*, i.e
$x \xrightarrow{\text{\*}} y$. *x* and *y* are **joinable** (*x* ↓ *y*) if there is a *z* such that $x \xrightarrow{\text{\*}} z \xleftarrow{\text{\*}} y$.

**Definition 3** (Terminating, Confluent). *A reduction → is called:

*terminating*iff there is not infinite descending chain $x_0 \rightarrow x_1 \rightarrow \cdots$*confluent*iff $x \xrightarrow{\text{\*}} z \xleftarrow{\text{\*}} y \implies x\downarrow y$*

Whether a string, term, or graph, rewriting system are mechanisms for computing stepwise transformations of objects. A term rewriting systems (TRS) is an abstract reduction system where the objects are first-order terms and where the reduction relation is presented as reduction or rewrite rules. The canonical term rewriting systems were viewed as decision procedures for proving the validity of equalities in first-order equational theories.

**I.c Term rewriting and all that!**

**Definition 4** (Term Rewriting System). A rewrite or reduction rule is an identity $l \equiv r$ where $l$ is not a variable and all the varialbles in $r$ are also in $l$. A term rewriting system is a set of a pairs consisting of the set of rewrite rules and a $\Sigma$ definition the non-logical symbols of the grammar.

How do we know when any two arbitrary terms (from some grammar) are
equivalent and why should we care if any two terms are equivalent? One
approach to answer this question is start from both terms and search
exhaustively search until we find term in a set of finite paths that
’generalizes’ the two terms - a process akin to anti-unification. The
other would be to use a set of rules to reduce both terms to their
normal forms and then testing that those normal forms are
joinable/equivalent - akin to unification. This is the task of
confluence tests. From this description, its clear that it is
difficult to prove confluence if our reductions steps never terminate.
Therefore its intuitive that termination is necessary to prove
confluence. This is in essence what we learn about term rewriting
systems: *confluence is undecidable for non-terminating term rewrite
systems*. However we find that in term graph rewriting, it is possible
to take a non-terminating term rewriting system and transform it into a
terminating term-graph rewrite system! For now, before we return to our
discussion on confluence, let’s introduce term rewriting and term graph
rewriting more formally using the universal algebra we presented
above.

**II. Context, overlaps, and critical pairs**

In term rewriting, a position in a term $t$ detemines both a prefix of $t$, i.e holes and the occurrence of the subterm with the prefix. The prefix of t that corresponds to p is denoted by $t[ ]_p$, the subterm occurring at position $p$ by $t|_p$. When rewrites occur they occur in some context.

$\begin{array}[t]{ccc} t = f_{1}(g_{2}(a_{3})) & t[]_2=f_{1}(\Box(a_{3})) & t|_{2} = g \\ \end{array}$

**Definition 5** (Context). A context is a term containing zero, one or more occurrences of a special constant symbols $\Box$ denoting holes, a term over the extended signature $\Sigma \cup \lbrace \Box \rbrace$. If $C$ is a context containing exactly n holes, and $t_1,\cdots,t_n$ are terms, then $C[t_1,\cdots,t_n ]$ denotes the result of replacing the holes of $C$ from left to right by $t_1,\cdots,t_n$ . To distinguish between difference occurrence of a sub term in a term we adopt a definition of occurrence. We define an occurrence as the ordered pair $\langle s | C[] \rangle$. This uniquely determines the occurrence of $s$ in $C[s]$ with the one-hole context $C[]$. That is every occurrence of the sub-term can be replaced by a one-hold context. For a given term $s$ this new term $s^'$ with holes can be called the prefix of $s$.

**Definition 6** (Reduction Step). A $\textit{reduction step}$ according to the reduction rule $p: l \rightarrow r$ consists of contracting a redex within an arbitrary context:

Given a reduction rule *p*, an instance of *p* is obtained by applying a
substitution *σ*. The result is an *atomic reduction step*
$l^{\sigma} \xrightarrow{p} r^{\sigma}$. The left-hand side
*l*^{σ} is called the **redex** and the right-hand side
*r*^{σ} is called its **embedding**. A term may contain one or
more occurrences of a redex. A reduction step consists of *contracting*
a redex within an arbitrary context.

**Example 1**. Given rule $p : F(G(x),y) \rightarrow F(x, x)$ and substitution $\sigma : \lbrace x \rightarrow 0, y \rightarrow G(x) \rbrace$, we get the following reduction step:

with redex $F(G(0), G(x))$, and embedding $F(0,0)$. With a term $F(z, G(F(G(0), (G(x)))))$ and the contraction describe above, we get the following reduction step

where the context is $F(z, G(\Box))$.

The contraction of redex can lead to some interesting and uninteresting conflicts. Non-confluence can usually be attributed to the specific case of conflicts : the overlapping of reductions. Remember that redexes depends on some rewriting rule and some substitution of terms. In order to understand if a TRS is confluent it is important to know when such overlaps are harmful or harmless. In general, a redex is harmful it is overlaps. The following example will illustrate this case:

**Example 2**. Consider the TRS with the following rules:

The term $F(G(a), x)$ can be reduced in two ways: $F(G(a),x) \xrightarrow[p]{} a$ and $F(G(a),x) \xrightarrow[p]{} F(b,x)$, where terms $a$ and $F(b,x)$ are normal forms. The following TRS is not confluent as $a$ and $F(G(b,x))$ have no common reduct. The reductions rules and substitutions give use the two redexes: $F(G(a),x)$ and $G(a)$. Both redexes share the function symbol $G$ in both. This sharing means that a contraction using the second rule $\textit{destroys}$ $G$ thus making it impossible to apply $p_1$. Each of the left-hand side of the rules on matches (redex) expresses in many ways the $\textit{context}$ of the rewriting. This say that the TRS does not support rewriting in arbitrary contexts in a way that preserves confluence. We need to find the redexes that cause these conflicts and use them to generate additional rules that allow us to reach a common reduction. This is known as completion or is the more operational contexts $\textit{saturation}$.

Again overlap result when symbols are shared between any two redexes. We do this by defining a $\textit{pattern}$ of a redex as the fixed part of the left-hand side. The result is a $\textif{prefix}$ of the redex where all its variables are left out, i,e a potential many-hole context. It is the context that is created by replacing all variables in the redex with holes. So to be more precise, two redexs overlap when their patterns share a symbol occurrence.

**II.a Redex considered harmful?**

However, it is not the case that all overlaps of redexes are harmful.
Some overlaps may occur after one-step reductions, but may be unified
after a finite number of steps. This is the difference between
*confluence* and *local confluence*. Another way to say this is that
local confluence can also be a sufficient criterion for confluence of a
term rewriting system (TRS). This allow us to understand confluence of a
TRS by thinking of how overlapping redexes over a number of steps/paths
are contracted. From the definition described above this requires
considering how holes in context can be substituted to preserve the
pattern between two redexes. But there are potentially infinitely many
possible substitutions and infinitely many cases of redex overlaps
accordingly. Operationally, we need an efficient method of proving
confluence that doesn’t require searching over the entire space of
substitutions. The idea here is to associate each pair of overlapping
redex rules with a more general cases of an overlap from which other
cases can be generated. In literature this is exactly where *critical
pairs* play a role.

The key idea behind critical pairs is the following: all overlapping
redexes can be treated as substitution instances of some general
pattern. Using our definition of confluence given in Section V on
abstract rewriting systems: a TRS is confluent if all of its critical
pairs are *joinable*.

**Definition 7** (Critical Pair). Let $p_i: l_i\rightarrow r_i$, $i = 1,2,$ be two rules whose variables have been renamed such that $\mathcal{V}ar(l_1,r_1) \cap \mathcal{V}ar(l_2,r_2) = \emptyset$. A pair of one-step reductions $\langle \theta r_{1}, \theta l_{1}[\theta r_2]_p \rangle$ is a **critical pair** if

Let $p \in \mathcal{P}os(l_1)$ such that $l_{1}|_{p}$ is not a variable

$\theta$ be an maximum unifier of $l_{1}|_{p} =^{?} l_{2}$.

This is a definition and constraint will come up again in confluence decision procedures in term graph rewriting. But before we get into the similarities let stalk a little but about the different between trees and graphs as applied to terms rewriting.

**II.b Structure and Contents (from Trees to Graphs)**

**Figure 1:**

The structure of a term can be represented by visualizing it as a tree
where function symbols are nodes are arrows point to arguments of the
function. There is a function node with no arrows point to it: we call
this node the **root node**. Except these are not your simple trees. We
require trees with a labeling and numbering on nodes. The numbering give
is a terms **position** in the tree. Formally, the **position** is a
string over the alphabet of positive integers where the root position
(the root node) is the empty string. Labelling is necessary to
distinguish between similar (isomorphic) trees. This is all to say is
that our classical *tree* is just a labelled rooted undirected graph.
The tree as a data structure captures the content of a term in node
labels. Instead of labelling the arrows between nodes, our labeling
rests with the node. What this does is to leave all information about
the *content* and *structure* of terms in the nodes. We can distinguish
the two trees in Figure 2b because testing for
equivalence is based on both its *position* and *node label*. However,
computationally this is an expensive representation of terms. In Figure
2a we have a situation where we
have a duplicated term. It would be more efficient to just *share*
references to this term rather than duplicating it. But this simple
approach would be problematic in this model. This is because our node
label contains information on both the *content* and *structure* of the
terms. So even if we see the term *b* at multiple levels in our tree,
they are indeed not equivalent. This is because our test of equivalence
would have to take into account both the *position* and
the *node* label. In order to actually share references, we need
to decouple *structure* from *content*. We
need to move information about the *position* to the graph level. In
this approach, our *position* or *numbering of nodes*
would now be attached to the arrows or edges. We would also need to
require that all isomorphic subtrees be replaced by only ‘one’ amounting
to an equivalence class of nodes each considered as a node. This process
would turn our previously rooted undirected graph into a directed
acyclic graph. One of the really interesting things about moving from
the former to a DAG is that what were once previously non-terminating
TRS can now become terminating. This has noting to do with our signature
and everything to do with the choice of a DAG.

In the next section we discuss the paper by Detlef Plump called
*Critical pairs in term graph rewriting*. The goal of this paper is to
understand how much of the work describe above for critical pairs that
is used in term rewriting (with trees) can apply to rewriting on graphs.
Before we move on let just review some keys points.

we are still working with first-order terms in a qualifier-free fragment of first-order logic:

*equality logic*We’ve moved from (simple trees) to graphs: Our signature has not changed just the data model used to represent terms

Our use of a DAG allows the use of references to used instead of duplicated nodes. Although, we will need to generalize our graph by removing the restrict that each edge have only two vertices (endpoints). That is we need to move from just the generic graph to the hypergraph.

**III. Algebraic graph transformation and Plump’s (strong) joinability**

There are two way of approaching graph rewriting. In many ways they
mirror term rewriting (matching, deleting, copying). However as we
discussed above the context is different. Our context is not a *strings
with a holes* but *graphs with holes*. This can be best visualized in the
algebraic approach to graph transformation via *pushouts*. Pushouts
are to graphs what syntactic unification and contraction are to term
rewriting (on trees). We will define the pushout approach in a bit but
first a bit about hypergraphs. In the previous section, we highlighted
how we can move from trees to graphs (DAGs). For term graph rewriting,
we will generalize graphs even further and use the notion of a
*hypergraph*. In a hypergraph unlike simple graphs, edge (called
hyperedges) can have multiple targets. The formal definition is as
follows:

**Definition 8** (Hypergraph). *A hypergraph G over* *Σ*, *X* is a
system
*G* = (*V*_{G}, *E*_{G}, *s*_{G}, *t*_{G}, *l*_{G})
where *V*_{G}, *E*_{G} are finite sets of nodes
(vertices) and hyperedges,
*s*_{G} : *E*_{G} → *V*_{G},
*t*_{G} : *E*_{G} → *V*_{G}^{*}
are mappings that assign a source and a list of target nodes to each
hyperedge, and *l*_{G} : *E*_{G} → *Σ* ∪ *X* is a
labelling map such that
**arity** (*l*_{G}(*e*)) = **length**(*t*_{G}(*e*)).

This again is a choice of implementation. With a hypergraph, we drop the restriction that edges must have only two end points. To capture this structure, our morphisms are also a bit different. Instead of relation on terms in a tree, our morphisms are between graphs.

**Definition 9** (Graph Morphism). A *graph morphism* *f* : *G* → *H*
between graphs *G* and *H* consists of two functions
*f*_{V} : *V*_{G} → *V*_{H} and
*f*_{E} : *E*_{G} → *E*_{H} that preserve
the labels and targets of nodes,
*l*_{H} ∘ *f*_{E} = *l*_{G} and
*t*_{H} ∘ *f*_{E} = *f*_{V}^{} ∘ *t*_{G}.
If this *f* is injective and surjective, then it is an *isomorphism* and
*G* and *H* are *isomorphic*.

In the algebraic/categorical approach, working with isomorphism classes
of term graphs would cause us to lose access to nodes and edges.
Instead, Plump uses *standard term graphs* which represent their
isomorphism classes of of those node. In order to do this we introduce
the notion of *access path*. An access path for a node *v* in term graph
*G* is a possible empty sequence of labels representing a path from the
root to v. For example, the access path
⟨*i*_{1}, *i*_{2}, ⋅*i*_{n}⟩ indicates that
following path exists
⟨*v*_{0}*i*_{1}, *v*_{1}, *i*_{2}, *v*_{2}, ⋅*i*_{n}, *v*⟩
where *v*_{0} = *root* and *v*_{n} = *v*. The
set of all access paths is denoted *Acc*(*v*). For every term graph
we can construct an isomorphic standard term graph by replacing each
node *v* with *Acc*(*v*) and modifying the edge set and the labeling
and target functions correspondingly. We will call a graph *H* a
*collapsed* version of *G*, if there is a surjective graph morphism
*f* : *G* → *H* such that
*f*_{v}(*root*_{G}) = *root*_{H}.
This is usually denoted ≥ and the inverse (copying) is denoted as ≤. A term graph is a tree if there is only a unique path from the
root to each other node and it is fully collapsed if and only if for all
nodes *v* and *w*, equality of the terms representing nodes*v* and *w*
implies that node *v* and *w* are equal.

Using the definitions of term rewriting given, we will now define term graph rewriting.

**III.a Instance, redex, and context**

**Definition 10** ((Hyper-)graph Rewriting System). A *hypergraph
rewriting system* *⟨**Σ*, ℛ⟩ consists of a signature *Σ* and a set of ℛ of
rules over *Σ*.

When proving confluence in hypergraphs, the goal is to find *isomorphic
graphs*. It is a view of confluence that considers hypergraphs
transformation “up to isomorphism”.

**Lemma 1**. A hypergraph transformation systems ⟨*Σ*, ℛ⟩ is
confluence (locally confluent) if and only if the relation ⇒_{ℛ}
on isomorphism classes of hypergraphs over *Σ* is confluent (locally
confluent). Additionally the system ⟨*Σ*, ℛ⟩ is terminating if
⇒_{ℛ} is terminating.

Using the same language we used for term rewriting, given a node *v* in
the term graph *G* and a term rewrite rule *l* → *r*, the pair
⟨*v*,,*l* → *r*⟩ is our redex if the term subgraph at *v* in *G* is an
instance of *l*. While term rewriting systems have *reduction rules*, in
term graph rewriting we have similar ideas except in a new context. As
previously mentioned, in a graph system a rewrite rule is morphism
between (hyper-)graphs. These morphisms are mappings between the sets of
nodes and edges that they preserve sources, targets, and labels.
Similarly in term rewriting systems, we have reductions steps. In term
graph rewriting we have the corresponding graph transformations -
evaluations steps. Evaluation steps create *derivations*. When we apply
a rewrite rule to a graph, the core idea is to identify the subgraph
corresponding to the left-hand side of the rewrite, “cut it out”,
replace it with the right-hand side graph, and then “glue” it back. This
is the ideas behind the *double pushout*.

**III.c The double pushout and duality of labeling and tracing**

The double pushout (DPO) might be hard to follow at first. As an aid,
we’ve include in Fig.3 a visualize of the DPO approach that
capture the rewrite steps in Fig.
4. (Also, Fig.4 represents the push described in Plump’s paper!). In the double pushout approach, our
rewriting rule *p* is a *span*
$\lozenge l \xleftarrow{l} \mathcal{D} \xrightarrow{r} \lozenge r$ of
morphisms that start from *gluing object* 𝒟 and ends in the left-hand
side ◊*l* and right-hand side ◊*r*. Our *r edex* for the rule

*p*is a morphism

*g*: ◊

*l*→ 𝒢 for the left-hand into an intermediate graph 𝒢. The pushout only exists if there is a

*host object*𝒢

_{1}with a morphism

*q*from our interface 𝒟 that allows us to recover the match and also embed our intermediate graph 𝒢. The match reconstructed from two morphisms (

*q*and

*l*) is called the

*pushout complement*of (

*l*and

*g*). One way to think of this push out is once we’ve found a graph (𝒢) that matched our left-hand side, this (sub)graph that is created by removing the nodes and edges that match except for those ’marked’ by the gluing object (our interface). If we for some reason remove these nodes then it is impossible to complete the pushout. There are two conditions the double pushout requires: the identification and dangling condition. Essentially, these two boil down to saying that the pushout complement must contain nodes in the image of

*g*and

*l*. Figures 3 and 4 show examples of a double pushout diagram. In Figure 3, the rewriting step that is able to complete the double pushout is called a

*direct derivation*.

**Definition 11** (Direct Derivation). Let G and H be hypergraphs,
$r: \langle L \hookleftarrow K \xrightarrow{\text{b}} R\rangle$ a rule
and *f* : *L* ↪ *G* an injective hypergraph morphism. The G directly
derive H by r and f, denoted *G*⇒_{r, f}*H*, if there exisit
two pushouts of the following form.

For a rule
$p : \lozenge l \xleftarrow{l} \mathcal{D} \xrightarrow{r} \lozenge r$,
a direct derivation can be written as
$\mathcal{G} \xRightarrow{p} \mathcal{H}$. What we call here a direct
derivation is equivalent to Plump’s *evaluation step* . Plump discusses
two other types of operations: *folding* and *tracing*. The goal of the
former is to increase the level of sharing between edges that share the
same labels and terms. The latter, tracing, is a bit more involved.

**III.d Tracing semantics**

In term rewriting and term graph rewriting, labeling allows us to “lift” our rewrite rules into a context where each reduction step can now track symbols and their occurrences through multiple derivations. This labeling can be extended to arbitrary rewrite systems with the condition that restrictions must to placed on the labelling to ensure that identical arguments of a redex are labelled in the same way. Tracing is the dual of labeling. While labeling records the history of a reduction internally, tracing or tracking does so externally. A trace is a relation on the positions of the source and target of a rewrite rule. The idea is that as we step through a series of derivations (apply rewrite rules) we keep track of the terms of the left-hand and right-hand side. When reasoning over the label via trace there are three parts we care about as we step through the trace: terms belonging to the pattern of the contracted redex, terms disjoint with the redex, and terms that are arguments to the redex.

We capture the following example of tracing and labeling from as a
pushout diagram in
Fig.5 . In Fig.
5, we consider the rewrite rule
*f*(*a*, *x*) → *f*(*f*(*x*, *x*), *a*) and the reduction step
*f*(*f*(*a*, *a*), *a*) → *f*(*f*(*f*(*a*, *a*), *a*), *a*). Our goal is
to trace the thee *a*’s that show up in original term - the left-hand
side of the reduction step. In the application graph (bottom-left) of
the pushout diagram, we label each a with a different letter (to
represent out coloring).
Fig.5 show this result of this reduction
and lifting of rewrite rules: $f(f(a_{\color{blue}{b}},a_{\color{red}{r}}),a_{\color{green}{g}}) \rightarrow f(f(f(a_{\color{red}{r}},a_{\color{red}{r}}),a),a_{\color{green}{g}})$. We can observe the following in our trace: (1) $a_{\color{blue}{b}}$ belong to the contracted redex (top-left) but has no descendents, (2) $a_{\color{green}{g}}$ is disjoint eith the redex and is copied one, and (3) $a_{\color{red}{r}}$ is the redex argument (hole) and is copied twice. Additionally, there is one more $a$ with no label. It sourced from the original term, but from the pattern
in the embedding. It has no ancestors. The occurrences of a term traced
through derivations by a label are the *descendants* and the original
term is the *ancestor*.

**Definition 12** (Descendant and Ancestor ). Let *t* be a term in a
TRS ℛ and let *f* be a function symbol occurring in *t*. We give *f* a
mark or *label* to be able to trace it during a sequence of rewrites.
For a unique label *b*, the labeled symbol *f* can be written as
*f*^{b}. Consider the rewrite step $t \xrightarrow{s} t'$
obtained by the contraction of the redex *s* in *t*. As a result of the
contraction, all occurrences of *f* in *t*′ which are labelled *b* are
the *descendents* of the original *f* in *t*. Given
the one-to-one correspondence between sub-terms and their head symbols,
descendants of redex can be found by tracing head symbols.

In regards to rewriting, symbols can be partitioned into two classes:
those that trace to its target and does that dont. The symbols that
leave a trace are needed. The symbols which are needed then in essence
become the context for further reductions. Tracing provides verification
that positions in the target are originated with the source or are
created dynamically by some rule applications. Tracing is necessary for
the double pushout, particularly in the creation of the pushout
complement. Given this labeling-tracing duality, asking how it can be
useful in proving confluence of graph rewriting systems is somewhat
equivalent to demonstrating that the *dangling condition* and the
*identification condition* are necessary in completing the pushout.

**III.d Overlaps in the context and critical pairs**

As we mentioned previously, overlaps occur. In the term rewriting context, to ensure local confluence we needed to show that through a finite number of derivations, our sub-graphs with conflicting reductions have a common reduct. In the graph rewriting context we have similar questions: (1) what is a “harmful” overlap? and (2) what is a sufficient criteria for proving joinability?

**Definition 13** (Critical Pair). Let S be a term graph and $S \rightarrow U_i$ be an evaluation step for a rewrite rule $l_i \rightarrow r_i$ and a hypergraph morphism $g_i: \lozenge l_i \rightarrow S$ for i = 1, 2. Then $U_1 \leftarrow S \rightarrow U_2$ is a critical pair if:
- $S = g_1(\lozenge l_1) U g_2(\lozenge l_2)$
- $g_1(e_1) \in g_2(\lozenge l_2)$ or $g_2(e_2) \in g_1(\lozenge l_1)$, where $e_i$ is the edge outgoing from $root_{\lozenge l_i}$ for i = 1, 2

Moreover, $g_1 \neq g_2$ is required for the case $(l_1 \rightarrow r_1) = (l_2 \rightarrow r_2)$.

From the Critical Pair Lemma discussed in the Plump paper , we know that
a hypergraph rewriting system is locally confluent if all its critical
pairs are *strongly joinable*. So in addition to the decision procedure
for critical pairs, we require an additional qualification for term
graph rewriting called *strong joinability*.

**Definition 14** (Joinabiility). A critical pair, $\Gamma: U_1 \Leftarrow S \Rightarrow U_2$ is $\textit{joinable}$ if there are derivations $U_i \Rightarrow^{*} X_i$ for i = 1, 2, and an isomorphism $f: X_1 \rightarrow X_2$. Additionally $\Gamma$ is *strongly joinable* if there exists for every node ins $S$ that can can be traced through derivations the following two condition:

tr

_{S ⇒ U1⇒*X1(v)}and tr_{S ⇒ U2⇒*X2(v)}*f*_{V}(tr_{S ⇒ U1⇒*X1(v)}) =*t**r*_{S ⇒ U2⇒*X2(v)}

So there you have it! As long as our definition of joinabilty ensures traces are consistent and compatible through derivations, then for a terminating term graph rewriting system, strong joinability is sufficient for (local) confluence. So we are settled, right? Maybe for the case of term graphs, but for arbitrary graphs, confluence is, unfortunately, undecidable.

**Theorem 1**. It is undecidable in general whether a finite,
terminating hypergraph rewriting system is confluent. A hypergraph
rewriting system is said to be finite if *Σ*_{V},
*Σ*_{E} and *R* are finite.

We discuss why below.

**IV. The insufficiency of strong joinability**

**Figure 7**

To explain why, we will borrow an instructive example from [5]. In
Fig.7 we consider an graph transformation
system {*Σ*, *R*} with three rewrite rules:
*r*_{1}, *r*_{2} and *r*_{3}. Some inspection
will show that this system is terminating: the right-hand side removes
edges from the left. We can also show that it is confluent as there are
derivations which will reduce any overlaps to a common reduct (or
specifically structurally isomorphic graphs). That is, any overlap is
*joinable*. However despite this confluence, the two critical pairs in
Figure 7 are not *strong joinable*. In the
first,*cp*_{1}, applying *r*_{1} give us two graphs in
normal form for which the ismorphism between them is not compatible with
their traces. By labeling the nodes, we have distinguish one isomorphic
graphs. Strong joinability require compatibility with traces. As a
result, the presense of critical pairs that are joinable implies that we
can report confluence, but the lack of strong joinability for at least
one pair implies that we cannot report confluence. Which is it? It seems
like neither is sufficient. In the previous section, we mentioned that
our signature has not change. Well, what happens if it does? To keep
thing minimally destructive, lets still remain in the domain of
first-order terms. Lets add *edge labels*. As you may surmise, our
“tracing” now have over *nodes* and *edges*. In Figure 7, *cp*_{2} is a critical
that results from rewriting a term with an edge label. In this case our
critcal pair is still joinable, but we lose confluence because our
definition of critical pairs did not account for compatibility with edge
labels. The core idea highlighted by Plump is that relatively harmless
*signature extensions* may not preserve confluence. We may need an even
*stronger* joinability that capture compatibility between node and edge
labels across derivations. This means that adding signture extensions
that are more “destructive” will likely break our current decision
procedure for confluence. Specifically, there are two cases where our
current decision procedure for confluence on term graphs breaks down:
*variable binding* and *higher-order logics*. The former is related to
the question posed in the
Sec.1: Why can’t we just apply the ideas from
to rewriting the untyped *λ*-calculus?

**V. Critical pairs for arbitrary graphs**

**Variable binding and higher-order rewriting.** First, let’s revisit
the basic term writing system {*Σ*, ℛ} but with a tiny signature
extension: (*t*_{1} *t*_{2}) and (*λx*.*t*). The first
is **application** and represents the application of a function
*t*_{1} to an argument *t*_{2}. The second is
**abstraction** and represent a function with a parameter *x* in the
body of *t*. In the lambda calculus, a variable *s* in a term *t* is
**bound** by the first *λ* above *s*. If there is no *λx* above then
the term is **free**. For the following term *t* := *λx*.*y* the
clearest way to represent this as a a term graph is a two-node graph
with the root labeled *λ**x* and the child node labeled *y*. It is clear
that the notion of *variable binding* is not reflect in the structure of
this graph. Instead it is represented as the *content*. What has
happened is that that simple signature extension is not so simple. In
fact, binding requires *higher-order term rewriting* which require
expanding and rethinking many of the formulation for *first-order
rewriting*. Here are some resource on higher-order equational logics and
rewriting: .

*double pushout with interfaces (DPOI).* Okay I know we said that
confluence for finite, terminating hypergraph rewrite systems was
undecidable, but there may be a way at least for string diagrams. The
work of double pushout with interfaces (DPOI) introduces a new notion of
*path joinability* that relies on lifting critical pairs into arbitrary
contexts. This work links hypergraphs and symmetric monoidal categories:
the former is a combinatorial representation of the latter. This work
says that we we can show that string diagram rewriting, represented as
hypergraphs with interfaces, is decidable! Our colleague will discuss
this a bit in their blog post, but our one little bit is that DPOI seems
like a double pushout with a single pullback. To tease, that work,
similar to theories and signatures for terms in our universal algebra,
the structure of a symmetric monoidal category can be represented with
the notion of a *symmetric monoidal theory*.

**Definition 15** (One-sorted Symmetric Monoidal Theory (SMT) (See [2])). A
one-sorted SMT is determined by (*Σ*, ℰ) where *Σ*, the signature,
consists of a set of *generators* *o* : *n* → *m* with arity *n* and
coarity *m* where *m*, *n* ∈ ℕ. The set of *Σ*-terms is obtained by
combining generators in *Σ*, the unit `i``d`

: 1 → 1, and the symmetry
*σ*_{1, 1} : 3 → 2 with sequencing (;) and parallel composition
(⊕). Any SMT (*Σ*, *E*) freely generates a product and permutation
category (PROP). For an arbitary PROP *X*, a rewriting rule is a pair
$langle l, r\range$ where *l*, *r* : *i* → *j* are arrows in *X* with
the same sourcre and target. A rewriting systems ℛ is a set of rewriting
rules.

**VI. Conclusion**

In term and string rewriting, confluence is decidable for terminating
systems requiring finding all critical terms *s* and and checking that
all critical pairs *t* and *u* in *t* ← *s* → *u* reduce to a common
term or string. In the case of terminating graph-transformation systems,
confluence is undecidable (using critical pairs as a DP) unless certain
restrictions are applied. In this setting, join-ability of critical
pairs does not need to imply the confluence of a rewriting systems. That
is, there are confluent rewriting systems where are critical pairs are
not (strongly) joinable. (Strong) joinability is not a necessary
condition for confluence of a rewriting system and can be used a a
decision procedure for general (hyper-)graph rewriting systems. This
result does not appear to apply to string diagram rewriting if we
treat them as symmetric monoidial categories with some extra structure.
In the category of symmetric monoidal categories with a Frobenius
structure, confluence of rewriting systems based on the theory is
decidable.

**Reference**

[1]: Franz Baader and Tobias Nipkow. Term rewriting and all that. 1998

[2]: Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–10, 2016

[3]: Jan Willem Klop Marc Bezem and Roel de Vrijer. Term rewriting systems. Cambridge Tracts in Theoretical Computer Science Cambridge University Press, 55, 2003

[4]: Detlef Plump. Critical pairs in term graph rewriting. In International Symposium on Mathematical Foundations of Computer Science, 1994.

[5]: Detlef Plump. Checking graph-transformation systems for confluence. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 26, 2010

[6]: Kroening O. Strichman. Decision procedures: An algorithmic point of view. 2008.