Confluence of drag rewriting
Jean-Pierre Jouannaud1 and Fernando Orejas2
12

École Normale de Paris-Saclay, Laboratoire de Spécification et Vérification,
FranceUniversitat Politècnica de Catalunya, Barcelona, Spain

Abstract
We develop a confluence result for graph rewriting based on the drag model [5].

1Introduction

Rewriting with graphs has a long history in computer science, graphs being used to represent
data structures, but also program structures and even concurrent and distributed computational models. They therefore play a key rôle in program evaluation, transformation, andoptimization, and more generally program analysis; see, for example, [2].
Our work is based on a recent, purely combinatorial view of graphs [5]. To assess ourclaim that drags are a natural generalization of terms, we extend the most useful term
rewriting techniques to drags: the recursive path ordering [4]; unification [8]; confluence inthis paper. Our main result is that confluence of a terminating set of drag rewrite rules
can be decided by the usual joinability test of their critical pairs. Comparisons with theliterature will be done at length in a forthcoming paper.

2

The drag model [5]Drags are finite, directed, ordered, rooted, labeled multi-graphs. Vertices with no outgoingedges are designated sprouts. Other vertices are internal. We presuppose: a set of function
symbols Σ, whose elements f , equipped with a fixed arity ∣f ∣, are used as labels for internalvertices; and a set of nullary variable symbols Ξ, disjoint from Σ, used to label sprouts.
▸ Definition 1 (Drags). A drag is a tuple ⟨V, R, L, X, S⟩, where
1. V is a finite set of vertices, denoted by Ver(D);
2. R ∶ [p .. p + ∣R∣] → V is a finite list of vertices, called roots; R(p + n − 1) refers to the nth
root in R; unless otherwise stated, p = 1; we use R(D) for the roots of D;
3. S ⊆ V is a set of sprouts, leaving V ∖ S to be the internal vertices;
4. L ∶ V → Σ ∪ Ξ is the labeling function, mapping internal vertices V ∖ S to labels from thevocabulary Σ and sprouts S to labels from the vocabulary Ξ, writing v ∶ f for f = L(v);5. X ∶ V → V ∗ is the successor function, mapping each vertex v ∈ V to a list of vertices in
V whose length equals the arity of its label (that is, ∣X(v)∣ = ∣L(v)∣).
The reflexive-transitive closure X ∗ of the relation X is called accessibility. Vertex v isaccessible if it is accessible from some root. A drag is clean if all its vertices are accessible.
Terms as ordered trees, sequences of terms (forests), terms with shared subterms (dags) andsequences of dags (jungles) are all particular kinds of clean rooted drags.
Sprouts may be roots, this is essential for having a nice algebra of drags.
We use Var(D) for the set of variables labeling the sprouts of D. A drag is linear if notwo sprouts have the same label, in which case variables and sprouts can be identified.

2

Confluence of drag rewriting

2.1

Drag composition

