Proceedings of the

9th International Workshop on Confluence
June 30th 2020
OnlineForeword
This report contains the proceedings of the 9th International Workshop on Confluence (IWC) which
took place on June 30th, 2020. It was due to be held in Paris, but had to be changed to a fully online
event due to the coronvirus pandemia. In addition, the proceedings include the system descriptionsof the 9th Confluence Competition (CoCo 2020). The workshop was part of the Paris Nord Summerof LoVe 2020, a joint event on LOgic and VErification at Université Paris 13, made of Petri Nets
2020, IJCAR 2020, FSCD 2020, and over 20 satellite events. We would like to thank the conference
chair Stefano Guerrini and the workshop organizer Giulio Manzonetto for their hard work on entirely
changing the organization of the conference.
Confluence provides a general notion of determinism and has been conceived as one of the central
properties of rewriting systems. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting,such as first-order rewriting, lambda-calculi, higher-order rewriting, constraint rewriting, conditional
rewriting, and so on. Recently there is a renewed interest in confluence research, resulting in newtechniques, tool support, confluence competition, and certification as well as in new applications. The
scope of the workshop is all these aspects of confluence and related topics. The goal of the IWC
workshop is to provide a forum for researchers interested in the topic of confluence to exchange andshare new developments in the field. The workshop will enable discussion on theoretical results, newproblems, applications, implementations and benchmarks, and share the current state-of-the-art on
the development of confluence tools.
The joint program contains 8 contributed talks as well as invited talks by Frédéric Blanqui andMargherita Zorzi. In addition, the program contains the system descriptions from the 8th Confluence
Competition (CoCo 2020). Many people contributed to the preparation and IWC. Hard work by the
program commitees, steering committees, and subreviewers made an exciting program of contributed
and invited talks possible. In addition, we are greatful to the organizing committee and workshop
chairs of FSCD-IJCAR for hosting the workshops.

June 11th, 2020, Paris
Mauricio Ayala-RincónSamuel Mimramii

Steering Committee• Takahito Aoto
• Nao Hirokawa

Program Committee• Beniamino Accattoli (INRIA & LIX, École Polytechnique)• Mauricio Ayala-Rincón (Universidade de Brası́lia), co-chair• Cyrille Chenavier (Centre Inria Lille)• Alejandro Dı́az-Caro (Universidad Nacional de Quilmes & ICC/UBA-CONICET)• Maribel Fernández (King’s College London)• Mario Florido (Universidade de Porto)• Makoto Hamana (Gunma University)• Philippe Malbos (Université Claude Bernard Lyon 1)• Samuel Mimram (LIX, École Polytechnique), co-chair• Camilo Rocha (Pontificia Universidad Javeriana - Cali)• Daniel Lima Ventura (Universidade Federal de Goiás)• Femke van Raamsdonk (VU University Amsterdam)• Johannes Waldmann (Hochschule für Technik, Wirtschaft und Kultur Leipzig)• Sarah Winkler (Università degli studi di Verona)

Additional reviewers• Claudia Faggian• Pablo Barenbaumiii

Contents
Forewordii

IWC 2020
Some symmetries of commutation diamonds
Vincent van Oostrom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Parallel Closedness Revisited
Kiraku Shintani, Nao Hirokawa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Algebraic critical pair lemma
Cyrille Chenavier, Benjamin Dupont, Philippe Malbos . . . . . . . . . . . . . . . . . .
On the reduction of the type-free computational λ-calculus
Ugo de’Liguoro, Riccardo Treglia . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Confluence in Lens Synthesis
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
Coherent Confluence in Modal n-Kleene Algebras
Cameron Calk . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Safety and Completeness of Disambiguation corresponds to Termination and Confluence ofReordering
Luıis Eduardo de Souza Amorim, Eelco Visser . . . . . . . . . . . . . . . . . . . . . .
Confluence of drag rewriting
Jean-Pierre Jouannaud, Fernando Orejas . . . . . . . . . . . . . . . . . . . . . . . . .

1

CoCo 2020
Confluence Competition 2020
Aart Middeldorp, Naoki Nishida, Kiraku Shintani, Johannes Waldmann . . . . . . . .
infChecker at the 2020 Confluence CompetitionRaúl Gutiérrez, Salvador Lucas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
CoLL-Saigawa 1.5: A Joint Confluence Tool
Kiraku Shintani, Nao Hirokawa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Moca 0.2: A First-Order Theorem Prover for Horn Clauses
Yusuke Oi, Nao Hirokawa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
CoCo 2020 Participant: CSI 1.2.4
Fabian Mitterwallner, Aart Middeldorp . . . . . . . . . . . . . . . . . . . . . . . . . . .
CoCo 2020 Participant: FORT-h 0.9
Fabian Mitterwallner, Aart Middeldorp, Bertram Felgenhauer . . . . . . . . . . . . . .
CoCo 2020 Participant: ConCon 1.10
Christian Sternagel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
CO3 (Version 2.1)
Naoki Nishida . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
CoLL 1.5: A Commutation Tool
Kiraku Shintani . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
CoCo 2020 Participant: nonreachFlorian Meßner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
ACP: System Description for CoCo 2020
Takahito Aoto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
AGCP: System Description for CoCo 2020
Takahito Aoto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
CoCo 2020 Participant: CSIˆho 0.3.2
Julian Nagele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
iv

1
7
13
19
29
35

41
47
53
53
55
57
59
61
63
65
67
69
71
73
75
77

CoCo 2020 Participant: CeTA 2.39
Jonas Schöpf, Christian Sternagel, René Thiemann, Akihisa Yamada . . . . . . . . . .
The System SOL version 2020
Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju . . . .
Author Index

79
81
82

v

vi

Proceedings of the 9th International Workshop of Confluence, 2020

Some symmetries of commutation diamonds
Vincent van Oostrom
University of Innsbruck
Vincent.van-Oostrom@uibk.ac.at
Abstract
We study commutation of rewrite systems under swapping, reversing.

1

Introduction

Commutation may be used as a building block in various settings ranging from the abstract tothe concrete. For instance, causality may be analysed as the independence of events which may
be modeled as their commutation, and correctness of compiler optimisations may be modeled
as commutation between evaluation and optimisation. Commutation generalises confluence,
which itself may be used for establishing consistency of and deciding equational theories.
In this short paper we investigate commutation under swapping and reversing of the rewrite
systems. We show that at the level of abstract rewriting this perspective, although bringing
nothing new per se, may serve to bring unity into disparate results in the literature. At thelevel of term rewriting some fun is to be had, albeit simple, because in the commutation-bycritical-pair-analysis (due to Knuth and Bendix and Huet for first-order term rewriting, andextended to higher-order term rewriting by Nipkow), rules are commonly assumed to conformto certain restrictions, restrictions that may not be preserved when reversing them.
Example 1. Reversing the term rewrite rules:
f (x) → x

f (x) → af (x) → g(x, x)(λx.F (x))G → F (G)violates the respective requirements that: the lhs should not be a variable (x is),1 variables in
the rhs should occur in the lhs (x does not occur in a), the lhs should be linear (x occurs twicein g(x, x)),2 the lhs should be a pattern (in the sense of Miller; F (G) is not a pattern).
Instead of a conclusion we have positions after each subtopic.3

2

Diamond symmetries in abstract rewriting

We assume knowlege of abstract and term rewriting [7]. We employ arrow-like notations I,., . . . for abstract rewrite systems or relations on a (the same) set of objects, reversing thesenotations J, /, . . . to denote the reverse systems,and their repetitions II, .., . . . to denote thereflexive–transitive closures. We define J. := J ∪ . and → := I ∪ .. As in [5], we extend
terminology and notation for a single rewrite system I to the diagonal I, I, i.e. such that
P (I) iff P (I, I) for P a property of (pairs of) rewrite systems.
Definition 1. The pair I,. has the diamond property if J · . ⊆ . · J, it commutes if II,..
has the diamond property, and has the Church–Rosser property if (J ∪ .)∗ ⊆ .. · JJ.
1 Variable-lhss are allowed by Huet in his Critical Pair Lemma, but not in Nipkow’s higher-order version.
2 Although non-left-linear rules are usually allowed in term rewriting, they do not go well with commutation:
Hirokawa and Shintani show in IWC 2015, for them commutation is not even preserved by signature extension.
3 For lack of space we often only provide hyperlinks for informal references to the literature.

1

2

Proceedings of the 9th International Workshop of Confluence, 2020

Commutation symmetries

V. van Oostrom

We may refer to the diagonal of P as self -P . For instance, self-commutation is conventionallyknown as confluence. The name of the diamond property derives from that it can be visualised
like that. The 8 symmetries of such a diamond (the dihedral group D4 ) give rise to 8 instancesof the diamond property, obtained by swapping and reversing the rewrite systems I, ., andhence also of commutation. We have visualised4 three of these, together with their respective(conventional) names:5

⇓

⇐

⇑

commutation

factorisation

upward commutation

Formally, letting P range over the properties in Definition 1, left–right reflecting the diamondcorresponds to swapping the pair I, . into ., I and is a symmetry: P (I, .) iff P (., I).6 Clockwise rotating the diamond corresponds to first swapping the pair I, . and then reversing thefirst element yielding /, I. The first displayed rotation turns commutation into factorisation,.. · II ⊆ II · .., which is equivalent to the Church–Rosser property of /, I, i.e. that a reductiona  b factors as a II · .. b. Symmetries preserve results. E.g. that the diamond property
implies the Church–Rosser property is the same result as that . · I ⊆ I · . implies factorisation.
Position 1. Results for diamond and commutation are to be taken up to symmetries.
How to show the Church–Rosser property of I, .? Based on a note from 1978 by De Bruijn,
we introduced the decreasing diagrams (DD) technique in my PhD thesis, requiring for each
local 7 peak a J · . b existence of a suitably constrained valley a .. · JJ b, a result we extended
in 2008 to allow conversions instead of valleys:
S
S
Definition 2. I, . is decreasing, if I := i∈I Ii , . := j∈J .j for families (Ii )i∈I , (.j )j∈J
and some well-founded strict order < on I ∪ J, such that for all i ∈ I,j ∈ J i J · .j ⊆ J.∗gi · .=j ·J.∗g{i,j} · i J= · J.∗gj , where gK := {k ∈ I ∪ J | ∃` ∈ K ` > k} and gk := g{k}.
Theorem 1 (Decreasing Diagrams, DD [4]). I, . commute if decreasing.

Since then, DD has found wide application in the literature in the study of confluence andcommutation (see below), but somewhat surprisingly (given their symmetry), as far as we know,
not yet within the study of factorisation. Here and in Section 3 we give examples8 illustrating
the power of DD also for establishing factorisation results, and at the same time how DD allows
one to focus on extracting appropriate families and orders on them, easing applicability.
S
S
Example 2. I := i Ii∈I and . := j∈I .j commute if for all i, j, .j is terminating and∗i J · .j ⊆ .j · (i J ∪ .i )(1)

To see this, first note it suffices to show Ii , . commutefor all i. Fixing i allows to turn (1)Sinto a DD by decomposing . into .i and .¬i := k6=i .k , ordering .¬i -steps above others, andordering Ii - and .i -steps via their targets by (IIi · i /·IIi )+ , well-founded by (1) [7, Exc. 1.3.19].
4 As usual, ordinary/dashed arrows represent universally/existentially quantified steps and reductions.
5 Other names of factorisation are postponement (from a .-perspective) or preponement (I-perspective).
6 This is apparent via left–right reflection of our formal notations, as these mirror those of the diamond.
7 Following Newman’s 1942 in localising properties P , we use local P to refer to P with its assumption
restricted to single steps (I,.) instead of general reductions (II,..). E.g., local commutation is J · . ⊆ .. · JJ.
8 Found by us over the past 20 years, but only privately communicated and circulated.

2

Proceedings of the 9th International Workshop of Confluence, 2020

Commutation symmetries

3

V. van OostromThat families →• := ( • , • ) and →◦ := ( ◦ , ◦ ) satisfy the conditions of a squarefactorisation system [1], directly entails ◦ , ◦ are terminating and (1) holds for9 • ←, →◦ ,yielding the main abstract factorisation result of that paper [1, Thm. 5.2].
Note that using DD not only allowed our statement and proof to be (much) more compact,10
but also our result to be (much) more general, not just because of allowing arbitrary size families;
already for families of size 2 it is more general: e.g. where square factorisation systems require+++•·◦ to be contained in◦·( • ∪◦)◦ ·• , (1) only requires it to be contained inand similarly for . In [4] we showed that in fact all ‘local commutation ⇒ commutation’results we knew of then, could be obtained as instances of DD. We did so by introducing various
basic techniques for finding families and orders such as self - and rule-labelling. For instance,
the Lemma of Hindley–Rosen was obtained by taking for > the empty order on families [4,Example 13], and the commutation version (due to Backhouse and Doornbos) of Newman’s
Lemma was obtained by self -labelling a step a → b by its source and ordering labels by ←+ [4,Example 12].11 DD has been formalised in Isabelle and is part of the AFP, due to Zankl for
Theorem 1 and to Felgenhauer for a proof order version. DD has been automated in tools suchas ACP and CSI, and many commutation results have been factored through DD and often
generalised by it, e.g. Toyama’s famous modularity of confluence result; see the introductionof [2] for more examples. Still we think that (much) more leverage could be gotten out of DD.
Remark 1. A main feature of the TRS confluence tool CoLL [6] is that it is not built on
confluence but on commutation criteria. The idea is to (rule-based) decompose a TRS R
into a family (Ri )i of TRSs. Confluence of R follows by the Lemma of Hindley–Rosen from
commutation of all pairs (including the diagonal) Ri , Rj of family members. We suggest also
there employing DD, instead of the lemma of Hindley–Rosen, could be beneficial. In fact, an
example of such a decomposition based on DD was already given as [4, Thm. 5]. Whether/how
such decompositions could be found automatically remains to be investigated. Moreover, it
seems interesting to consider decompositions other than rule-based ones, e.g. ones obtained byinstantiation or by strategies.
Position 2. DD is the swiss-army-knife for commutation, its symmetries (factorisation), andits instances (confluence). Trying to extract appropriate families and orders on them for establishing these properties via DD, results often in (more) powerful yet (more) compact results.
How powerful is the DD technique exactly, for showing confluence and commutation?
Theorem 2.12 The DD technique is complete for confluence of rewrite systems. More precisely,
every countable13 confluent rewrite system →, is decreasing for some family and order.
As the name suggests, more than being a 1-dimensional confluence result, DD establishes a 2dimensional diagrammatic confluence result: Every peak b  a  c can be completed by somevalley b  d  c into a confluence diagram, by means of repeatedly adjoining locally decreasing
diagrams; even stronger, repeatedly adjoining such locally decreasing diagrams must terminate
after finitely many steps into a decreasing confluence diagram. We now show that countable
9 Note the reversal for the relations of the first family, turning commutation into factorisation.
10 2 lines vs. 8 lines respectively 3 lines vs. 3 pages.
11 Pous showed in 2005 that termination of (J+ · /+ )+ instead of of ←+ suffices; again DD applies, but using
step labelling instead of source-labelling [4, Example 17].
12 This was established independently by Ken Mano and the author (see Remark 2.3.29 in my PhD thesis).
The proofs employed a decomposition into a natural–number-indexed family. Recently Klop asked the question
whether smaller families suffice, upon which Endrullis, Klop and Overbeek showed that in fact doubletons do.
13 The case of uncountable systems, conjectured to be false in my PhD thesis, remains open.

3

4

Proceedings of the 9th International Workshop of Confluence, 2020

Commutation symmetries

V. van Oostrom

confluence suffices even to obtain a 3-dimensional (decreasing) diagrammatic confluence result,by a process we dub cutting 14 faces, which will be discussed more extensively below.15
Lemma 1.16 Every countable confluent rewrite system → admits a residual system [7, Sect. 8.7](−→,
◦ 1, /) with → ⊆ −→◦ ⊆ .
Proof. By countable confluence → has a spanning forest F [2, Lem. 1]. Let the relation −→◦comprise the steps of → not in F , and the reductions of F . Viewing steps of an F -reduction
as its faces its transformation into a single −→-step◦can be viewed as cutting faces, in this caseresulting in a diamond : Define the residual %/φ of % : a −→◦ b after φ : a −→◦ c by cases on theirsources and targets to be % if c = a, 1 if a = b, and c −→◦ d otherwise with d the least common
descendant of b, c in F . One checks that the (designated) diamond property, i.e. if % : a −→◦ b,
φ : a −→
◦ c then %/φ : c −→◦ d, φ/% : b −→◦ d for some d, and the (3-dimensional) cube identity(%/φ)/(ψ/φ) = (%/ψ)/(φ/ψ) hold by uniqueness of least common descendants in F .
The process of tiling by 2-dimensional local diagrams, introduced in [3] and later resumed
by Melliès, for the purpose of establishing confluence and standardisation, need not entail the
3-dimensional cube property; the edges of the 6 plane surfaces obtained by 2-dimensional tilingneed not match up. It fails both for terms [7, Fig. 8.53] and (positive) braids [7, Sect. 8.9].
Position 3. It is of interest to study residual systems for commutation ( coloured cubes).
Is DD also complete for commutation? We raised this question in [4] and at ISR 2008.
It was summarily confuted, then and there, by two participants, Endrullis and Grabmayer:
α
γ


δ

β

α

δ
(β · δ)

ζ
β

α2

δ2

γ2

(β · δ)10ζ0(β · δ)1δ

