Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Confluence of Drag Rewriting
Jean-Pierre Jouannaud, Fernando Orejas
École Nornale Supérieure de Paris-SaclayUniversitat Politècnica de Catalunya

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

1 Introduction

Outline

1 Introduction

2 From tree composition to graph composition

Outline

1 Introduction

2 From tree composition to graph composition

3 Drags and Drag Composition

Outline

1 Introduction2 From tree composition to graph composition

3 Drags and Drag Composition

4 Unification

Outline

1 Introduction

2 From tree composition to graph composition

3 Drags and Drag Composition

4 Unification

5 ConfluenceOutline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Outline1 Introduction
2 From tree composition to graph composition
3 Drags and Drag Composition
4 Unification
5 Confluence

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drags, Terms and Graphs

Drags are a generalization of terms
Drags are a special kind of labelled graphs with variables

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Confluence of Graph Rewriting

Confluence for terminating graph rewriting systems isundecidable [Plump 1993]

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Confluence of Graph Rewriting

Confluence for terminating graph rewriting systems isundecidable [Plump 1993]
Confluence for terminating graph rewriting systems withinterfaces is decidable [Bonchi et al 2017]

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Confluence of Graph Rewriting

Confluence for terminating graph rewriting systems isundecidable [Plump 1993]
Confluence for terminating graph rewriting systems withinterfaces is decidable [Bonchi et al 2017]
Confluence for Drags rewriting systems is decidable

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Outline1 Introduction2 From tree composition to graph composition
3 Drags and Drag Composition
4 Unification
5 Confluence

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Tree Rewriting and Composition

@

C @

@
@
L @
@

@

σ

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting

@

C @@

=⇒R @@@
@
@

σ@
@
@

École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Tree Rewriting and Composition

@C @

@
@
L @
@@@

=⇒

@

@

C @
@

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting

R @@@@σ(@C @σσ@ )
@
@

@
@
@

@

L @
@

École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Tree Rewriting and Composition@C @@@L @@@@

=⇒@


@

C @
@

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting

R @@@@σ(@C @σσ@@ ) ⊗ξ@@

@@@L @@

École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag Rewriting and Composition
@C @
@
R
@

L @
@

RR

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewritingσ@@@École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag Rewriting and Composition@C @@R@L @@RσR(@@@C @@Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting@σ@ )
@@

@

L @
@

École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag Rewriting and Composition@C @@R@L @@RσR(@@@C @@Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting@σ@ ) ⊗ξ@@

@L @@

École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag Rewriting and Composition

Context W?

@R@L@R@?

Substitution W

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag Rewriting and Composition
Context W?
z?
1 z2

r1?

r3@R? @z?
3
r2 r3

@R@

r1 r2

⊗ξLx?

x? y?

Substitution W

Linear context, non-linear left-hand side
Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Outline1 Introduction
2 From tree composition to graph composition
3 Drags and Drag Composition
4 Unification
5 Confluence

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drags
We presuppose two sets Σ (function symbols) and Ξ (variables)
whose elements have a fixed arity. Variables have arity 0.
Definition
A drag is a tuple hV , R, S, L, X i, where1

V is the finite set of vertices;2

R : [1..|R|] → V is a finite list of vertices, called roots;

3

S ⊆ V is the set of sprouts, V \S is the set of internal vertices;4

L : V → Σ ∪ Ξ is the labeling function, mapping internalvertices to labels from the vocabulary Σ and sprouts to labelsfrom the vocabulary Ξ;

5

X : V → V ∗ is the successor function, mapping each vertexv ∈ V to a list of vertices in V such that |X (v )| = |L(v )|.

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag Composition uses a Switchboard
Definition
Let D = hV , R, L, X , Si and D 0 = hV 0 , R 0 , L0 , X 0 , S 0 i be drags. A
switchboard ξ for (D, D 0 ) is a pairhξD : S → [1 .. |R 0 |], ξD 0 : S 0 → [1 .. |R|]i of partial injectivefunctions (we also say that (D 0 , ξ) is an extension of D), such that(i) ∀s, t ∈ S such that s ∈ DomξD and L(s) = L(t), then t ∈ DomξDand R 0 (ξD (s)) = R 0 (ξD (t));(ii) ∀s, t ∈ S 0 such that s ∈ DomξD and L0 (s) = L0 (t), then t ∈DomξD and R(ξD 0 (s)) = R(ξD 0 (t));(iii) ξ∗ does not induce cycles among the sprouts of the two drags.

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Rewriting Switchboard

Definition (Rewriting switchboard and extension)ξ is a rewriting switchboard for (D, L) if
ξD is linear and surjective (all roots of L must disappear)ξL is total (all sprouts must disappear)(D, ξ) is called a rewriting extension of L.

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

OutlineIntroduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Examples of composition↓↓↓f ⊗{x7→1} f = f↓↓↓xyf↓
Substitution y

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Examples of composition↓↓↓f ⊗{x7→1} f = f
↓
↓↓xyf
↓
Substitution y

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting↓↓↓↓f⊗ {x 7→ 1, g = f Y.&↓↓↓
y 7→ 2} yx xgForced sharing: a choiceÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

OutlineIntroduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Examples of composition↓↓↓↓f⊗ {x 7→ 1, g = f Y.&↓↓↓
y 7→ 2} yx xg↓↓↓
f ⊗{x7→1} f = f
↓
↓
↓
xyf
↓
Substitution y1