A variable in a drag should be understood as a potential connection to a root of anotherdrag, as specified by a connection device called a switchboard. A switchboard ξ is a pair ofpartial injective functions, one for each drag, whose domain Dom(ξ) and image Im(ξ) are a
set of sprouts of one drag and a set of positions in the list of roots of the other, respectively.
▸ Definition 2 (Switchboard). Let D = ⟨V, R, L, X, S⟩ and D′ = ⟨V ′ , R′ , L′ , X ′ , S ′ ⟩ be drags.
A switchboard ξ for D, D′ is a pair ⟨ξD ∶ S → [1 .. ∣R′ ∣]; ξD′ ∶ S ′ → [1 .. ∣R∣]⟩ of partial injectivefunctions such that
1. s∈Dom(ξD ) and L(s)=L(t) imply t∈Dom(ξD ) and ξD (s)=ξD (t) for all sprouts s, t∈S;
2. s∈Dom(ξD′ ) and L′ (s)=L′ (t) imply t∈Dom(ξD′ ) and ξD′ (s)=ξD′ (t) for all s, t∈S ′ ;3. ξ is well-behaved: it does not induce any cycle among sprouts, using ξ, R, R′ relationally:∃/ n > 0, s1 , . . . , sn+1 ∈ S, t1 , . . . , tn ∈ S ′ , s1 = sn+1 . ∀i ∈ [1..n]. si ξD R′ X ′∗ ti ξD′ RX ∗ si+1
The pair ⟨D′ , ξ⟩ is an extension of D, a rewriting extension if ξD is surjective and ξD′ total.
Sprouts labelled by the same variable should be connected to the same vertex, as stipulated by conditions (1,2). It follows that ξD (Dom(ξD )) must be a set, making the set
difference [1 .. ∣R′ ∣] ∖ ξD (Dom(ξD )) well defined.
We now move to the composition operation on drags induced by a switchboard. The
essence of this operation is that the (disjoint) union of the two drags is formed, but withsprouts in the domain of the switchboards merged with the roots to which the switchboard
images refer. Merging sprouts with their images requires one to worry about the case wheremultiple sprouts are merged successively, when the switchboards map sprout to rootedsprout to rooted-sprout, until, eventually, an internal vertex of one of the two drags must
be reached because a switchboard is well-behaved. That vertex is called target:▸ Definition 3 (Target). Let D = ⟨V, R, L, X, S⟩ and D′ = ⟨V ′ , R′ , L′ , X ′ , S ′ ⟩ be drags suchthat V ∩ V ′ = ∅, and ξ be a switchboard for D, D′ . The target ξ ∗ (s) is a mapping fromsprouts in S ∪ S ′ to vertices in V ∪ V ′ defined as follows:
Let v = R′ (n) if s ∈ S, and v = R(n) if s ∈ S ′ , where n = ξ(s).
1. If v ∈ (V ∪ V ′ ) ∖ (S ∪ S ′ ), then ξ ∗ (s) = v.
2. If v ∈ (S ∪ S ′ ) ∖ Dom(ξ), then ξ ∗ (s) = v.
3. If v ∈ Dom(ξ) , then ξ ∗ (s) = ξ ∗ (v).
The target mapping ξ ∗ (_) is extended to all vertices of D and D′ by letting ξ ∗ (v) = v whenv ∈ (V ∖ S) ∪ (V ′ ∖ S ′ ).
We are now ready for defining the composition of two drags. Its set of vertices will be theunion of two components: the internal vertices of both drags, and their sprouts which are
not in the domain of the switchboard. The labeling is inherited from that of the components.
▸ Definition 4 (Composition). Let D = ⟨V, R, L, X, S⟩ and D′ = ⟨V ′ , R′ , L′ , X ′ , S ′ ⟩ be drags
such that V ∩ V ′ = ∅, and let ξ be a switchboard for D, D′ . Their composition is the dragD ⊗ξ D′ = ⟨V ′′ , R′′ , L′′ , X ′′ , S ′′ ⟩, with interface (R′′ , S ′′ ) denoted (R, S) ⊗ξ (R′ , S ′ ), where
1. V ′′ = (V ∪ V ′ ) ∖ Dom(ξ);
2. S ′′ = (S ∪ S ′ ) ∖ Dom(ξ);
3. R′′ = ξ ∗ (R([1 .. ∣R∣] ∖ ξD′ (Dom(ξD′ )))) ∪ ξ ∗ (R′ ([1 .. ∣R′ ∣] ∖ ξD (Dom(ξD ))));
4. L′′ (v) = L(v) if v ∈ V ∩ V ′′ ; and L′′ (v) = L′ (v) if v ∈ V ′ ∩ V ′′ ;5. X ′′ (v) = ξ ∗ (X(v)) if v ∈ V ∖ S; and X ′′ (v) = ξ ∗ (X ′ (v)) if v ∈ V ′ ∖ S ′If ⟨D, ξ⟩ is a rewriting extension of D′ , then all roots and sprouts of D′ disappear in thecomposed drag. The drag D can then be seen as the context of the left-hand side of a ruleD′ → R, where R must have the same number of roots as D′ (and Var(R) ⊆ Var(D′ ).)Jean-Pierre Jouannaud and Fernando Orejas

3

1

1

1

1

1

1

↓
g
↓
f
↓↑
f

↓
f
↓
y′

Ð→
↓
g
↓
f←2
↓
x′

↓
f
↓
y′

↓
h
=
↓
x′← 2

↓
h
↓
f
↺

=