The rewrite system on the left is not (and cannot be made) decreasing. Even stronger, although
the system commutes, that cannot be shown by tiling with local commutation diagrams, as it
embeds (omit , ζ) the standard counterexample against ‘local commutation ⇒ commutation’.
As in the previous section, cutting faces comes to the rescue: Looking at the commutation
diagram (2nd from left) for the local peak α J · .δ we see it is not yet a diamond since itneeds the 2-step reduction comprising β and δ. However, cutting the reduction into a fresh
face (step) we name (β · δ), the local diagram (3rd from left) cuts a better figure/diamond.17
Adjoining (β · δ) and, symmetrically, (α · γ) gives rise to new peaks, but we see these can also
be completed into diamonds (right diagram). The rewrite system obtained is decreasing forthe labels in the natural numbers ordered by ≤, as displayed in the rightmost two diagrams.
Cutting is a common process, e.g., parallel steps −→p p for TRSs and multi-steps −→◦ for HRSs
and braids [7] can be seen as being obtained by repeatedly cutting diagrams into diamonds.18
Position 4. Minimally19 cutting faces is useful to get diamonds, decreasing diagrams and cubes.
14 Our (tentative) naming is based on that used for processing raw diamonds. However, adjoining transitive
inferences (cutting corners), is at the basis of both our cuts and those in proof theory, where, e.g., Γ ` ∆ may
be obtained by cutting the occurrence of A between Γ ` A and A ` ∆.
15 We learned the technique of cutting faces in 1995 from Hans Zantema, for braids.
16 This result was obtained in 2008, in our collaboration with Patrick Dehornoy on the Z-property.
17 The diamond is still not square, but could be made so by adjoining empty reductions reified into steps.
18 Somewhat miracuously, in these 3 cases even cubes are obtained.
19 Cutting reductions into steps by need only; if I, . commutes, simply taking II, .. as steps yields a diamond.

4Proceedings of the 9th International Workshop of Confluence, 2020

Commutation symmetries

3

5

V. van Oostrom

Diamond symmetries in term rewriting

Commutation between term rewrite systems is standardly reduced to an analysis of their criticalpeaks, cf. [6]. Symmetry suggests the same applies to factorisation, but then for peaks withrespect to the reverse of the second system. Despite that standard term rewriting theory is not
well-adapted to reverse rules, cf. Example 1, it can often be easily adapted, as we illustrate:
Example 3. Factorisation holds in the untyped λ-calculus for I := →β , . := →η . Note thereverse P → λy.P y of the η-rule is not a higher-order pattern rule in the sense of Nipkow,
as its left-hand side P is a variable. Still, we do have a (single) critical peak à la Huet withthe β-rule: Q := (λy.(λx.M )y)N . (λx.M )N I M [x:=N ] =: R; in rewriting terminology, the.-step is said to create the I-step. Toward factorisation, note the critical peak can be completed
as Q I (λx.M )N I R. Observing the first I-step is affine (non-duplicating) we decompose I
into affine I1 and non-affine steps I2 . We claim that then all local peaks are decreasing for theorder I1 < / < I2 . For the above critical diagram this holds per construction of our order. A
non-critical, i.e. non creating, local peak . · Ii can be completed by Ii · .. by standard residual
theory, using that the η-rule is linear, which again yields a decreasing diagram.
Position 5. Extending Nipkow’s higher-order critical pair lemma to allow for variable-lhss (àla Huet) is useful. Lifting results should be unproblematic (exception: development-closedness).
Example 4. To show head,internal-factorisation for untyped λβ-calculus, first note that although critical peaks seem intricate as the reverse of the β-rule is not a pattern-rule (Example 1), here there are in fact none as a step creating a head-step outside it must be head itself, so
not internal. Next, note it suffices to show I, .-factorisation for I := →h and . := −→◦ i since→i ⊆ −→◦ i ⊆ i . Finally, we conclude by DD ordering I < / since . · I ⊆ I · −→◦ ⊆ I · II · .=where the 1st inclusion holds by Church–Rosser as the I-step must be a unique residual as →i steps can neither create (noted) nor replicate I-steps, and the 2nd20 by exhaustively (it stops
by Finite Developments) selecting I-steps from −→◦ until the residual is a .-step or empty.21
Position 6. Factorisation of term rewrite system( strategie)s is best22 analysed by a criticalpeak analysis between rules and reverse rules.

References[1] B. Accattoli. An abstract factorization theorem for explicit substitutions. In Proc. 23rd RTA,
volume 15 of LIPIcs, pages 6–21. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2012.
[2] N. Hirokawa, J. Nagele, V. van Oostrom, and M. Oyamaguchi. Confluence by critical pair analysis
revisited. In Proc. 27th CADE, volume 11716 of LNCS, pages 319–336. Springer, 2019.
[3] J.W. Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht, 1980.
[4] V. van Oostrom. Confluence by decreasing diagrams, converted. In Proc. 19th RTA, volume 5117
of LNCS, pages 306–320. Springer, 2008.
[5] V. van Oostrom and Y. Toyama. Normalisation by Random Descent. In Proc. 1st FSCD, volume 52of LIPIcs, pages 32:1–32:18. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016.
[6] K. Shintani and N. Hirokawa. Coll: A confluence tool for left-linear term rewrite systems. In Proc.
25th CADE, volume 9195 of LNCS, pages 127–136. Springer, 2015.
[7] Terese. Term Rewriting Systems. Cambridge University Press, 2003.
20 Thanks to the IWC reviewers for pointing out that by mistake I had oversimplified this (part of the) proof.
21 A similar analysis applies to strategies other than head, e.g. spine or left.
22 As observed by Geuvers in (the ‘Stellingen’ going with) his PhD thesis, the above critical peak between thereverse of η and β, was missed by Barendregt in the proof of Corollary 15.1.5 in his book The Lambda Calculus.

5

6

Proceedings of the 9th International Workshop of Confluence, 2020

Parallel Closedness Revisited
Kiraku Shintani1 and Nao Hirokawa1
JAIST, Japan{s1820017,hirokawa}@jaist.ac.jp∗
Abstract
In this note we present a simple proof of Huet’s parallel closedness theorem (1980).
We also show that Toyama’s almost parallel closedness (1988), a generalization of Huet’s
theorem, is subsumed by his earlier result (1981), which is known to be a generalization ofGramlich’s confluence criterion based on parallel critical pairs (1996).

1

Introduction

The parallel closedness theorem by Huet [3] is a pioneering work in analyzing confluence of leftlinear term rewrite systems (TRSs). It claims that a left-linear TRS is confluent if every criticalq His theorem, including its ingenious proof technique, had
pair is closed by parallel step −→.
a significant influence on later confluence research. In 1996, Gramlich [2] introduced parallel
critical pairs to make a powerful variant of Huet’s theorem. While the resulting criterion enables
us to use relaxed forms for the closing condition, he also showed that it is not comparable with
Huet’s theorem. This might give us the impression that criteria based on parallel critical pairs
cannot supersede ones based on ordinary critical pairs (see e.g. [1, Section 6.5]). However, thisis wrong. We will show that Toyama’s earlier result [9] subsumes Huet’s theorem as well as
Gramlich’s criterion. Actually it subsumes the almost parallel closedness theorem [10], whichis Toyama’s later work and known as a generalization of Huet’s theorem.
In the remaining part of the note we revisit Huet’s and Toyama’s parallel closedness theorems. Introducing a new induction measure, we give a simple proof of the parallel closedness
theorem in Section 2. In Section 3 we show that Toyama’s earlier result subsumes his later
result. We assume familiarity with term rewriting [1, 8].

2

Huet’s Parallel Closedness

In this section we present a simple proof of Huet’s parallel closedness theorem [3] with a newmeasure. By denoting the critical pair t ← · →− u by t ←o→− u, the theorem is stated as follows:qDefinition 1 ([3]). A TRS is parallel closed if ←o→− ⊆ −→.

Theorem 1 ([3]). A left-linear TRS is confluent if it is parallel closed.
We prepare notations for our new measure. Let t be a term. The size of t is denoted by|t|. Given a set P of positions in t, we write |t|P for the sum of |(t|p )| for all p ∈ P . Notethat |t| > |t|P holds if P is a set of parallel positions of t. We define the strict order  as thelexicographic product of the standard order > on N and the proper superterm relation B. WeP
also prepare terminologies for analyzing peaks. Let Γ : t ←q− `σ →− rσ be a peak, where ` → r
is a rewrite rule. We say that Γ is overlapping if some position p ∈ P is a function position inP` and in the case of P = {} the rule employed in t ←q− `σ is not a variant of ` → r. Otherwise,Γ is non-overlapping. We are ready for proving the theorem.
∗ Supported by JSPS KAKENHI Grant Number 17K00011 and Core-to-Core Program.

7

8

Proceedings of the 9th International Workshop of Confluence, 2020

Parallel Closedness RevisitedK. Shintani and N. Hirokawa

||

I.H.

||

||

·

>

t

u

(ii) non-root

Q
||

s


u




PML

t

s

q

s0

||

>
||

P0

·

||

t

(iii) non-overlapping

Q0
||

u

I.H.

||

s

||

(iv) overlapping·

Figure 1: Proof of Theorem 1.
Proof of Theorem 1. Let R be a left-linear and parallel closed TRS. It is sufficient to show thatQP
q u be a peak. By well-founded induction onq has the diamond property. Let Γ : t ←q− s −→−→q(|t|P + |u|Q , s) with respect to  we show t −→ · ←q− u. Depending on the shape of Γ, we
distinguish four cases. Figure 1 illustrates cases (ii)–(iv).
q u or t ←q− u. In either case the claim holds.
(i) If P or Q is empty then t −→q f (u1 , . . . , un )(ii) If P * {} and Q * {} then Γ is of form f (t1 , . . . , tn ) ←q− f (s1 , . . . , sn ) −→PiQi

q ui for all 1 6 i 6 n. Here Pi = {p | ip ∈ P } and Qi = {q | iq ∈ Q}. Forwith ti ←q− si −→each i ∈ {1, . . . , n}, we have |t|P > |ti |Pi and |u|Q > |ui |Qi , and therefore |t|P + |u|Q >|ti |Pi + |ui |Qi . Since (|t|P + |u|Q , s)  (|ti |Pi + |ui |Qi , si ) holds, the induction hypothesis
q vi ←q− ui for some vi . Thus, t −→q f (v1 , . . . , vn ) ←q− u follows.
yields ti −→(iii) If Γ is non-overlapping and P or Q is {} then the Parallel Moves Lemma applies [1,Lemma 6.4.4]. Figure 1(iii) illustrates the case of P = {}.
(iv) If Γ is overlapping and P or Q is {}, say P = {}, then there exists an overlapping peak
Q0

q



P0

q u for Q0 = Q \ {q}. By parallel closedness we have s0 −→q t fort←−s−→ s0 with s0 −→0some P . As |t|{} > |t|P 0 and |u|Q > |u|Q0 hold, |t|{} + |u|Q > |t|P 0 + |u|Q0 holds. Sinceq · ←q− u.
(|t|{} + |u|Q , s)  (|t|P 0 + |u|Q0 , s0 ) holds, the induction hypothesis yields t −→With a small example taken from [2], we illustrate the usage of the theorem.
Example 1. Consider the left-linear and non-terminating TRS [2]:a→bf(a, a) → g(f(a, a))f(b, x) → g(f(x, x))f(x, b) → g(f(x, x))

While the TRS admits three critical peaks, all of them are closed by single parallel steps:f(a, a)f(b, a)g(f(a, a))f(a, a)f(a, b)||f(b, b)g(f(a, a))||g(f(b, b))g(f(b, b))||Thus, the TRS is parallel closed. Hence, the TRS is confluent.
Using the TRS in Example 1, we compare our induction measure with Huet’s original
measure [3]. Our proof measures a peak by the amount of contractums. Consider e.g. the peak:
{1,2}

{}

q g(f(a, a))f(b, b) ←q− f(a, a) −→2

Proceedings of the 9th International Workshop of Confluence, 2020

Parallel Closedness Revisited9

K. Shintani and N. Hirokawa

The overlined part indicates the contractums in the target terms of the parallel steps.1 So the
P2
P1
q u by theamount is |b| + |b| + |g(f(a, a))| = 6. Huet’s proof [3, 1] measures a peak t ←q− s −→amount of overlaps of redexes:X(s|p )|s, P1 , P2 | :=p∈Q1 ∪Q2

where Q1 = {p ∈ P1 | p > q for some q ∈ P2 } and Q2 = {p ∈ P2 | p > q for some q ∈ P1 }.
In the above peak the doubly underlined part indicates the overlaps of the redexes. So theamount is 2. Even with this measure the same proof goes through, provided that well-foundedinduction on (|s, P, Q|, s) with respect to  is performed. However, proving the inequality|s, {}, Q| > |s0 , P 0 , Q0 | in case (iv) is notoriously difficult [5, 4]. This part is trivial in our proof.

3

Toyama’s Extensions

Toyama made two variations of Huet’s parallel closedness theorem in 1981 [9] and in 1988 [10],but their relation has not been known. In this section we briefly recall his and related results,
and then show that Toyama’s earlier result subsumes the later one.
In 1988, Toyama showed that the closing form for overlay critical pairs, originating fromproot overlaps, can be relaxed. Let t ←−·→− u be a critical pair. We write t ←−o→ u if p = ,>and t ←−−o→ u if p > .


q · ∗← andDefinition 2 ([10]). A TRS is almost parallel closed if the inclusions ←−o→ ⊆ −→
>q hold.
←−−o→ ⊆ −→Theorem 2 ([10]). A left-linear TRS is confluent if it is almost parallel closed.
Inspired by almost parallel closedness, Gramlich [2] developed a confluence criterion basedon parallel critical pairs in 1996.