2

12Forced sharing: a choice

12

↓↓
↓
↓ ↓f 3 f ⊗{x7→1} a = f 3 4 f
&↓.
& ↓.
ax
Root transfer
Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Examples of composition↓↓↓↓f⊗ {x 7→ 1, g = f Y.&↓↓↓
y 7→ 2} yx xg↓↓↓
f ⊗{x7→1} f = f
↓
↓
↓
xyf
↓
Substitution y

1

2

12Forced sharing: a choice1212

121 23↓↓↓↓ ↓f 3 f ⊗{x7→1} a = f 3 4 f
&↓.
& ↓.
ax

↓↓ ↓↓ ↓f 3 f ⊗{x 7→ 1, y = f→f&↓.
y 7→ 2}xRoot transferDouble root transfer

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Outline1 Introduction
2 From tree composition to graph composition
3 Drags and Drag Composition
4 Unification
5 Confluence

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de CatalunyaDrag unification versus tree unification@@T @T’ @@@Drag unification versus tree unification
@

@

T @

T’ @

@

@

@=T @

@

T’ @

@σ@
@
@
@

σ is a unifier of D and D 0σ@@@

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Drag unification versus tree unification

?

@R@?

U?

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag Rewriting?

V?

? ? ? ?

École Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Outline

Introduction

From tree composition to graph composition

Drags and Drag CompositionUnification

Confluence

Drag unification versus tree unification
Extension C?

Extension C?

U@R@?

=?

V? ?

?

C is a unifier of U and V
Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Unifiers

Definition
Given- two drags U, V that share no vertex names nor root numbers,- two lists of internal partner vertices u ∈ U, v ∈ V of equal length,
the unification problem U[u] = V [v ] admits as solutions orunifiers, the common extensions of both U and V which identify
U ⊗ξ C and V ⊗ξ C below u and v respectively, that is, thesubdrags of U ⊗ξ C at u and of V ⊗ξ C at v must be isomorphic,that is, identical up to vertex names.

Subsumption
Definition
We say that a drag U subsumes a drag V if there is a context
extension (C , ξ) of U such that V = C ⊗ξ U.
Lemma
Subsumption is a quasi-order whose equivalence is variable
renaming, and strict-part is well-founded.
Subsumption extends naturally to context extensions. Given a setof unifiers, its minimal elements are said to be most-general.
Theorem
A solvable unification problem has a most general unifying
extension computable in quadratic time and linear space.

Outline

Introduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Outline1 Introduction
2 From tree composition to graph composition
3 Drags and Drag Composition
4 Unification
5 Confluence

Jean-Pierre Jouannaud, Fernando Orejas
Confluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Local Confluence

UL→RG →DST∗∗WOverlap versus absence of overlap 1/2lg

Overlap versus absence of overlap 1/2l=gl⊗ξgOverlap versus absence of overlap 1/2l=gXXXl

XXX

XX
•
•Xg

•
XXX •XX X XXXl⊗ξgOverlap versus absence of overlap 1/2ll=glg•
XXX •XX X
 XXX
gXXX

XX

XXX


XXX



XX•
•X

⊗ξ

=mgue(l,g)@@@⊗ξCOverlap versus absence of overlap 2/2
Lemma (Commutation)
Assume that U = V ⊗ξ W , V −→V 0 and W −→ W 0 . Then:l→rg→dV ⊗ξ WL→RG →DV 0 ⊗ξ WV ⊗ξ W 0∗

∗V 0 ⊗ξ W 0

Overlap versus absence of overlap 2/2

Lemma
Let S←− U −→ T , and let us assume that U has an internal vertexl→r g→dw which is an internal vertex of both l and g. Then, there existu ∈ Ver(l) and v ∈ Ver(g), and a unifying extension hE , ζi of theequation l[u] = g[v ] such that U = l ⊗ζ E = g ⊗ζ E .

OutlineIntroduction

From tree composition to graph composition

Drags and Drag Composition

Unification

Confluence

Confluence reduces to critical pairs joinability

Definition (Critical pair)
Let l → r and g → d be two rules that are unifiable at partner
vertices v , w , and hC , ξi be an mgu. Then, hl ⊗ξ C , g ⊗ξ C ) is
called a critical pair of l, g → d at v , w .
Theorem
Let S be a terminating rewrite system on drags. Then, S isconfluent iff all its critical pairs are joinable.

Jean-Pierre Jouannaud, Fernando OrejasConfluence of Drag RewritingÉcole Nornale Supérieure de Paris-Saclay Universitat Politècnica de Catalunya

Achievements and Problems
A rich algebra of drags based on COMPOSITION
that provides a natural definition of rewriting
Dershowitz&Jouannaud, TCS, 2019
A rewrite ordering ordering over drags(wich is total up to permutation of roots)
Dershowitz&Jouannaud, LPAR, 2018
Drag unification is unitary (with quadratic complexity)
Jouannaud&Orejas, UNIF , 2020
Confluence of drag rewriting reduces to critical pairs joinability
Jouannaud&Orejas, IWC , 2020
Graph Rewriting versus Drag Rewriting
Dershowitz, Jouannaud&Orejas, Draft, 2020
Applications: logic programming, cyclic lambda-calculus,
Koszul’s completion of operads, etc.

Last slide

Thank you for your attention