⊗ {x′ ↦ 1, y ′ ↦ 2}

⊗ {x′ ↦ 1, y ′ ↦ 2}

Figure 1 Rewriting and cycles.

2.2

Drag rewriting

Rewriting with drags is similar to rewriting with trees: we first select an instance of the lefthand side L of a rule in a drag D by exhibiting an extension ⟨W, ξ⟩ such that D = W ⊗ξ L – thisis drag matching, then replace L by the corresponding right-hand side R in the composition.
A very important condition for the result to be a drag is, accordingly, that the left- andright-hand sides of rules have the same number of roots:▸ Definition 5 (Rules). A drag rewrite rule is a pair of clean drags, written l → r, such that(i) ∣R(l)∣ = ∣R(r)∣, and (ii) Var(r) ⊆ Var(l). A drag rewriting system is a set of drag rewrite
rules.
Condition (i) ensures that l and r have a perfect fit with any same environment, that is,both can be composed with any extension of l. Condition (ii) is standard for rewrite rules.
▸ Definition 6 (Rewriting). Let S be a drag rewrite system. We say that a nonempty clean
drag D rewrites to a clean drag D′ , and write D Ð→S D′ , iff D = C ⊗ξ l and D′ = C ⊗ξ r forsome drag rewrite rule l → r ∈ S and clean rewriting extension ⟨C, ξ⟩ of l.
Because ξ is a rewriting switchboard, ξC must be linear, implying that the variables
labeling the sprouts of C that are not already sprouts of D must all be different. Then,ξC must be surjective, implying that the roots of l (hence those of r) disappear in thecomposition, a case where the composition is commutative –we shall mostly write the context
on the left, though. Further, ξl must be total, implying that the sprouts of l (hence thoseof r) disappear in the composition. Finally, D and C being clean, it is easy to show that
D′ is clean as well, which is therefore a property rather than a requirement.
▸ Example 7 (Figure 1). The (red) rewrite rule g(f (x′ )) → h(x′ ), whose roots are g andf on the left-hand side and h and x′ on the right-hand side, applies with a blue context,
colours which are reflected in the input and output terms (the rule applies across the cycle).
We are now finished with the material from [5] needed for the rest of this paper.

2.3

Drag unification [8]The purpose here is to identify two clean drags U, V by composing them with the same minimal rewriting context ⟨C, ξ⟩, resulting in the same drag W . An identification corresponds
to the fact that we want the same drag to be rewritten by two different rewrite rules whose
left-hand sides are U and V . In order for C ⊗ξ U and C ⊗ξ V to both make sense, we assume
that U, V are renamed apart (variables and root numbers).
▸ Definition 8. Given drags U, V , we call partner vertices two lists LU , LV of equal lengthof internal vertices of U and V , respectively, such that no two vertices u, u′ ∈ LU (resp.,v, v ′ ∈ LV ) are in relationship with XU (resp., XV ).

4

Confluence of drag rewriting▸ Definition 9. Two drags U, V are identified with a drag W at partner vertices (u, v) by an
injective function o ∶Ver(U ) ∪ Ver(V ) → Ver(W ) called identification, written U [u]=o V [v], iff:
1. o(u) = o(v);2. ∀w ∈ Ver(U ), w′ ∈ Ver(V ) such that o(w) = o(w′ ), w ∶ f iff w′ ∶ f iff o(w) = o(w′ ) ∶ f ;3. ∀w ∈ Ver(U ), w′ ∈ Ver(V ) such that o(w) = o(w′ ), o(XU (w)) = o(XV (w)).
While two terms u, v are unified at their root, the solution being a substitution σ suchthat uσ = vσ, two drags U, V are unified at partner vertices (u, v), the solution being an
extension ⟨C, ξ⟩ of both U and V that identifies C ⊗ξ U and C ⊗ξ V at these partner vertices:▸ Definition 10. A unification problem is a pair of clean drags (U, V ) that are renamed
apart, together with partner vertices P = {(u, v)}, which we write U [u] = V [v]. A solution(or unifier) to the unification problem U [u] = V [v] is a clean rewriting extension ⟨C, ξ⟩such that the overlap drags C ⊗ξ U and C ⊗ξ V are identified at P . A unification problem
U [u] = V [v] is solvable if it has a solution.
We want unification to be minimal, that is, to capture all possible extensions that identify
U and V , without useless identifications occuring above or below partner vertices.
▸ Definition 11. We say that a drag U is an instance of a drag V , or that V subsumes U ,and write U ⪰ V , if there exists a clean context extension ⟨C, ξ⟩ such that U = C ⊗ξ V .
Cleanness is essential here, since otherwise any drag would be an instance of any otherdrag, which is also the reason why rewriting considers clean extensions only. In the following,
we assume for convenience that the sprouts of U, V are labelled by different sets of variables.
▸ Lemma 12. ⪰ is a quasi-order whose equivalence is variable renaming and strict part is awell-founded order.
We now extend the (of course well-founded) subsumption order to context extensions:▸ Definition 13. Let U be a drag, of which ⟨C, ξ⟩ and ⟨D, ζ⟩ are two context extensions.
We say that (D, ζ) is an instance of (C, ξ) (or that (C, ξ) subsumes (D, ζ)) w.r.t. U , andwrite (D, ζ) ⪰U (C, ξ), if (D ⊗ζ U ) is an instance of (C ⊗ξ U ).
We show in [8] the following key result:▸ Theorem 14. Given a unification problem, there is a unique most general unifying extension, if any, computable in quadratic time.