Definition 3. We say that (`σ)[rp ]p∈P ←q− `σ →− rσ is a parallel critical peak of a TRS R if
• P ⊆ PosF (`) is a non-empty set of parallel positions in `,• ` → r and `p → rp (for p ∈ P ) are variants of R-rules having no common variables,• σ is a most general unifier of {`p ≈ (`|p )}p∈P , and• if P = {} then ` → r is not a variant of ` → r.
>

P



− u is a parallel critical peak and P 6= {}.
We write t ←q−o→ u if t ←q− s →q · ∗← andTheorem 3 ([2]). A left-linear TRS is confluent if the inclusions ←o→− ⊆ −→>←q−o→ ⊆ →∗ hold.
Unfortunately, this criterion by Gramlich does not subsume (almost) parallel closedness.
Example 2 (Continued from Example 1). The TRS admits the following non-overlay parallel
critical peak f(b, b) ←q− f(a, a) →− g(f(a, a)). However, f(b, b) →∗ g(f(a, a)) does not hold.
1 Up to our best knowledge, this idea first appeared in the paper by Oyamaguchi and Ohta [7].

3

10Proceedings of the 9th International Workshop of Confluence, 2020

Parallel Closedness RevisitedK. Shintani and N. Hirokawa

As noted in the paper [2], Toyama [9] had already obtained in 1981 a closedness result that
subsumes Theorem 3.
Theorem 4 ([9]). A left-linear TRS is confluent if the following conditions hold.
q · ∗← holds.
(a) The inclusion ←o→− ⊆ −→PQ(b) Every parallel critical peak t ←q− s →− u admits S
a valley of the form t →∗ v ←q− u with
Var(s, P ) ⊇ Var(v, Q). Here Var(s, P ) stands for p∈P Var(s|p ).

Example 3. Consider again the TRS of Example 1. As witnessed in Example 1, the inclusionq holds. Thus, condition (a) of Theorem 4 holds. There are four parallel critical←o→− ⊆ −→
peaks and they can be closed as follows:g(f(a, a))f(a, b)g(f(a, a))∗g(f(b, b))∗g(f(b, b))f(b, b)g(f(a, a))

∗

∗

||

||

f(b, a)f(a, a)||f(b, b)||f(a, a)||f(a, a)g(f(b, b))

It is easy to see that the diagrams fulfil condition (b). Hence, confluence follows by Theorem 4.
We show that Theorem 4 even subsumes Theorem 2. The next lemma relates the Parallel
Moves Lemma [1, Lemma 6.4.4] to the variable condition of Theorem 4.
P





Q

Lemma 1. Let R be a left-linear TRS. If t ←q− s →− u is non-overlapping then t →− v ←q− u andVar(s, P ) ⊇ Var(v, Q) for some term v and set Q of parallel positions.
The above statement is extended to parallel peaks for almost parallel closed TRSs.
P1

P2

q u thenLemma 2. Let R be a left-linear almost parallel closed TRS. If t ←q− s −→Q1

• t →∗ v1 ←q− u and Var(s, P1 ) ⊇ Var(v1 , Q1 ) for some v1 and Q1 , andQ2

q v2 ∗← u and Var(s, P2 ) ⊇ Var(v2 , Q2 ) for some v2 and Q2 .
• t −→
P1

P2

q u. We perform well-founded induction on (|t|P1 + |u|P2 , s) with respect
Proof. Let Γ : t ←q− s −→to . We distinguish cases, depending on the shape of Γ.
Pq v.
(i) If P1 or P2 is ∅ then the claim follows from the fact: Var(w, P ) ⊇ Var(v, P ) if w −→(ii) If P1 * {} and P2 * {} then we may assume s = f (s1 , . . . , sn ), t = f (t1 , . . . , tn ), u =
Pi

Pi

1
q2 ui for all 1 6 i 6 n. Here Pki denotes the set {p | i·p ∈ Pk }.
f (u1 , . . . , un ), and ti ←q−si −→As in case (ii) of the proof of Theorem 1 we can deduce (|t|P1 +|u|P2 , s)  (|ti |P1i +|ui |P2i , si ).

Pi

Pi

1
q2 ui . By the induction hypothesis it admits valleys ofConsider an i-th peak ti ←q−
si −→

Qi

Qi

2
q1 v1i ∗← ui and ti →∗ v2i ←q−ui such that Var(vki , Qik ) ⊆ Var(si , Pki ) for boththe forms ti −→k ∈ {1, 2}. For each k, take Qk = {i · q | 1 6 i 6 n and q ∈ Qik } and vk = f (vk1 , . . . , vkn ).

QQ1
q2 v2 ∗← u hold, and moreover the inclusion
Then, t →∗ v1 ←q− u and t −→Var(vk , Qk ) =

n
[

i=1

Var(vki , Qik ) ⊆holds for each k. Hence, the claim follows.
4

n
[

i=1

Var(si , Pki ) = Var(s, Pk )

Proceedings of the 9th International Workshop of Confluence, 2020

Parallel Closedness Revisited11

K. Shintani and N. Hirokawa(iii) If Γ is non-overlapping and P1 or P2 is {} then the claim is straightforward from Lemma 1.
Q1(iv) If Γ is overlapping with P1 = P2 = {} then by almost parallel closedness t →∗ v1 ←q− uQ2

q v2 ∗← u for some v1 , v2 , Q1 , and Q2 . For each k ∈ {1, 2} we have s →∗ vk , soand t −→
Var(vk ) ⊆ Var(s) follows. Therefore, Var(vk , Qk ) ⊆ Var(vk ) ⊆ Var(s) = Var(s, {}). The
claim holds.

(v) If Γ is overlapping with P1 = {} and P2 6= {} then there exists p ∈ P2 such that
p

s −
→ s0

P2 \{p}

q
−→

P10



p

u and t ←− s −→ s0 is an instance of a critical peak. By almost parallel

closedness t ←q− s0 for some P10 . As in case (iv) of the proof of Theorem 1 we can deduce(|t|P1 +|u|P2 , s)  (|t|P10 +|u|P2 \{} , s0 ). Thus, the claim follows by the induction hypothesisP0

P \{p}

2
1
q u and Var(s0 , P2 \ {p}) ⊆ Var(s, P2 ).
for t ←q−s0 −→Theorem 5. Every left-linear and almost parallel closed TRS satisfies conditions (a) and (b)of Theorem 4. In other words, Theorem 4 subsumes Theorem 2.
q Lemma 2 entails the claim.
Proof. Since (parallel) critical peaks are instances of ←q− · −→,4

Concluding Remark

We presented a simple proof of Huet’s parallel closedness theorem, using a new measure, andalso proved that Toyama’s almost parallel closedness theorem is subsumed by his earlier result
based on parallel critical pairs. We anticipate that our measure can be adapted to otherconfluence criteria for term rewriting and conditional rewriting, while it is unclear whether it
can be adapted to the proof of van Oostrom’s development closedness [6]. At least the current
definition does not go through. Despite its powerfulness, Theorem 4 has not been well studied.
In particular, whether the variable condition of Theorem 4 is essential is our primary question.

References[1] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[2] B. Gramlich. Confluence without termination via parallel critical pairs. In Proc. 21st CAAP,
volume 1059 of LNCS, pages 211–225, 1996.
[3] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems.
Journal of the ACM, 27:797–821, 1980.
[4] J. Nagele. Mechanizing Confluence. PhD thesis, University of Innsbruck, 2017.
[5] J. Nagele and A. Middeldorp. Certification of classical confluence results for left-linear term rewrite
systems. In Proc. 7th ITP, volume 9807 of LNCS, pages 290–306, 2016.
[6] V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.
[7] M. Oyamaguchi and Y. Ohta. A new parallel closed condition for Church-Rosser of left-linear
term rewriting systems. In Proc. 10th RTA, volume 1232 of LNCS, pages 187–201, 1997.
[8] TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
[9] Y. Toyama. On the Church-Rosser property of term rewriting systems. Technical Report 17672,
NTT Electro-Technical Laboratory, 1981. In Japanese.
[10] Y. Toyama. Commutativity of term rewriting systems. In Programming of Future Generation
Computers II, pages 393–407. North-Holland, 1988.

5

12

Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic critical pair lemma
Cyrille Chenavier, Benjamin Dupont, and Philippe Malbos
1
2,3

Johanes Kepler University, Linz, Austria, cyrille.chenavier@jku.atUniversité de Lyon, France, {bdupont,malbos}@math.univ-lyon1.fr
Abstract

Convergent rewriting systems on algebraic structures give methods to prove coherence
results and compute homological invariants of these structures. These methods are basedon higher-dimensional extensions of the critical pair lemma that characterizes local confluence from confluence of critical pairs. The analysis of local confluence of rewriting systems
on algebraic structures, such as groups or linear algebras, is complicated because of theunderlying algebraic axioms, and local confluence properties require additional termination conditions. In this work, we define the structure of algebraic polygraph modulo thatformalizes the interaction between the rules of the rewriting system and the inherent algebraic axioms, and we show a critical pair lemma algebraic polygraphs. We deduce fromthis result a critical pair lemma for rewriting systems on algebraic structures specified byrewriting systems convergent modulo AC. As an illustration, we explicit our constructions
on linear rewriting systems.

1

Introduction

The critical-pair completion (CPC) is an approach developed in the mid sixties that combinescompletion procedure and the notion of critical pair [2]. It originates from theorem proving [12],polynomial ideal theory [1], and the word problem [9, 11]. In the mid eighties, CPC has foundoriginal and deep applications in algebra to solve coherence problems [14], or to compute homological invariants [13]. More recently, higher-dimensional extensions of the CPC approach wereused for the computation of cofibrant replacements of algebraic and categorical structures [5, 6].
These constructions based on CPC are known for monoids, small categories, and algebras overa field. However, the extension of these methods to a wide range of algebraic structures is madedifficult because of the interaction between the rewriting rules and the inherent axioms of thealgebraic structure. For this reason, the higher-dimensional extensions of the CPC approach
for a wide range of algebraic structures, including groups, Lie algebras, is still an open problem.
One of the main tools to reach confluence in CPC procedure for algebraic rewriting systems isthe critical pair lemma, or critical branching lemma (CBL). Its proof is based on classification of
the local branchings into orthogonal branchings, that is involving two rules that do not overlap,
overlapping branchings involving two rules that overlap. A critical branching is a minimal
overlapping application of two rules on the same redex. When the orthogonal branchings
are confluent, if all critical branchings are confluent, then local confluence holds. Thus, themain argument to achieve CBL is to prove that orthogonal and overlapping branchings areconfluent. For string and term rewriting systems, orthogonal branchings are always confluent,and confluence of critical branchings implies confluence of overlapping branchings. The situation
is more complicated for rewriting systems on a linear structure.
The well known approaches of rewriting in the linear context consist in orienting the ruleswith respect to an ambient monomial order, and CBL is well known in this context. However,some algebras do not admit any higher-dimensional finite convergent presentation on a fixed setof generators with respect to a monomial order, [5]. However, when the orientation of rules does
not depend on a monomial order, as in [5], the CBL requires additional assumptions, namely

13

14

Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

termination and positivity of reductions. A positive reduction for a linear rewriting system,as defined in [5], is the application of a reduction rule on a monomial that does not appear in
the polynomial context. For instance, consider the linear rewriting system on an associative
algebra over a field K given in [5] defined by rules α : xy → xz and β : zt → 2yt. It has no
critical branching, but it has a non-confluent additive branching:
2xβ

αt + xzt // 4xyt4αtxzt + xβ+=
xyt + xzt
3 xzt + 2xyt
. 3xyt αt + 2xyt
xyt + xβ
/ 3xzt
3αt
3xβ

4xβ

/ ···

/ 4xzt2xzt/ 6xyt6αt/ ···The dotted arrows correspond to non positive reductions. We note that the lack of termination
is an obstruction to confluence of orthogonal branchings.
In this work we introduce an algebraic setting for the formulation of the CBL. We define
the structure of algebraic polygraph modulo which formalizes the interaction between the rulesof the rewriting system and the inherent axioms of the algebraic structure. We show a CBL
for algebraic polygraphs modulo. We deduce from this result a CBL for rewriting systems on
algebraic structures whose axioms are specified by term rewriting systems that are convergent
modulo associativity and commutativity. Finally, we explicit our results in linear rewriting, andexplain why termination is a necessary condition to characterize local confluence in that case.
In Section 2, we recall the categorical structure of cartesian polygraph introduced in [10]. In
Section 3, we introduce the notion of algebraic polygraph modulo, and we refer the reader to [4]for a categorical interpretation of the given constructions. In Section 4, we present confluence
property of algebraic polygraphs modulo from [4] and algebraic polygraphs modulo with respect
a positive strategy σ. Finally, we state the algebraic critical branching lemma. This abstract
is a short version of the preprint [3], where more detailed constructions and examples can befound.

2

Cartesian polygraphs

A signature is defined by a set P0 of sorts and a set P1 of operations on the free monoid overP0 . We denote by s0 (α) and t0 (α) the arity and coarity of α ∈ P1 . When s1 , . . . , sk are sorts,
we denote s = s1 . . . sk their product in the free monoid over P0 . We denote by P1× the freetheory generated by a signature (P0 , P1 ). Its 1-cells, also called terms on the signature (P0 , P1 )s
are defined inductively. The canonical projections xi : s → si are variables, and for any terms
f : s → r and f 0 : s → r 0 in P1× , we denote by hf, f 0 i : s → rr 0 , the pairing of terms f, f 0 . A(cartesian) 2-polygraph is a data made of a signature (P0 , P1 ), and a set P2 equipped with twomaps t1 , s1 : P2 → P1× , satisfying the globular conditions s0 s1 = s0 t1 and t0 s1 = t0 t1 . Anelement α of P2 is called a rule, and relates terms of same arity and coarity.
2.1. Two-dimensional theories. Recall that a 2-theory is a 2-category with an additional
cartesian structure on its 1-cells and 2-cells [10]. We denote by P2× the free 2-theory generated
by a cartesian 2-polygraph (P0 , P1 , P2 ). Its underlying 1-category is the free theory P1× , andits 2-cells are defined inductively as follows. For α : f ⇒ f 0 in P2 and h ∈ P1× , there is a 2-cell
αh : f ? h ⇒ f 0 ? h in P2× , and for β : g ⇒ g 0 in P2× , there is a 2-cell hα, βi : hf, gi ⇒ hf 0 , g 0 i.
2Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic critical pair lemma

15

Chenavier, Dupont, and Malbos

Finally, there are 2-cells in P2× of the form A[α] : A[f] ⇒ A[f 0 ] where A[] denotes an algebraic
context of the form: khidk1 , . . . , i , . . . , idkj i : s → r, where k1 , . . . , kj : s → ri and k : r → r
belong to P1× , and i is the i-th element of the pairing. These 2-cells are required to satisfy
exchange relations, see [10]. The source and target maps s1 , t1 extend to P2× and we denote a−
and a+ for s1 (a) and t1 (a). A ground term in P1× is a term with source 0. A 2-cell a in P2× isground when a− is a ground term. An algebraic context A[] = fhf1 , . . . , i , . . . f|r| i is called
ground when the fi are ground terms.
The free (2, 1)-theory generated by a cartesian 2-polygraph (P0 , P1 , P2 ), denoted by P2> , isthe free 2-theory P2× whose any 2-cell is invertible with respect the ?-composition. The 2-cellsof the (2, 1)-theory P2> corresponds to elements of the equivalence relation generated by P2 .
2.2. Rewriting properties of cartesian polygraphs. The algebraic contexts of a 2polygraph P can be composed as follows AA 0 [] := A[A 0 []]. One defines a bi-context as
B[i , j ] := fhidf1 , . . . , i , . . . , j , . . . , idfk i where the fk : s → rk and f : r → r are terms in
P1× , and i (resp. j ) has to be filled by a term gi : s → ri (resp. gj : s → rj ). A 2-cellof the form A[αw] where A is an algebraic context, w is a term in P1× and α ∈ P2 is calleda P-rewriting step. A P-rewriting path is a non-identity 2-cell of P2× . Such a 2-cell can be
decomposed as a ?-composition of rewriting steps α = A1 [α1 w1 ] ? . . . Ak [αk wk ].

3

Algebraic polygraphs modulo

Let (P0 , P1 ) be a signature, and Q be a set of generating ground terms whose target is a sort×in P0 . We denote by P1 hQi the set of ground terms of the free theory (P1 ∪ Q) . An algebraic
polygraph is a data made of a 2-polygraph P, a family of set of constant 1-cells Q, and a cellularextension R of the set of ground terms P1 hQi, that is a set equipped with two source andtarget maps R → P1 hQi. A R-rewriting step is a ground 2-cell in the free 2-theory R× of theform A[α] : A[f] → A[g], where A[] is a ground context. A R-rewriting path is a finite or
infinite sequence a1 ? . . . ? ak ? . . . of R-rewriting steps ai . The size of a R-rewriting path a,denoted by |a|, is the number of rewriting steps needed to write a as a composition as above.
The cellular extension P2 defined on P1× extends to a cellular extension on the free 1-theory×b2 . We denote by P2 hQi the set of ground 2-cells in the free 2-theory(P1 ∪ Q) denoted by P×b2 ) . The algebraic polygraph (P, Q, P2 hQi) is called the algebraic polygraph of axioms. We(Pdenote by PhQi the quotient of P1 hQi by the congruence generated by relations in P2 hQi.

3.1. Positive strategies. Denote by f the image of a ground term f by the canonical projection π : P1 hQi → PhQi. Let σ : PhQi → Set be a map such that for any f ∈ PhQi, σ(f) isa chosen non-empty subset of π−1 (f). Such a map is called a positive strategy with respect to(P, Q). A R-rewriting step a is called σ-positive if a− belongs to σ(a− ), and a R-rewriting patha1 ? . . . ? ak is called σ-positive if any of its rewriting steps is positive.
We will use positive strategies wrt a 2-polygraph P such that P2 = P20 ∪P200 , with P20 confluent
modulo P200 . For every 1-cell f in PhQi, we set σ(f) = NF(f, P20 mod P200 ), where f ∈ π−1 (f),the set of normal forms of f for P20 modulo P200 . This is well-defined following [7], since if
f, f 0 ∈ π−1 (f), then NF(f, P20 mod P"2 ) ≡P"2 NF(f 0 , P20 mod P"2 ).

3.2. Algebraic polygraphs modulo. Given an algebraic polygraph P = (P, Q, R) and apositive strategy σ on P, one denotes by P RP the cellular extension of P1 hQi whose elements
are of the form e ? a ? e 0 , where e and e 0 are 2-cells in P2 hQi> and a is a R-rewriting step such3

16

Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

0that e+ = a− and a+ = e−
, see [4] for a detailed construction. A 2-cell e ? a ? e 0 in P RP iscalled σ-positive if a is a σ-positive R-rewriting step. An algebraic polygraph modulo, APM forshort, is a data (P, Q, R, S) made of an algebraic polygraph (P, Q, R), and a cellular extension S
of P1 hQi such that R ⊆ S ⊆ P RP .
An algebraic polygraph (P, Q, R) is called quasi-terminating if for each sequence (fn )∈N of
1-cells of P1 hQi such that for each n ∈ N, there is a rewriting step fn → fn+1 , the sequence(fn )∈N contains an infinite number of occurrences of same 1-cell. An APM (P, Q, R, S) is called
quasi-terminating if the algebraic polygraph (P, Q, S) is quasi-terminating. A 1-cell f of P1 hQi
is quasi-irreducible if for any S-rewriting step f → g, there exists a S-rewriting sequence from g
to f. A quasi-normal form of a 1-cell f in P1 hQi is a quasi-irreducible 1-cell fe of P1 hQi such thate For a quasi-terminating APM, any 1-cell f ofthere exists a S-rewriting sequence from f to f.
P1 hQi admits at least a quasi-normal. A quasi-normal form strategy is a map s : P1 hQi → P1 hQiesending a 1-cell f on a chosen quasi-normal f.
An algebraic rewriting system on (P, Q, R, S, σ) is a cellular extension S of PhQi defined byσσ
S = {a : a− ⇒ a+ | a ∈ S}. Let us consider the subset S of S defined by S = {a : a− ⇒σ
×a+ | a is a σ-positive S-rule}. A S-rewriting step (resp. a S -rewriting step) is a 2-cell in S
σ×

(resp. S ) of the form C[a] : C[a− ] ⇒ C[a+ ] , where C is a ground context of P1 hQi and C[a]is a S-rewriting step (resp. σ-positive S-rewriting step). A S-rewriting path is a sequence of
S-rewriting steps.

4

Confluence in algebraic polygraphs modulo

Let P = (P, Q, R, S) be an APM with a positivity strategy σ. A σ-branching of P is a triple(a, e, b) where a, b are σ-positive 2-cells of S× and e is a 1-cell of P2 hQi> such that e− =a− and e+ = b− . It is local if a is a S-rewriting step, b is a 2-cell of S× and e a 2-cellof P2 hQi> such that |e| + |b| = 1. Note that the 2-cell b (resp. e) can be an identity 2cell of S× (resp of P2 hQi> ), and in that case the σ-branching is of the form (a, e) (resp.
(a, b)). Such a σ-branching is σ-confluent modulo if there exist σ-positive 2-cells a 0 and b 0
0
in S× and a 2-cell e 0 of P2 hQi> as depicted on the right. We say that f a / f 0 a / h
the APM P is confluent modulo (resp. locally confluent modulo) if any e
 e0

/ g0
/ h0
σ-branching modulo (resp. local branching modulo) is confluent modulo. g
0bb

4.1. Theorem (Newman lemma modulo for algebraic polygraphs modulo). Let P bea quasi-terminating APM, and σ be a positive strategy on P. If P is locally σ-confluent modulo,
then it is σ-confluent modulo.
The proof of this result, and of Thm. 4.4 are based on the principle of double induction
on the distance to the quasi-normal form, and are extensions to quasi-terminating setting of
Huet’s constructions based on double induction principle [7] in the terminating setting. Let
d : P1 hQi → N maping a 1-cell f to the length d(f) of the shortest P RP -rewriting path from fe that we extend to a map on σ-branchings (a, e, b) by setting d(a, e, b) := d(a− ) + d(b− ).
to f,
We define a well-founded order ≺ on the set of σ-branchings of P by (a, e, b) ≺ (a 0 , e 0 , b 0 ) ifd(a, e, b) < d(a 0 , e 0 , b 0 ).
4.2. Classification of local σ-branchings modulo. The local σ-branchings modulo of S
can be classified in the following families:
A[a+ ] o4aA[a− ]
Triviala/ A[a+ ]A[a+ ] oabA[a− ] = A[A 0 [b− ]]Inclusion independant/ A[A 0 [b+ ]]Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic critical pair lemma

B[a,b− ]Chenavier, Dupont, and Malbos/ B[a+ , b− ]=B[a− , b− ]B[a− , b− ]17

B[a− , e− ]B[a,e− ]/ B[a+ , e− ]B[a− ,e]B[a− ,b]/ B[a− , b+ ]OrthogonalB[a− , t1 (e)]Orthogonal modulo

together with symmetries on orthogonal σ-branchings modulo, for some σ-positive S-rewriting
steps a, b, 2-cell e in P2 hQi> , ground contexts A, A 0 , and ground bi-contexts B, B 0 . The
remaining local σ-branchings modulo are called non-orthogonal σ-branchings modulo.
We define an order relation on σ-branchings modulo of P = (P, Q, R, S) by setting (a, e, b) v
(A[a], A[e], A[b]) for a ground context A. A critical σ-branching modulo is a local σ-branchingmodulo P which is non trivial, non orthogonal and minimal wrt the order relation v.
4.3. Positive confluence. An APM (P, Q, R, S) with a positive strategy σ is called σ-positively
confluent if, for any S-rewriting step f, there exists a representing
a0
/
af
−
0
0
af
− ∈ σ(a− ) of a− and two σ-positive S-reductions a and b ofe e 00size at most 1 as in the following on the right.
/
/
/
a
−

a

e0

b0

4.4. Theorem (Terminating critical branching theorem modulo). Let (P, Q, R, S) be aquasi-terminating and positively σ-confluent APM with a positive strategy σ. Then it is locally
σ-confluent modulo if and only if the two following properties hold:a0 ) any critical σ-branching modulo (a, b) made of S-rewriting steps is σ-confluent modulo.
b0 ) any critical σ-branching modulo (a, e), with a S-rewriting step and e is a 2-cell in P2 hQi>
of length 1, is σ-confluent modulo.
When all the reductions are positive, that is S(u) = π−1 (u) for any u, the quasi-termination
assumption in Prop. 4.4 are not needed. In that case, the positive confluence is always satisfied.
4.5. Algebraic critical branching lemma. Let A be an algebraic rewriting system on an
APM P = (P, Q, R, S). The critical branchings of A are the projections of the critical σσbranchings modulo of P of the form a0 ), that is pairs (a, b) of S -rewriting steps such thatfthere is a σ-branching modulo in P with source (af− , b− ). From Prop. 4.4, we deduce our main
result.

4.6. Theorem. Let P = (P, Q, R, S) be an APM such that P RP is quasi-terminating and positively confluent. Let A be an algebraic rewriting system on P. Then A is locally confluent if
and only if its critical branchings are confluent.

4.7. CBL for linear rewriting. Suppose that P contains the convergent 2-polygraph modulo
AC that presents the theory of modules over commutative rings given in [8], denoted by RMod.
If P200 is the 2-polygraph of associativity and commutativity relations, and P20 is RMod, thenThm. 4.6 corresponds to CBL for linear rewriting systems proved in [5]. Indeed, given an APM(P, Q, R, S) with the σ-strategy defined in 3.1, one proves that the positivity confluence of S withrespect to σ implies the factorization property of [5]. This property means that any rewritingσstep a of S can be decomposed as a = b ? c−1 where b and c are either rewriting steps of S or
identities. Finally, the quasi-termination assumption of P RP is equivalent to the termination
assumption in [5].
5

18Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

References[1] B. Buchberger. An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo
a Zero Dimensional Polynomial Ideal. PhD thesis, University of Innsbruck, Austria, 1965.
[2] B. Buchberger. History and basic features of the critical-pair/completion procedure. J. Symbolic
Comput., 3(1-2):3–38, 1987. Rewriting techniques and applications (Dijon, 1985).
[3] Cyrille Chenavier, Benjamin Dupont, and Philippe Malbos. Algebraic polygraphs modulo andlinear rewriting. preprint, arXiv:2004.14361, 2020.
[4] B. Dupont and P. Malbos. Coherent confluence modulo relations and double groupoids.
arXiv:1810.08184, Hal-01898868, 2018.
[5] Y. Guiraud, E. Hoffbeck, and P. Malbos. Convergent presentations and polygraphic resolutions ofassociative algebras. Math. Z., 2019.
[6] Y. Guiraud and P. Malbos. Higher-dimensional normalisation strategies for acyclicity. Adv. Math.,
231(3-4):2294–2351, 2012.
[7] G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. J.
Assoc. Comput. Mach., 27(4):797–821, 1980.
[8] J.-M. Hullot. A catalogue of canonical term rewriting systems. 1980. SRI International, Technical
Report CSL 113.
[9] D. Knuth and P. Bendix. Simple word problems in universal algebras. In Computational Problems
in Abstract Algebra (Proc. Conf., Oxford, 1967), pages 263–297. Pergamon, Oxford, 1970.
[10] P. Malbos and S. Mimram. Cartesian polygraphic resolutions. in progress, 2020.
[11] M. Nivat. Congruences parfaites et quasi-parfaites. In Séminaire P. Dubreil, 25e année (1971/72),
Algèbre, Fasc. 1, Exp. No. 7, page 9. Secrétariat Mathématique, Paris, 1973.
[12] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12:23–41,
1965.
[13] C. Squier and F. Otto. The word problem for finitely presented monoids and finite canonicalrewriting systems. In RTA, 1987, volume 256 of LNCS, pages 74–82. 1987.
[14] C. C. Squier, F. Otto, and Y. Kobayashi. A finiteness condition for rewriting systems. TCS,
131(2):271–294, 1994.

6

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus
Ugo de’Liguoro and Riccardo Treglia
Università di Torino, Turin, Italyugo.deliguoro@unito.it
riccardo.treglia@unito.it
Abstract
We study the reduction of the computational λ-calculus in the untyped case. To thisaim, we consider a minimal fragment of the λ-calculus with monads as introduced byWadler, and define a notion of call-by-value reduction just by orienting the three monadequational laws. We then prove confluence of its compatible closure. Finally, we show
factorization of any reduction sequence into essential and inessential steps.

1

Introduction

The computational λ-calculus, called λc , was introduced by Moggi [Mog89, Mog91] as a metalanguage to describe non functional effects in programming languages via an incremental approach. Much as for ordinary λ-calculus, the equational theory of λc can be modelled by theconvertibility relation induced by a reduction relation. Building the reduction theory of λc ishowever quite challenging. A first attempt is in §6 of [Mog89], where the defined notion of
reduction consists of six rules plus η. Proving confluence of this reduction relation revealed tobe quite hard; it was studied in the context of call-by-need calculi, e.g. in [MOTW99, AFM+ 95]
obtaining partial results, but a full proof has been achieved only recently in [Ham18].
Aiming at a logical analysis of the semantics of the untyped λc in terms of an intersection
type assignment system, we proposed in [dT19] a simplified syntax, which is derived from
Wadler’s λ-calculus with monads, and defined reduction just by orientating the three monadlaws in [Wad92, Wad95]. We dub λuc our calculus, and −→λC the reduction relation. This is
the content of section 2 of the present note.
Although one can translate Moggi’s syntax into ours, preserving and reflecting the respective
reduction relations, the inverse translation just preserves conversion, so that confluence in our
calculus cannot rest on the same property of the original λc , and the proof had to be reworked
anew. We sketch the proof from [dT19] in section 3.
Confluence is not the only fundamental property of reduction in λ-calculi; further examples
are standardization and the existence of normalizing strategies. Toward the study of theseproperties in the case of λuc and −→λC , we explore here in section 4 factorization for our
calculus by adapting results in [AFG19].
While the confluence proof is included in a revised version of [dT19] and has been submitted
for publication, the factorization results are new.

2

Untyped λc -calculus

The syntax of the untyped computational λ-calculus, shortly λuc , and its reduction relation as
introduced in [dT19], are reported below:

19

20

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus

de’Liguoro, Treglia

Definition 2.1 (Terms of λuc ). The terms of the untyped computational λ-calculus, shortly
λuc , consist of two sorts of expressions:
Val :
Com :

V, W
M, N

::= x | λx.M::= unit V | M ? V(values)(computations)where x ranges over a denumerable set Var of variables. We set Term = Val ∪ Com; FV(V )and FV(M ) are the sets of free variables occurring in V and M respectively, and are definedin the obvious way. Terms are identified up to clash avoiding renaming of bound variables(α-congruence).
With respect to Moggi’s λc -syntax, we do not have the let construct, which is considered assyntactical sugar for bind and abstraction:
let x = N in M ≡ N ? λx.M
Notably we do not have application in the syntax, since it is definable (see below).
Definition 2.2 (Reduction). Define the following reduction relation 7→λC = 7→βc ∪ 7→id ∪ 7→ass
over Com by:
βc )
id )
ass )

unit V ? (λx.M ) 7→
M ? λx.unit x 7→
(L ? λx.M ) ? λy.N 7→

M [V /x]M
L ? λx.(M ? λy.N )for x 6∈ F V (N )where M [V /x] denotes the capture avoiding substitution of V for x in M . Finally define therelation −→λC as the compatible closure of 7→λC .
Rule βc is reminiscent of the left unit law in [Wad95]; we call it βc because it performs callby-value β-contraction in λuc . In fact, by reading ? as postfix functional application and merging
V into its trivial computation unit V , βc is the same as βv in [Plo75]. Now, let V, W ∈ Val andM, N ∈ Com; then define:
VW
VN≡ unit W ? V≡ N ?VMV
MN≡≡

M ? (λz.unit V ? z)
M ? (λz.N ? z)∗∗

where z is fresh. Then it is easy to see that, if M −→λC unit (λx.M 0 ) and N −→λC unit V∗
then M N −→λC M 0 [V /x].

3

Confluence

Following a strategy used in case of call-by-need calculi with the let construct (see [AFM+ 95,
MOTW99]), and more recently with the variant of call-by-value λ-calculus in [CG14], we split
the proof in three steps, proving confluence of βc ∪ id and ass separately, eventually combining
these results by means of the commutativity of these relations.
In the first step we adapt the parallel reduction method, originally due to Tait and MartinLöf, and further developed by Takahashi [Tak95]. See e.g. the book [Ter03] ch. 10. Let’s define
the following relation −→:◦Definition 3.1. The relation −→◦ ⊆ Term × Term is inductively defined by:2

Proceedings of the 9th International Workshop of Confluence, 2020

21

On the reduction of the type-free computational λ-calculus

de’Liguoro, Tregliai) x −→◦ xii) M −→
◦ N ⇒ λx.M −→◦ λx.Niii) V −→◦ V 0 ⇒ unit V −→◦ unit V 00iv) M −→
◦ M and V −→◦ V 0 ⇒ M ? V −→◦ M0 ? V 000v) M −→◦ M and V −→◦ V ⇒ unit V ? λx.M −→◦ M 0 [V 0 /x]
00vi) M −→
◦ M ⇒ M ? λx.unit x −→◦ MBy i) - iv) above, relation −→◦ is reflexive and coincides with its compatible closure. Also−→βc ,id ⊆ −→;◦ intentionally, this is not the case w.r.t. the whole −→λC . Now, by means of∗Lemma 3.2 one easily proves that −→◦ ⊆ −→βc ,id .
Lemma 3.2. For M, M 0 ∈ Com and V, V 0 ∈ Val and every variable x, if M −→◦ M 0 and
0
0
0
V −→
◦ V , then M [V /x] −→◦ M [V /x].
The next step in the proof is to show that the relation −→◦ satisfies the triangle property:∀P ∃P ∗ ∀Q. P −→◦ Q ⇒ Q −→
◦ P∗

TP :

where P, P ∗ , Q ∈ Term. TP implies the diamond property, which for −→◦ is:∀P, Q, R. P −→◦ Q & P −→◦ R ⇒ ∃P 0 . Q −→◦ P 0 & R −→
◦ P0

DP :

In fact, if TP holds then we can take P 0 ≡ P ∗ in DP, since the latter only depends on P . We
then define P ∗ in terms of P as follows:i) x∗ ≡ xii) (λx.M )∗ ≡ λx.M ∗iii) (unit V )∗ ≡ unit V ∗iv) (unit V ? λx.M )∗ ≡ M ∗ [V ∗ /x]v) (M ? λx.unit x)∗ ≡ M ∗ , if M 6≡ unit V for V ∈ Valvi) (M ? V )∗ ≡ M ∗ ? V ∗ , M 6≡ unit W for W ∈ Val and V 6≡ λx.unit x
Lemma 3.3. For all P, Q ∈ Term, if P −→◦ Q then Q −→◦ P ∗ , namely −→◦ satisfies TP.
According to [Bar84], Def. 3.1.11, a notion of reduction R is said to be confluent or Church∗
Rosser, shortly CR, if −→R satisfies DP; more explicitly for all M, N, L ∈ Com:
∗

∗

∗

∗

M −→R N & M −→R L ⇒ ∃M 0 ∈ Com. N −→R M 0 & L −→R M 0
Corollary 3.4. The notion of reduction βc ∪ id is CR.
To prove confluence of ass we use Newman Lemma (see [Bar84], Prop. 3.1.24). A notion of
reduction R is weakly Church-Rosser, shortly WCR, if for all M, N, L ∈ Com:∗∗

M −→R N & M −→R L ⇒ ∃M 0 ∈ Com. N −→R M 0 & L −→R M 0
Lemma 3.5. The notion of reduction ass is WCR.
Recall that a notion of reduction R is strongly normalizing, shortly SN, if there exists no
infinite reduction M −→R M1 −→R M2 −→R · · · out of any M ∈ Com.
Lemma 3.6. The notion of reduction ass is SN.
Corollary 3.7. The notion of reduction ass is CR.
3

22

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus

de’Liguoro, Treglia

Proof. By Lem. 3.5, 3.6 and by Newman Lemma, stating that a notion of reduction which is
WCR and SN is CR.
Finally we show that −→βc ,id and −→ass commute. The following definitions are from
[BN98], Def. 2.7.9. Relations −→1 and −→2 strongly commute if, for all M, N, L: N 1 ←−=∗=M −→2 L ⇒ ∃P. N −→2 P 1 ←− L where −→2 is −→2 ∪ =, namely at most one reduction
step.
Lemma 3.8. Reductions −→βc ,id and −→ass strongly commute, then commute.
Proof. By Lemma 2.7.11 in [BN98], two strongly commuting relations commute, and commutativity is clearly symmetric; hence it suffices to show that=∗

N βc ,id←− M −→ass L ⇒ ∃P ∈ Com. N −→ass P βc ,id←− L.
We can limit the cases to the critical pairs. For a full development see [dT19].
By the commutative union lemma (see [BN98], Lem. 2.7.10 and [Bar84], Prop. 3.3.5), if−→βc ,id and −→ass and are both CR (Cor. 3.4 and 3.7), and commute (Lem. 3.8) follows:
Theorem 3.9 (Confluence). The notion of reduction λC is CR.

4

Factorization

Specializing the definition of factorization in [AFG19], we say that an abstract reduction system(Term, −→) factorizes via −→e , −→¬e if −→ = −→e ∪ −→¬e and for all M, N ∈ Term,∗∗∗
M −→ N implies that there exists L ∈ Term such that M −→e L −→¬e N . We abbreviate the∗∗last condition by M −→e · −→¬e N .
Now, we take −→ = −→λC and construct the relations −→e , −→¬e , called the essential andinessential in [AFG19], by closing 7→λC under two sorts of contexts:
Inessential contexts:
Essential contexts:

¬E
E

::=
::=

h·C i | unit λx.¬E | M ? λx.¬E | ¬E ? V
h·C i | E ? V

where the hole h·C i can be filled by terms in Com only. Then −→e and −→¬e are the least
relations including 7→λC such that for all M, N ∈ Com, essential context E and inessential
context ¬E it holds:
M 7→λC N =⇒ EhMi −→e EhNi

and

M 7→λC N =⇒ ¬EhMi −→¬e ¬EhNi

We highlight that relations −→e and −→¬e are actually not disjoint, as essential steps are also
inessential.
The factorization property ensures that any finite reduction can be re-arranged into an
essential reduction followed by some inessential steps. In our case, this corresponds to a weakhead reduction, with the twist that in a bind expression the argument appears to the left of
the function.
The key of the proof of the Factorization Theorem 4.4 is the construction of two further
auxiliary relations ⇒¬e and ⇒λC , such that the conditions in Proposition 4.3 hold.
Definition 4.1 (Inessential parallel reduction). The relation ⇒¬e ⊆ Term×Term is inductively
defined by:4

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus

23de’Liguoro, Tregliai) x ⇒¬e xii) M ⇒λC N ⇒ λx.M ⇒¬e λx.Niii) V ⇒λC V 0 ⇒ unit V ⇒¬e unit V 0iv) M ⇒¬e M 0 and V ⇒¬e V 0 ⇒ M ? V ⇒¬e M 0 ? V 0v) L ⇒¬e L0 and M ⇒λC M 0 and N ⇒λC N 0 ⇒ (L?λx.M )?λy.N ⇒¬e L0 ?λx.(M 0 ?λy.N 0 )nDefinition 4.2 (Indexed parallel reduction). The relation =⇒ ⊆ Term × Term is inductively
defined by:0i) x =
⇒x
n

n

n

n

ii) M =⇒ N ⇒ λx.M =⇒ λx.Niii) V =⇒ V 0 ⇒ unit V =⇒ unit V 0
n

m

n

m

n+m

iv) M =⇒ M 0 and V =⇒ V 0 ⇒ M ? V ===⇒ M 0 ? V 0n+|M 0 |x ·m+1v) M =⇒ M 0 and V =⇒ V 0 ⇒ unit V ? λx.M =========⇒ M 0 [V 0 /x]nnvi) M =⇒ M 0 ⇒ M ? λx.unit x =⇒ M 0
n

m

p

n+m+p

vii) L =⇒ L0 and M =⇒ M 0 and N =⇒ N 0 ⇒ (L ? λx.M ) ? λy.N =====⇒ L0 ? λx.(M 0 ? λy.N 0 )where |M |x is the number of free occurrences of x in M .
01

nNote that =⇒ is the identity relation on Term, =⇒ is −→λC defined in 2.2, and =⇒⊆−→n .
nDefine ⇒λC := ∪n∈N =⇒. Observe that the above definition is essentially the same as that oneof −→◦ in Def. 3.1, but for clause vii): adding the latter to −→◦ would break property DP, thatindeed is not satisfied by ⇒λC .
An abstract reduction system that satisfies the following conditions is called a macro-stepsystem in [AFG19].
Proposition 4.3 (λC Macro-step system).
i) Merge: if M ⇒¬e · −→e M 0 then M ⇒λC M 0nn−1ii) Indexed split: if M =⇒ M 0 , then M ⇒¬e M 0 , or n > 0 and M −→e · ===⇒ M 0∗iii) Split: If M ⇒λC M 0 , then M −→e · ⇒¬e M 0 .

Once we have established that (Term, −→e ∪ −→¬e ) is a macro-step system with respect to⇒λC and ⇒¬e . Since in [AFG19] is proved that every Macro-step system satisfies factorization,
we have the following theorem.
Theorem 4.4 (Factorization). The reduction system (Term, −→λC ) factorizes via −→e , −→¬enamely∗∗∗M −→λC M 0 ⇒ M −→e · −→¬e M 0

References[AFG19]Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorization and normalization, essentially. In APLAS 2019: Programming Languages and Systems, volume 11893
of Lecture Notes in Computer Science, page 159–180. Springer Verlag, 12 2019.

5

24

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus[AFM+ 95]

de’Liguoro, Treglia

Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The
call-by-need lambda calculus. In Ron K. Cytron and Peter Lee, editors, Conference Recordof POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, San Francisco, California, USA, January 23-25, 1995, pages 233–246. ACM
Press, 1995.
[Bar84]
H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.
[BN98]
Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University
Press, 1998.
[CG14]
Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-byvalue solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, volume 8412 of Lecture
Notes in Computer Science, pages 103–118. Springer, 2014.
[dT19]
Ugo de’Liguoro and Riccardo Treglia. Intersection types for the computational lambdacalculus. CoRR, abs/1907.05706, 2019.
[Ham18]
M. Hamana. Polymorphic rewrite rules: Confluence, type inference, and instance validation. In Functional and Logic Programming - 14th International Symposium, FLOPS 2018,
Nagoya, Japan, May 9-11, 2018, Proceedings, volume 10818 of Lecture Notes in Computer
Science, pages 99–115, 2018.
[Mog89]E. Moggi. Computational Lambda-calculus and Monads. In Proceedings of Logic in Computer Science (LICS), pages 14–23, 1989.
[Mog91]
E. Moggi. Notions of Computation and Monads. Information and Computation, 93:55–92,
1991.
[MOTW99] John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-byvalue, call-by-need and the linear lambda calculus. Theor. Comput. Sci., 228(1-2):175–210,
1999.
[Plo75]G. D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer
Science, 1:125–159, 1975.
[Tak95]
M. Takahashi. Parallel reduction in lambda-calculus. Information and Computation,
118:120–127, 1995.
[Ter03]
Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer
Science. Cambridge University Press, 2003.
[Wad92]
P. Wadler. The essence of functional programming. In Conference Record of the Nineteenth
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
Albuquerque, New Mexico, USA, January 19-22, 1992, pages 1–14, 1992.
[Wad95]
P. Wadler. Monads for Functional Programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming TechniquesTutorial Text, volume 925 of Lecture Notes in Computer Science, pages 24–52. SpringerVerlag, 1995.

6

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculusA

25

de’Liguoro, Treglia

Proof of Factorization
n

n

m

k

Lemma A.1. (Substitutivity of =⇒) If M =⇒ M 0 and V =⇒ V 0 then M [V /x] =⇒ M 0 [V 0 /x]
where k = n + |M 0 |x · m.

Proof. Proof by induction on the structure of M . We will show just notable cases:
Application: This case occurs when the last rule applied is
n

n

N
⇒ N0
N ==

n +n

W
⇒ W0
W ==

=⇒ N 0 ? W 0 = M 0
M = N ? W ==N===Wk1
N 0 [V 0 /x] where k1 = nN + |N 0 |x · m
by i.h. N [V /x] ==⇒k

2
W 0 [V 0 /x] where k2 = nW + |W 0 |x · m
and W [V /x] ==⇒
then
k1
k2
N 0 [V 0 /x]
W [V /x] ==⇒W 0 [V 0 /x]
N [V /x] ==⇒k

M [V /x] = N [V /x] ? W [V /x] =⇒ N 0 [V 0 /x] ? W 0 [V 0 /x] = M 0 [V 0 /x]
where k = k1 +k2 = nN +|N 0 |x ·m+nW +|W 0 |x ·m = n+|M 0 |x ·m, in fact |M 0 |x = |N 0 |x +|W 0 |x .
βc −step: This case occurs when the last step has the following shape:
n

n

W
W ==
⇒ W0

n

N
N ==
⇒ N0

M = unit W ? λy.N =⇒ N 0 [W 0 /y] = M 0
where n = nN + |N 0 |y · nW + 1.
Assuming wlog x 6= y, |M 0 |x = |N 0 [W 0 /y]|x = |N 0 |x + |N 0 |y · |W 0 |x
M [V /x] = unit W [V /x] ? λy.N [V /x]
M 0 [V 0 /x] = N 0 [V 0 /x][W 0 [V 0 /x]/y]k

1
By i.h. N [V /x] ==⇒N 0 [V 0 /x] where k1 = nN + |N 0 |x · mkk2
W [V /x] ==⇒W 0 [V 0 /x] where K2 = nW + |W 0 |x · m, then M [V /x] =⇒ M 0 [V 0 /x] wherek= k1 + |N 0 |y · k2 + 1 == nN + |N 0 |x · m + |N 0 |y · (nW + |N 0 |x · m) + 1 == nN + |N 0 |y · nW + 1 + |N 0 | · m + |N 0 |y · |W 0 |x · m == n + |M 0 |x · m

id−step:nN =⇒ N 0n

M = N ? λy.unit y =⇒ N 0 = M 0
And M [V /x] = N [V /x] ? λy.unit y[V /x]k1
By i. h. N [V /x] ==⇒N 0 [V 0 /x] where k1 = n + |N 0 |x · m

7

26

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus

de’Liguoro, Treglia

0λy.unit y[V /x] =⇒ λy.unit y.
k1
N 0 [V 0 /x]
N [V /x] ==⇒k

M [V /x] = N [V /x] ? λy.unit y[V /x] =⇒ N 0 [V 0 /x] = M 0 [V 0 /x]
Then k = k1 .
n

n

n

N
⇒ N 0,
ass−step: M = (L ? λy.N ) ? λz.P =⇒ L0 ? λy.(N 0 ? λz.P ) where L ==L⇒ L0 , N ==n

P ==P⇒ P 0 and n = Nl + nN + nP .
by i.h.
k1
L0 [V 0 /x] where k1 = nL + |L0 |x · m
L[V /x] ==⇒k2
N 0 [V 0 /x] where k2 = nN + |N 0 |x · m
N [V /x] ==⇒k3
P 0 [V 0 /x] where k3 = nP + |P 0 |x · m
P [V /x] ==⇒k

1
L[V /x] ==⇒L0 [V 0 /x]k2
N [V /x] ==⇒N 0 [V 0 /x]k

3
P [V /x] ==⇒P 0 [V 0 /x]k

M [V /x] = (L[V /x] ? λy.N [V /x]) ? λz.P [V /x] =⇒ L0 [V 0 /x] ? λy.(N 0 [V 0 /x] ? λz.P [V 0 /x])
where k = k1 + k2 + k3 = nL + |L0 |x · m + nN + |N 0 |x · m + nP + |P 0 |x · m = n + |M 0 |x · m.
Proposition A.2 (λC Macro-step system).
1. Merge: if M ⇒¬e · −→e M 0 then M ⇒λC M 0nn−1
2. Indexed split: if M =⇒ M 0 , then M ⇒¬e M 0 , or n > 0 and M −→e · ===⇒ M 0
3. Split: If M ⇒λC M 0 , then M −→∗e · ⇒¬e M 0 .

Proof. 1.Merge: by structural induction on M ⇒¬e N .
Following hypothesis, since N −→e M 0 , M 0 cannot be unit V for any V ∈ Val , then there exists
an essential context E, computations N̄ , M̄ 0 , such that N = EhN̄ i →e EhM̄ 0 i = M 0 .
Hence N = N̄ ? V̄ =→e M̄ 0 ? V¯0 = M 0 and M ⇒¬e N is derived as follows
N0 ⇒¬e N̄

V0 ⇒¬e V̄

M = N0 ? V0 ⇒¬e N̄ ? V̄ = N• if N̄ −→e M̄ 0 then M 0 = M̄ 0 ? V̄ .
The i.h. gives N0 ⇒λC M̄ 0 , and M ⇒λC M 0 is derived as follows
N0 ⇒λC M̄ 0

V0 ⇒λC V̄

M = N0 ? V0 ⇒λC M̄ 0 ? V̄ = M 0• if N 7→id M 0 this means that N̄ = M 0 and V̄ = λx.unit x, and M ⇒λC M 0 is derived asfollows (since ⇒¬e ⊆⇒λC )N0 ⇒λC N̄

M = N0 ? λx.unit x ⇒λC N̄ = M 0
8

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus

27

de’Liguoro, Treglia• if N 7→βc M 0 then V̄ = λx.L and N̄ = unit W 0 .
By definition of ⇒¬e the step V0 ⇒¬e V̄ ha the form
λx.L ⇒¬e λx.L0 for some L such that L ⇒λC L0
this means that M ⇒λC M 0 = L[W 0 /x] following the next derivation
L ⇒λC L0W ⇒λC W 0

M = unit W ? λx.L ⇒λC L0 [W 0 /x] = M 0• if N 7→ass M 0 then N = N̄ ? V̄ = (P ? λx.Q) ? V̄ and M 0 = M̄ 0 ? V¯0 = P ? λx.(Q ? V̄ ).
Since N0 ⇒¬e N̄ = P ? λx.Q, it follows that N0 has the shape N0 = P0 ? λx.Q0 whereP0 ⇒¬e P and Q0 ⇒λC Q, thenP0 ⇒λC P

Q0 ⇒λC Q

V0 ⇒λC V̄

M = (P0 ? λx.Q0 ) ? V0 ⇒λC P ? λx.(Q ? V̄ ) = M 0
The associativity case follows similarly.
n

2. Indexed split: by induction on M =⇒ M 0 . We will show just notable cases concerning
to the reduction steps:nid−step: M = N ? λx.unit x =⇒ N 0 = M 0 . Thenn

N =⇒ N 0n

M = N ? λx.unit x =⇒ N 0 = M 0
by i.h. either M ⇒¬e M 0 (but there is no ⇒¬e rule that can occur) or M 6⇒¬e M 0 .
n−1This means that M 6⇒¬e N 0 and by i.h. there exists N 00 s.t. M →e N 00 ===⇒ N 0 son−1

M = N ? λx.unit x →e N 00 ? λx.unit x ===⇒ N 0 .
knβc −step: M = unit V ? λx.N =⇒ N 0 [V 0 /x] where k = n + |N 0 |x · m + 1, where N =⇒ N 0m

and V =⇒ V 0 .

n

We have M = unit V ? λx.N →e N [V /x] and the substitutivity of =⇒ gives M 00 =n+|N 0 |x ·m

N [V /x] =======⇒ N 0 [V 0 /x].
nnass−step: If M =⇒ M 0 where M = (L ? λx.N ) ? λy.P , M 0 = L0 ? λx.(N 0 ? λy.P 0 ) and L ==L⇒ L0 ,
n

n

N
N ==
⇒ N 0 , P ==P⇒ P 0 . There are two sub cases: either it is the case M ⇒¬e M 0 , and L ⇒¬e L0 ,N ⇒¬e N 0 , P ⇒¬e P 0 , then the claim holds.
Otherwise, if M 6⇒¬e M 0 , L 6⇒¬e L0 and nL > 0 have to hold (otherwise M ⇒¬e M 0 ).
n −1
By i.h. there exists L̄ such that L −→e L̄ ==L==⇒ L0 . So M = (L ? λx.N ) ? λy.P −→en−1(L̄ ? λx.N ) ? λy.P ===⇒ M 0 .
n