3

Confluence

Confluence of a terminating term rewriting system follows from the joinability of its criticalpairs, obtained by unifying overlapping left-hand sides of rules [9]. Our goal is to generalize this result to the drag framework. For non-terminating countable systems, replacing
joinability by the existence of decreasing diagrams [10] should also work.
▸ Lemma 15. Let S←Ðl→r U Ð→g→d T , and assume that U has no internal vertex being at
the same time an internal vertex of l and of g. Then, there exist two drags V, W and aswitchboard ξ such that U =V ⊗ξ W , V Ð→l→r V ′ , W Ð→g→d W ′ , S =V ′ ⊗ξ W and T =V ⊗ξ W ′ .
Proof. By definition of rewriting, there exist rewriting extensions ⟨A, ξ⟩ and ⟨B, ζ⟩ suchthat U = A ⊗ξ l = B ⊗ζ g. We assume without loss of generality that l and g are renamed
apart as well as A and B, making ξl ∪ ζg well defined, as well R(A) ∪ R(B).

Jean-Pierre Jouannaud and Fernando Orejas

5

Let now C be the drag whose internal vertices are those of U which are not internalvertices of either l or g, its roots and sprouts are those of A plus those of B, and its
successor relationship is inherited from that of U .
Since l and g do not share internal vertices by assumption, B = l ⊗ξ C while A = g ⊗ζ C,
hence U = l ⊗ξ C ⊗ζ g (using associativity of composition [5]). We then take V = l and
W =C ⊗ζ g.
◂▸ Lemma 16 (Commutation). Assume that U = V ⊗ξ W , V Ð→l→r V ′ and W Ð→g→d W ′ . Then,U Ð→l→r V ′ ⊗ξ W Ð→g→d V ′ ⊗ξ W ′ and U Ð→g→d V ⊗ξ W ′ Ð→l→r V ′ ⊗ξ W ′ .
Proof. Easy consequence of associativity of composition.