3. Split: if M ⇒λC M 0 then there exists n such that M =⇒ M 0 . By induction on n: byindexed split property just proved there are two cases:928

Proceedings of the 9th International Workshop of Confluence, 2020

On the reduction of the type-free computational λ-calculus

de’Liguoro, Treglia∗

1. M ⇒¬e M 0 and the statement is proved since −→e is reflexive.
n−1

n−1

2. n > 0 and there exists M̄ such that M −→e M̄ ===⇒ M 0 . By i.h. applied to M̄ ===⇒ M 0∗

there exists M 00 such that M̄ −→e M 00 ⇒¬e M 0 and so M −→e M 00 ⇒¬e M 0 .

10Proceedings of the 9th International Workshop of Confluence, 2020

Confluence in Lens Synthesis
Anders Miltner1 , Kathleen Fisher2 , Benjamin C. Pierce3 , David Walker4 , andSteve Zdancewic5
1
Princeton University
amiltner@cs.princeton.edu
2
Tufts University
kfisher@eecs.tufts.edu
3
University of Pennsylvania
bcpierce@cis.upenn.edu
4Princeton University
dpw@cs.princeton.edu
5
University of Pennsylvania
stevez@cis.upenn.edu

Abstract
A lens is a program that can be executed both forwards and backwards, from input tooutput and from output back to input again. Domain-specific languages for defining lenses
have been developed to help users synchronize text files, and construct different “views” ofdatabases, among other applications. Recent research has shown how string lenses can besynthesized from their types, which are pairs of regular expressions. However, guaranteeingthat we can synthesize all possible lenses is quite tricky on these languages, due in largepart to the many equivalences on regular expressions.
The proof that all string lenses are synthesizeable involves proving a confluence-like
property, parameterized by a an additional binary relation R. We call this property Rconfluence. In this model, standard confluence is the specific case where R is equality. In
this paper, we show how existing techniques for demonstrating confluence do not work in
the domain of R-confluence, and find that if the rewrite system is =-confluent and satisfies
a commutativity property with R, then the system is R-confluent.

1

Introduction

Bidirectional transformations are pervasive in modern software systems, occuring as database
views and view updaters, parsers and pretty-printers, data synchronization tools, and more.
Instead of manually building the functions that comprise a bidirectional transformation, programmers can build them both “at once” using a bidirectional programming language. Bidirectional
programming languages have been developed for creating view updaters [3], Linux configuration
file editors [1], direct manipulation programming systems [11], and more [7, 5, 18]. Lenses area particularly well-behaved class of bidirectional programs, where the underlying transformations are guaranteed to satisfy a number of “round-tripping” laws. Lens-based bidirectional
programming languages often provide round-tripping guarantees through a set of typing rules;
well-typed lens expressions are guaranteed to satisfy the round-tripping laws.
Optician [13], an extension of Boomerang, makes bidirectional programming easier by
supporting synthesis of bidirectional string transformations. More specifically, it takes as input
two regular expressions (R and S , which serve as the type of a Boomerang lens) and a setof examples specifying input-output behavior, and synthesizes a well-typed lens between thelanguages of those regular expressions. For brevity, we will not provide formal definitions forsome aspects of Optician; the interested reader can find such definitions in the original Optician

29

30

Proceedings of the 9th International Workshop of Confluence, 2020

Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewic

paper [13]. Furthermore, examples detailing the use of synthesized lenses in practice (which we
also elide for space) can be found in that paper and follow-up work [8, 14].
To indicate a lens l is well typed, and converts between the languages of R and S , we writel : R ⇔ S . For synthesis, given R and S , we must find a lens l such that l : R ⇔ S . In
the context of lens synthesis, there are three sorts of lens typing rules: syntax-directed rules,
composition, and type equivalence.
For syntax-directed rules, the syntax for the types closely mirrors the syntax of the expressions.
As an example, consider the following rule for disjunction:
Or Lens

l1 : R1 ⇔ S1
l2 : R2 ⇔ S2
L(R1 ) ∩ L(R2 ) = ∅L(S1 ) ∩ L(S2 ) = ∅or (l1 , l2 ) : R1 | R2 ⇔ S1 | S2
Consider finding a lens of type R1 | R2 ⇔ S1 | S2 . With only syntax-directed rules, the only
lens that can be well-typed would be an or lens.
Composition sequentially composes two lenses.
Composition

l1 : R1 ⇔ R2
l2 : R2 ⇔ R3
l1 ; l2 : R1 ⇔ R3
Composition is difficult in the context of lens synthesis. If trying to synthesize a composition
lens, one has to pull the central regular expression “out of thin air.”
The last typing rule is type-equivalence. If two regular expressions are star-semiring equivalent
to the type of a lens, those equivalent regular expressions also serve as the type of the lens.
Type Equivalencel :R⇔SR ≡s R 0
l : R0 ⇔ S 0

S ≡s S 0

This rule is difficult in the context of synthesis, as it forces a search through equivalent regularexpressions. This rule can also be applied at any point in the derivation, which makes the searcheven harder.
To address the difficulties with composition and type-equivalence rules, we synthesize lenses inan alternative language of disjunctive normal form (DNF) lenses. DNF lenses are in pseudonormal
form, containing no composition operator, and so their synthesis never needs to pull regularexpressions “out of thin air.” The types of DNF lenses are pairs of regular expressions ina pseudonormal form, DNF regular expressions. Because DNF regular expressions are in a
pseudonormal form, fewer equivalent regular expressions need to be searched through.
In our search algorithm, we only search through equivalent regular expressions once, before
processing any syntax directed-rules. We formalize this in the typing of DNF regular expressions
by only permitting the application of type-equivalence once, after all syntactic rules have been
applied. This is enforced by having two typing judgements: one for the “rewriteless” type of thelens (meaning no type-equivalence rules were applied) and one of the “full” type of the lens. If
dl :̃ DR ⇔ DS , then dl is a DNF lens of rewriteless type DR ⇔ DS . If dl : DR ⇔ DS , then dl
is a DNF lens of full type DR ⇔ DS . The following rule is used to get the full type of a DNF
lens from the rewriteless type.
Rewrite DNF Regex Lens

DR 0 →∗ DR

2

DS 0 →∗ DS
dl :̃ DR ⇔ DS
00dl : DR ⇔ DS

Proceedings of the 9th International Workshop of Confluence, 2020

Confluence in Lens Synthesis

31

Miltner, Fisher, Pierce, Walker and Zdancewic

dl2 ~: DR3 ⇔ DS3
...

...

DR2
...

DS2
...

...

...

dl1 ~: DR1 ⇔ DS1

⇓R2

...

⇓S2
...

⇓R1

⇓S1

Figure 1: Diagram constructing a well-typed DNF lens between ⇓ R2 and ⇓ S2 . Single lined
arrows indicate rewrites (→), and triple lines indicate equivalence (≡→ ).
Note that instead of using directionless equivalences, Rewrite DNF Regex Lens uses
directioned rewrites. The relationship between the two is formalized by the following theorem:
Theorem 1. If R ≡s S , then ⇓ R ≡→ ⇓ S , where ⇓ R and ⇓ S are R and S in DNF form
(respectively), and ≡→ is the reflexive, transitive, and symmetric closure of →.
Proving that our search procedure can generate any lens reduces to proving DNF lenses
complete with respect to our standard lens language. In particular, we wish the prove:
Theorem 2. If l : R ⇔ S , then there exists a DNF lens, dl , such that dl :⇓R ⇔⇓S and thesemantics of l and dl are equivalent.
We prove this propety by induction on the structure of the typing derivation. Particulardifficulty lies in the lens equivalence rule. We begin this case below:l : R 1 ⇔ S1

R 1 ≡s R 2
l : R2 ⇔ S 2

S1 ≡ s S2

By induction assumption, there exists dl :⇓R1 ⇔⇓S1 , where the semantics of dl are equivalent
to those of l . By inversion on the derivation of dl :⇓R1 ⇔⇓S1 , there exists DR 1 and DS 1 suchthat:
⇓R1 →∗ DR 1

⇓S1 →∗ DS 1
dl :̃ DR 1 ⇔ DS 1
dl :⇓R1 ⇔⇓S1

To complete this case, we need to find a DNF lens dl 0 :⇓R2 ⇔⇓S2 with equivalent semantics
to l .
We first show that there exist DR 2 and DS 2 such that ⇓R2 →∗ DR 2 and ⇓DR 1 →∗ DR 2 and⇓S2 →∗ DS 2 and ⇓DS 1 →∗ DS 2 . To do this, we first prove that → is confluent. By Theorem 1,
we know that ⇓R1 ≡→ ⇓R2 , so confluence implies the existance of such a DR 2 and DS 2 .
After this, we have dl :̃ DR 1 ⇔ DS 1 and DR 1 →∗ DR 2 and DS 1 →∗ DS 2 . If we can provea confluence-like property that would show the existance of some dl 0 :̃ DR 3 ⇔ DS 3 , where
DR 2 →∗ DR 3 and DS 2 →∗ DS 3 , we would be done. This property is R-confluence for a properlychosen R (which we describe in §2). This case is diagrammed in Figure 1.
3

32

Proceedings of the 9th International Workshop of Confluence, 2020

Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewics2

R(s1,t)Figure 2: Rewrite system that satisfies the R-diamond property, but is not R-confluent.

2

R-Confluence Formulation

Let S be an underlying set, and → and R be binary relations. The rewrite system (S, →) is
R-confluent, if for all s1 , s2 ∈ S, if R(s1 , s2 ), s1 →∗ s01 , and s2 →∗ s02 , then there exist s001 and s002
such that R(s001 , s002 ), s01 →∗ s001 , and s2 →∗ s002 .
In the context of lens synthesis, S is the set of DNF REs, the rewrites are →∗ , and given a
DNF lens dl , Rdl (DR, DS ) is true if there exists a DNF lens dl 0 such that dl 0 :̃ DR ⇔ DS anddl is equivalent to dl 0 .
Now that R-confluence has been formally defined, we can ask ourselves: “What is a good
approach to proving R-confluence?” One approach is to prove that our rewrite system is locallyconfluent, which is equivalent to =-confluence in a terminating system [6]. Unfortunately, ourrewrites are not terminating, so this approach does not work.
An approach pioneered by Tait and Martin-Löf [2] still works in non-terminating systems.
This approach uses the diamond property: A rewrite system (S, →) satisfies the diamondproperty if s1 → s2 and s1 → s3 implies that there exists s4 such that s2 → s4 , and s2 → s4 . If
a rewrite system satisfies the diamond property, then it is also confluent. Unfortunately, thisapproach does not work, as the parameterized version of the diamond property does not imply
R-confluence.

3

Proving (S,→∗ ) R-Confluent

In the Tait and Martin-Löf approach to proving (S, →) confluent, one must first prove (S, →)satisfies the diamond property. Consider a parameterized property analogous to the diamondproperty, the R-diamond property: A rewrite system (S, →) satisfies the R-diamond property if
s1 → s2 and t1 → t2 and R(s1 , t1 ) implies that there exists s3 , t3 such that s2 → s3 and t2 → t3
and R(s3 , t3 ).
However, satisfying the R-diamond property is not sufficient for R-confluence. Consider thesimple rewrite system shown in Figure 2. In this rewrite system, there are 3 elements, s1 , s2 ,and t. In this setup, R(s1 , t) and s1 → s2 . R-confluence requires some s3 , t0 such that s2 →∗ s3
and t→∗ t0 and R(s3 , t0 ), but no such values exist.
To get around this issue, we require a different set of properties.
1. (S, →) must be =-confluent.
2. R must be a bisimilulation relation for (S, →∗ ). In other words if R(s1 , t1 ), and s1 →∗ s2 ,then there exists t2 such that t1 →∗ t2 and R(s2 , t2 ); and if R(s1 , t1 ), and t1 →∗ t2 , thenthere exists s2 such that s1 →∗ s2 and R(s2 , t2 ).
Theorem 3. Let (S, →) be =-confluent, and R be a bisimilulation relation for (S, →∗ ). If
R(s1 , t1 ) and s1 →∗ s2 and t1 →∗ t2 , then there exists s3 , t3 such that s2 →∗ s3 and t2 → t3 andR(s3 , t3 ).
4

Proceedings of the 9th International Workshop of Confluence, 2020

Confluence in Lens Synthesis

33

Miltner, Fisher, Pierce, Walker and Zdancewic

R(s5,t5)
...

...
s3

R(s4,t4)
...

...

s2

t2
...

...

R(s1,t1)

Figure 3: Diagram showing how we prove the inductive case of R-confluence of the transitive
closure of a rewrite system. R(s4 , t4 ) comes from the inductive hypothesis. The existance of s5
is guaranteed through =-confluence. R(s5 , t5 ) is guaranteed because R is a bisimulation relation.
Proof. By induction length of the reduction of s1 →∗ s2

Case 1 (Base Case). Let R(s1 , t1 ) and t1 →∗ t2 . As R is a bisimulation relation for (S, →∗ ), there
exists s2 such that s1 →∗ s2 and R(s2 , t2 ), as desired.

Case 2 (Inductive Case). Let R(s1 , t1 ) and s1 →∗ s2 and s2 → s3 and t1 →∗ t2 . By the induction
hypothesis, there exists s4 , t4 such that R(s4 , t4 ) and s2 →∗ s4 and t2 → t4 .
Because (S, →) is =-confluent, there exists s5 such that s3 →∗ s5 and s4 →∗ s5 . As (S, →∗ ) isa bisimilulation relation on (S, →∗ ), there exists t5 such that t4 →∗ t5 and R(s5 , t5 ), as desired.
This case is diagrammed in Figure 3.

4

Related Work

The concept of R-confluence is related to the notion of confluence modulo ∼ [6]. The definitionof confluent modulo ∼ is almost the same as ∼-confluence, the only difference is that confluence
modulo ∼ requires ∼ to an equivalence relation. Conditions that suffice to prove a rewrite
system confluent modulo ∼ are not generally sufficient to prove R-confluence (and vice versa).
Furthermore, our bisimulation relations are closely related to local coherence modulo ∼ .
Bisimulation relations come from concurrency theory [15], but a related notion, commuting
rewrites [16], appear in the confluence literature. We require a single rewrite of R to commute
with an arbitrary number of rewrites of →, which commuting rewrites do not express.
The full proof of completeness is contained in the appendix of the full version of the original
optician paper [12]. The original proof of R-confluence for the transitive closure of → required
additional assumptions. These unnecessary assumptions have been identified and removed in thispaper. Future work used the proof of completeness over our lens language to show that quotientbijective lenses are also synthesizeable [8]. Lastly, while synthesizeability was not proven forsymmetric lenses [14], such a proof would likely have proven R-confluence in a similar manner.
This work continues a trend in making programming easier through synthesis [4]. Whilesynthesis is one approach to make bidirectional programming easier, it is not the only approach.
Work has gone into building lenses without requiring a point-free combinator style [10]. Other
work has found applicative [9] and monadic [17] approaches to compositionally building lenses.
534

Proceedings of the 9th International Workshop of Confluence, 2020

Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewic

References[1] Augeas - A configuration API. http://augeas.net/index.html.
[2] H. P. Barendregt. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland,
revised edition, 1984. http://www.cs.ru.nl/ henk/Personal Webpage.
[3] Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce. Relational lenses: A language for
updateable views. In Principles of Database Systems (PODS), 2006. Extended version available as
University of Pennsylvania technical report MS-CIS-05-27.
[4] Sumit Gulwani, Alex Polozov, and Rishabh Singh. Program Synthesis, volume 4. NOW, August
2017.
[5] Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, and Keisuke
Nakano. Bidirectionalizing graph transformations. In Proceeding of the 15th ACM SIGPLAN
international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA,
September 27-29, 2010, pages 205–216, 2010.
[6] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems:
Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, October
1980.
[7] Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. BiGUL: A formally verified core language forputback-based bidirectional programming. In Proceedings of the 2016 ACM SIGPLAN Workshop
on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January
20 - 22, 2016, pages 61–72, 2016.
[8] Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic. Synthesizing quotient lenses. Proc. ACM Program. Lang., 2(ICFP), July 2018.
[9] Kazutaka Matsuda and Meng Wang. Applicative bidirectional programming with lenses. SIGPLAN
Not., 50(9):62–74, August 2015.
[10] Kazutaka Matsuda and Meng Wang. Hobit: Programming lenses without using lens combinators.
In Amal Ahmed, editor, Programming Languages and Systems, pages 31–59, Cham, 2018. Springer
International Publishing.
[11] Mikaël Mayer, Viktor Kuncak, and Ravi Chugh. Bidirectional evaluation with direct manipulation.
Proc. ACM Program. Lang., 2(OOPSLA), October 2018.
[12] Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic.
Synthesizing bijective lenses, 2017. https://arxiv.org/abs/1710.03248.
[13] Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing bijective lenses. In Proceedings of the 45th Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL 2018, 2018.
[14] Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic. Synthesizing symmetric lenses. Proc. ACM Program. Lang., 3(ICFP), July 2019.
[15] Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press,
USA, 2011.
[16] Yoshihito Toyama. Commutativity of term rewriting systems. Programming of future generation
computers II, pages 393–407, 1988.
[17] Li-yao Xia, Dominic Orchard, and Meng Wang. Composing bidirectional programs monadically. In
Luı́s Caires, editor, Programming Languages and Systems, pages 147–175, Cham, 2019. Springer
International Publishing.
[18] Zirun Zhu, Hsiang-Shang Ko, Pedro Martins, João Saraiva, and Zhenjiang Hu. Biyacc: Roll
your parser and reflective printer into one. In Proceedings of the 4th International Workshop on
Bidirectional Transformations co-located with Software Technologies: Applications and Foundations,
STAF 2015, L’Aquila, Italy, July 24, 2015., pages 43–50, 2015.

6

Proceedings of the 9th International Workshop of Confluence, 2020

Coherent Confluence inModal n-Kleene Algebras
Cameron Calk
Laboratoire de l’École Polytechnique (LIX), Paris, France
cameron.calk@inria.fr
Abstract
This work concerns the algebraic formalisation of coherence and confluence. The Church-Rosser
theorem states that the confluence of branchings and the confluence of zig-zags are equivalent properties.
On the one hand, the coherent version of this theorem has been formulated in the language of higher
dimensional globular categories. On the other hand, the Church-Rosser theorem has also beenformulated using the structure of modal Kleene algebra. This work provides an algebraic formulationof the coherent Church-Rosser theorem. To this end, we introduce the structure of n-dimensional
modal Kleene algebra satisfying globularity properties, providing a higher dimensional generalisationof modal Kleene algebra. In this setting, we give abstract definitions of coherent rewriting properties
and, via modal operators, present novel proofs of the Church-Rosser theorem with higher-dimensional
witnesses.

1

Introduction

In rewriting theory, a central theme is that of completing certain branching shapes, i.e. (local) branchingsor zig-zags, with confluences, thus obtaining confluence diagrams. This is classically described withrelations, but has more recently been formulated in the higher dimensional setting of polygraphs [2, 5].
While this approach is adapted to the study of string rewriting systems, it also provides a natural setting forthe study of coherence [5] in abstract rewriting systems. Furthermore, a point-free algebraic formalisationof confluence is given in [7]. This abstracts the relational approach to the setting of Kleene algebras,
providing a more general framework for the study of confluence. In this work, we combine these
two approaches by introducing the structure of n-Kleene algebra, a natural setting for abstract, higher
dimensional confluence proofs, and illustrate its use with the example of the Church-Rosser theorem.
In the relational setting, confluence is characterised, for an abstract rewriting system →, i.e. a binary
relation on some set, by the inclusion
∗

∗

∗

∗

← · → ⊆ → · ←,∗where → denotes the reflexive, transitive closure of →, ← denotes its converse and · denotes relational
composition. The Church-Rosser property is characterised by the inclusion∗∗∗↔ ⊆ → · ←,where ↔ = (← ∪ →) is the symmetric, reflexive, transitive closure of →. The Church-Rosser theorem,
which states that these two properties are equivalent, can be formulated with similar expressions in Kleene
algebra using the star operation, an abstraction of the notion of reflexive, transitive closure, see Section 2.
The coherent formulation of this theorem takes place in the context of polygraphs. Roughly, it statesthat if there exists a set Γ of higher dimensional cells (with a globular shape) such that every branching canbe completed to a confluence diagram filled by some element of Γ , then every zig-zag may be completedwith a Church-Rosser diagram filled by a composition of elements in Γ , see [2]. In diagrams, thesestatements are respectively represented by:
∗

∗

35

36

Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic Coherent Confluence

Cameron Calk

u

f
u1

w
f

0

'

&

 α
u

0 x

g

h

u1 o

g
u2

f0

0

/ u2

 β
u0

~

g0

where α ∈ Γ and β is a composition of elements of Γ . This is a coherence result akin to e.g. Mac Lane’s
theorem for monoidal categories, since local data, i.e. existence of confluence diagrams, is constructively
used to prove a global result, i.e. existence of Church-Rosser diagrams.
In this abstract, we recall the structure of modal n-Kleene algebra from [2] and illustrate its use in thealgebraic formalisation of coherence results by formulating and giving a proof sketch of the coherent
Church-Rosser theorem. In Section 2 we provide background material, defining modal Kleene algebras
as in [3] and Γ -coherence properties, an extension of constructions from [4]. Next, we introduce thenovel structure of modal n-Kleene algebra and provide axioms for globularity in Section 3. Finally,in Section 4, we formalise the notion of coherence, state the Church-Rosser theorem in the setting of
n-Kleene algebras and give a short proof sketch.

2

Modal Kleene Algebras and Coherence

Modal Kleene Algebras, [3]. Recall that a dioid is a semiring (S, +, ·, 0, 1) in which addition is
idempotent, i.e. for all x ∈ S, we have x + x = x. In this case, the natural partial order on S is defined byx ≤ y ⇔ x + y = y. A domain semiring is a dioid (S, +, ·, 0, 1) equipped with a domain operationd : S → S that satisfies, for all x, y ∈ S, the following axioms :x ≤ d(x)x (1)d(xy) = d(xd(y)) (2)d(x) ≤ 1(3)
d(0) = 0(4)d(x + y) = d(x) + d(y) (5)where juxtaposition indicates multiplication. These axioms characterise domain in the case of relational
algebras. For a more detailed account, see [3]. In particular, they imply that Sd := d(S) forms a
distributive lattice with the induced operations + as join and · as meet, bounded by 0 and 1.
The opposite of a semiring S, in which the order of multiplication has been reversed, is denoted by
Sop . A codomain semiring is a semiring equipped with a map r : S → S such that (Sop , r) is a domain
semiring. A modal semiring is both a domain semiring and a codomain semiring, with additional axioms
d ◦ r = r and r ◦ d = d, which imply that Sd = Sr . We include these definitions for use in Section 3, in
which the term modal will be justified.
A (modal) Kleene algebra is a (modal) semiring K equipped with an operator (−)∗ : K → K called
Kleene star. It satisfies, for all x, y, z ∈ K, the unfold and induction axioms
1 + xx∗ ≤ x∗
1 + x∗ x ≤ x∗
(6)
z + xy ≤ y ⇒ x∗ z ≤ y

z + yx ≤ y ⇒ zx∗ ≤ y(x and y semi-commute)(x and y are Church-Rosser.)(7)

In a Kleene algebra K, the Church-Rosser theorem is expressed as follows: for elements x, y ∈ K, thefollowing are equivalent:x ∗ y∗ ≤ y∗ x ∗(x + y)∗ ≤ y∗ x∗(8)Γ -Coherence Properties. Recall that an n-polygraph P is a data consisting of sets (Pk )0≤k≤n andsource and target maps (sk , tk : Pk+1 → Pk∗ )0≤k<n satisfying globularity conditions, where Pk∗ is the2Proceedings of the 9th International Workshop of Confluence, 2020

37

Algebraic Coherent Confluence

Cameron Calk∗
free k-category generated by the globular set (P0 , P1∗ , . . . , Pk−1
, Pk ). A cellular extension of P is a set Γ>>and (globular) attaching maps sn , tn : Γ → Pn , where Pn is the free (n, n − 1)-category generated by
P. See [5] for a more detailed account of polygraphs and their use in rewriting theory.
Given an n-polygraph P and a cellular extension Γ , we say that P is Γ -confluent (resp. Γ -Church∗ 2>
Rosser) if, for every branching (f, g) ∈ (Pn) of n-cells (resp. every zig-zag h ∈ Pn), there exist
00>a confluence (f , g ) and a (n + 1)-cell α ∈ Γ (resp. α ∈ Pn (Γ ), the free (n + 1, n − 1)-category
generated by (P, Γ )) such that
h
/= v
u
g
f− 6 u
'
 α
u1
−
7 v1
f0 " 0
 α
g0
u
'
0
0
−
f
u 0 (g )−α : f− ?n−1 g → f 0 ?n−1 (g 0 )−(resp. α : f → f 0 ?n−1 g 0 ),where, for n-cells f1 , f2 of P, f1 ?n−1 f2 denotes their composition with respect to the (n−1)-dimensionaltarget (resp. source) of f1 (resp. f2 ). Readers familiar with polygraphic rewriting may notice thatthe filling cells are usually oriented from left to right, rather than from top to bottom. We choose thisorientation to better reflect the approach used in the setting of Kleene algebras, in which branching shapes,
such as x∗ y∗ and (x + y)∗ , are related to confluence shapes y∗ x∗ , as recalled in (8). This will equally be
the case in n-Kleene algebra, see Section 4.
The coherent Church-Rosser theorem [2] is formulated as follows: given P a n-polygraph, and Γ acellular extension of P, if P is Γ -confluent, then P is Γ -Church-Rosser.

3

Higher Dimensional Modal Kleene Algebra

n-Dioids. For n ≥ 1, an n-dioid is a structure (S, +, 0, i , 1i )0≤i<n such that (S, +, 0, i , 1i ) is adioid for 0 ≤ i < n, the lax interchange change laws hold, and units are idempotent with respect to lower
dimensional multiplications, i.e.
(A

0
jA )

i (B

0
j B ) ≤ (A

i B)

j (A

0

0
iB )

and

1j

(9)

i 1j = 1j ,op

for all A, A , B, B ∈ S and 0 ≤ i < j < n. The opposite n-semiring of S, denoted S , is that in which
the order of every multiplication operation has been reversed.
00

Globular n-Semirings with Domains. A domain n-semiring is an n-dioid (S, +, 0, i , 1i )0≤i<nequipped with n domain maps (di : S → S)0≤i<n , such that (S, +, 0, i , 1i , di ) is a domain semiringand di+1 ◦ di = di for all 0 ≤ i < n − 1. A n-semiring with codomains is equipped with maps
(ri : S → S)0≤i<n such that Sop is a domain n-semiring with respect to the (ri )0≤i<n .
A modal n-semiring is an n-semiring with domains and codomains, in which the coherence conditions
di ◦ ri = ri and ri ◦ di = di hold for all 0 ≤ i < n. Given S a modal n-semiring, we define forward andbackward i-diamond operators defined via (co-)domain operators in each dimension, as in [3]. For any
0 ≤ i < n, A ∈ S and φ ∈ Si , we define|Aii (φ) = di (A

i φ),

and

hA|i (φ) = ri (φ

(10)

i A).

These are modal operators on the distributive lattice Si in the sense of [6]. A modal semiring S is called
globular if the following globular relations hold for 0 ≤ i < j < n and A, B ∈ K:di ◦ dj = di and di ◦ rj = di ,(11)
dj (A i B) = dj (A) i dj (B),(13)
ri ◦ dj = ri , and ri ◦ rj = ri ,

(12)

rj (A

i B) = rj (A)i rj (B).

(14)

Modal n-Kleene Algebra. A n-Kleene algebra is a n-semiring K equipped with maps (−)∗i : K → K

3

38

Proceedings of the 9th International Workshop of Confluence, 2020

Algebraic Coherent Confluence

Cameron Calksuch that (K, +, 0, i , 1i , (−)∗i ) is a Kleene algebra for 0 ≤ i < n, and for 0 ≤ i < j < n, the Kleeneplus operator (−)+j , defined by A+j = A j A∗j , is a lax morphism with respect to the i-multiplicationof j-dimensional elements on the right (resp. left) in the sense that for all A ∈ K and φ ∈ Kj ,
φ

+j
≤ (φ
iA

i A)

+j

,

and

(resp. A+ji φ ≤ (A

i φ)

+j

(15)

).

When the underlying semiring is globular and modal, we say that K is a globular modal n-Kleene algebra.
To provide a link to the polygraphic case, we remark that the power set of theset of n-cells in the free n-category generated by an n-polygraph P constitutes
a globular modal n-Kleene algebra K(P). Following this intuition, an element
A of a globular modal n-Kleene algebra will be represented with respect to its
i- and j-(co)domains as in the adjacent diagram.

4

dj (A)⇓Adi (A)$ri (A)9rj (A)

Church-Rosser theorem

Let K be a globular modal n-Kleene algebra and 0 ≤ i < j < n. Given elements φ and ψ of Kj , we saythat A ∈ K is a i-confluence filler for (φ, ψ) if |Aij (ψ∗i i φ∗i ) ≥ φ∗i i ψ∗i .
In the modal n-Kleene algebra K(P) corresponding to a polygraph P, taking i = n − 2, j = n − 1,letting ψ be the set of (n − 1)-cells of P and letting φ be the set of their inverses, this signifies that A isa set of n-cells containing a filling cell for a confluence diagram corresponding to each branching of(n − 1)-cells.
4.1. Theorem (Coherent Church-Rosser in globular n-MKA). Let K be a globular modal n-Kleene
algebra. Given φ, ψ ∈ Kj , for 0 < j < n, for any i-confluence filler A ∈ K for (φ, ψ), we have^ ∗j ij (ψ∗i φ∗i ) ≥ (φ + ψ)∗i ,|A^ := (φ + ψ)∗i i A i (φ + ψ)∗i .
where A^ ∗j ij (ψ∗i φ∗i ) ≥ (φ + ψ)∗i signifies that the domain of A
^ ∗j , when
Note that the expression |A∗i ∗i∗irestricted on the right to confluences ψ φ , contains at least all of the zig-zags (φ + ψ) .
To finish this section, we provide a sketch of the proof, a detailed version of which can be found in [2].
To ease notation, juxtaposition will denote i-multiplication. By (7) and (15), we have^ ∗j ij (ψ∗i φ∗i ) ≤ |A
^ ∗j ij (ψ∗i φ∗i ) ⇒ (φ + ψ)∗i ≤ |A
^ ∗j ij (ψ∗i φ∗i )1i + (φ + ψ)|A^ ∗j ij (ψ∗i φ∗i ), it remains to show that
Observing that 1i ≤ ψ∗i φ∗i ≤ |A
^ ∗j ij (ψ∗i φ∗i ) ≤ |A
^ ∗j ij (ψ∗i φ∗i ).
(φ + ψ)|A

By distributivity, we may prove this for each of the summands. Below, we show the formal calculationsin the n-Kleene algebra on the left, which are reflected in the diagrammatic representations on the right:^ ∗j ij (ψ∗i φ∗i ) ≤ |φA^ ∗j ij (φψ∗i φ∗i )φ|A^ ∗j ij (|Aij (ψ∗i φ∗i )φ∗i )≤ |φA^ ∗j ij (|Aφ∗i ij (ψ∗i φ∗i φ∗i ))≤ |φA^ ∗j j Aφ∗i ij (ψ∗i φ∗i )≤ |φA^ ∗j j Ai^ j (ψ∗i φ∗i )≤ |A^ ∗j ij (ψ∗i φ∗i )
≤ |A
4

·

φ

(φ+ψ)∗i

/·o
ψ∗i

ψ∗i

⇓ Aφ∗i
·

^ ∗j
⇓ φA

!

>·

φ∗i

/= ·
φ∗i

Proceedings of the 9th International Workshop of Confluence, 2020

39

Algebraic Coherent Confluence

Cameron Calk

^ ∗j ij (ψ∗i φ∗i ) ≤ |ψA^ ∗j ij (ψψ∗i φ∗i )ψ|A^ ∗j ij (ψ∗i φ∗i )≤ |ψA^ ∗j ij (ψ∗i φ∗i )
≤ |A

·

ψ

(φ+ψ)∗i

/·o
=

ψ∗ i
ψ∗ i

</ ·

^ ∗j

⇓ ψA

"+

φ∗i

·

·

5

Conclusion

By introducing the structure of modal n-Kleene algebra, we have provided an algebraic framework forcoherent confluence proofs in higher dimensional rewriting theory. A more detailed account of thisstructure and its properties can be found in [2]. There, in addition to the Church-Rosser theorem, a notionof termination in modal n-Kleene algebras is formalised, and a coherent version of Newman’s lemma is
formulated and proved in the setting of globular modal n-Kleene algebra.
Perspectives for future work most notably include a formulation of the coherent confluence Squiertheorem [5] for abstract rewriting systems in globular modal n-Kleene algebras. This result concerns
homotopical properties of polygraphs considered as cofibrant objects in the folk model structure of
ω-categories. A central goal is thus to formalise the notion of cofibrant object in the language of modal
n-Kleene algebras, and thereby relate these to questions in homotopy type theory. Other avenues of
future work include formalising the structure of modal n-Kleene algebra in the proof assistant Isabelle,
following [1], and developing a cubical approach.

References[1] A. Armstrong, V. Gomes, and G. Struth. Algebras for program correctness in Isabelle/HOL. volume8428, 04 2014.
[2] C. Calk, E. Goubault, P. Malbos, and G. Struth. Algebraic coherent confluence and higher-dimensional
Kleene algebras. Work in progress, 2020.
[3] J. Desharnais and G. Struth. Internal axioms for domain semirings. Science of Computer Programming,
76(3):181–203, 2011.
[4] Y. Guiraud, E. Hoffbeck, and P. Malbos. Convergent presentations and polygraphic resolutions ofassociative algebras. Math. Z., 293(1-2):113–179, 2019.
[5] Y. Guiraud and P. Malbos. Polygraphs of finite derivation type. Math. Structures Comput. Sci.,
28(2):155–201, 2018.
[6] B. Jónsson and A. Tarski. Boolean algebras with operators. Part I. American Journal of Mathematics,
73(4):891–939, 1951.
[7] G. Struth. Abstract abstract reduction. J. Log. Algebr. Program., 66(2):239–270, 2006.

5

40

Proceedings of the 9th International Workshop of Confluence, 2020

Safety and Completeness of Disambiguation corresponds to
Termination and Confluence of ReorderingLuı́s Eduardo de Souza Amorim1 and Eelco Visser2
1

Australian National University, Australia
LuisEduardo.deSouzaAmorim@anu.edu.au
2
Delft University of Technology, The Netherlands
e.visser@tudelft.nl
Abstract
Associativity and priority are well known techniques to disambiguate expression grammars. In recent work we develop a direct semantics for disambiguation by associativity
and priority rules and prove that a safe and complete disambiguation relation produces
a safe and complete disambiguation. The proof approach relies on a correspondence between disambiguation and term rewriting such that safety of disambiguation corresponds
to termination of the rewrite system and completeness of disambiguation correspond toconfluence of the rewrite system. In this extended abstract we illustrate that approach
using diagrams.

1

Introduction

Associativity and priority are well known techniques to lexical syntax
disambiguate expression grammars. Figure 1 illustrates
ID = [a-zA-Z][a-zA-Z0-9]*
the approach. An expression grammar defines the infix context-free syntax
operators of an expression language using left- and rightExp.Var = IDrecursive productions such as Exp.Add = Exp "+" Exp.
Exp.Add = Exp "+" Exp {left}
Exp.Min = Exp "-" Exp {left}
Such a grammar is ambiguous; an expression such as a +Exp.Mul = Exp "*" Exp {left}
b + c can be read as (a + b) + c or as a + (b + c).
Exp.Div = Exp "/" Exp {left}
One way to disambiguate an expression grammar is toExp.Pow = Exp "^" Exp {right}
transform it to a grammar that uses extra non-terminals
to represent priority levels. However such grammars are context-free priorities
Exp.Powharder to read and the direct correspondence to the un> {left: Exp.Mul Exp.Div}
derlying abstract syntax trees is lost. An alternative ap> {left: Exp.Add Exp.Min}
proach is to augment an ambiguous expression grammar
Figure 1: SDF3 definition.
with associativity and priority rules. The semantics ofsuch disambiguation rules is typically defined indirectlyin the implementation of parser generators or by means of grammar transformations. In recent
work, we have developed a direct semantics for associativity and priority in terms of subtree
exclusion that extends to expression grammars with prefix and postifix operators, mixfix operators, indirect recursion, and overlap. We are currently revising a paper about this work for
the TOPLAS journal [2]. A previous version of the semantics of disambiguation rules appearedin [1], but did not feature the proof technique based on rewriting. We refer to those papers fora discussion of related work.
To verify the approach we developed a technique based on term rewriting that shows thatsoundness and completeness of disambiguation corresponds to termination and confluence reordering parse trees. In this extended abstract we illustrate the proof technique for the case of
infix expression grammars. We omit formal definitions and mostly explain the approach using
diagrams.

41

42

Proceedings of the 9th International Workshop of Confluence, 2020

Safety and Completeness of Disambiguation

Amorim and Visser

a+b*c-d

Add
a

Add

+ Mul
b

a

-

+ Min
Mul -

* Min
c

Mul

d

b

*

d

a

Min

Add

*

Min

+

b c

-

Add a

d

Min
d

Mul Add *

+ Mul

c

b

*

c

a

+

d

c

b

matchesE

matchesmatches

Mul

Add

* Min
E

-

E
E

Mul
E

+ Min
E

M ul > M inmatches

-

Mul

* Min
E

E

Add left M in

-

Add *
E

E

M ul > M in

+

E

E

M ul > Add

Figure 2: Parse trees for an ambiguous expression, and its disambiguation using subtree exclusion rules

2

Disambiguation by Subtree Exclusion

An ambiguous sentence has multiple parse trees. The diagram in figure 2 shows the parse trees
for the expression a + b * c - d according the underlying grammar of figure 1. Disambiguation by subtree exclusion defines conflict patterns that should not occur in selected parse trees.
The safe subtree exclusion rules (for infix expressions) of SDF3 [2] are defined as follows:
A.C1 > A.C2
C1
C2
α

A.C1 > A.C2
C1

β

α

A

A.C1 left A.C2
C1

C2
A

A
β

α

C2

A

β

A.C1 right A.C2
C1

A

A

C2

β

α

A

A

Instantiating these rules to some of the disambiguation rules in figure 1 leads to the following
subtree exclusion patterns (aka conflict patterns):
E.M ul > E.Add
Mul

E
2

Add

*

+

E

E

E.M ul > E.Add
Mul

E.Add left E.Add
Add

E

E

*

Add

E

+

E

+

Add

E

+

E

Proceedings of the 9th International Workshop of Confluence, 2020

43

Safety and Completeness of Disambiguation

Amorim and Visser

Applying these rules to the expression in figure 2 shows that the sentence is completely disambiguated as all but one parse tree for the expression are rejected.
A set of disambiguation rules is safe when each sentence in the underlying grammar isalso a sentence in the disambiguated grammar. That is, no sentences are excluded. A set of
disambiguation rules is complete when each sentence in the underlying grammar has at most one
parse tree in the disambiguated grammar. That is, each sentence is completely disambiguated.
How can we prove that set of disambiguation rules safe and complete? That is a central questionin our work on the semantics disambiguation rules [2].

3Proving Safety and CompletenessThe central insight in our approach to proving safety and completeness of disambiguation is thatdisambiguation by means of associativity and priority rules corresponds to reordering of parsetrees. For infix expression grammars we define a rewrite system generated by instiantiating thefollowing rewrite rule schemas for each pair of productions in a grammar:
RI

C1

t21

C2

op1

op2

t22

t12

t21

op2

C1

t22

op1

RI

C1
t11

C2

op1

C2

t21

op2

t22

t12

C2

t11

C1

op2

op1

t21

t22

When we apply these rules to the expression in figure 2, we see that all trees can be converted
into each other using these rewrite rules:
Add
a

Add

RI

+ Mul
b

a

* Min
c

-

Mul -

yield

b

a+b*c-d

a

Add

*

Min

+

b c

-

Min
Mul Add *

d
a

+

b

c

yield

yield
RI

*

RI

yield

Mul

d

yield

d

RI

+ Min

c

Min

RI

d

Add a

d

+ Mul
b

*

c

3

44

Proceedings of the 9th International Workshop of Confluence, 2020

Safety and Completeness of Disambiguation

Amorim and Visser

In general, we have a theorem that states that all ambiguities in an infix expression grammar
are related by reordering, expressed diagrammatically as follows:

w

yield

yield

yield

t1

RI

...

RI

ti

RI

...

RI

tn

The reordering rewrite system is non-terminating. Each tree can be converted in each othertree. Using the subtree exclusion patterns generated from the associativity and priority rulesof a grammar, we direct the rules of the rewrite system, leading to the following rule schemas:
DI

C1

t21

C2

op1

op2

t22

t12

t21

op1

C2

t21

op2

t22

if

op2

C1

t22

op1

RI

C1
t11

C2

C2

t11

A

t12
if

C1

op2

op1

t21

t22

∈Q

C1
C2

op1

op2

A

A

∈Q

C1
A

op1

C2

A

op2

A

In our paper [2] we show that safety of disambiguation corresponds to termatination of thisrewrite system and that completeness of disambiguation corresponds to confluence of the rewrite
system. We illustrate that here using the diagrams in figures 3, 4, and 5.

Add
a

Add

M ul>M in

+ Mul
b

a

Mul -

* Min
c

-

d

b

Mul

Min

M ul>M in

Add

*

Min

+

b c

-

Mul Add *

d
a

c

+

c

Min

M ul>Add

d

Add a

b