◂▸ Lemma 17 (Critical overlap). Let S←ÐL→R U Ð→g→D T , and let us assume that U has aninternal vertex w which is an internal vertex of both l and g. Then, there exist u ∈ Ver(l)and v ∈ Ver(g), and a unifying extension ⟨E, ζ⟩ of the equation l[u] = g[v] such thatU = l ⊗ζ E = g ⊗ζ E.
Proof. Let A be the subset of internal vertices of U which are also internal vertices of l andof g, roots of l, U, g being considered as specific internal vertices. By assumption, A ≠ ∅,implying that l and g overlap. The core of the proof is the definition of two lists v, w ofpartner vertices of l, g which generate A, that is, all vertices of A are accessible from v inl and from w in g. As partner vertices, vi and wi must coincide, that is, be identified in A.
Let us denote vertices of A by u, v and w according to their origin, in U, l and g respectively.
Because left-hand sides of rules are clean drags, for all internal vertices u ∈ A, there
exists some root r ∈ R(l) ∪ R(g) such that, r (Xl∗ ∪ Xg∗ ) v. There are therefore three kindsof partner vertices (v, w): v, w are roots of l, g; or v is a root of l and w is not a root ofg; or v is not a root of l and w is a root of g. Eliminating redundancies (with respect toaccessibility) yields two lists of vertices that satisfy the conditions for being partner vertices,and generate A.
We now show that U defines a unifying extension of the equation l[v] = g[w]. Since l andg match U , U = l[v]⊗γ C = g[w]⊗δ D for some rewriting extensions ⟨C, γ⟩ and ⟨D, δ⟩ of l andg respectively. Assuming that l, g are renamed apart, then U = (l[v] ⊕ g[w]) ⊗γ∪δ (C ⊕ D).
Hence l and g are unifiable at partner vertices (v, w) with the extension (C ⊕ D, γ ∪ δ). ◂▸ Definition 18 (Critical pair). Let l → r and g → d be two rules that are unifiable at partner
vertices v, w, and ⟨C, ξ⟩ be an mgu. Then, ⟨l⊗ξ C, g⊗ξ C) is called a critical pair of l, g → d
at v, w.
Note that the notion of drag critical pair becomes symmetric.
Given a drag rewriting system, how many critical pairs can be generated ? Their number
is indeed bounded by the potential choices for partner vertices, which must satisfy theconstraints stated in the proof of Lemma 17. In practice, this number should remain small,as is the case for terms.
We can now end up with our main result, which follows easily from Lemmas 15, 16
and 17:▸ Theorem 19. Let S be a terminating rewrite system on drags. Then, S is confluent iff allits critical pairs are joinable.
As for terms: (i) termination is not essential: the same result could be rephrased, we
believe, by using decreasing diagrams instead of joinability; and (ii) redundancy criteria [1],should allow to filter out useless critical pairs.

6

Confluence of drag rewriting

4

Conclusion

Drags appear to be an extremely handy generalization of terms, dags and jungles: theintuitions behind them all are very similar, as well as the most important algorithms for
implementing rewriting and testing its termination and confluence, despite the possibility of
having arbitrary cycles in drags. This is made possible by a powerful composition operator.
Drags do not exactly generalize terms, though, as is pointed out in [5]. This is because
our definition of composition forces sharing, as does term rewriting in practice. Capturing
the term case requires using a composition operator based on drag isomorphism instead ofdrag equality in presence of non-linear variables in rules. This is of course possible, and iscurrently being investigated.
Finally, the present result together with the drag path ordering given in [4] shoud allow
the development of completion procedures for drag rewriting systems.
Warm thanks to Anne Yenan and José Motos who provided a deluxe roof to the firstauthor during his one month stay in Barcelona at the invitation of the second author.
References
1

2

3

4

5
6
7
8
9
10

Leo Bachmair and Harald Ganzinger. On Restrictions of Ordered Paramodulation with
Simplification. In Mark E. Stickel editor, 10th International Conference on AutomatedDeduction, Kaiserslautern, July 24-27, 1990. Lecture Notes in Computer Science 449,
pages 427–441, Springer, 1990.
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.
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.
Nachum Dershowitz and Jean-Pierre Jouannaud. Graph path orderings. In Gilles Barthe,
Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on
Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in
Computing, pages 307–325. EasyChair, 2018.
Nachum Dershowitz and Jean-Pierre Jouannaud. Drags: A compositional algebraic framework for graph rewriting. Theor. Comput. Sci., 777:204–231, 2019.
Annegret Habel, Hans-Jörg Kreowski, and Detlef Plump. Jungle evaluation. Fundam.
Inform., 15(1):37–60, 1991.
Gérard Huet. Unification dans les langages d’ordre 1, . . . , ω. PhD thesis, Université Paris7, Paris, France, 1976.
Jean-Pierre Jouannaud and Fernando Orejas. Unification of drags. In UNIF 2020. available
at https://hal.inria.fr/hal-02562152.
Donald Knuth and Peter Bendix. Simple word problems in universal algebras. In J. Leech,
editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
Vincent van Oostrom. Confluence by decreasing diagrams. Theor. Comput. Sci.,
126(2):259–280, 1994.