Figure 3: Unsafety corresponds to non-termination4*d

Add right M inAdd left M in

M ul>Add

a

+ Min

d

+ Mul
b

*

c

Proceedings of the 9th International Workshop of Confluence, 2020

45

Safety and Completeness of Disambiguation

Amorim and Visser

Add
a

Add

+ Mul
b

a

Mul -

* Min
c

-

d

b

*

d

c

Add left M in

M ul>Add

Mul

a

+ Min

Min

Add

*

Min

+

b c

-

Mul Add *

d
a

+

Min

M ul>Add

Add -

d

c

a

b

d

+ Mul
b

*

c

Figure 4: Incompleteness corresponds to non-confluence (non-Church Rosser)
Add
a

Add

M ul>M in

+ Mul
b

a

Mul -

* Min
c

-

d

b

*

d

c

Add left M in

M ul>Add

Mul

a

+ Min

Min

M ul>M in

Add

*

Min

+

b c

-

Mul Add *

d
a

+

b

c

Min

M ul>Add

d

Add a

d

+ Mul
b

*

c

Figure 5: Safety and completeness correspond to termination and confluence.

References[1] Luı́s Eduardo de Souza Amorim. Declarative Syntax Definition for Modern Language Workbenches.
PhD thesis, Delft University of Technology, 2019.
[2] Luı́s Eduardo de Souza Amorim and Eelco Visser. A direct semantics for declarative disambiguationof expression grammars. ACM Transactions on Programming Languages, 2020. under revision.

5

46

Proceedings of the 9th International Workshop of Confluence, 2020

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.

47

48

Proceedings of the 9th International Workshop of Confluence, 20202

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′ ).)Proceedings of the 9th International Workshop of Confluence, 2020

49

Jean-Pierre Jouannaud and Fernando Orejas
1

1

↓
g
↓
f
↓↑
f

=

↓
f
↓
y′

1

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

Ð→
↓
g
↓
f←2
↓
x′

3
1

↓
f
↓
y′

1

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

↓
h
=
↓
x′← 2

1

↓
h
↓
f
↺

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 ).

50

Proceedings of the 9th International Workshop of Confluence, 20204

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).

Proceedings of the 9th International Workshop of Confluence, 2020

51

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.

52

Proceedings of the 9th International Workshop of Confluence, 20206

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.

Proceedings of the 9th International Workshop of Confluence, 202053

Confluence Competition 2020
Aart Middeldorp1 , Naoki Nishida2 , Kiraku Shintani3 , and Johannes Waldmann4
1

2

Department of Computer Science, University of Innsbruck, Austria
Department of Computing and Software Systems, Nagoya University, Japan3
School of Information Science, JAIST, Japan
4HTWK Leipzig, Germany

The next few pages in these proceedings contain the descriptions of the tools participating in
the 9th Confluence Competition (CoCo 2020). CoCo is a yearly competition in which softwaretools attempt to automatically (dis)prove confluence and related properties of rewrite systems
in a variety of formats. For a detailed description we refer to [1]. This year there were 14 tools(listed in order of registration) participating in 12 categories (listed in order of first appearancein CoCo):TRS CPF-TRS CTRS HRS GCR CPF-CTRS UNR UNC NFP COM INF SRS
infChecker
CoLL-Saigawa
Moca
CSI
FORT-hConConCO3
CoLL
nonreach
ACP
AGCP
CSIˆho
CeTA
SOL

X
X

X
X

X

X

X
X

X
X
X

X
X

X
X

X
X

X

X
X
X
X

X

X

X

X

X

X

X
X
X

X
X

New this year was that the winning tools1 of CoCo 2019 participated as demonstration tools, toprovide a benchmark to measure progress. Also new is that there are separate winners for YES
answers, NO answers, and combined YES/NO answers. The live run CoCo 2020 on StarExec [2]can be viewed at http://cocograph.uibk.ac.at/2020.html. Further information about CoCo
2020, including a description of the categories and detailed results, can be obtained fromhttp://project-coco.uibk.ac.at/2020/

References[1] A. Middeldorp, J. Nagele, and K. Shintani. Confluence Competition 2019. In Proc. 25th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11429 of
LNCS, pages 25–40, 2019. doi: 10.1007/978-3-030-17502-3 2.
[2] A. Stump, G. Sutcliffe, and C. Tinelli. StarExec: A Cross-Community Infrastructure for Logic
Solving. In Proc. 7th International Joint Conference on Automated Reasoning, volume 8562 of
LNCS (LNAI), pages 367–373, 2014. doi: 10.1007/978-3-319-08587-6 28.
1 They are not listed in the table but see http://project-coco.uibk.ac.at/2019/results.php.

54Proceedings of the 9th International Workshop of Confluence, 2020

55

infChecker at the 2020 Confluence Competition∗Raúl Gutiérrez1 and Salvador Lucas2
1

Universidad Politécnica de Madrid, Madrid, Spainr.gutierrez@upm.es
2
VRAIN, Universitat Politècnica de València, Valencia, Spainslucas@dsic.upv.es1Overview,→

infChecker 1.0 is a tool for checking (in)feasibility of goals G = {Fi }mi=1 where Fi = (sij ./ij
iand ./ij ∈ {→, →∗ , →+ , ,→, ,→∗ , ,→+ , , , ↓, , ↔, ←tij )ni=1,→, ↔∗ , ←,→∗ } where predicates ./ij
represent binary relations on terms (most of them well-known or easy generalizations of wellknown relations) defined by provability of goals s ./ij t with respect to a first-order theories
Th./ij [2, 4]. The tool is available here: http://zenon.dsic.upv.es/infChecker/. It is
written in Haskell and provides a first implementation of the Feasibility Framework [2], where
three processors have been implemented:• PSat integrates the satisfiability approach described in [3] to prove infeasibility.
infChecker, we use the model generators AGES [1] and Mace4 [6] to find a proof.

In• PProv integrates the logic-based approach to program analysis described in [3] to provefeasibility by theorem proving. In infChecker, we use the theorem prover Prover9 [6].
• PNC adapt the processor that narrow conditions in the 2D DP framework for proving
operational termination of CTRs [5] to be used with feasibility sequences.
Our proof strategy is: (1) first, we try to prove feasibility using PProv ; (2) if PProv fails, we apply
PSat ; (3) if PSat fails, we apply PNC ; (4) if PNC succeeds and modifies the feasibility sequence,
we go to (2), otherwise we return MAYBE.

References[1] R. Gutiérrez and S. Lucas. Automatic Generation of Logical Models with AGES. In CADE 2019:
Automated Deduction - CADE 27, LNCS 11716:287:299. Springer, 2019.
[2] R. Gutiérrez and S. Lucas. Automatically Proving and Disproving Feasibility Conditions. In Proc.
of IJCAR’2020, LNCS to appear. Springer, 2020.
[3] S. Lucas. Proving semantic properties as first-order satisfiability. Artificial Intelligence 277, paper
103174, 24 pages, 2019.
[4] S. Lucas and R. Gutiérrez. Use of Logical Models for Proving Infeasibility in Term Rewriting.
Information Processing Letters, 136:90–95, 2018.
[5] S. Lucas, J. Meseguer, and R. Gutiérrez. The 2D Dependency Pair Framework for conditional
rewrite systems. Part I: Definition and basic processors. Journal of Computer and System Sciences,
96:74–106, 2018.
[6] W. McCune. Prover9 and Mace4. [online]. Available at https://www.cs.unm.edu/~mccune/mace4/.
∗ Partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32 andby the Spanish Generalitat Valenciana under grant PROMETEO/2019/098.

56

Proceedings of the 9th International Workshop of Confluence, 2020

CoLL-Saigawa 1.5: A Joint Confluence Tool∗
Kiraku Shintani and Nao Hirokawa
JAIST, Japan

CoLL-Saigawa is a tool for automatically proving or disproving confluence of (ordinary) term
rewrite systems (TRSs). The tool, written in OCaml, is freely available at:
http://www.jaist.ac.jp/project/saigawa/
The typical usage is: collsaigawa <file>. Here the input file is written in the TRS format [6].
The tool outputs YES if confluence of the input TRS is proved, NO if non-confluence is shown,and MAYBE if the tool does not reach any conclusion.
CoLL-Saigawa is a joint confluence tool of CoLL v1.5 [9] and Saigawa v1.9 [2]. If an input
TRS is left-linear, CoLL proves confluence. Otherwise, Saigawa analyzes confluence. CoLL is acommutation tool specialized for left-linear TRSs. It proves confluence as self-commutation byusing Hindley’s commutation theorem [1] together with the three commutation criteria: Almost
development closeness [10], rule labeling with weight function [11], and Church-Rosser modulo
A/C [4]. Saigawa can deal with non-left-linear TRSs. The tool employs the four confluence
criteria: The criteria based on critical pair systems [3, Theorem 3] and on extended criticalpairs [5, Theorem 2], rule labeling [11], and Church-Rosser modulo AC [4]. Furthermore,version 1.5 supports the following confluence criteria: parallel closedness based on parallel
critical pairs [12], simultaneous closedness [7], and also parallel-upside and outside closedness [8].

References[1] J. R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis,
University of Newcastle-upon-Tyne, 1964.
[2] N. Hirokawa. Saigawa: A confluence tool. In 3rd Confluence Competition, pages 1–1, 2014.
[3] N. Hirokawa and A. Middeldorp. Commutation via relative termination. In Proc. 2nd IWC, pages
29–33, 2013.
[4] J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM
Journal on Computing, 15(4):1155–1194, 1986.
[5] D. Klein and N. Hirokawa. Confluence of non-left-linear TRSs via relative termination. In Proc.
18th LPAR, volume 7180 of LNCS, pages 258–273, 2012.
[6] A. Middeldorp, J. Nagele, and K. Shintani. Confluence Competition 2019. Proc. 25th TACAS,
volume 11429 of LNCS, pages 25–40, 2019.
[7] S. Okui. Simultaneous critical pairs and Church–Rosser property. In Proc. 9th RTA, volume 1379
of LNCS, pages 2–16, 1998.
[8] M. Oyamaguchi and Y. Ohta. On the open problems concerning Church-Rosser of left-linear term
rewriting systems. IEICE Transactions on Information and Systems, 87(2):290–298, 2004.
[9] K. Shintani and N. Hirokawa. CoLL: A confluence tool for left-linear term rewrite systems. In
Proc. 25th CADE, volume 9195 of LNAI, pages 127–136, 2015.
[10] V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.
[11] V. van Oostrom. Confluence by decreasing diagrams converted. In A. Voronkov, editor, Proc. 19th
RTA, volume 5117 of LNCS, pages 306–320, 2008.
[12] Y. Toyama. On the Church-Rosser property of term rewriting systems. NTT ECL Technical
Report, No.17672, NTT, 1981.
∗ Supported by JSPS KAKENHI Grant Number 17K00011.

57

58

Proceedings of the 9th International Workshop of Confluence, 2020

59

Moca 0.2: A First-Order Theorem Prover for Horn Clauses
Yusuke Oi and Nao Hirokawa
JAIST, Japan

Moca is a fully automatic first-order theorem prover for Horn clauses. The tool, written in
Haskell, is freely available from:http://www.jaist.ac.jp/project/maxcomp/
The usage is: moca.sh <file>. Given a satisfiability problem in the TPTP CNF format [5],the tool outputs Satisfiable or Unsatisfiable if its satisfiability or unsatisfiability is proved,
respectively, and Maybe otherwise. Given an infeasibility problem in the CoCo format [2], thetool outputs YES if its infeasibility is proved, and MAYBE otherwise.
Moca implements maximal ordered completion [6] and new approximation techniques. Witha small example we illustrate how Moca uses them to solve problems. Consider the infeasibility
problem of the conversion x−x ↔∗ s(x) for the TRS {x−0 → x, 0−x → 0, s(x)−s(y) → x−y}.
The problem can be regarded as the satisfiability problem of the Horn clauses:
x−0≈x

0−x≈0

s(x) − s(y) ≈ x − y

x − x 6≈ s(x)By applying the split-if encoding [1] the problem reduces to the word problem of deciding
T 6≈E F for the equational system E:
x−0≈x

0−x≈0

s(x) − s(y) ≈ x − yf(s(x), x) ≈ F

f(x − x, x) ≈ T

x−0≈x

0−x≈0

s(x) − s(y) ≈ x − yf(s(x), x) ≈ F

f(x − x, y) ≈ T

In order to solve it our tool attempts to construct a ground-complete presentation of E byusing maximal ordered completion. However, the attempt is doomed to fail as the completion
diverges. Moca overcomes the divergence by approximating the last equation to the moregeneral equation f(x − x, y) ≈ T. This results in the following equational system:
Now maximal ordered completion builds up the finite ground-complete presentation R of theapproximated equational system:
x−0→x

0−x→0

s(x) − s(y) → x − yf(0, y) → T

f(s(x), x) → F∗

f(x − x, y) → T

Since T↓R 6= F↓R holds, infeasibility of the conversion x−x ↔ s(x) is concluded. Version 0.2 ofMoca supports the generalized split-if encoding [3] and inlining for conditional rewrite rules [4].

References[1] K. Claessen and N. Smallbone. Efficient Encodings of First-Order Horn Formulas in Equational
Logic. In Proc. 9th IJCAR, LNCS 10900, pp. 388–404, 2018.
[2] A. Middeldorp, J. Nagele, and K. Shintani. Confluence Competition 2019. In Proc. 25th TACAS(Part III), LNCS 11429, pp. 25–40, 2019.
[3] Y. Oi. Refutation by Completion and Approximations. Master’s thesis, JAIST, 2019.
[4] C. Sternagel and T. Sternagel. Certifying Confluence of Quasi-Decreasing Strongly Deterministic
Conditional Term Rewrite Systems. In Proc. 26th CADE, LNCS 10395, pp. 413–431, 2017.
[5] G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: From CNF to TH0,
TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017.
[6] S. Winkler and G. Moser. MædMax: A Maximal Ordered Completion Tool. In Proc. 9th IJCAR,LNCS 10900, pp. 472–480, 2018.

60

Proceedings of the 9th International Workshop of Confluence, 2020

CoCo 2020 Participant: CSI 1.2.4
Fabian Mitterwallner and Aart Middeldorp
Department of Computer Science, University of Innsbruck, Austria
fabian.mitterwallner@uibk.ac.at, aart.middeldorp@uibk.ac.at

CSI is an automatic tool for (dis)proving confluence and related properties of first-order term
rewrite systems (TRSs). It has been in development since 2010. Its name is derived from theConfluence of the rivers Sill and Inn in Innsbruck. The tool is available fromhttp://cl-informatik.uibk.ac.at/software/csi
under a LGPLv3 license. A detailed description of CSI can be found in [3]. Some of theimplemented techniques are described in [1, 2, 4]. Compared to last year’s version, CSI 1.2.4
contains an implementation of the upside-parallel-closure criterion for confluence by Oyamaguchi
and Ohta [5]. Additionally some minor changes to the strategy have been made.
CSI participates in the following CoCo 2020 categories: CPF-TRS, NFP, SRS, TRS, UNC,
and UNR.

References[1] B. Felgenhauer. Confluence for Term Rewriting: Theory and Automation. PhD thesis, University of
Innsbruck, 2015.
[2] J. Nagele. Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order
Rewrite Systems. PhD thesis, University of Innsbruck, 2017.
[3] J. Nagele, B. Felgenhauer, and A. Middeldorp. CSI: New Evidence – A Progress Report. In Proc.
26th International Conference on Automated Deduction, volume 10395 of Lecture Notes in Artificial
Intelligence, pages 385–397, 2017. doi: 10.1007/978-3-319-63046-5_24.
[4] H. Zankl. Challenges in Automation of Rewriting. Habilitation thesis, University of Innsbruck, 2014.
[5] M. Oyamaguchi and Y. Ohta. A New Parallel Closed Condition for Church-Rosser of Left-Linear
Term Rewriting Systems. In Proc. 8th International Conference on Rewriting Techniques andApplications, volume 1232 of Lecture Notes in Computer Science, pages 187–201, 1997. doi: 10.1007/
3-540-62950-5_70

61

62

Proceedings of the 9th International Workshop of Confluence, 2020

CoCo 2020 Participant: FORT-h 0.9∗
Fabian Mitterwallner, Aart Middeldorp, and Bertram Felgenhauer
Department of Computer Science, University of Innsbruck, Austria
fabian.mitterwallner@uibk.ac.at, aart.middeldorp@uibk.ac.at, int-e@gmx.de

The first-order theory of rewriting is a decidable theory for finite left-linear right-groundrewrite systems. The decision procedure goes back to Dauchet and Tison [1] and is implemented
in FORT [3,4]. In this theory confluence-related properties on ground terms are easily expressible.
FORT-h implements a new variant, described in [2], of the decision procedure for the larger
class of linear variable-separated rewrite systems. This variant supports a more expressive theory
and is based on anchored ground tree transducers. FORT-h 0.9 is implemented in Haskell. A
command-line version of the tool can be downloaded fromhttp://cl-informatik.uibk.ac.at/software/FORT/
FORT-h participates in the following CoCo 2020 categories: COM, GCR, NFP, UNC, and UNR. A
future release of FORT-h will produce certificates for the YES/NO answers that will be checkedby an independent certifier based on the Isabelle/HOL formalization described in [2].

References[1] M. Dauchet and S. Tison. The Theory of Ground Rewrite Systems is Decidable. In Proc. 5th IEEE
Symposium on Logic in Computer Science, pages 242–248, 1990. doi: 10.1109/LICS.1990.113750.
[2] B. Felgenhauer, A. Lochmann, A. Middeldorp, and F. Mitterwallner. Formalizing the First-Order
Theory of Rewriting. Submitted for publication, 2020.
[3] F. Rapp and A. Middeldorp. Automating the First-Order Theory of Left-Linear Right-Ground Term
Rewrite Systems. In Proc. 1st International Conference on Formal Structures for Computation and
Deduction, volume 52 of Leibniz International Proceedings in Informatics, pages 36:1–36:12, 2016.
doi: 10.4230/LIPIcs.FSCD.2016.36.
[4] F. Rapp and A. Middeldorp. FORT 2.0. In Proc. 9th International Joint Conference on AutomatedReasoning, volume 10900 of LNCS (LNAI), pages 81–88, 2018. doi: 10.1007/978-3-319-94205-6 6.

∗ Supported by FWF (Austrian Science Fund) project P30301.

63

64

Proceedings of the 9th International Workshop of Confluence, 2020

CoCo 2020 Participant: ConCon 1.10
Christian Sternagel
DVT, Innsbruck, Austria

ConCon is a fully automatic confluence checker for oriented first-order conditional term
rewrite systems (CTRSs). It is written in Scala and available under the LGPL license at
http://cl-informatik.uibk.ac.at/software/concon
For more details on its implementation and employed methods we refer to an earlier systemdescription [5].
Starting from version 1.10 ConCon supports arbitrary external tools for proving infeasibility.
In CoCo 2020 this will be showcased by using nonreach (version 1.2.2) [3] as external tool.
Other external tools that are used to discharge subgoals concerning (non-conditional) confluence and termination are CSI (version 1.2.3) [2] and TTT2 (version 1.20) [1].
While most other methods of ConCon can be certified using CeTA (version 2.39) [4, 6],certification of nonreach proofs is future work.

References[1] Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool
2 In Proc. 20th RTA, 2009, doi:10.1007/978-3-642-02348-4 21[2] Bertram Felgenhauer, Aart Middeldorp, and Fabian Mitterwallner. CoCo 2019 Participant: CSI
1.2.3. In Proc. 8th IWC, 2019. http://iwc2019.cic.unb.br/proc-HOR-IWC-CoCo.pdf[3] F. Meßner. CoCo 2020 Participant: nonreach. In Proc. 9th IWC, 2020. To appear.
[4] J. Schöpf, C. Sternagel, R. Thiemann, and A. Yamada. CoCo 2020 Participant: CeTA 2.39. In Proc.
9th IWC, 2020. To appear.
[5] C. Sternagel and S. Winkler. CoCo 2019 Participant: ConCon 1.9. In Proc. 8th IWC, 2019.
http://iwc2019.cic.unb.br/proc-HOR-IWC-CoCo.pdf[6] R. Thiemann and C. Sternagel. Certification of Termination Proofs using CeTA. In Proc. 22nd
TPHOLs, volume 5674 of LNCS, pages 452–468, 2009. doi:10.1007/978-3-642-03359-9 31.

65

66

Proceedings of the 9th International Workshop of Confluence, 2020

CO3 (Version 2.1)
Naoki Nishida
Nagoya University, Nagoya, Japannishida@i.nagoya-u.ac.jp

CO3, a converter for proving confluence of conditional TRSs,1 tries to prove confluence ofconditional term rewriting systems (CTRSs, for short) by using a transformational approach(cf. [4]). The tool first transforms a given weakly-left-linear (WLL, for short) 3-DCTRS into
an unconditional term rewriting system (TRS, for short) by using Uconf [2], a variant of theunraveling U [6], and then verifies confluence of the transformed TRS by using the following
theorem: a 3-DCTRS R is confluent if R is WLL and Uconf (R) is confluent [1, 2]. The toolis very efficient because of very simple and lightweight functions to verify properties such asconfluence and termination of TRSs. Since version 2.0, a narrowing-tree-based approach [5, 3] toprove infeasibility of a condition w.r.t. a specified CTRS has been implemented. The approach
is applicable to syntactically deterministic CTRSs that are operationally terminating and ultraright-linear w.r.t. the optimized unraveling. In the present version, bugs in version 2.0 has been
fixed and the computation of SCCs for termination has slightly been improved.
To prove confluence by means of narrowing trees, the tool first computes the (conditional)
critical pairs, and then proves their joinability as follows: a critical pair hs, ti ⇐ c is joinable if(1) c is the empty list and s = t, or (2) the narrowing tree for c can be simplified to a tree thatdefines the empty set of substitutions. For example, let us consider 489.trs in Cops which isan operationally terminating normal 1-CTRS, and has a conditional critical pair htrue, falsei ⇐o(x)  true, e(x)  true. As a narrowing tree for condition o(x)  true, e(x)  true w.r.t.
489.trs, we construct the following production rules for a regular tree grammar [5]:Γe(x)true & o(x)true → Rec(Γe(x0 )true , {x 7→ x0 }) & Rec(Γo(x00 )true , {x 7→ x00 })Γe(x0 )true → id &{x0 7→ 0} | Rec(Γo(x00 )true , {x1 7→ x00 }) & id &{x0 7→ s(x1 )}| Rec(Γe(x0 )true , {x2 7→ x0 }) & ∅ &{x0 7→ s(x2 )}Γo(x00 )true → ∅ &{x00 7→ 0} | Rec(Γe(x0 )true , {x37→ x0 }) & id &{x00 7→ s(x3 )}| Rec(Γo(x00 )true , {x4 7→ x00 }) & ∅ &{x00 7→ s(x4 )}These rules can be simplified to Γe(x)true & o(x)true → ∅, and the critical pair is infeasible.
To prove infeasibility of a condition c, the tool first prove confluence, and then linearizes c
if failed to prove confluence; then, the tool computes and simplifies a narrowing tree for c, andexamines the emptiness of the narrowing tree.

References[1] K. Gmeiner, B. Gramlich, and F. Schernhammer. On soundness conditions for unraveling deterministic conditional rewrite systems. In Proc. RTA 2012, vol. 15 of LIPIcs, pp. 193–208, 2012.
[2] K. Gmeiner, N. Nishida, and B. Gramlich. Proving confluence of conditional term rewriting systems
via unravelings. In Proc. IWC 2013, pp. 35–39, 2013.
[3] Y. Maeda, N. Nishida, M. Sakai, and T. Kobayashi. Extending narrowing trees to basic narrowing
in term rewriting. IEICE Tech. Rep. SS2018-39, Vol. 118, No. 385, pp. 73–78, 2019, in Japanese.
[4] N. Nishida, T. Kuroda, and K. Gmeiner. CO3 (Version 1.3). In Proc. IWC 2016, p. 74, 2016.
[5] N. Nishida and Y. Maeda. Narrowing trees for syntactically deterministic conditional term rewriting
systems. In Proc. FSCD 2018, vol. 108 of LIPIcs, pp. 26:1–26:20, 2018.
[6] E. Ohlebusch. Termination of logic programs: Transformational methods revisited. Appl. AlgebraEng. Commun. Comput., 12(1/2):73–116, 2001.
1 http://www.trs.css.i.nagoya-u.ac.jp/co3/

67

68

Proceedings of the 9th International Workshop of Confluence, 2020

CoLL 1.5: A Commutation Tool
Kiraku Shintani
JAIST, Japans1820017@jaist.ac.jp

CoLL (version 1.5) is a tool for automatically proving commutation of left-linear term rewrite
systems (TRSs). The tool, written in OCaml, is freely available at:
http://www.jaist.ac.jp/project/saigawa/coll/
The typical usage is: coll <file>. Here the input file is written in the commutation problem
format [10]. The tool outputs YES if commutation of the input TRSs is proved, NO if noncommutation is shown, and MAYBE if the tool does not reach any conclusion.
In this tool commutation of left-linear TRSs is shown by Hindley’s Commutation Theorem:
Theorem 1 ([3]). ARSs A = hA, {→α }α∈I i and B = hA, {→β }β∈J i commute if →α and →βcommute for all α ∈ I and β ∈ J.
Here indexes are interpreted as subsystems of the input TRSs. For every pair of subsystems thetool proves the commutation property, employing the three criteria: Development closeness [2,7], rule labeling with weight function [8, 1], and Church-Rosser modulo A/C [4]. A detailed
description of CoLL can be found in [6].
As a final remark, the bug of AC-related method, reported in [9], has been fixed in thecurrent version of CoLL.

References[1] T. Aoto. Automated confluence proof by decreasing diagrams based on rule-labelling. In Proc.
21st RTA, volume 6 of LIPIcs, pages 7–16, 2010.
[2] T. Aoto, J. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically.
In Proc. 20th RTA, volume 5595 of LNCS, pages 93–102, 2009.
[3] J. R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis,
University of Newcastle-upon-Tyne, 1964.
[4] J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM
Journal on Computing, 15(4):1155–1194, 1986.
[5] B. K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM,
20:160–187, 1973.
[6] K. Shintani and N. Hirokawa. CoLL: A confluence tool for left-linear term rewrite systems. In
Proc. 25th CADE, volume 9195 of LNAI, pages 127–136, 2015.
[7] V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.
[8] V. van Oostrom. Confluence by decreasing diagrams converted. In A. Voronkov, editor, Proc. 19th
RTA, volume 5117 of LNCS, pages 306–320, 2008.
[9] J. Nagele, B. Felgenhauer, and A. Middeldorp. CSI: New evidence – a progress report. Proc. 26th
CADE, volume 10395 of LNAI, pages 385–397, 2017.
[10] A. Middeldorp, J. Nagele, and K. Shintani. Confluence Competition 2019. Proc. 25th TACAS,
volume 11429 of LNCS, pages 25–40, 2019.

69

70

Proceedings of the 9th International Workshop of Confluence, 2020

CoCo 2020 Participant: nonreach∗
Florian Meßner
University of Innsbruck, Innsbruck, Austria florian.g.messner@uibk.ac.at

The tool nonreach is an automated, efficient tool to check infeasibility with respect to oriented conditional term rewrite systems (CTRSs). The Haskell source code can be obtained
from a public git repository hosted on bitbucket:
https://bitbucket.org/fmessner/nonreach
Given a CTRS (or a TRS) and one or more infeasibility problems, nonreach uses a
combination of decomposition, based on narrowing (with some heuristics) and proving rootnonreachability [2], and fast checks, based on etcap [3] and the inductive symbol transition
graph [2].
These methods are applied by turns until I either obtain infeasibility (by simplifying the tree
to False), a satisfying substitution or reach a user-defined threshold of iterations (and nonreachconcludes MAYBE).
I outline the main new features of nonreach 1.2 compared to the version participating in lastyear’s CoCo.
• Certification of (some) proofs (which is not visible in the competition for the lack of a
CPF-INF category).
• Positive reachability results found through narrowing now yield NO together with a satisfying assignment.
While refactoring was necessary in order to generate certificates, and as a nice side-effectleads to more detailed and more readable proofs, I lose a few infeasibility results compared tolast year. Furthermore, after finding a bug in internal meetability problem handling, which inrare cases could lead to unsound results, I disabled almost all of those methods, thus losing a
few more infeasibility results.

References[1] Florian Meßner and Christian Sternagel. nonreach - A tool for nonreachability analysis. In Proc.
25th TACAS, pages 337–343, 2019. doi:10.1007/978-3-030-17462-0_19.
[2] Christian Sternagel and Akihisa Yamada. Reachability analysis for termination and confluence of
rewriting. In Proc. 25th TACAS, pages 262–278, 2019. doi:10.1007/978-3-030-17462-0_15.
[3] René Thiemann and Christian Sternagel. Certification of Termination Proofs using CeTA. In Proc.
22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of LNCS,
pages 452–468. Springer, 2009. doi:10.1007/978-3-642-03359-9_31.

∗ This work is supported by the Austrian Science Fund (FWF): project P27502.

71

72

Proceedings of the 9th International Workshop of Confluence, 2020

ACP: System Description for CoCo 2020
Takahito Aoto1
Institute of Science and Technology, Niigata University
aoto@ie.niigata-u.ac.jp

A primary functionality of ACP is proving confluence (CR) of term rewriting systems(TRSs). ACP integrates multiple direct criteria for guaranteeing confluence of TRSs. It also
incorporates divide–and–conquer criteria by which confluence or non-confluence of TRSs canbe inferred from those of their components. Several methods for disproving confluence are also
employed. For some criteria, it supports generation of proofs in CPF format that can be certified by certifiers. The internal structure of the prover is kept simple and is mostly inheritedfrom the version 0.11a, which has been described in [3]. It also deal with confluence of oriented
conditional term rewriting systems. Besides confluence, ACP now supports proving the UNC
property (unique normal form property w.r.t. conversion) and the commutation property ofterm rewriting systems. The ingredients of the former property have been appeared in [2, 4].
Our (dis)proofs of commutation are based on a development closed criterion [5] and a simple
search for counter examples. No new (CR/UNC) criterion has been incorporated from the one
submitted for CoCo 2019.
ACP is written in Standard ML of New Jersey (SML/NJ) and the source code is also available
from [1]. It uses a SAT prover such as MiniSAT and an SMT prover YICES as external provers. It
internally contains an automated (relative) termination prover for TRSs but external (relative)
termination provers can be substituted optionally. Users can specify criteria to be used so thateach criterion or any combination of them can be tested. Several levels of verbosity are available
for the output so that users can investigate details of the employed approximations for eachcriterion or can get only the final result of prover’s attempt.

References[1] ACP (Automated Confluence Prover). http://www.nue.ie.niigata-u.ac.jp/tools/acp/.
[2] T. Aoto and Y. Toyama. Automated proofs of unique normal forms w.r.t. conversion for term
rewriting systems. In Proc. of 12th FroCoS, volume 11715 of LNAI, pages 330–347. Springer-Verlag,
2019.
[3] T. Aoto, J. Yoshida, and Y. Toyama. Proving confluence of term rewriting system automatically.
In Proc. of 20th RTA, volume 5595 of LNCS, pages 93–102. Springer-Verlag, 2009.
[4] M. Yamaguchi and T. Aoto, A fast decision procedure for uniqueness of normal forms w.r.t.
conversion of shallow term rewriting systems. In Proc. of 5th FSCD, volume 167 of LIPIcs, pages
9:1–9:23. Schloss Dagstuhl, 2020.
[5] J. Yoshida, T. Aoto, and Y. Toyama. Automating confluence check of term rewriting systems.
Computer Software, 26(2):76–92, 2009.

73

74

Proceedings of the 9th International Workshop of Confluence, 2020

75

AGCP: System Description for CoCo 2020
Takahito Aoto
Institute of Science and Technology, Niigata University
aoto@ie.niigata-u.ac.jp

AGCP (Automated Groud Confluence Prover) [1] is a tool for proving ground confluence ofmany-sorted term rewriting systems. AGCP is written in Standard ML of New Jersey (SML/NJ).
AGCP proves ground confluence of many-sorted term rewriting systems based on two ingredients.
One ingredient is to divide the ground confluence problem of a many-sorted term rewriting
system R into that of S ⊆ R and the inductive validity problem of equations u ≈ v w.r.t. S
for each u → r ∈ R \ S. Here, an equation u ≈ v is inductively valid w.r.t. S if all its ground∗instances uσ ≈ vσ is valid w.r.t. S, i.e. uσ ↔S vσ. Another ingredient is to prove groundconfluence of a many-sorted term rewriting system via the bounded ground convertibility of
the critical pairs. Here, an equation u ≈ v is said to be bounded ground convertibile w.r.t. a∗∗quasi-order % if uθg ←→R vθg for any its ground instance uσg ≈ vσg , where x ←→ y iff there%%

exists x = x0 ↔ · · · ↔ xn = y such that x % xi or y % xi for every xi .
Rewriting induction [3] is a well-known method for proving inductive validity of manysorted term rewriting systems. In [1], an extension of rewriting induction to prove bounded
ground convertibility of the equations has been reported. Namely, for a reduction quasi-order% and a quasi-reducible many-sorted term rewriting system R such that R ⊆ , the extension
proves bounded ground convertibility of the input equations w.r.t. %. The extension not only
allows to deal with non-orientable equations but also with many-sorted TRSs having non-freeconstructors. Several methods that add wider flexibility to the this approach are given in[2]: when suitable rules are not presented in the input system, additional rewrite rules areconstructed that supplement or replace existing rules in order to obtain a set of rules thatis adequate for applying rewriting induction; and an extension of the system of [2] is used if
if the input system contains non-orientable constructor rules. AGCP uses these extension of
the rewriting induction to prove not only inductive validity of equations but also the bounded
ground convertibility of the critical pairs. Finally, some methods to deal with disproving groundconfluence are added as reported in [2].
No new ground (non-)confluence criterion has been incorporated from the one submitted
for CoCo 2019.

References[1] T. Aoto and Y. Toyama. Ground confluence prover based on rewriting induction. In Proc. of 1st
FSCD, volume 52 of LIPIcs, pages 33:1–33:12. Schloss Dagstuhl, 2016.
[2] T. Aoto, Y. Toyama and Y. Kimura. Improving Rewriting Induction Approach for Proving Ground
Confluence. In Proc. of 2nd FSCD, volume 84 of LIPIcs, pages 7:1–7:18. Schloss Dagstuhl, 2017.
[3] U.S. Reddy. Term rewriting induction. In Proc. of CADE-10, volume 449 of LNAI, pages 162–177.
Springer-Verlag, 1990.

76

Proceedings of the 9th International Workshop of Confluence, 2020

CoCo 2020 Participant: CSIˆho 0.3.2
Julian Nagele
London, UK
mail@jnagele.net

CSIˆho is a tool for automatically (dis)proving confluence of higher-order rewrite systems,
specifically pattern rewrite systems (PRSs) as introduced by Nipkow [1,4]. CSIˆho is an extension
of CSI, a confluence prover for first-order rewrite systems.
No new features were added to CSIˆho since CoCo 2018—it ran unopposed in the HRS
category of CoCo 2019. A detailed description of CSIˆho be found in [2,3] or earlier CoCo systemdescriptions. The tool is available at
http://cl-informatik.uibk.ac.at/software/csi/ho

References[1] R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. TCS, 192(1):3–29, 1998.
[2] Julian Nagele. Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order
Rewrite Systems. PhD thesis, University of Innsbruck, 2017.
[3] Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. CSI: New evidence — A progress report.
In Proc. 26th CADE, volume 10395 of LNCS (LNAI), pages 385–397, 2017.
[4] T. Nipkow. Higher-order critical pairs. In Proc. 6th LICS, pages 342–349, 1991.

77

78

Proceedings of the 9th International Workshop of Confluence, 2020

CoCo 2020 Participant: CeTA 2.39∗
Jonas Schöpf1 , Christian Sternagel2 , René Thiemann1 , and Akihisa Yamada3
1

University of Innsbruck, Austria
2
DVT, Austria
3
National Institute of Advanced Industrial Science and Technology, JapanThe tool CeTA [2] is a certifier for, among other properties, (non-)confluence of term rewrite
systems with and without conditions. Its soundness is proven as part of the formal proof
library IsaFoR, the Isabelle Formalization of Rewriting. For a complete reference of supported
techniques we refer to the certification problem format (CPF) and the IsaFoR/CeTA website:
http://cl-informatik.uibk.ac.at/isafor/
In the following, we describe what is new in version 2.39 of CeTA. Although there are no
new techniques in CeTA that are specific for confluence proving, we like to mention two newly
supported termination methods [3]. Both of these extensions have the potential to increase thepower of confluence techniques that rely upon termination or relative termination.
The first extension consists of support for the weighted path order (WPO) [5], a termorder that unifies and extends well-known path orders such as the Knuth–Bendix order andthe lexicographic path order. In particular, confluence provers can now for the first time use
NaTT [4] – which is specialized on WPO – as external termination prover in order to produce
certifiable confluence proofs.
The second extension is the support for max-polynomial interpretations [1], i.e., polynomialinterpretations that additionally allow the maximum operator. In CeTA these orders can beused stand-alone, but also in combination with WPO.
We would like to welcome all confluence tool developers to experiment with whether our two
extensions are indeed helpful for confluence proving, and are looking forward to certify these
new kinds of proofs via CeTA.

References[1] Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl. Maximal Termination. In Rewriting Techniques and Applications, 19th International
Conference, Proceedings, volume 5117 of LNCS, pages 110–125. Springer, 2008.
[2] René Thiemann and Christian Sternagel. Certification of Termination Proofs Using CeTA. In
Theorem Proving in Higher Order Logics, 22nd International Conference, Proceedings, volume 5674
of LNCS, pages 452–468. Springer, 2009.
[3] René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada. Certifying the Weighted
Path Order. In Formal Structures for Computation and Deduction, 5th International Conference,
Proceedings, 2020. To appear.
[4] Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Nagoya Termination Tool. In Rewriting
and Typed Lambda Calculi - Joint International Conference, Proceedings, volume 8560 of LNCS,
pages 466–475. Springer, 2014.
[5] Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. A Unified Ordering for Termination
Proving. Sci. Comput. Program., 111:110–134, 2015.
∗ Jonas Schöpf and Christian Sternagel were supported by FWF project P27502. René Thiemann was supported by the Austrian Science Fund (FWF) project Y757. A part of Akihisa Yamada’s contribution was madewhile working at the University of Innsbruck supported by FWF projects Y757 and P27502.

79

80

Proceedings of the 9th International Workshop of Confluence, 2020

The System SOL version 2020
Makoto Hamana1 , Kentaro Kikuchi2 ,Date Yao Faustin Dieudonne1 , Kazuki Fuju1
1

Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp
2
RIEC, Tohoku University, Japankentaro.kikuchi@riec.tohoku.ac.jp

SOL is a Haskell-based tool for confluence and strong normalisation of higher-order computation. SOL is intended to be a generic higher-order computation analysis tool that is applicableto the modern theories of higher-order programming languages. This aim is demonstrated in[Ham19] and further developed in [Ham18].
Based on the foundation of second-order algebraic theories [FH10] and its computationalcounter part [Ham19] and polymorphic extension [Ham18], we implemented various resultson higher-order syntax and computation in SOL, including Knuth and Bendix’s critical pairchecking for confluence, and Function-as-Constructor Unification (FCU) [LM16] for unification.
Termination analysis is based on the General Schema criterion [Bla00, Bla16].

References[Bla00]F. Blanqui. Termination and confluence of higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833, pages 47–61. Springer, 2000.
[Bla16] F. Blanqui. Termination of rewrite relations on λ-terms based on Girard’s notion of reducibility. Theor. Comput. Sci., 611:50–86, 2016.
[FH10] M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL’10, LNCS 6247,
pages 320–335, 2010.
[Ham19] M. Hamana. How to prove decidability of equational theories with second-order computation
analyser SOL. Journal of Functional Programming, Cambride University Press, Vol. 29, e20,
2019.
[Ham18] M. Hamana. Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation, Functional and Logic Programming (FLOPS’18), Lecture Notes in Computer Science
10818, pp.99-115, Springer, 2018.
[LM16] T. Libal and D. Miller. Functions-as-Constructors Higher-Order Unification. In Proc. of
FSCD 2016, volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages
26:1–26:17, 2016.
[Nip93] T. Nipkow. Functional unification of higher-order patterns. In Proc. of (LICS’93), pages
64–74, 1993.

81

Author Index
Aoto, Takahito 73, 75
Calk, Cameron 35
Chenavier, Cyrille 13de Souza Amorim, Luıis Eduardo 41
de’Liguoro, Ugo 19
Dieudonne, Date Yao Faustin 81
Dupont, Benjamin 13
Felgenhauer, Bertram 63
Fisher, Kathleen 29
Fuju, Kazuki 81
Gutiérrez, Raúl 55
Hamana, Makoto 81
Hirokawa, Nao 7, 57, 59
Jouannaud, Jean-Pierre 47
Kikuchi, Kentaro 81
Lucas, Salvador 55
Malbos, Philippe 13
Meßner, Florian 71
Middeldorp, Aart 53, 61, 63

Miltner, Anders 29
Mitterwallner, Fabian 61, 63
Nagele, Julian 77
Nishida, Naoki 53, 67
Oi, Yusuke 59
Orejas, Fernando 47
Pierce, Benjamin C. 29
Schöpf, Jonas 79
Shintani, Kiraku 7, 53, 57, 69
Sternagel, Christian 65, 79
Thiemann, René 79
Treglia, Riccardo 19
van Oostrom, Vincent 1
Visser, Eelco 41
Waldmann, Johannes 53
Walker, David 29
Yamada, Akihisa 79
Zdancewic, Steve 2982