Proceedings of the
13th International Workshop on Confluence
July 9, 2024
Tallinn, Estonia

Foreword
The 13th International Workshop on Confluence (IWC 2024) is held on July 9, 2024, in Tallinn, Estonia,
affiliated with the 9th International Conference on Formal Structures for Computation and Deduction(FSCD 2024).
Confluence, as a general notion of determinism, is an essential property of rewrite systems and has
emerged as a crucial concept for many applications. However, the confluence property is also relevant
to various further areas of rewriting, such as completion, commutation, termination, modularity, andcomplexity. The International Workshop on Confluence was created as a forum to discuss all these
aspects, as well as related topics, implementation issues, and new applications.
IWC 2024 continues this tradition. The present report comprises nine regular submissions and the abstract of an invited talk, as well as descriptions of tools participating in the 13th Confluence Competition(CoCo 2024). In the invited talk, Aart Middeldorp highlights confluence of Logically Constrained Term
Rewrite Systems, which has been attracting attention recently, and for which a new category of CoCo
has started this year. The contributions in these proceedings reflect the wide scope of current research on
confluence, ranging from new confluence criteria and novel confluence-related properties over formalization of confluence results to implementation aspects and applications. At the same time, the spectrum of
rewrite formalisms (first- as well as higher-order, conditional rewriting, rewriting under strategies) used
to model problems from different application areas underlines the importance of confluence for various
domains.
The renewed interest in confluence research in the last decade resulted in a variety of novel approaches,
which were also implemented in powerful tools that compete in the annual confluence competition. The
second part of this report devoted to CoCo 2024 provides a general overview as well as system descriptionsof all competition entrants.
IWC 2024 was made possible by the commitment of many people who contributed to the submissions,the preparation and the program of the workshop, as well as the confluence competition. These include
authors of papers and tools, committee members, external reviewers, and the organizers of CoCo, theorganizers of FSCD, as well as the local organizers. Their hard work is very much appreciated.
Cyrille Chenavier and Naoki Nishida

Limoges and Nagoya, 26 June 2024

ii

Organization
IWC Steering Committee• Mauricio Ayala-Rincón, Brasilia University, Brasil• Sarah Winkler, Free University of Bozen-Bolzano, Italy

IWC Program Committee• Sandra Alves, Universidade do Porto, Portugal• Cyrille Chenavier, Université de Limoges, France (co-chair)• Nao Hirokawa, JAIST, Japan• Dohan Kim, University of Innsbruck, Austria• Maja Hanne Kirkeby, Roskilde University, Denmark• Salvador Lucas, Universitat Politècnica de València, Spain• Naoki Nishida, Nagoya University, Japan (co-chair)• Femke van Raamsdonk, Vrije Universiteit Amsterdam, Netherlands

Additional Reviewers• Jörg Endrullis, Vrije Universiteit Amsterdam, Netherlands• Jan Willem Klop, Vrije Universiteit Amsterdam, Netherlands• Johannes Niederhauser, University of Innsbruck, Austria• René Thiemann, University of Innsbruck, Austria

CoCo Steering Committee• Raúl Gutiérrez, Universidad Politécnica de Madrid, Spain• Aart Middeldorp, University of Innsbruck, Austria• Naoki Nishida, Nagoya University, Japan• Teppei Saito, JAIST, Japan• René Thiemann, University of Innsbruck, Austriaiii

Contents
Forewordii

Organizationiii

Abstracts of Invited Talks
Confluence of Logically Constrained Rewrite Systems
Aart Middeldorp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

Workshop Contributions
On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs
Misaki Kojima and Naoki Nishida . . . . . . . . . . . . . . . . . . . . . . . . . . .
From Subtree Replacement Systems to Term Rewriting Systems: a Roadmap to Orthogonality
Salvador Lucas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
The problem of the calissons, by rewriting
Vincent van Oostrom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
A Roadmap to Orthogonality of Conditional Term Rewriting Systems
Salvador Lucas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems
Ievgen Ivanov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Orthogonality of Generalized Term Rewriting Systems
Salvador Lucas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Second-order Church-Rosser modulo, without normalization
Thiago Felicissimo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Rule Removal for Confluence
Nao Hirokawa and Kiraku Shintani . . . . . . . . . . . . . . . . . . . . . . . . . . .
Confluence by the Z-property for De Bruijn’s lambda-calculus with nameless dummies,
based on PLFA
Vincent van Oostrom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

1

2

9
16
23

30
36
43
50

56

Confluence Competition
63
Confluence Competition 2024
Raúl Gutiérrez, Aart Middeldorp, Naoki Nishida, Teppei Saito, and René Thiemann 63
crest 0.8
Jonas Schöpf and Aart Middeldorp . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
Hakusan 0.11: A Confluence Tool
Fuyuki Kawano, Nao Hirokawa, and Kiraku Shintani . . . . . . . . . . . . . . . . . 67
Moca 0.3: A First-Order Theorem Prover for Horn Clauses
Yusuke Oi, Nao Hirokawa, and Teppei Saito . . . . . . . . . . . . . . . . . . . . . . 69
CO3 (Version 2.5)
Naoki Nishida and Misaki Kojima . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
CONFident
Miguel Vı́tores, Raúl Gutiérrez, and Salvador Lucas . . . . . . . . . . . . . . . . . 73
infChecker
Raúl Gutiérrez, Salvador Lucas, and Miguel Vı́tores . . . . . . . . . . . . . . . . . 75
AGCP
Takahito Aoto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
ACP
Takahito Aoto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
CeTA 3.1
Dohan Kim, Christina Kirk, Teppei Saito, and René Thiemann . . . . . . . . . . . 78
CSI 1.2.7
Fabian Mitterwallner and Aart Middeldorp . . . . . . . . . . . . . . . . . . . . . . 80
FORT-h 2.1
Fabian Mitterwallner and Aart Middeldorp . . . . . . . . . . . . . . . . . . . . . . 81

iv

FORTify 2.1
Fabian Mitterwallner and Aart Middeldorp . . . . . . . . . . . . . . . . . . . . . .
CRaris: CR checker for LCTRSs in ARI Style
Naoki Nishida and Misaki Kojima . . . . . . . . . . . . . . . . . . . . . . . . . . .

v

82
83

Confluence of Logically Constrained Rewrite Systems
Aart Middeldorp
Department of Computer Science, University of Innsbruck, Austria

Logically constrained rewrite systems [1] are a natural extension of plain term rewrite systems
with native support for constraints that are handled by SMT solvers. In this talk, which isbased on joint work with Jonas Schöpf and Fabian Mitterwallner, we provide an overview of theconfluence results for logically constrained rewrite systems reported in the literature [1–4].

References[1] Cynthia Kop and Naoki Nishida. Term Rewriting with Logical Constraints. In Proc. 9th International
Symposium on Frontiers of Combining Systems, volume 8152 of LNCS (LNAI), pages 343–358, 2013.
doi: 10.1007/978-3-642-40885-4 24.
[2] Jonas Schöpf and Aart Middeldorp. Confluence Criteria for Logically Constrained Rewrite Systems.
In Proc. 29th International Conference on Automated Deduction, volume 14132 of LNCS (LNAI),
pages 474–490, 2023. doi: 10.1007/978-3-031-38499-8 27.
[3] Jonas Schöpf, Fabian Mitterwallner and Aart Middeldorp. Confluence of Logically Constrained
Rewrite Systems Revisited. In Proc. 12th International Joint Conference on Automated Reasoning,
LNCS (LNAI), 2024. To appear.
[4] Sarah Winkler and Aart Middeldorp. Completion for Logically Constrained Rewriting. In Proc. 3rd
International Conference on Formal Structures for Computation and Deduction, volume 108 of Leibniz
International Proceedings in Informatics, pages 30:1–30:18, 2018. doi: 10.4230/LIPIcs.FSCD.2018.30.

1

On Proving Confluence of Concurrent Programs by
All-Path Reachability of LCTRSs∗
Misaki Kojima1†and Naoki Nishida1
Nagoya University, Nagoya, Japan
k-misaki@nagoya-u.jp nishida@i.nagoya-u.ac.jp
Abstract
A logically constrained term rewrite system (LCTRS, for short) modeling a concurrent
program is usually non-terminating, left-linear, and overlapping, but sometimes confluent
w.r.t. an initial ground term which corresponds to an initial configuration of the program.
In this paper, we show how to prove confluence of such an LCTRS w.r.t. the initial term.
To be more precise, we add the rule from the initial term to a fresh constant to the LCTRS,
and construct a proof tree for the all-path reachability problem from the initial term to theconstant. If the directed graph obtained from the proof tree by considering it as a cyclic
proof is strongly connected and each node corresponds to a single term, then all terms
reachable from the initial term can be reduced back to the initial one and thus the original
LCTRS is confluent w.r.t. the initial one.

1

Introduction

Recently, approaches to program verification by means of logically constrained term rewrite
systems (LCTRSs, for short) [12] are well investigated [5, 15, 4, 13, 6, 7, 11, 8, 9, 3, 10].
LCTRSs are extensions of term rewrite systems (TRSs, for short) by allowing rewrite rules
to have guard constraints which are evaluated under built-in theories. A constrained rewrite
rule is applied to a term if the matching substitution satisfies the guard constraint of therule. LCTRSs are reasonable and useful as computation models of not only functional but
also imperative programs. For instance, equivalence checking by means of LCTRSs is usefulto ensure the correctness of terminating functions (cf. [5]). Transformations [5, 6] of sequential
programs into LCTRSs have been extended to concurrent programs with semaphore-based
exclusive control [11], and the extended transformation is applicable to asynchronous integertransition systems with shared variables (AITS, for short) [8].
The LCTRS obtained from a concurrent program by the aforementioned transformation isusually non-terminating, left-linear, and overlapping, but sometimes confluent w.r.t. an initial
ground term which corresponds to an initial configuration of the program (or an initial state of
the transition system). Here, an LCTRS R is said to be confluent w.r.t. a term t if the ARS(T, →R ∩ (T × T )) is confluent, where T is the set of reachable terms from t w.r.t. →R .
Let us consider the program graph in Figure 1 for Peterson’s mutual exclusion algorithm [1,Example 2.25]. Two processes P0 , P1 share Boolean variables b0 , b1 and an integer variable x;
bi indicates that Pi wants to enter the critical section criti ; x stores the identifier—0 or 1—of
the process that has priority for the critical section at that time. The LCTRS R1 for the AITS
consisting of PG 0 and PG 1 is illustrated in Figure 2.1 The initial state ⟨noncrit0 , noncrit1 , {b0 7→∗ This work was partially supported by JSPS KAKENHI Grant Number 24K02900 and Grant-in-Aid for JSPS
Fellows Grant Number 24KJ1240.
† JSPS Research Fellow
1 In the first rule of R , we may replace b′ and x′ by true and 1, respectively. However, for the correspondence
10with the program graphs PG 0 , PG 1 , we remain the label of the corresponding edge as the constraint “b′0 ∧ x′ =1”of the rule.

2

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs⟨b , x⟩ := ⟨true, 1 − i⟩ 
/ waiti/ noncriti m ibi := false

x = i ∨ ¬b1−i

Kojima and Nishida/ critiFigure 1: Program graph PG i (i = 0, 1) for Peterson’s mutual exclusion algorithm.

cnfg(noncrit0 , p1 ,b0 , b1 , x) → cnfg(wait0 , p1 ,b′0 , b1 , x′ )cnfg(wait0 , p1 ,b0 , b1 , x) → cnfg(crit0 ,p1 ,b0 , b1 , x ) cnfg(crit ,
p
,
b
,
b
,
x)
→
cnfg(noncrit,p,b′0 , b1 , x )
0
1
0 1
0 1
R1 =
 cnfg(p0 ,noncrit1 , b0 , b1 , x) → cnfg(p0 ,wait1 , b0 , b′1 , x′ )
 cnfg(p0 ,wait1 , b0 , b1 , x) → cnfg(p0 ,crit1 ,
b0 , b1 , x )
cnfg(p0 ,crit1 ,
b0 , b1 , x) → cnfg(p0 ,noncrit1 , b0 , b′1 , x )[ b′0 ∧ x′ = 1 ] [ x = 0 ∨ ¬b1 ] 


[
¬b′0
] 

[ b′1 ∧ x′ = 0 ] [ x = 1 ∨ ¬b0 ] 


[
¬b′1
]

Figure 2: LCTRS R1 for the AITS consisting of PG 0 and PG 1 in Figure 1.

false, b1 7→ false, x 7→ 0}⟩ is represented by the term cnfg(noncrit0 , noncrit1 , false, false, 0). The
LCTRS R1 is non-terminating, left-linear, and overlapping, and has non-trivial critical pairs.
Note that R1 has no normal form that is rooted by cnfg and reachable from the initial term.
One of the simplest sufficient conditions for confluence of an LCTRS R w.r.t. an initial(ground) term is (ground) confluence of R. However, it is not so easy to prove (ground)
confluence of the above example because, e.g., R1 does not satisfy some well-known existing
criteria—“(weak) orthogonality” [12] and “termination and joinability of critical pairs” [14]—for
confluence of LCTRSs. In addition, non-termination often makes it difficult to prove joinability
and its related properties (e.g., strong closedness) of critical pairs (see Example 6).
In this paper, for the LCTRS R obtained from a concurrent program, we show how to prove
confluence of R w.r.t. an initial ground term s0 which corresponds to an initial configurationof the program. To be more precise, we first add to R the rule from the initial term s0 toa fresh constant init, obtaining the LCTRS R′ = R ∪ {s0 → init}. Secondly, using a proof
system for APR problems, we try to construct a proof tree for the all-path reachability problem(APR problem, for short) from the initial term to the constant w.r.t. R′ : {s0 } ⇒ {init}. An
APR problem of R′ considered as a transition system is a pair P ⇒ Q of state sets P, Q and isdemonically valid (i.e., solved) if every finite execution path of R′ —a transition sequence startingwith a state in P and ending with a terminating state—includes a state in Q [4]. Thirdly, weconstruct the directed graph from the proof tree by considering it as a cyclic proof [2] and by
removing the nodes labeled with the axiom/c-subs rule of the proof system. Finally, we showthat if the directed graph is strongly connected and each node corresponds to a single term,then all terms reachable from the initial one can be reduced back to the initial one and thus
the original LCTRS is confluent w.r.t. the initial one.

2

All-path Reachability Problems of LCTRSs

A logically constrained term rewrite system (LCTRS, for short) [12, 5] is a set R of constrained
rewrite rules defined over two kinds of signatures, Σtheory and Σterms , and a set V of variables.
The theory signature Σtheory equipped with interpretations I and J defines built-in objects
which are either values in Val (⊆ Σtheory ) or operators: For each theory sort ι, I specifies theuniverse of ι; J assigns an interpretation to each built-in operator, assigning to a ground termwith sort ι an element in I(ι). The non-theory signature Σterms is a set of function symbols for3

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs

Kojima and Nishidauser-defined functions and constructors. Constrained rewrite rules in R specify the behavior ofsome function symbols in Σterms , and R implicitly includes rules for calculation symbols such
as +: x + y → z [ z = x + y ].
We typically choose a theory-sort set Stheory and a theory signature Σtheory such that
Stheory ⊇ {bool }, Σtheory ⊇ Σcore
theory = {true, false : bool , ∧, ∨, =⇒ , ⇐⇒ : bool × bool ⇒bool , ¬ : bool ⇒ bool } ∪ {=ι , ̸=ι : ι × ι ⇒ bool | ι ∈ Stheory }, I(bool ) = {⊤, ⊥}, and J interpretsthese symbols as expected: J (true) = ⊤ and J (false) = ⊥. We omit the sort subscripts ι from=ι and ̸=ι when they are clear from context. A theory term with sort bool is called a concorestraint. The standard integer signature Σint
theory is Σtheory ∪ {+, −, ×, exp, div, mod : int × int ⇒int} ∪ {≥, > : int × int ⇒ bool } ∪ Valint where Stheory ⊇ {int, bool }, Valint = {n | n ∈ Z},
I(int) = Z, and J (n) = n for any integer n ∈ Z. Note that we use n (in sans-serif font) as thefunction symbol for n ∈ Z (in math font). We define J in a natural way. An LCTRS with thestandard integer signature is called an integer LCTRS.
Example 1. Let S = {int, bool }, Σ = Σterms ∪ Σint
theory and Σterms = {fact : int ⇒ int} ∪ {n :int | n ∈ Z}. To implement an integer LCTRS calculating the factorial function over Z, we use
the signature Σ above and the following LCTRS:
fact(x) → x × fact(x − 1) [ x > 0 ]R2 = fact(x) → 1 [ x ≤ 0 ]Note that R2 implicitly includes rules for calculation symbols such as − and ×: x − y → z [ z =x − y ] and x × y → z [ z = x × y ]. The term fact(3) is reduced by R2 to 6: fact(3) →R2
3 × fact(3 − 1) →R2 3 × fact(2) →R2 3 × (2 × fact(2 − 1)) →R2 3 × (2 × fact(1)) →R2 3 × (2 × (1 ×fact(1 − 1))) →R2 3 × (2 × (1 × fact(0))) →R2 3 × (2 × (1 × 1)) →R2 3 × (2 × 1) →R2 3 × 2 →R2 6.

A constrained term is a pair ⟨t | ϕ⟩ of a term t and a constraint ϕ, which can be considered theset of all instances of t w.r.t. substitutions that respect ϕ:2 ⟨t | ϕ⟩ = {tγ | γ respects ϕ}. An allpath reachability problem (APR problem, for short) of an LCTRS R is a pair ⟨s | ϕ⟩ ⇒ ⟨t | ψ⟩ ofconstrained terms ⟨s | ϕ⟩, ⟨t | ψ⟩ for state sets. We call ⟨s | ϕ⟩ ⇒ ⟨t | ψ⟩ constant-directed if ⟨t | ψ⟩is a singleton set of a constant normal form c [8]. A (possibly infinite) reduction sequence of R
is called an execution path if the reduction sequence either is infinite or ends with an irreducible
term. If ⟨t | ψ⟩ = {c} for some constant normal form c, then we abbreviate ⟨s | ϕ⟩ ⇒ ⟨t | ψ⟩ to⟨s | ϕ⟩ ⇒ c. A constant-directed APR problem ⟨s | ϕ⟩ ⇒ c is demonically valid w.r.t. R if every
finite execution path starting from a term in ⟨s | ϕ⟩ ends with c.
The proof system c-DCC [8, 9] for constant-directed APR problems is a weakened but easilyimplementable variant of the proof system DCC [4] for arbitrary APR problems.
Definition 2 (c-DCC [8, 9]). Let R be an LCTRS, and G a finite set of constant-directed
APR problems. The set ofS derivatives of a constrained term w.r.t. an LCTRS R is defined
as follows: ∆R (⟨s | ϕ⟩) = ℓ→r [φ]∈R ∆ℓ,r,φ (⟨s | ϕ⟩), where ℓ → r [φ] has no shared variablewith ⟨s | ϕ⟩3 and ∆ℓ,r,φ (⟨s | ϕ⟩) = {⟨(s[r]p )γ | (ϕ ∧ φ)γ⟩ | p ∈ Pos(s), s|p ∈/ V, s|p and ℓ are
unifiable, γ = mgu(s|p , ℓ), Ran(γ|Var(ϕ,φ) ) ⊆ Val ∪ V, (ϕ ∧ φ)γ is satisfiable}. The proof system
c-DCC(R, G) consists of the following proof rules:
ϕ is unsatisfiable or s = c(axiom/c-subs)⟨s | ϕ⟩ ⇒ c⟨s1 | ϕ1 ⟩ ⇒ cwhere ∆R (⟨s | ϕ⟩) = {⟨si | ϕi ⟩ | 1 ≤ i ≤ n⟩} for some n > 0.

...
⟨sn | ϕn ⟩ ⇒ c(c-der)⟨s | ϕ⟩ ⇒ c∃(⟨s′ | ϕ′ ⟩ ⇒ c) ∈ G. ⟨s | ϕ⟩ ⊆ ⟨s′ | ϕ′ ⟩(weak circ)⟨s | ϕ⟩ ⇒ c

2 A substitution γ is said to respect a constraint ϕ if γ(x) ∈ Val for all x ∈ Var(ϕ), and J (ϕγ) = ⊤.

3 When there exists a shared variable, we rename the variables in ℓ → r [φ].

4On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs(2)(w. circ)(9)(3)(w. circ)(c-der)(5)(w. circ)(3)(c-der)(10)(c-der)(2)(w. circ)(10)(c-der)(6)(c-der)(w. circ)(2)(c-der)(11)(c-der)(7)(11)(w. circ)
(8)

(3)

(1)

(c-der)(1)

Kojima and Nishida(w. circ)(c-der)(4)(a./c-subs)(c-der)where(1) ⟨cnfg(noncrit0 , noncrit1 , false, false, 0) | true⟩ ⇒ init(2) ⟨cnfg(wait0 , noncrit1 , true, false, 1) | true⟩ ⇒ init(3) ⟨cnfg(noncrit0 , wait1 , false, true, 0) | true⟩ ⇒ init(4) ⟨init | true⟩ ⇒ init(5) ⟨cnfg(crit0 , noncrit1 , true, false, 1) | true⟩ ⇒ init(6) ⟨cnfg(wait0 , wait1 , true, true, 0) | true⟩ ⇒ init(7) ⟨cnfg(wait0 , wait1 , true, true, 1) | true⟩ ⇒ init(8) ⟨cnfg(noncrit0 , crit1 , false, true, 0) | true⟩ ⇒ init(9) ⟨cnfg(noncrit0 , noncrit1 , false, false, 1) | true⟩ ⇒ init
(10) ⟨cnfg(crit0 , wait1 , true, true, 0) | true⟩ ⇒ init
(11) ⟨cnfg(wait0 , crit1 , true, true, 1) | true⟩ ⇒ init

Figure 3: A proof tree for the APR problem ⟨cnfg(noncrit0 , noncrit1 , false, false, 0) | true⟩ ⇒ init.
Theorem 3 (soundness of c-DCC [9]). Let R be an LCTRS, and G a finite set of constantdirected APR problems. Suppose that for each problem (⟨s | ϕ⟩ ⇒ c) ∈ G, there exists a proof
tree T under c-DCC(R, G), each circ node of which has a c-der node as an ancestor. Then, R
demonically satisfies all APR problems in G.
For an APR problem ⟨s | ϕ⟩ ⇒ c, a construction of a single proof tree in the style of cyclic
proofs [2] has been proposed [10].

3

Confluence w.r.t. Ground Initial Terms

Confluence of an LCTRS R w.r.t. a initial (ground) term is equivalent to the property that any
two of the reachable terms are joinable. If a term can be reduced to the initial term, then it
is joinable with any other term. Thus, a trivial sufficient condition for the property is that all
the reachable terms can be reduced back to the initial one. It is not so easy to prove that R
satisfies this sufficient condition in the case where the set of reachable terms is infinite. In thissection, we show how to prove it by using proof trees of APR problems.
Let us consider the LCTRS R1 and the initial term s0 = cnfg(noncrit0 , noncrit1 , false, false, 0)
in Section 1 again. We prepare a fresh constant init and add the rule s0 → init to R1 , obtaining
R′1 = R1 ∪ {s0 → init}. Then, the APR problem ⟨cnfg(noncrit0 , noncrit1 , false, false, 0) | true⟩ ⇒init is demonically valid w.r.t. R′1 because of the proof tree illustrated in Figure 3. Since neither
R1 nor R′1 has a normal form rooted by cnfg, there is no finite execution path starting fromthe initial term. For this reason, it is trivial that the APR problem above is demonically valid
w.r.t. R′1 . Though, the proof tree can be used to prove confluence w.r.t. the initial term.
By considering the proof tree as a cyclic proof and identifying weak circ nodes with othernodes having the same APR problems, we obtain the proof graph [2], which is a directed graph.
All axiom/c-subs nodes have the APR problem ⟨init | true⟩ ⇒ init which is not relevant to the
reduction of the original LCTRS R. Thus, we remove the axiom/c-subs nodes from the axiom/csubs nodes from the proof graph, obtaining a directed graph. If the directed graph is strongly
connected and each node corresponds to a single term, then all reachable nodes are reachable
back to the root one, i.e., all reachable terms from the initial one can be reduced back to theinitial one. For example, we remove node (4) from the proof tree in Figure 3, obtaining astrongly connected directed graph such that each node corresponds to a single term. Therefore,
R1 is confluent w.r.t. the initial term.

5

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs

(9) d

9
(5) e

(10)

(11)

(6)

(7)

O
O

O

. (2)

% 
y

O

Kojima and Nishida

e
9 (8)

9 (3)
e
(1) p

Figure 4: The proof graph obtained from the proof tree in Figure 3 by removing all axiom/c-subs
nodes.
Theorem 4. Let R be the LCTRS obtained from a concurrent program, s0 be an initial term
corresponding to an initial configuration of the program, and init a fresh constant. Suppose that
we have a proof tree for the APR problem ⟨s0 | true⟩ ⇒ init. Let G be the directed graph obtained
from the proof graph of the proof tree by removing all axiom/c-subs nodes. Suppose that G isstrongly connected and one of the following holds:(a) for every node of G, the constrained term ⟨s | ϕ⟩ of the attached APR problem ⟨s | ϕ⟩ ⇒ init
is singleton, or(b) the directed graph obtained from G by removing the root is acyclic.
Then, R is confluent w.r.t. s0 .
Proof. Recall that by assumption, thee is no reachable normal form rooted by cnfg. For reachable terms t1 , t2 with s0 →∗R t1 and s0 →∗R t2 , we show that t1 and t2 are joinable. Let v1 , v2
be nodes of G such that APR problems ⟨s1 | ϕ1 ⟩ ⇒ init and ⟨s2 | ϕ2 ⟩ ⇒ init are the attached
APR problems of v1 and v2 , respectively, ti ∈ ⟨si | ϕi ⟩ for i = 1, 2, and the paths from the root
node to v1 and v2 correspond to s0 →∗R t1 and s0 →∗R t2 , respectively. We make a case analysis
depending on which premise holds, (a) or (b).
(a) In this case, we have that {ti } = ⟨si | ϕi ⟩ for i = 1, 2, Since every node corresponds to asingle term, paths of G coincide with reduction sequences. In addition, since G itself isstrongly connected, there exist paths from v1 and v2 to the root node, respectively, andhence we have that t1 →∗R s0 and t2 →∗R s0 .
(b) Since the graph without the root node is acyclic, there exist unique paths from v1 and v2
to the root node, respectively. Thus, we have that t1 →∗R s0 and t2 →∗R s0 .
Therefore, t1 and t2 are joinable.
Example 5. We obtain the proof graph in Figure 4 from the proof tree in Figure 3 by removing
all axiom/c-subs nodes. The proof graph is strongly connected, and for every node, the attachedconstrained term is singleton because every term rooted by cnfg has a unique reduct. Therefore,by Theorem 4, R1 is confluent w.r.t. cnfg(noncrit0 , noncrit1 , false, false, 0).
Example 6. Consider the LCTRS R1 in Figure 2 again. This LCTRS is linear and allits critical pairs are strongly closed and thus, R1 is strongly confluent (i.e., confluent) [14].
In fact, crest,4 Constrained REwriting Software Tool, succeeds in proving confluence of R1 .
However, crest failed to prove confluence of the LCTRS obtained from R1 by adding the rules
4 http://cl-informatik.uibk.ac.at/software/crest/

6

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs

Kojima and Nishida{cnfg(s0 , p1 , b0 , b1 , x) → cnfg(s0 , p1 , b0 , b1 , x) | s0 ∈ {noncrit0 , wait0 , crit0 }, p1 , b0 , b1 , x ∈ V} ∪{cnfg(p0 , s1 , b0 , b1 , x) → cnfg(p0 , s1 , b0 , b1 , x) | s1 ∈ {noncrit1 , wait1 , crit1 }, p0 , b0 , b1 , x ∈ V}. On
the other hand, in our approach, we succeed in constructing a proof tree which is almost the sameas the tree in Figure 3, and the corresponding graph satisfies the condition shown in Theorem 4.
Therefore, the LCTRS is confluent w.r.t. the initial term cnfg(noncrit0 , noncrit1 , false, false, 0).
The following examples shows the reason why the condition (a) is assumed in Thereom 4.
Example 7. Consider the following LCTRS:
cnfg(f(x)) → cnfg(g(x, y)) [ y ≥ x ]








cnfg(g(x,y))→
cnfg(f(x))
[
y
≤
x
]






′
′
cnfg(g(x, y)) → cnfg(g(x, y )) [ y > x ∧ y = y + 1 ]R2 =cnfg(f(x)) → cnfg(h(x, y)) [ y ≥ x ]








cnfg(h(x,y))→
cnfg(f(x))
[
y
≤
x
]






′
′
cnfg(h(x, y)) → cnfg(h(x, y )) [ y > x ∧ y = y + 1 ]This LCTRS is not confluent w.r.t. cnfg(f(0)). For the APR problem ⟨cnfg(f(0)) | true⟩ ⇒ init,
we obtain an APR proof, the proof graph of which is strongly connected. The root node(12) with ⟨cnfg(f(0)) | true⟩ ⇒ init has two children (13) and (14) with the APR problems⟨cnfg(g(0, y)) | y ≥ 0⟩ ⇒ init and ⟨cnfg(h(0, y)) | y ≥ 0⟩ ⇒ init, respectively, both of which
are sets of two or more terms. There is a path from (13) to (12), but not all terms in (13) canbe reduced to the initial term cnfg(f(0)). For example, cnfg(g(0, 1)) cannot be reduced to theinitial term, and all reduction sequences from cnfg(g(0, 1)) follow the path (13),(13),. . .

4Conclusion

In this paper, we showed how to prove confluence of an LCTRS w.r.t. an initial term. The
proposed method succeeded in proving confluence of concurrent programs w.r.t. their initialstates, e.g., the AITS defined by the program graphs in Figure 1.
One may think that we do not have to use the APR setting in order to prove our confluence
problems. In the case where the set of reachable terms from an initial one is finite, confluencew.r.t. the initial term is decidable and we do not have to reduce the confluence problem to an
APR problem. In the other case, as for R1 , our approach may work for the confluence problem.
In addition, our approach can be automated by using the implementation of the proof system
for APR problems, i.e., we do not have to implement a new tool from scratch.
A future work is the automation of the proposed method, i.e., to adapt our implementation
for APR problems to confluence w.r.t. an initial one. Given an LCTRS R and its initial terms0 , using the proof system for constant-directed APR problems, we automatically construct a
proof tree for the APR problem ⟨s0 | true⟩ ⇒ init w.r.t. R, obtaining the proof graph. Note that
we may fail the construction even if R is confluent (w.r.t. s0 ). The strong connectedness andthe condition (b) in Theorem 4 are decidable. On the other hand, we have not had sufficientconditions for the condition (a) in Theorem 4 yet. It is also our future work to find a decidable
sufficient condition for the condition (a).

References[1] C. Baier and J. Katoen. Principles of model checking. MIT Press, 2008.

7

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs

Kojima and Nishida[2] J. Brotherston. Cyclic proofs for first-order logic with inductive definitions. In B. Beckert, editor,
Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableauxand Related Methods, volume 3702 of Lecture Notes in Computer Science, pages 78–92, Springer,
2005.
[3] Ş. Ciobâcă, D. Lucanu, and A. Buruiana. Operationally-based program equivalence proofs using
LCTRSs. Journal of Logical and Algebraic Methods in Programming, 135:1–22, 2023.
[4] Ş. Ciobâcă and D. Lucanu. A coinductive approach to proving reachability properties in logically constrained term rewriting systems. In D. Galmiche, S. Schulz, and R. Sebastiani, editors,
Proceedings of the 9th International Joint Conference on Automated Reasoning, volume 10900 of
Lecture Notes in Computer Science, pages 295–311, Springer, 2018.
[5] C. Fuhs, C. Kop, and N. Nishida. Verifying procedural programs via constrained rewriting induction. ACM Transactions on Computational Logic, 18(2):14:1–14:50, 2017.
[6] Y. Kanazawa and N. Nishida. On transforming functions accessing global variables into logicallyconstrained term rewriting systems. In J. Niehren and D. Sabel, editors, Proceedings of the 5thInternational Workshop on Rewriting Techniques for Program Transformations and Evaluation,
volume 289 of Electronic Proceedings in Theoretical Computer Science, pages 34–52, Open Publishing Association, 2019.
[7] Y. Kanazawa, N. Nishida, and M. Sakai. On representation of structures and unions in logicallyconstrained rewriting. IEICE Technical Report SS2018-38, Vol. 118, No. 385, pp. 67–72, theInstitute of Electronics, Information and Communication Engineers, 2019 (in Japanese).
[8] M. Kojima and N. Nishida. From starvation freedom to all-path reachability problems in constrained rewriting. In M. Hanus and D. Inclezan, editors, Proceedings of the 25th International
Symposium on Practical Aspects of Declarative Languages, volume 13880 of Lecture Notes in Computer Science, pages 161–179, Springer Nature Switzerland, 2023.
[9] M. Kojima and N. Nishida. Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. Journal of Logical and Algebraic Methods in Programming,
135:1–19, 2023.
[10] M. Kojima and N. Nishida. A sufficient condition of logically constrained term rewrite systems for
decidability of all-path reachability problems with constant destinations. Journal of Information
Processing, 32:417–435, 2024.
[11] M. Kojima, N. Nishida, and Y. Matsubara. Transforming concurrent programs with semaphores
into logically constrained term rewrite systems. In A. Riesco and V. Nigam, editors, Informal Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations
and Evaluation, pages 1–12, 2020.
[12] C. Kop and N. Nishida. Term rewriting with logical constraints. In P. Fontaine, C. Ringeissen, and
R. A. Schmidt, editors, Proceedings of the 9th International Symposium on Frontiers of Combining
Systems, volume 8152 of Lecture Notes in Artificial Intelligence, pages 343–358, 2013.
[13] N. Nishida and S. Winkler. Loop detection by logically constrained term rewriting. In R. Piskac and
P. Rümmer, editors, Proceedings of the 10th Working Conference on Verified Software: Theories,
Tools, and Experiments, volume 11294 of Lecture Notes in Computer Science, pages 309–321,
Springer, 2018.
[14] J. Schöpf and A. Middeldorp. Confluence criteria for logically constrained rewrite systems. In
B. Pientka and C. Tinelli, editors, Proceedings of the 29th International Conference on AutomatedDeduction, volume 14132 of Lecture Notes in Computer Science, pages 474–490, Springer, 2023.
[15] S. Winkler and A. Middeldorp. Completion for logically constrained rewriting. In H. Kirchner,
editor, Proceedings of the 3rd International Conference on Formal Structures for Computation
and Deduction, volume 108 of Leibniz International Proceedings in Informatics, pages 30:1–30:18,
Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2018.

8

From Subtree Replacement Systems to Term Rewriting
Systems: a Roadmap to Orthogonality∗
Salvador Lucas
DSIC & VRAIN, Universitat Politècnica de València, Spainslucas@dsic.upv.es
Abstract
Orthogonality plays an important role in the analysis of confluence of term rewriting
systems, and also in related subfields like optimality, strategic rewriting, etc. However, theterm “orthogonality” was introduced by Dershowitz and Jouannaud in 1990 after morethan 20 years of developments, often “hidden” under terminologies which are not usedanymore. This paper collects concepts, terminologies, and notations which have been
relevant in this process, together with the main works that introduced them.
Man gave names to all the animals (Bob Dylan)

1

Motivation

Confluence is a central property of Term Rewriting Systems (TRSs). A helpful notion to prove
confluence of TRSs is orthogonality. Since the nineties of the XXth century, the notion of an(almost, weakly) orthogonal TRS has been used and taught as presented in existing books onterm rewriting systems, notably [1, 21, 24]. However, it took 20 years to fix the notion anddenomination we use since then. In the meantime, different definitions and results were proposed
and obtained by different authors whose research did not specifically focus on “term rewriting
systems” or “orthogonality”. This paper is an effort to provide a sequence of references where
the evolution of the main involved notions and results can be found. Nowadays, the possibilityof an electronic access to “old” documents makes this task easier than some years ago. Althoughconsidering all relevant references is difficult, we hope this paper can be a useful and sufficiently
detailed roadmap to orthogonality (e.g., for students).

2

Confluence

Church and Rosser investigated reduction of λ-expressions [5]. They introduced several terms
in use today: conversion, reduction, reducible (p. 472); contract(ion), peak, valley, residual (p.
473). They proved that, if two λ-expressions A and B are convertible (A ↔∗ B in the current
notation), then there is a valley between A and B (we often say that A and B are joinable) [5,Theorem 1]. Nowadays, this result is known as the Church-Rosser property (of λ-calculus).
According to Newman, results like [5, Theorem 1] would be considered as a theorem ofconfluence [19, Introduction], in what seems to be the first use of the word “confluence” applied
to the joinability of peaks. Such confluence property is further developed in [19, Section 3]. In
particular Newman defines confluence as the property presented in item (A) of Section 3, whichjust formulates the Church-Rosser property in Newman’s terminology. Newman’s property∗ Partially
supportedby
MCIN/AEI
project
PID2021-122830OB-C42
fundedby
MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe” and by the grant
CIPROM/2022/6 funded by Generalitat Valenciana.

9A Roadmap to Orthogonality of Term Rewriting Systems

Salvador Lucas(B) is presented as a consequence of his property (A), i.e., (A) ⇒ (B) holds. Newman relies
on notions and notations coming from the theory of partially ordered sets. However, onlytransitivity of the relation (denoted >, which actually coincides with →+ , see the last paragraphof [19, Section 2]) is required. Property (B) is formulated as follows: if x1 and x2 have an upperbound they have also a lower bound, i.e.,
if there is x such that x ≥ x1 and x ≥ x2 , then there is x0 such that x1 ≥ x0 andx2 ≥ x0 .
Nowadays we would say that ≥ is →∗ ; hence
property (B) in [19, Section 3] is what we call confluence today.
See [13, Definition D7] and [20, Definition 24] for more explicit definitions, including the usual
diagramatic representation. Curry and Feys’ Property (B) in [6, page 110] is equivalent toNewman’s property (B) and [6, Theorem 3] proves that (B) ⇒ (A) holds,1 thus establishing
the well-known equivalence between confluence and Church-Rosser property.

3

Orthogonality of TRSs

In the development of orthogonality of TRSs as a syntactic criterion for confluence, there are
two milestones: in 1970 Rosen proved confluence of (left-linear) closed Subtree Replacement
Systems where no overlap is allowed (which correspond to orthogonal systems); then, in 1977
Huet and O’Donnell (independently) extended Rosen’s result to TRSs with a restricted subclassof overlaps (weakly orthogonal TRSs).
Rosen (1970): Closed Subtree Replacement Systems. Following Brainerd’s work [4,3, 2], Rosen investigated confluence of Subtree Replacement Systems (SRSs [23, Definition 5.1],
although [22, Definition 2.1] uses PBS, standing for Post-Brainerd Systems), consisting of a(possibly infinite) set of tree transformation rules. As in [10], each (finite) tree R with labels
in a set V is a mapping R : Dom R → V from a tree domain Dom R, i.e., a nonempty
subset of sequences in N∗>0 , the set of sequences of positive numbers to a set V of labels (e.g., ofsymbols from an alphabet) associated to the node indicated by a sequence i1 .i2 . . . . .in of positive
numbers. The tree domain Dom R must satisfy two closure properties: for all p ∈ N∗>0 andi ∈ N>0 , (i) if p.i ∈ Dom R, then p ∈ Dom R (‘down’ closed) and (ii) if p.(i + 1) ∈ Dom R, thenp.i ∈ Dom R (‘left’ closed ) [22, Section 2]. Although Rosen’s notion of tree does not imposethat nodes labeled with a given symbol have a fixed number of ‘offsprings’, in [22, Definition
3.1] he considers properly ranked trees where symbols have a fixed rank (i.e., an arity) and eachk-ary symbol has exactly k associated subtrees.
Remark 1. If terms t are viewed as properly ranked trees R, then Dom R is just the set Pos(t)of positions of t.
In the second column of [22, page 119], Rosen explains how to define an SRS (or PBS)
by ‘instantiating’ a set of rule schemata. A rule schema is a pair R → S of trees2 R and S
where some leaves are labeled with the so-called parameters u from a set U , which play therole of variables. The left-hand sides R of a rule schema may contain at most one occurrenceof each parameter u. Thus, Rosen’s rule schemata correspond to left-linear TRSs. As done by
1 Curry and Feys use (χ) to refer to Newman’s property (A).
2 The arrow was already used by Brainerd.

10

A Roadmap to Orthogonality of Term Rewriting Systems

[18]
TRSs
[18]
TRSs

Salvador Lucas

Table 1: Terms, substitutions, and term rewriting in [18]Operators with degrees Words Pure word
Nontrivial subword
Signature
Terms Ground term Non-variable subterm
Relations (λ, %)Rules ` → r

Set of relations R
TRS R

α reduces to α0 w.r.t. R
α rewrites to α0

α → α0 (R)α →R α0

Church and Rosser for the λ-calculus, Rosen developed an appropriate notion of residual to keep
track of redexes that remain as redexes (and therefore can be reduced) after the applicationof a rewriting step using a rule ‘above’ the position of such a redex. He called such SRSs
closed [22, Definition 2.3]. The main idea of closedness is depicted in [23, Figure 7]. Closed
and unequivocal SRSs are confluent [22, Theorem 2.5]. Unequivocal SRSs are those which canbe seen as mappings from trees to trees [22, Definition 2.1], i.e., no pair of rules share thesame left-hand side [23, Definition 5.2]. Then, [22, Lemma 2.4] proves that SRSs obtained byinstantiating the rules of a set of a specific class of rule schemata are closed. Such a class ofrule schemata is defined by items (1) and (2) of [22, Lemma 2.4] (see also [23, Theorem 6.5]).
Item (1) says that each rule in an SRS comes from the instantiation of a single rule in the rule
schemata; item (2) says that, for all instances σ(A) and σ(C) of the left-hand sides A and C ofrule schemata A → B and C → D, and all nonempty positions p 6= Λ, if σ(A)|p = σ(C) holds,
then p ∈/ PosF (A). They correspond to what we understand as an orthogonal TRS today.
Orthogonal TRSs are clearly unequivocal. Thus,
confluence of orthogonal TRSs is a consequence of [22, Lemma 2.4 & Theorem 2.5].3
Knuth & Bendix (1970): Superposition. Knuth and Bendix followed a different approachto the analysis of confluence of TRSs [18]. Since their terminology was quite different from what
is used today, Table 1 provides some hopefully useful connections to read the paper. The notionof critical pair is usually credited to [18], but they do not use this name which is due to Huet
(see below). In [18, Section 5], Knuth and Bendix define a superposition process to check thelattice condition formulated in [18, Theorem 4] as follows: “if s → t and s → t0 , then there
exists u such that t →∗ u and t0 →∗ u”. Of course, this is what we call local confluence today.
In the description of the superposition process, the notion of critical pair arises from the final
consideration, in page 274 (Case 2, equation (5.4)), of the situation when σ(`0 ) = σ(`|p ) forsome rules ` → r and `0 → r0 and p ∈ PosF (`), the only one which may lead to a failure in
the “lattice condition”. In [18, Theorem 5], this is called the “superposition of `0 on p in `”.
Then, the corollary in page 275 rephrases Theorem 4 by replacing the lattice condition (i.e.,
local confluence) by the joinability of terms C[σ(r0 )]p and σ(r) (see their equation (5.9)).4
The pair hC[σ(r0 )]p , σ(r)i, obtained from (5.9), is what we call critical pair today.
Knuth and Bendix pay no attention to non-superposition, i.e., the absence of critical pairs.
O’Donnell (1977): Non-overlappingness. Following Rosen’s approach [22, 23], O’Donnell
used non-overlapping to refer to rule schemata consisting of left-linear rules (in the current
terminology, see condition (4) in [20, Definition 45]) where for all instances σ(A) and σ(C) of
3 Huet remarks that Rosen’s result concerns ground terms only [13, page 42, column 2, last paragraph].
4 There is a typo the second member of (5.9), where % should be % . Also, there is a typo in the joinability
12
condition of the second line after (5.9): σ 00 →∗ σ000 should be written instead of σ000 →∗ σ000 .

11A Roadmap to Orthogonality of Term Rewriting Systems

Salvador Lucasthe left-hand sides A and C of rule schemata A → B and C → D, and all nonempty positions
p 6= Λ such that σ(A)|p = σ(C), we have p ∈/ PosF (A) [20, Definition 48]. Note, however, that
this definition does not consider the case when σ(A) = σ(C). Thus, in contrast to Rosen’s
approach, there can be non-overlapping rule schemata including rules A → B and C → D suchthat σ(A) = σ(C) holds and no further restriction is imposed on σ(C) and σ(D). Actually,
this situation is handled by introducing the notion of a consistent rule schemata [20, Definition
49]. A rule schemata is consistent if for all pairs of rule schemata A → B and C → D, if
σ(A) = σ(C) holds, then B and D are identical up to renaming. Therefore,
non-overlapping and consistent rule schemata correspond to weakly orthogonal TRSs.
Accordingly, confluence of weakly orthogonal TRSs follows from [20, Theorems 17 and 6]. Notethat there is no reference to any notion of critical pair.
Huet (1977): Critical Pairs of Term Rewriting Systems. Knuth and Bendix did
not employ the terminology “term rewriting system” or “critical pair”. Apparently, they wereintroduced by Huet,5 possibly as part of his description of Knuth & Bendix superposition
algorithm in [13, page 38].
Definition 2 (Critical pair [13, p. 38]). Let R be a TRS, α : ` → r and α0 : `0 → r0 be rulesof R sharing no variable (rename if necessary), and p ∈ PosF (`) be a nonvariable position of` such that `|p and `0 unify with mgu θ. Then, hθ(`[r0 ]p ), θ(r)i is a critical pair (CP for short)of R. If α and α0 are renamed versions of the same rule, then the case p = Λ is excluded.6
The set of CPs of R is CP(R). Huet also investigated conditions guaranteeing confluence of
TRSs. In [13, Lemma 9] he proved that joinability of critical pairs characterizes local confluence7
of a TRS. As remarked above, this was anticipated by Knuth & Bendix. Thus, terminating
TRSs all whose critical pairs are joinable are confluent. In order to avoid the requirement oftermination, in [13, Section 3] Huet investigates free TRSs. According to [13, Section II.1], freeterms are what we call linear terms today. In [13, Section II.3], Huet introduces left-free, rightfree and free TRSs, which, nowadays, we know as left-linear, right-linear, and linear TRSs,
respectively. In the second column of page 41, Huet’s corollary of [13, Lemma 11] establishes
that left-free parallel-0 closed term rewriting systems are confluent. Parallel-0 closed TRSs arethose whose critical pairs hs, ti satisfy that t can be obtained from s by a single step of parallel
rewriting, written s →k t, which consists of the simultaneous contraction in s of a (possibly
empty) set P of disjoint redexes, see the last paragraph of the second column in [13, page 40];
since P can be empty, →k is reflexive. Weakly orthogonal TRSs only have trivial critical pairs
ht, ti for which such a condition trivially holds, as parallel rewriting is reflexive. Thus,
confluence of weakly orthogonal TRSs follows from [13, Lemma 11].
Huet & Lévy (1979): Left-linearity. Non-ambiguity. Huet’s left-free TRSs were called
left-linear in [12, page 4]. The notions of left-free, right-free and free TRSs in [13] became
left-linear, right-linear, and linear TRSs in [14]. Also, in [12, page 4],
5 His notion of term rewriting system, introduced in [13, Section II.2], is essentially the current one, exceptthat left-hand sides ` of rules ` → r are not required to be non-variable terms
6 In the first sentence of the last paragraph in [18, Section 5], Knuth and Bendix suggest omiting superpositions of `0 on Λ in ` if ` and `0 are renamed versions of the same term; however, they justify the saying that, in
this case, the obtained critical pair would be trivial, for which the equality of right-hand sides r and r0 of theinvolved rules should be required as well, as done by Huet.
7 Local confluence coincides with the Weak Church-Rosser property in [16, Definition I.5.2(2)], where theusual acronym WCR is also introduced.

12

A Roadmap to Orthogonality of Term Rewriting Systems

Salvador Lucasa TRS is called non-ambiguous if for all (variable disjoint) left-hand sides ` and `0of rules and non-variable position p ∈ PosF (`), `|p and `0 do not unify.
In [12, page 5, paragraph 2] they remark that this corresponds to TRSs without critical pairs.
Klop (1980): Regular Combinatory Reduction Systems. In his 1980 PhD Thesis,
Klop investigated Combinatory Reduction Systems (CRSs), which properly include TRSs (in[16, Remark II.1.17], he cites [13] referring to the notion of TRS). When restricted to TRSs,
his definition ofregular CRS [16, Definition II.1.16] as a left-linear and non-ambiguous CRS
coincides with the current notion of orthogonality, see [17, Section 8].
Dershowitz (1981): Non-overlapping TRS.

Dershowitz defineda TRS as non-overlapping if no left-hand side ` overlaps a different left-hand side
`0 and no proper subterm of ` overlaps all of ` [8, last paragraph of page 449].
Here, a term t is said to overlap a term t0 if t0 can be unified with some (not necessarily proper)
subterm s of t. He also remarks that this condition is equivalent to R having no critical pairs(as Huet & Lévy’s non-ambiguity).
Dershowitz & Jouannaud (1990): Orthogonality. As suggested in the second paragraphof [15, Section 2], and kindly confirmed by Nachum Dershowitz [7],the word “orthogonal” was suggested by Dershowitz and Jouannaud and first introduced in [9, Section 7.2]
to avoid the cumbersome phrase ‘non-ambiguous and left-linear’ [17, Chapter 8]. However,Dershowitz and Jouannaud’s definition of an orthogonal TRS in [9, Section 7.2] corresponds towhat is called a weakly orthogonal TRS today. The current definition of (weakly) orthogonal
TRSs was fixed by Klop.
Klop (1990): (Weakly) Orthogonal TRSs. Klop argues that providing a clear distinction
between orthogonal and weakly orthogonal TRSs is important (see the footnote of [17, page67]). According to the footnote in [17, page 67], the current definition of orthogonal and weakly
orthogonal TRSs was first given in [17, Definition 8.1].
Definition 3 (Orthogonal TRS [17, Definition 8.1] & [15, Definition 3.1.1]). A TRS R is
orthogonal if R is left-linear and there are no critical pairs. R is weakly orthogonal if R isleft-linear and R contains only trivial critical pairs.
Such a definition is used in current books on term rewriting, e.g., [1, Definition 6.3.6 & page155], [21, Definition 4.3.4], and [24, Definitions 4.1.1 & 4.1.2].
Hanus (1994): Almost orthogonality. Item 4 of [21, Definition 4.3.4] corresponds to thenotion of almost orthogonality, which is missing in [1, 24] and provides an intermediate step
between orthogonality and weak orthogonality. In [11], Hanus gave the following definition ofan almost orthogonal TRS:

13

A Roadmap to Orthogonality of Term Rewriting Systems

Salvador Lucas

Definition 4 (Almost orthogonal TRS [11, page 669]). A TRS is almost orthogonal if all rules
are left-linear and for each pair of rules ` → r, `0 → r0 , nonvariable subterm `|p of `, and mgu
θ for `|p and `0 , p is the root position Λ and the terms θ(r) and θ(r0 ) are identical.
Some important properties of orthogonal TRSs are still valid for almost orthogonal TRSs
but not for weakly orthogonal TRSs. For instance, descendants of redexes in almost orthogonal
TRSs are still redexes, but this does not hold for weakly orthogonal TRSs [21, pager 54]. Almost
orthogonality is closely related to the notion of overlay critical pairs, which are those obtained
from overlaying rules: two (variable-disjoint) rules ` → r and `0 → r0 overlay if ` and `0 unify[21, Definition 4.3.3]. Thus, Ohlebusch’s book provides a complete picture of orthogonality.
Definition 5 (Orthogonality of TRSs [21, Definition 4.3.4]). A left-linear TRS R is orthogonal
if CP(R) = ∅; it is almost orthogonal if every critical pair in CP(R) originates from an overlayof rewrite rules of R and is trivial; it is weakly orthogonal if all CPs in CP(R) are trivial.

4

Conclusions

We have traced the development of the notion of orthogonality of TRSs, since the introductionof the central property of non-overlappingness, coined by O’Donnell in 1977, but already present
in previous works by Rosen (on closed and unequivocal subtree replacement systems) and Knuth& Bendix (introducing superposition of rewrite rules), to the name “orthogonality” suggested
by Dershowitz and Jouannaud in 1990 (also considering the notion of left-linearity used by Huet
and Lévy in 1979) and applied to TRSs in its usual form today by Klop, also in 1990.
Acknoledgments. I thank Nachum Dershowitz and Michael Hanus for kindly considering
my requests about terminological and historical aspects of orthogonality.

References[1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press,
1998.
[2] Walter S. Brainerd. Semi-thue systems and representations of trees. In 10th Annual Symposium on
Switching and Automata Theory, Waterloo, Ontario, Canada, October 15-17, 1969, pages 240–244.
IEEE Computer Society, 1969.
[3] Walter S. Brainerd. Tree generating regular systems. Inf. Control., 14(2):217–231, 1969.
[4] Walter Scott Brainerd. Tree Generating Generating Systems and Tree Automata. PhD thesis,
University of Purdue, 1967.
[5] Alonzo Church and J. B. Rosser. Some properties of conversion. Transactions of the American
Mathematical Society, 39(3):472–482, 1936.
[6] Haskell B. Curry and Robert Feys. CombinatoryLogic. North-Holland Publishing Company, 1958.
[7] Nachum Dershowitz. Personal communication, March 13, 2024.
[8] Nachum Dershowitz. Termination of linear rewriting systems (preliminary version). In Shimon
Even and Oded Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre
(Akko), Israel, July 13-17, 1981, Proceedings, volume 115 of Lecture Notes in Computer Science,
pages 448–458. Springer, 1981.
[9] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems. In Jan van Leeuwen, editor,
Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 243–320. Elsevier and MIT Press, 1990.

14

A Roadmap to Orthogonality of Term Rewriting Systems

Salvador Lucas[10] Saul Gorn. Explicit definitions and linguistic dominoes. In John F. Hart and Satoru Takasu,
editors, Systems and Computer Science Conference, pages 77–115. University of Western Ontario,
1965.
[11] Michael Hanus. On extra variables in (equational) logic programming. In Leon Sterling, editor,
Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming,
Tokyo, Japan, June 13-16, 1995, pages 665–679. MIT Press, 1995.
[12] Gérard Huet and Jean-Jacques Lévy. Call by need computations in non-ambiguous linear term
rewriting systems. Technical report, IRIA Rocquencourt, France, 1979. Rapport Laboria 359.
[13] Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting
systems. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode
Island, USA, 31 October - 1 November 1977, pages 30–45. IEEE Computer Society, 1977.
[14] Gérard P. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting
Systems. J. ACM, 27(4):797–821, 1980.
[15] J. W. Klop. Chapter 1: Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaurn,
editors, Handbook of Logic in Computer Science, pages 1–116. Oxford University Press, 1992.
[16] Jan Willem Klop. Combinatory Reduction Systems, PhD Thesis. PhD thesis, University of Utrecht.
ILLC Historical Dissertation (HDS) Series, HDS-33, 2022.
[17] Jan Willem Klop. Term rewriting systems. Technical report, Centrum voor Wiskunde en Informatica, CWI, 1990. Report CS-R9073.
[18] Donald E. Knuth and Peter E. Bendix. Simple Word Problems in Universal Algebra. In J. Leech,
editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
[19] M. H. A. Newman. On Theories with a Combinatorial Definition of ”Equivalence”. Annals of
Mathematics, 43(2):pp. 223–243, 1942.
[20] Michael J. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes
in Computer Science. Springer, 1977.
[21] Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002.
[22] Barry K. Rosen. Tree-manipulating systems and church-rosser theorems. In Patrick C. Fischer,
Robert Fabian, Jeffrey D. Ullman, and Richard M. Karp, editors, Proceedings of the 2nd Annual
ACM Symposium on Theory of Computing, May 4-6, 1970, Northampton, Massachusetts, USA,pages 117–127. ACM, 1970.
[23] Barry K. Rosen. Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM, 20(1):160–
187, 1973.
[24] Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science.
Cambridge University Press, 2003.

15

The problem of the calissons, by rewriting∗Vincent van Oostrom
University of Sussex, School of Engineering and Informatics, Brighton, UK
Vincent.van-Oostrom@sussex.ac.uk
Abstract
We show each of four confluence techniques: random descent, proof orders for decreasing
diagrams, bricklaying, and local undercutting, serves to solve the problem of the calissons.

Introduction The problem of the calissons as presented in [2] is to show that if a box, aregular hexagonal, can be filled with calissons, so named after certain diamond-shaped sweets,then in the resulting filled box the numbers of calissons in each of their 3 orientations are thesame; in a formula r = g = b for r, g and b the numbers of red, green and blue1 calissons in
the box. For instance, for a box B with sides of length 2, there are 4 calissons for each of thecalisson in 3 orientations

hexagonal box B

filled B-box B1

filled B-box B2

Figure 1: The Problem of the Calissons
3 orientations in both the filled B-boxes B1 and B2 in Figure 1; ri = g i = bi = 4 for i ∈ {1, 2}.
The problem has received quite some attention since; the paper [2] currently has ≈150
citations. We refer the reader to that literature for descriptions, solutions, generalisations,applications and other discussions. The sole purpose here is to offer a rewriting perspective on
the problem. We present four solutions, each based on a confluence technique.
Instead of requiring boxes to be equiangular hexagons that are also equilateral we relax thelatter requirement to being zonogonal, i.e. to only having opposite sides of the same length. We
show that if such a box is filled, then for each of their 3 orientations the number of calissons isalways the same; if B1 and B2 fill the same box B, then r1 = r2 , g 1 = g 2 and b1 = b2 . Thissolves the original problem of the calissons since if B is equilateral, is a regular hexagon, the 3numbers of calissons must in fact be the same as seen by rotational symmetry.
Looking at the filled boxes B1 and B2 in Figure 1 it’s almost impossible not to see them as
different stackings of small cubes inside a large cube. From that three-dimensional perspective,
the generalisation considered here corresponds to stacking small cubes inside a large (rectangular) cuboid. That perspective suggests the number of calissons of a given orientation, is the
product of the lengths of the sides of the hexagon parallel to the sides of calissons of thatorientation; since B in Figure 1 ‘is’ a cube with sides of length 2, the number of calissons ofeach type is 2 × 2 = 4 as indeed is the case for B1 and B2 in the figure.
∗ This note is under the Creative Commons Attribution 4.0 International License L M.

1 We assign colours to the orientations for convenient referencing and reasons of aesthetics.

16

The problem of the calissons, by rewriting

⇒4

back

up

⇒

V. van Oostrom

⇒3
⇒

⇒
⇒

left

⇒

front

calissons as ⇒-rules

right

down

⇒4
⇒3

⇒6

⇒2

⇒5

⇒1

⇒7

⇒

⇒6

⇒2

⇒5

⇒1

⇒7

⇒8

⇒9
⇒8

filling by a blue calisson; a ⇒-stepfilling ⇒⇒ and edge-names

Figure 2: Solving the problem of the calissons by random descent
Random descent In the first approach to the problem by rewriting we view each calisson
as a rewrite rule ⇒ used to transform the left leg up–left–front of the box into its right leg
back–right–down, see Figure 2. A filling is a ⇒-reduction gradually transforming the path fromthe bullet • at the top to the • at the bottom of the box, into the dashed path, in the figure:
Definition 1. Filling ⇒ is the string rewrite system (SRS) over the alphabet {edges and rewrite rules
⇒
,
⇒
,
⇒
.

,

,

} of

A possible filling F1 fromtois ⇒⇒⇒⇒⇒⇒⇒⇒⇒⇒⇒⇒;
it corresponds to the filled box B1 above. Other fillings for the same filled box B1 are possible,
but does any filled box B have some filling? Any partial filling F of B ends in a path P allowing
a filling step. If none of them would yield a partial filling of B again, then there could not be
any occurrence ofin P by the assumptions. Moreover, a rightmost occurrence ofin
P would then be filled in B by a pair of green,blue calissons and to the right of the blue one only
other such could occur, giving a contradiction (to B being a filled box). Analogous reasoning
pertains to a leftmost occurrence ofin P , showing there’s always some way to let filling
make progress toward B. For instance, Figure 2 depicts that after the first 8 filling steps of F1 ,progress toward B1 is made by the further ⇒-step (not by the, also possible, ⇒-step!).
Having established adequacy of the modelling, the problem of the calissons resurfaces as aquantitative confluence question:
Does random descent hold for measure ⇒ 7→ (1, 0, 0), ⇒ 7→ (0, 1, 0), ⇒ 7→ (0, 0, 1)?
Recall [9, 10, 13, 11] that a rewrite system having random descent (RD) means that for any
object that is normalising, rewrites to a normal form, we have (i) maximally rewriting the former
always ends in the latter, and (ii) that all such rewrite sequences have the same measure.
In this case, filling ⇒ is seen to be normalising (WN) for the same reason that sorting is; the⇒-rules simply sort edges into red–green–blue order, cf. [10, Example 7], showing that filling
does result in a filled box.
Also RD is easily seen to hold: Because the (only) critical peak⇐⇒is joinable as⇒⇒⇐⇐
and both legs
have measure (1, 1, 1), ordered local confluence (OWCR) holds entailing RD by [13, Lem. 24].
Finally, to see that by having answered the quantitative confluence question in the affirmative we have solved the problem of the calissons, note that the measure given counts therespective numbers of red, green and blue steps while filling. Hence the triple of numbers ofred, green and blue of calissons in a filled box, its spectrum [4], is the measure of its filling.
Indeed, the measure (4, 4, 4) of the filling F1 is the same as the spectrum of the filled box B1 .

17

The problem of the calissons, by rewriting

V. van Oostrom

2
Pr
3

Pb
P

2

4

3

2

2

2

Pg
2

Figure 3: Volume of path P as areas of 3 projections Pr , Pg , Pb (by ‘forgetting’ colours)
Proof orders for decreasing diagrams Above we proceeded by (weak) normalisation (WN)
and ordered local confluence (OWCR). Here we proceed instead by termination (SN) and local
confluence (WCR) of filling ⇒, as suggested by WN & OWCR ⇐⇒ SN & WCR [11].
Since the single critical peak of ⇒ was shown to be joinable already, yielding WCR, itsuffices to show termination of ⇒ by a measure from which the numbers of calissons can be
retrieved. To realise the idea that was given at the bottom of the first page we make use of thearea measure on conversions, introduced for measuring decreasing diagrams in [5, Example 3].
Definition 2. The area measure of a conversion comprising ℓ forward and r backward steps,
is a triple (ℓ, a, r) measuring how many square tiles a are needed to complete the conversion
into a valley. The volume of a path P is the triple (r, g, b) of area measures of the conversions
Pr , Pg and Pb obtained from P by forgetting respectively the red, green and blue edges.
Referring the reader to [5, Example 3] for formal details, we illustrate the definition bymeans of the path P given by
as depicted in Figure 3. Then Pr is theconversion →←→→← obtained by forgetting the-edges in P and orienting the- and-edges in opposite directions, yielding area (3, 2, 2), Pg is the conversion ←→→← having
area (2, 2, 2) and Pb the conversion ←→←←→ with area (3, 4, 2).
We claim that if V is the volume (r, g, b) of the initial path P of a filling F of box B, thenthe spectrum of the box is the triple V 2 of second components of V . For instance, the volume of
the initial path for box B in Figure 1 is ((2, 4, 2), (2, 4, 2), (2, 4, 2)), and indeed its triple (4, 4, 4)of second components is the spectrum of B comprising 4 calissons of each colour.
To prove the claim we prove the property that for any filling step of a given colour only
the second component of that colour is decremented in the volume, with the areas of the othercolours being unchanged. This suffices, since for a filling yielding a filled box, the volume ofits final path Q has second components that are all 0, since ‘forgetting’ then yields valleys:
Qr has shape ↠↞, Qg has shape ↠↞ and Qb shape ↠↞. To see the property holds observethat a filling step of a given colour swaps adjacent edges of the other colours, so leaves theareas of those other colours unchanged, but decrements that of the given colour. Indeed,
the filling ⇒-step in Figure 2 transforms
intoand volume((2, 1, 2), (2, 1, 2), (2, 2, 2)) into ((2, 1, 2), (2, 1, 2), (2, 1, 2)), decrementing (only) the blue area.

18

The problem of the calissons, by rewriting

V. van Oostrom

bricklaying rule (snapped to triangular grid)

bricklaying step

⇛

v′

⇛

v

brick bed search

Figure 4: Solving the problem of the calissons by bricklaying
Bricklaying For the third approach to the problem of the calissons by rewriting we change
the modelling; filled boxes are now the objects of a rewrite system ⇛ having bricklaying as
rule [12] displayed on the left in Figure 4, allowing to locally rearrange the calissons in a box.
1√  1√ 

3
3−
Definition 3. Linear combinations rr 2− 1 + rg 10 + rb −2 1give the grid of vertices for22

natural number scalars rr , rg , rb , a box when restricting them to real intervals [0, w], [0, h], [0, d]
for natural number width w, height h, depth d, and calissons when further restricting twoamong w, h, d to 1 and the other (its colour ) to 0; reversing this yields edges. Box, diamondand edge occurrences arise by translation. We suppress writing ‘occurrence’. A family
DI ofS
diamonds is a tiling (of a box B) if Di ∩ Dj is a subset of some edge for i ̸= j (and DI ⊆ B).
W.l.o.g. we analyse
only the discrete problem where calissons occur at vertices, B at theS
origin, and B = DI . By the spectrum obviously being invariant under ⇛, the problem of thecalissons resurfaces as the confluence / uniqueness of normal form question:
S
S
Does DI = B = DJ′ for box B, entail DI , DJ′ have the same ⇛-normal form?

Mapping calissons to their vertices and (coloured) edges, turns tilings into bed-graphs [12]: (i)every green tile is a tetragonal cycle of shape ←←→→ and similarly for red and blue tiles; (ii)vertices have at most a single in-/out-edge of a given colour; (iii) there are no paths having
edges of each of the 3 colours; (iv) every path →→ belongs to some tile and similarly for othercolour-pairs; (v) if ← a → does not belong to a tile then a has a green in-edge and similarly forother colour-triples. Taking edges as vectors in the 3 colour-dimensions
∞ shows tilings even are
beds [12], i.e. are plane bed-graphs under projection from viewpoint ∞ , as used in illustrations.
∞
Let an i-peak for such a tiling DI be a vertex in B having exactly i out-edges. Then 0 ≤ i ≤ 3
by there being 3 colours, and we distinguish cases on whether or not there are 3-peaks:
If there are 3-peaks, then the bricklaying ⇛-rule is applicable to at at least one of them.
This holds for any bed [12] as depicted in Figure 4: If v is a 3-peak but ⇛ does not apply, thenby (v) it has an in-edge of colour c from v ′ , which is a 3-peak by (iv) and its in-edge, if any, hascolour c by (iii) from which we conclude by finiteness of tilings / monochrome paths in beds.
If there are no 3-peaks, then we have one large brick [12] generalising that in the rhs of the⇛-rule in Figure 4. That is, at the top we must have a big green calisson composed of smaller
such and mutatis mutandis the same for blue / red at the bottom–left / right. This holds infact for any bed: Any ←→-peak then must belong to a green tile since otherwise (v) and theabove reasoning would give rise to a 3-peak contradicting the assumption. The big red, green,
blue calissons share boundary paths and these 3 rays end up in the same nexus, the common
reduct; this holds by monochrome paths being finite and (iii), with the former a consequenceof the bed-graph being plane. We conclude by noting the 3 big calissons only depend on B.

19

The problem of the calissons, by rewriting

V. van Oostrom

·
⇒4
⇒3
Φ

Ψ

⇒2
⇒1

⇓1
⇒11

⇒6
⇒5

⇒10
⇒9

⇒7
⇒8

→ := → ∪ → ∪ →⇓2filling Φ ⇒
⇒Ψ

⇒12

iff

⇓3
⇓4

⇓5

⇓7

⇓6

⇓8

⇓10

⇓12

⇓9

(not showing 6
trivial ⇓-steps)⇓11

projection Φ−1 · Ψ ⇓⇓εFigure 5: Solving the problem of the calissons by local undercutting; filling iff projection
Local undercutting Our fourth approach to the problem of the calissons by rewriting, inspired by [3, Proposition 4.16(4.18)], mixes the above modellings: We again view the grid for abox B as a rewrite system → := → ∪ → ∪ → but with green →-steps now oriented downward as
displayed on the left in Figure 5. Calissons now are diamonds χϕ ⋄ψυ inducing filling ϕ · χ ⇒ ψ · υ
respectively projection ϕ−1 · ψ ⇓ χ · υ −1 rules. Filling is modelled as Φ ⇒⇒ Ψ for left,right legsΦ, Ψ of B, and we claim it holds iff projecting Φ, Ψ is empty, i.e. iff Φ−1 · Ψ ⇓⇓ ε with the spectraof filling and projection the same, from which we conclude as the spectrum of projection only
depends on B, as seen before. Here we use Υ, Φ, X, Ψ, . . . to range over conversions, elementsof the free (typed) involutive monoid over →-steps υ, ϕ, χ, ψ, . . ., with · denoting compositionand −1 reverse; conversions are (possibly empty; ε) compositions of steps and reverse steps [5].
Definition 4. A local undercutting 2 (LUC) is a collection of diamonds D consisting of for every
ϕ ϕ
local peak ϕ−1 · ψ at most one diamond of shape Xϕ ⋄ψΥ for reductions X, Υ such that: ε ⋄ε ∈ D,
and (ϕ · X)−1 · ψ · Υ ⇓⇓ ε if ϕ−1 · χ · χ−1 · ψ ⇓⇓ X · Υ−1 . D is spectrum-preserving if the spectraof the latter two projections are the same (they are unique by random descent [10] of ⇓).

Calissons induce a spectrum-preserving LUC after adjoining ϕε ⋄ϕε ; per definition of → the only
non-trivial case is (←·→·←·→) ⇓3 (→·→·←·←) for which we indeed have (←·←·←·→·→·→) ⇓6ε, and both projections have spectrum (1, 1, 1). To prove the claim, it suffices that filling iff
projection for spectrum-preserving LUCs, cf. Figure 5 right. To enable proving it by inductions,
we rephrase filling using the notion of foliage 3 imaged on the left in Figure 6: a cyclic conversion
Z = Z1 · . . . · Zn of length n, together with reductions Ξi for 0 ≤ i ≤ n with Ξ0 = ε = Ξn , andfillings Ξi−1 ⇒⇒ Zi · Ξi if Zi is a step and Zi−1 · Ξi−1 ⇒⇒ Ξi if Zi is a reverse step.

Theorem 1. If → is terminating and D LUC, then there is a foliage for conversion Z iff Z ⇓⇓ ε.
If D moreover is spectrum-preserving then the foliage and the projection have the same spectra.
See the appendix for a proof. Here we conclude by observing a filling Φ ⇒⇒ Ψ for left,rightlegs Φ, Ψ of a box B gives rise to a foliage for Φ−1 · Ψ with the same spectrum, and vice versa.

Remark. The diagrammatic perspective originates with Newman’s II-Lemma [9, Section 6]:
If → is terminating, there is a diamond in D for every local peak, and J K is a typed involutive
monoid homomorphism to a typed group mapping diamonds in D to 0, then J K maps every
conversion cycle to 0. Proof. For any conversion Z there is a valley X·Υ−1 with JZK = JX·Υ−1 K,by enriching Newman’s Lemma with that J K maps diamonds in D to 0. Hence if Z is a conversion
cycle, say on a, then JΦ−1 · Z · ΦK = JεK for Φ a reduction from a to normal form, so JZK = 0.2
What Newman’s Lemma is to the Critical Peak Lemma [6, Lemma 2.4] is Newman’s II-Lemma
to Squier’s Finite Derivation Type method [14, 1]; it ought to be better-known.
2 It expresses cut-elimination (transitivity-elimination) replacing two diamonds by a single one under them.
3 Originally introduced for proving [12, Theorem 4].

20

The problem of the calissons, by rewriting

V. van Oostrom

Z

S

⇒ ⇒
⇒ ⇒
⇒
⇒
⇒ ⇒
Ξ Ξ′ Ξ′′DI = O =S

DJ′Figure 6: foliage (left), non-fillable box (middle), non-convex non-⇛-convertible (right)
Conclusion This note illustrates the power of modern confluence techniques: The first threeprovided solutions out of the box. The fourth, inspired by [3, Proposition 4.16(4.18)], is novel.
The equiangular hexagonal B in the middle in Figure 6 is not zonogonal;
S filling gets
S stuck.
Still, as shown on the right, the spectra of both tilings DI , DJ′ of B for DI = O = DJ′ (atriangle is ‘missing’) are the same [4]. We leave it to future research to investigate whether thetechniques presented here can be appropriately adapted (we expect the first and fourth can).
Acknowledgment. Jan Willem Klop brought the problem of the calissons, it being amenable
to rewrite techniques, and ‘piling = tiling’ (Theorem 1, cf. [7][15, Chapter 8]) to my attention.

References[1] D. Ara, A. Burroni, Y. Guiraud, P. Malbos, F. Métayer, and S. Mimram. Polygraphs: From
rewriting to higher categories, 2023. doi:10.48550/arXiv.2312.00429.
[2] G. David and C. Tomei. The problem of the calissons. The American Mathematical Monthly,
96(5):429–431, 1989. doi:10.1080/00029890.1989.11972212.
[3] P. Dehornoy and alii. Foundations of Garside Theory. EMS, 2015. doi:10.4171/139.
[4] E.W. Dijkstra. On the problem of the calissons. Technical Report 1055, University of Texas, 1989.
URL: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1055.html.
[5] B. Felgenhauer and V. van Oostrom. Proof orders for decreasing diagrams. In RTA, volume 21 of
LIPIcs, pages 174–189, 2013. doi:10.4230/LIPIcs.RTA.2013.174.
[6] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems.
Journal of the ACM, 27(4):797–821, October 1980. doi:10.1145/322217.322230.
[7] J.W. Klop, V. van Oostrom, and R.C. de Vrijer. Course notes on braids, 1998. URL: http://www.javakade.nl/research/pdf/braids.pdf.
[8] J.-J. Lévy. Réductions correctes et optimales dans le λ-calcul. Thèse de doctorat d’état, Université
Paris VII, 1978. URL: http://pauillac.inria.fr/~levy/pubs/78phd.pdf.
[9] M.H.A. Newman. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics, 43:223–243, 1942. doi:10.2307/2269299.
[10] V. van Oostrom. Random descent. In RTA, volume 4533 of Lecture Notes in Computer Science,
pages 314–328, 2007. doi:10.1007/978-3-540-73449-9_24.
[11] V. van Oostrom. Uniform completeness. In 11th IWC, pages 19–24, 2022. URL: http://cl-informatik.uibk.ac.at/iwc/2022/proceedings.pdf.
[12] V. van Oostrom. Residuation = skolemised confluence. In 12th IWC, pages 20–25, 2023. URL:
http://cl-informatik.uibk.ac.at/iwc/2023/proceedings.pdf.
[13] V. van Oostrom and Y. Toyama. Normalisation by Random Descent. In FSCD, volume 52 of
LIPIcs, pages 32:1–32:18, 2016. doi:10.4230/LIPIcs.FSCD.2016.32.
[14] C.C. Squier, F. Otto, and Y. Kobayashi. A finiteness condition for rewriting systems. TheoreticalComputer Science, 131(2):271–294, 1994. doi:10.1016/0304-3975(94)90175-9.
[15] Terese. Term Rewriting Systems. Cambridge University Press, 2003.

21

The problem of the calissons, by rewriting

V. van Oostrom

Appendix In the proof of Theorem 1 we measure a foliage for conversion Z by the multisetof pairs where the ith object a (height) of Z is paired with the number of ⇒-root-steps in
Zi−1 · Ξi−1 ⇒⇒ Ξi ⇒⇒ Zi+1 · Ξi+1 if a is the apex of a local peak and 0 otherwise (width). The
multiset extension of the lexicographic product of ←+ and < well-foundedly orders measures.
Proof of Theorem 1. We prove the if-direction by induction on the number of steps p in Z ⇓p ε,
cf. [12, Theorem 4]. If p = 0, we trivially conclude as Z = ε. Otherwise, for some Xϕ ⋄ψΥ we have
Z = Z l · ϕ−1 · ψ · Z r and Z ⇓ Z ′ and Z ′ ⇓p−1 ε for Z ′ = Z l · X · Υ−1 · Z r . By the IH there
is a foliage for Z ′ (with spectrum that of Z ′ ⇓p−1 ε); its subconversions Z l , Z r combined withprefixing ϕ to the last reduction of Z l then give a foliage for Z (with spectrum that of Z ⇓p ε).
We prove the only–if-direction by induction on the measure of the foliage for Z and cases
on Z. If Z is a valley, then by definition of foliage Z = ε using that the legs of diamonds in
D are non-empty, and we conclude. Otherwise, Z has shape Z ℓ · ϕ−1 · ψ · Z r with ϕ · Ξi−1 ⇒⇒Ξi ⇒⇒ ψ · Ξi+1 and we distinguish cases on the width w of the apex of the local peak.
If w = 0 then ϕ = ψ and Ξi−1 ⇒⇒ Ξi+1 . Then Z ⇓ Z ′ for Z ′ := Z ℓ · Z r by LUC. Replacing4
Ξi−1 by Ξi+1 in the foliage for Z ℓ renders Z ′ a foliage. We conclude by the IH for Z ′ .
If w = 1 then ϕ · Ξi−1 ⇒⇒ ϕ · X · Ξ′ ⇒ ψ · Υ · Ξ′ ⇒⇒ ψ · Ξi+1 for some diamond Xϕ ⋄ψΥ ∈ D and′some Ξ , where the displayed ⇒⇒ do not have head-steps. Then Z ⇓ Z ′ for Z ′ := Z ℓ ·X ·Υ−1 ·Z r .
Replacing (cf. footnote 4) Ξi−1 by X · Ξ′ in the foliage for Z ℓ and replacing Ξi+1 by Υ · Ξ′ inthe foliage for Z r , renders Z ′ a foliage again. We conclude by the IH for Z ′ .
If w > 1 then ϕ · Ξi−1 ⇒⇒ ϕ · Φ · Ξ′ ⇒ χ · Ψ · Ξ′ ⇒⇒ χ · X · Ξ′′ ⇒ ψ ′ · Υ · Ξ′′ ⇒⇒ ψ · Ξi+1 for someϕ χ χ ψ′′′′diamonds Φ ⋄Ψ , X ⋄Υ ∈ D and some Ξ , Ξ , where the first two displayed horizontal reductions
do not have head-steps (we may but need not have ψ ′ = ψ). The second induces a foliage forthe peak (Ψ · Ξ′ )−1 · X · Ξ′′ to which the IH applies (by its apex being reached via χ), yielding⇓ ε. By random descent for ⇓, this projection factors as Ψ−1 · X· ⇓⇓ X ′ · Ψ′−1
(Ψ · Ξ′ )−1 · X · Ξ′′ ⇓⇓ ε for some reductions X ′ , Ψ′ .
and Ξ′−1 · X ′ · Ψ′−1 · Ξ′′ ⇓The former ⇓⇓ combined with two ⇓-steps for the diamonds gives ϕ−1 · χ · χ−1 · ψ ′ ⇓⇓ Φ · X′ ·
′ −1
′ −1
′ ⇓
(Υ · Ψ ) for which LUC entails (ϕ · Φ · X ) · ψ · Υ · Ψ ⇓ ε. The if-direction then yields afoliage for it, so ϕ · Φ · X ′ ⇒⇒ ψ · Υ · Ψ′ having exactly 1 head-step (by a diamond for ϕ, ψ).
For the latter ⇓⇓ the if-direction yields a foliage so Ξ′ ⇒⇒ X ′ · Ξ̂ and Ψ′ · Ξ̂ ⇒⇒ Ξ′′ for some Ξ̂.
′′′′Combining both shows that ϕ · Φ · Ξ ⇒⇒ ψ · Υ · Ξ using a single head-step, instead of thetwo before. Hence we conclude by the IH for the same Z but with this alternative foliage.
ψ ϕDefinition 5. local semi-lattice (LSL) is LUC with commutativity of D: Φϕ ⋄ψΨ ∈ D iff Ψ ⋄Φ ∈ D.

Observe that to establish LUC it suffices to consider triples ϕ, ψ, χ where ϕ ̸= χ ̸= ψ sinceif, say, ϕ = χ then the assumption simplifies to ϕ−1 · ψ ⇓⇓ X · Υ−1 , which is seen to entail−1⇓
the conclusion (ϕ · X) · ψ · Υ ⇓ ε using that peaks between a step and itself were assumed
trivial. LSL allows to also assume ϕ ̸= ψ, since if ϕ = ψ then ϕ−1 · χ · χ−1 · ϕ ⇓⇓ X · Υ−1 entails
ϕ χ χ ϕ−1⇓
X = Φ = Υ for Φ ⋄Ψ , Ψ ⋄Φ ∈ D so (ϕ · X) · ϕ · Υ ⇓ ε, using trivial peaks have trivial diamonds.
This resumes our attempts [7][15, Chapter 8] at a theory of orthogonality for rewriting andalgebra: LSL holds for the λβ-calculus [8] (local cube) and for positive braids [3, Example 4.20].
Though neither →β nor braids (Artin’s σi ) are terminating, that can be brought about (byfiniteness of family developments [15] respectively right-Noetherianity [3]) making Theorem 1
applicable. From a rewriting / order perspective Theorem 1 aims at showing that permutationequivalence = projection equivalence [15] / reductions constitute a semi-lattice [8] (whence LSL).
Contrapositively, it enables showing reductions do not have a common reduct (no upperbound )by showing projection of their peak does not terminate (no least upperbound) [3, Example 4.28].
4 If Z ℓ = ε replacing is not allowed but not needed: then Ξ22

i−1 = ε = Ξi+1 as legs of diamonds are non-ε.

A Roadmap to Orthogonality of Conditional Term
Rewriting Systems∗
Salvador Lucas
DSIC & VRAIN, Universitat Politècnica de València, Spainslucas@dsic.upv.es
Abstract
There are different definitions of orthogonality of conditional term rewriting systems.
This paper collects concepts, denominations, notions, and notations which have been important in their development, together with the main works that introduced them.
Intelligence, give me the exact name of things! (Juan Ramón Jiménez)

1

Motivation

A Term Rewriting System (TRS) is orthogonal if it is (i) left-linear and (ii) non-overlapping(or non-ambiguous), i.e., it has no critical pairs [11, Definition 3.1.1]. When orthogonality
is ported to Conditional Term Rewriting Systems (CTRSs) R, consisting of conditional rules
α : ` → r ⇐ c for terms ` and r and conditions c, some particularities and difficulties arise:
1. The conditional part c of conditional rules α may have different shapes and interpretations.

2. Rewriting steps σ(`) → σ(r) for some substitution σ require that the instance σ(c) of theconditional part c of the rule “holds”. It is possible, though, that no substitution satisfies
c, i.e., c is infeasible and the rule useless. However (in)feasibility is undecidable, in general.
3. Left-linearity is always required, but non-ovelappingness (ii) is required in different ways:(ii.1) by a direct definition of overlap without referring conditional critical pairs [13]; (ii.2)
referred to orthogonality of the unconditional part Ru of R [2]; (ii.3) mimicking Klop’s
definition of orthogonality on the basis of the notion of conditional critical pair [18, 14];
(ii.4) as in (ii.3), but considering feasible conditional critical pairs only [4, 17, 19].
4. Orthogonality as a purely syntactic criterion for confluence fails to hold with CTRSs.
Concepts and results addressing such problems often came first. Later on, appropriate denominations were found and became stable and widely used. We briefly discuss this process.

2

Orthogonality of Conditional Term Rewriting Systems

A CTRS R consists of conditional rules ` → r ⇐ s1 ≈ t1 , . . . , sn ≈ tn , where conditions si ≈ ti
may have different evaluation semantics (join, oriented, semi-equational, etc. [11, Definition
4.0.2] and [14, Definition 7.1.3]). Rules are often classified according to the distribution ofvariables [12, Definition 6.1]: type 1, if Var(r) ∪ Var(c) ⊆ Var(`); type 2, if Var(r) ⊆ Var(`);
type 3, if Var(r) ⊆ Var(`) ∪ Var(c); and type 4, otherwise. A rule of type n is often called ann-rule. A CTRS R is called an n-CTRS if all its rules are of type n; if R contains at least one
n-rule which is not an m-rule for some m < n, then we say that R is a proper n-CTRS.
∗ Partially
supportedby
MCIN/AEI
project
PID2021-122830OB-C42
fundedby
MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe” and by the grant
CIPROM/2022/6 funded by Generalitat Valenciana.

23

A Roadmap to Orthogonality of Conditional Term Rewriting Systems

Salvador LucasO’Donnell (1977): Non-overlapping and consistent generalized CTRSs. Regarding
conditional rewriting systems, O’Donnell pioneered the analysis of confluence of Rule Schemata[13, Definition 45], which generalize Rosen’s Rule Schemata [16], and can be viewed as sets R
of conditional, left-linear rules ` → r ⇐ P (x1 , . . . , xn ), for terms ` and r and a predicate P ,where all variables in r and x1 , . . . , xn already occur in ` (only 1-rules are allowed).
Remark 1 (Generalized CTRSs). In [11, Definition 4.0.2(4)], O’Donnell’s rules were slightly
generalized1 to ` → r ⇐ P1 (x1 , . . . , xm ), . . . , Pn (x1 , . . . , xm ) with several predicates P1 , . . . , Pn
and variables x1 , . . . , xm which do not need to occur in `. Sets of such rules are called Generalized CTRSs. We often use this denomination for O’Donnell systems as well.
In [13, Definition 48], O’Donnell called non-overlapping to rule schemata such that, for all
instances σ(`) and σ(`0 ) of the left-hand sides ` and `0 of rules α : ` → r ⇐ P (x1 , . . . , xm )and α0 : `0 → r0 ⇐ P 0 (x01 , . . . , x0n ), and all nonempty positions p 6= Λ, if σ(`)|p = σ(`0 ) forsome substitution σ, then (NOv.1) p = q.p0 for some q ∈ PosX (`), e.g., `|q = xi for somevariable xi , 1 ≤ i ≤ m, and (NOv.2) P (σ(x1 ), . . . , σ(xi )[σ(r0 )]p0 , . . . , σ(xm )) holds. Since thecase σ(`) = σ(`0 ) is not considered, non-overlapping rule schemata may include rules α and
α0 such that σ(`) = σ(`0 ) holds. This situation is handled through the notion of consistency.
A rule schemata is consistent if for all pairs of rule schemata ` → r ⇐ P (x1 , . . . , xm ) and`0 → r0 ⇐ P 0 (x01 , . . . , x0n ), if σ(`) = σ(`0 ) holds for some substitution σ, then r and r0 are
identical up to renaming [13, Definition 49]. As a consequence of [13, Theorems 17 and 6]:
Non-overlapping and consistent (generalized) rule schemata are confluent.
Note, however, that O’Donnell’s non-overlappingness does not admit a purely syntactic checking
due to (NOv.2). This was later addressed by Bergstra and Klop by imposing additional requirements on the shape and interpretation of the conditional part of rules.
Kaplan (1984): Conditional Critical Pairs for CTRSs. Kaplan introduced conditional
critical pairs2 to investigate confluence of CTRSs.
Definition 2 (Conditional critical pairs [9, 10, Definition 3.2]). Let R be a CTRS, α : ` → r ⇐ cand α0 : `0 → r0 ⇐ c0 be rules of R sharing no variable (rename if necessary), and p ∈ PosF (`)
be a nonvariable position of ` such that `|p and `0 unify with mgu θ. Then,hθ(`[r0 ]p ), θ(r)i ⇐ θ(c), θ(c0 )(1)is a conditional critical pair (CCP for short) of R, often denoted πα,p,α0 .
Kaplan distinguishes feasible and infeasible conditional critical pairs (roughly speaking a
CCP hs, ti ⇐ c is feasible if σ(c) holds for some substitution σ) and remarks that “whentesting confluence, only feasible (conditional) critical pairs are relevant” [9, above Definition
3.2]. Definition 2 is essentially reproduced in, e.g., [4, Definition 3] and [11, Definition 4.0.14(1)].
A CCP hs, ti ⇐ c is called trivial if s = t.
Bergstra and Klop (1986): Orthogonality of the unconditional part. In [2, Section3], Bergstra and Klop considered O’Donnell’s conditional systems R with rules ` → r ⇐P (x1 , . . . , xn ). However, they changed O’Donnell’s non-overlappingness by a combination of
1 Plaisted had already generalized O’Donnell’s rules allowing for arbitrary atoms and literals (i.e., negatedatoms) in the conditional part of rules [15]. However, he did not consider any orthogonality-like result.
2 He named them Contextual Critical Pairs.

24

A Roadmap to Orthogonality of Conditional Term Rewriting Systems

Salvador Lucas

two properties: (i) the unconditional part Ru = {` → r | ` → r ⇐ c ∈ R} of R [2, page 334,
item (ii)] must be of type 0, i.e., a left-linear and non-ambiguous (that is, orthogonal ) TRS [2,page 324]; and (ii) the conditions in rules of R are stable, according to the following:
Definition 3 (Stable condition [2, Definition 3.1]). Let R be a Generalized CTRS. A condition
P (x1 , . . . , xn ) is called stable if for all substitutions σ and 1 ≤ i ≤ n, if σ(xi ) →R t for someterm t and P (σ(x1 ), . . . , σ(xi ), . . . , σ(xn )) holds, then P (σ(x1 ), . . . , t, . . . , σ(xn )) holds.
Stability of conditions in rules, although undecidable, guarantees that (NOv.2) is fulfilled.
Requirement (i) above is more restrictive than (NOv.1) (as it forbids overlaps at the root of
lhs’s of rules, not forbidden by (NOv.1)), but implicates O’Donnell’s consistency as it forbids
the situation σ(`) = σ(`0 ) for (different) rules α : ` → r ⇐ P (x1 , . . . , xm ) and α0 : `0 → r0 ⇐P 0 (x01 , . . . , x0n ). On the basis of O’Donnell results, Bergstra and Klop conclude:
Generalized CTRSs R such that Ru is of type 0 (i.e., orthogonal) and all conditions
in rules are stable are confluent [2, Theorem 3.2].
Since the undecidable notion of stability is used, in order to obtain a purely syntactic criterion
for confluence, Bergstra and Klop considered 2-CTRSs R such that Ru is orthogonal and R
consists of rules α : ` → r ⇐ c with c of the form s1 ≈ t1 , . . . , sn ≈ tn for terms si , ti , 1 ≤ i ≤ n,and ≈ is given a fixed interpretation so that stability of c is guaranteed [2, Definition 2.1(i)]:• Type I CTRSs, where conditions s ≈ t ∈ c are interpreted as conversion statementss ↔∗ t (nowadays we call them semi-equational CTRSs).
• Type IIIn CTRSs, where for all conditions s ≈ t ∈ c, t is a ground Ru -irreducible termand ≈ is interpreted as reachability →∗ (nowadays we call them normal CTRSs).
[2, Corollary 3.3 and Theorem 3.5] prove confluence of CTRSs of type I and IIIn , respectively.
Dershowitz, Okada, and Sivakumar (1987): Non-overlappingness; overlays. In contrast to O’Donnell, [4] defines non-overlappingness using conditional critical pairs (1):A CTRS is non-overlapping if it has no feasible, non-trivial (conditional) criticalpairs [4, Definition 4].
If p = Λ in (1), then (1) is an overlay [4, Definition 8]. In contrast to [2], Dershowitz, Okada
and Sivakumar also considered 3-CTRSs whose rules may non-trivially overlay themselves.
Example 1. Consider the 3-CTRS R [4, Conclusion]:a →f(x) ⇐ p(x) ≈ ttp(b) →

tt

p(c) →

tt

The CCP hf(x), f(x0 )i ⇐ p(x) ≈ tt, p(x0 ) ≈ tt is feasible and not trivial. Thus, R is overlapping.
In contrast to [4, 9, 10], Avenhaus and Lorı́a-Sáenz distinguish proper and improper CCPs.
Definition 4 (Proper and improper CCPs [1, Def. 4.2]). Let R be a CTRS and πα,p,α0 be a
CCP of R. If α and α0 are renamed versions of the same rule and p = Λ, then πα,p,α0 is called
improper; otherwise, it is called proper.
However, no notion of (weak) orthogonality of CTRSs is given in [4] or [1].

25A Roadmap to Orthogonality of Conditional Term Rewriting Systems

Salvador Lucas

Klop (1992): (Weakly) Orthogonal 2-CTRSs. Klop adopted Dershowitz and Jouannaud’s term orthogonality [3, Section 7.2] to provide the current definition of (weakly) orthogonal TRSs [11, Definition 2.1.1]. He also adopted the notions of semi-equational and normal
CTRSs from [5] (among others). Following [2], Klop introduced the following.
Definition 5 ((Weakly) Orthogonal CTRS [11, Definition 4.0.5]). A CTRS (of any type:semi-equational, normal,. . . ) is (weakly) orthogonal if Ru is (weakly) orthogonal.
Definition 5 implicitly restricts (weak) orthogonality to 2-CTRSs, as Ru must be a TRS andthis is possible only if R is a 2-CTRS. Taking full power of O’Donnell’s results for Generalized
CTRSs, actually covering weakly orthogonal CTRSs, Klop establishes:
Weakly orthogonal semi-equational CTRSs are confluent [11, Corollary 4.0.8].
Weakly orthogonal normal CTRSs are confluent [11, Theorem 4.0.10].
Unfortunately, these results do not extend to other well-known evaluation modes for the conditions s ≈ t in rules (e.g., joinability, where s ≈ t is interpreted as joinability of terms s andt, written s ↓ t, or reachability, where s ≈ t is interpreted as reachability s →∗ t).3
Gramlich (1994): A more restrictive definition of conditional critical pair. In [7,Definition 2], Gramlich defines a notion of conditional critical pair for 2-CTRSs so that improperconditional critical pairs in Definition 4 are explicitly discarded. Such a more restricted notionof conditional critical pair can be found in Ohlebusch’s book for arbitrary CTRSs [14, Definition
7.1.8(1)].
Definition 6 (Conditional critical pair [7, Def. 2], [14, Def. 7.1.8(1)]). Let R be a CTRS,
α : ` → r ⇐ c and α0 : `0 → r0 ⇐ c0 be rules of R sharing no variable (rename if necessary),and p ∈ PosF (`) be a nonvariable position of ` such that `|p and `0 unify with mgu θ. We callhθ(`[r0 ]p ), θ(r)i ⇐ θ(c), θ(c0 )a conditional critical pair of R. If α and α0 are renamed versions of the same rule, we
do not consider the case p = Λ.
The important change with respect to Definition 4 is that improper CCPs are neglected.
Example 2. The (improper) CCP in Example 1 obtained from the root overlap of renamed
versions of the conditional rule is dimissed as a conditional critical pair by Definition 6.
Hanus (1994): Almost orthogonal CTRSs. Hanus’ definition of almost orthogonality of
CTRSs follows the definition style of [2], i.e., the property is referred to the unconditional part
Ru . Thus, it is also restricted to 2-CTRSs, although this is not explicit in [8]. A left-linear
TRS is almost orthogonal if for each pair of rules ` → r, `0 → r0 , nonvariable subterm `|p of `,and mgu θ for `|p and `0 , p is the root position Λ and θ(r) = θ(r0 ) [8, page 669].
Definition 7. A 2-CTRS is almost orthogonal if Ru is almost orthogonal [8, page 669].

3 Some authors include additional requirements regarding the conditions of rules to provide a more restrictive
notion of orthogonality of CTRSs deriving more “direct” confluence results, e.g., [6, Definition 10.9].

26

A Roadmap to Orthogonality of Conditional Term Rewriting Systems

Salvador Lucas

Suzuki, Middeldorp, and Ida (1995): Confluence of orthogonal 3-CTRSs. Although[19] defines orthogonality of CTRSs R as orthogonality of Ru , in [18], mimicking the usual
definition of orthogonality of TRSs (based on the absence of critical pairs), but using Definition
6, where only proper CCPs are considered, they provided the following.
Definition 8 (Orthogonality of CTRSs [18, page 3]). A left-linear CTRS without ( proper)
conditional critical pairs is called orthogonal.
Accordingly, R in Example 1 is orthogonal. They prove new results for oriented and join
CTRSs, where conditions s ≈ t are treated as reachability and joinability tests, respectively:
Orthogonal properly oriented right-stable 3-CTRSs are confluent [19, Cor. 4.7].
Orthogonal properly oriented right-stable join 3-CTRSs are confluent [19, Cor. 5.3].
Here, a 3-CTRS R is properly oriented if S
every rule ` → r ⇐ s1 ≈ t1 , . . . , sn ≈ tn satisfies: if
i−1
Var(r) 6⊆ Var(`), then Var(si ) ⊆ Var(`) ∪ j=1 Var(tj ) for all 1 ≤ i ≤ n [19, Definition 3.1]. A
CTRS is right-stableif for every rule ` → r ⇐ s1 ≈ t1 , . . . , sn ≈ tn ∈ R and for all 1 ≤ i ≤ n,Si−1(a) (Var(`) ∪ j=1 Var(sj ≈ tj ) ∪ Var(si )) ∩ Var(ti ) = ∅, and (b) ti is either a linear constructor
term or a ground Ru -irreducible term [19, Definition 3.6]. The authors claim that their results
apply to Hanus’ almost orthogonal 2-CTRSs as well [19, last paragraph of Section 6].
Suzuki, Middeldorp, and Ida (1995): Infeasible CCPs in orthogonal CTRSs. In[19, Section 7], the authors consider the possibility of discarding infeasible critical pairs which(as anticipated by Kaplan) would be excluded from the analysis of confluence of CTRSs. Theysay that orthogonality can be strengthened by allowing infeasible (conditional) critical pairs.
Ohlebusch (2002): Almost and weak orthogonality as the absence of proper CCPs.
Extending Definition 8, Ohlebusch provides the following.4
Definition 9 (Orthogonality of CTRSs [14, Definition 7.1.10]). Let R be a left-linear CTRS.
Then, R is orthogonal if it has no proper conditional critical pair; R is almost orthogonal ifevery proper conditional critical pair is a trivial overlay; R is weakly orthogonal if every properconditional critical pair is trivial.
Sternagel and Sternagel (2016): orthogonality modulo feasibility. Following [4, Definition 4] and [19, Section 7], Sternagel & Sternagel’s definition of (almost) orthogonality of(oriented) CTRSs modulo infeasibility restricts the attention to feasible (proper) conditional
critical pairs, thus making explicit the aforementioned idea of Suzuki, Middeldorp and Ida.
Definition 10 ([17, Definition 2]). A left-linear CTRS R is orthogonal (modulo infeasibility)
if for all pairs α : ` → r ⇐ c and α0 : `0 → r0 ⇐ c0 of (possibly renamed) variable disjoint rulesof R, and p ∈ PosF (`) such that πα,p,α0 exists, then πα,p,α0 is improper or infeasible.
Dershowitz et al.’s notion of non-overlapping CTRS, see above, anticipated this. Clearly,
orthogonality according to Definition 8 implies orthogonality modulo infeasibility.

4 In personal communication, Ohlebusch said that he origin of this definition is unclear.

27

A Roadmap to Orthogonality of Conditional Term Rewriting Systems

3

Salvador Lucas

Different notions of orthogonality of CTRSs

The previous definitions of orthogonality are not equivalent, in general, even for 1-CTRSs.
Example 3. Consider the oriented 1-CTRS R = {a → b ⇐ b ≈ c, a → b ⇐ b ≈ a, c → b}.
• By Definition 5, R is orthogonal, as Ru = {a → b, c → b} is.

• By Definition 8, R is not orthogonal: there is a CCP hb, bi ⇐ b ≈ c, b ≈ a.

• By Definition 10, R is orthogonal modulo infeasibility: the CCP is infeasible as b 6→∗R c.

Now, if a join semantics is assumed, then R is orthogonal according to Definition 5, but the
CCP is not infeasible, as b ↓ c and hence b ↓ a. Thus, R is not orthogonal modulo infeasibility.
Finally, note that Definitions 8 and 10 depend on the notion of CCP in Definition 6, whichcorrespond to proper CCPs in Definition 4. Do we obtain a different definition of (almost, weak)orthogonality if every CCP is considered? Since every rule ` → r ⇐ c induces an improper
CCP, no CTRS would be orthogonal. For instance, the 3-CTRS R in Example 1 would not
be orthogonal now. As for almost and weak orthogonality, all CCPs should be trivial. Givenvariable-disjoint rules α : ` → r ⇐ c and α0 : ` → r ⇐ c, if πα,p,α0 is trivial, then both α and α0
are 2-rules, i.e., only 2-CTRSs would be almost or weakly orthogonal. Since improper CCPs of
2-rules are trivial, nothing new is obtained regarding almost/weak orthogonality.

4

Conclusions

We have traced the development of the notion of orthogonality of CTRSs, generalizing the corresponding notion for TRSs. Since the early research by O’Donnell, generalizing Rosen’s work
for subtree replacement systems by considering conditional rule schemata, different notions havebeen proposed. Bergstra and Klop referred orthogonality of CTRSs R to that of the unconditional part Ru . Suzuki, Middeldorp, and Ida used (the absence of) proper CCPs as a suitabledefinition of orthogonality for left-linear CTRSs. Sternagel and Sternagel introduced orthogonality modulo infeasibility, exploiting an early observation by Kaplan (and then by Suzuki
et al.) about the harmlessness of infeasible CCPs regarding confluence of CTRSs. Example
3 shows that such notions do not coincide, even for 1-CTRSs, although that of Definition 8
implies that of Definition 10. The evaluation semantics of the conditions also matters.
Acknoledgments. I thank Nachum Dershowitz, Michael Hanus, and Enno Ohlebusch forkindly attending my requests about terminological and historical aspects of orthogonality. I
also thank Aart Middeldorp for providing access to [18]. Finally, I thank the reviewers for manysuggestions for (future) improvements.

References[1] Jürgen Avenhaus and Carlos Lorı́a-Sáenz. On Conditional Rewrite Systems with Extra Variables
and Deterministic Logic Programs. In Frank Pfenning, editor, Logic Programming and AutomatedReasoning, 5th International Conference, LPAR’94, Proceedings, volume 822 of Lecture Notes in
Computer Science, pages 215–229. Springer, 1994.
[2] Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. J.
Comput. Syst. Sci., 32(3):323–362, 1986.

28

A Roadmap to Orthogonality of Conditional Term Rewriting Systems

Salvador Lucas[3] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems. In Jan van Leeuwen, editor,
Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 243–320. Elsevier and MIT Press, 1990.
[4] Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of Conditional Rewrite
Systems. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop, Proceedings, volume 308 of Lecture Notes in Computer
Science, pages 31–44. Springer, 1987.
[5] Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Canonical conditional rewrite systems.
In Ewing L. Lusk and Ross A. Overbeek, editors, 9th International Conference on AutomatedDeduction, 1988, Proceedings, volume 310 of Lecture Notes in Computer Science, pages 538–549.
Springer, 1988.
[6] Nachum Dershowitz and David A. Plaisted. Rewriting. In John Alan Robinson and Andrei
Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 535–610. Elsevier and
MIT Press, 2001.
[7] Bernhard Gramlich. On termination and confluence of conditional rewrite systems. In Nachum
Dershowitz and Naomi Lindenstrauss, editors, Conditional and Typed Rewriting Systems, 4thInternational Workshop, CTRS-94, Notes in Computer Science, pages 166–185. Springer, 1994.
[8] Michael Hanus. On extra variables in (equational) logic programming. In Leon Sterling, editor,
Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming,
13-16, 1995, pages 665–679. MIT Press, 1995.
[9] Stéphane Kaplan. Fair conditional term rewriting systems: Unification, termination, and confluence. In Hans-Jörg Kreowski, editor, Recent Trends in Data Type Specification, 3rd Workshop on
Theory and Applications of Abstract Data Types, 1984, Selected Papers, volume 116 of InformatikFachberichte, pages 136–155. Springer, 1984.
[10] Stéphane Kaplan. Simplifying Conditional Term Rewriting Systems: Unification, Termination
and Confluence. J. Symb. Comput., 4(3):295–334, 1987.
[11] J. W. Klop. Chapter 1: Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaurn,
editors, Handbook of Logic in Computer Science, pages 1–116. Oxford University Press, 1992.
[12] Aart Middeldorp and Erik Hamoen. Completeness results for basic narrowing. Appl. Algebra Eng.
Commun. Comput., 5:213–253, 1994.
[13] Michael J. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes
in Computer Science. Springer, 1977.
[14] Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002.
[15] David A. Plaisted. A Logic for Conditional Term Rewriting Systems. In Stéphane Kaplan and JeanPierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop,
Proceedings, volume 308 of Lecture Notes in Computer Science, pages 212–227. Springer, 1987.
[16] Barry K. Rosen. Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM, 20(1):160–
187, 1973.
[17] Christian Sternagel and Thomas Sternagel. Certifying confluence of almost orthogonal ctrss via
exact tree automata completion. In Delia Kesner and Brigitte Pientka, editors, 1st International
Conference on Formal Structures for Computation and Deduction, FSCD 2016 Proceedings inInformatics (LIPIcs), pages 29:1–29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
[18] Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-Confluence of Conditional Rewrite Systems
with Extra Variables in Right-Hand Sides. 1995. revised version of [19], available: http://
cl-informatik.uibk.ac.at/users/ami/research/publications/proceedings/95rta.pdf.
[19] Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-Confluence of Conditional Rewrite Systems
with Extra Variables in Right-Hand Sides. In Jieh Hsiang, editor, Rewriting Techniques andApplications, 6th International Conference, RTA-95, Proceedings, volume 914 of Lecture Notes in
Computer Science, pages 179–193. Springer, 1995.

29

On Non-triviality of the Hierarchy of Decreasing
Church-Rosser Abstract Rewriting Systems
Ievgen Ivanov
Taras Shevchenko National University of Kyiv, Ukraine
ivanov.eugen@gmail.com
Abstract
We propose an answer to a question posed by J. Endrullis, J.W. Klop, and R. Overbeek
about the existence of a confluent abstract rewriting system (ARS) that does not belong to
the class DCR2 of confluent ARS for which confluence can be proved with the help of thedecreasing diagrams method using the label set {0, 1} ordered in such a way that 0 < 1.
We show that there exists an uncountable confluent ARS outside of the class DCR2
and provide a formal proof of a formalized version of this statement in Isabelle proof
assistant using HOL logic. We also show that the hierarchy of decreasing Church-Rosser
ARS introduced by J. Endrullis, J.W. Klop, R. Overbeek does not collapse at the level 2.

1Introduction

Perhaps the most widely known confluence criterion for abstract rewriting systems (ARS) is
Newman’s lemma [8, 4], which, in modern reformulations, establishes the equivalence between
the confluence and the local confluence property for terminating ARS. An obvious limitation ofthis lemma is the termination assumption. A frequently cited example of an acyclic, inductive,
locally confluent, but not confluent relation due to Newman [4, Figure 6a] (Newman’s counterexample) and an example of a finite, locally confluent, but not confluent relation with cycles
due to Hindley [4, Figure 6b] show that the termination assumption cannot be omitted fromthe statement of this lemma in the general case. Besides, there exists a strengthened version
of Newman’s counterexample [6, Theorem 2] that is an acyclic, locally confluent, but not confluent ARS (A, →) such that (A, →∗ ) is a strictly inductive poset, i.e. a partially ordered set
where every nonempty chain has a least upper bound, where →∗ denotes the reflexive-transitive
closure of → on A (however, unlike the regular Newman’s counterexample which is countable,
the mentioned strengthened Newman’s counterexample is necessarily uncountable).
Van Oostrom’s decreasing diagrams method [10] provides one of the approaches to proving
confluence of ARS that overcomes limitations of Newman’s lemma. Semi-formally, to provethat an ARS is confluent using this method, one needs to find a set of labels I together with awell-founded partial order ≺ on it, and find a labeled version of an ARS that satisfies a condition
reminiscent to the local confluence, but with special constraints on how labels associated with
reduction steps that appear in this condition are related by ≺. In a rigorous way it can beformulated using the notion of a decreasing Church-Rosser (DCR) ARS [10].
Importantly, unlike the case of confluence proofs based on Newman’s lemma, the decreasing
diagrams method requires one to choose/guess a set of labels, a well-founded order on it, an
assignment of labels to rewrite steps that can be thought of as method parameters. This leads toquestions about the possible redundancy of these parameters and the possibility of minimizationof the parameter space. In part, a setting for studying the latter questions can be formalizedusing a hierarchy of subclasses of DCR ARS indexed by ordinals introduced by J. Endrullis,
J.W. Klop, and R. Overbeek in [2]:DCR0 ⊆ DCR1 ⊆ DCR2 ⊆ ...

30

(1)

On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems

I. IvanovSemi-formally, for each ordinal α, DCRα is the class of confluent ARS for which confluencecan be proved with the help of the decreasing diagrams method using a fixed set of labels{β | β < α} (ordinals less than α) and a fixed order on them that is a restriction of the usual
order on ordinals to {β | β < α} (note that since a label set and an order on it are fixed, only
an assignment of labels to rewrite steps remains a method parameter).
In the works [2, 3] it was shown that every confluent ARS with at most countable set ofelements belongs to the class DCR2 , so the hierarchy of intersections DCRα ∩ CN T , where
CN T is the class of ARS with at most countable set of elements, collapses at the level 2.
However, in [2, 3] various questions concerning the hierarchy (1) in the general case (without
countability assumption) were not studied, and a number of open problems were formulated.
In particular, [3, Open Problem 6.3] asks whether there is a confluent uncountable ARS
outside of the class DCR2 . In this work we show that the answer to this question is aﬃrmative(Theorem 1), so the class DCR2 does not coincide with the class of all confluent ARS. We
provide a concrete example of such an ARS. Additionally, we show that this example belongs
to the class DCR3 (Theorem 2). Thus the hierarchy (1) does not collapse at the level 2, unlike
the countable DCR ARS hierarchy.

2

Preliminaries

An abstract rewriting system (ARS) is a pair (A, →), where A is a set and → ⊆ A × A is abinary relation (called reduction or rewrite relation). We will use the following notation:• →+ is the transitive closure of →• →= is the reflexive closure of → (on A)• →∗ is the reflexive-transitive closure of → (on A)• ¬, ∨, ∧, ⇒ are logical negation, disjunction, conjunction, and implication respectively.
An ARS (A, →) is• confluent, if ∀a, b, c ∈ A (a →∗ b ∧ a →∗ c ⇒ ∃d ∈ A (b →∗ d ∧ c →∗ d)).

For any ordinal α denote as ⋎α the set of all ordinals below β, i.e. {β | β < α}, where < isthe usual order on ordinals. Note that in the case of usual set-theoretic definitions of ordinals,
e.g. [7, Chapter 4], < is the membership ∈ and ⋎α is the ordinal α itself, however, we will use⋎α to highlight that α is considered as a set of ordinals.
Remark 2.1. A separate notation for {β | β < α} is also useful for some approaches to ordinals
in non-set-theoretic contexts [1, 9], e.g. used in some proof assistants, where < is not ∈.
The following definition is based on [3, Definition 4.4] and [3, Definition 4.2].
Definition 2.1. Let γ be a (fixed) ordinal. An ARS (A, →) belongs to the class DCRγ , if there
exists an indexed family (→α )α∈(⋎γ) of binary relations on A (indexed by ordinals α < γ) suchthat for every ordinals α, β ∈ (⋎γ) and for every a, b, c ∈ A the following implication holds:
ifa →α b ∧ a →β c,(2)then there exist elements b′ , b′′ , c′ , c′′ , d ∈ A such that
(
) (
∗
∗
∗
=
∗
′ =
′′
b 99K b 99K b 99K d ∧ c 99K c′ 99K c′′ 99K⋎α{β}⋎α ∪⋎β

⋎β

31

{α}

⋎β ∪⋎α)d ,(3)

On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems
=

∗

K

K

I. Ivanovwhere symbols of the form 99K and 99K , where K is an expression that denotes a set of ordinals,
have the following meaning:=

99K = {(a, a) | a ∈ A} ∪
K

∪

→κ

κ∈K

∗

and 99K = {(a, a) | a ∈ A} ∪
K

(

∪

κ∈K

→κ

)+

.

(4)

An illustration for Definition 2.1 is given below.
a

b

b

b

α

⋎α *
b′
b

{β} =

β

b′′
b

⋎α ∪ ⋎β *
b

c

*
⋎β

b

′

c

=
{α}

b

c′′

*
⋎β ∪ ⋎αbdFigure 1: Illustration of the conditions (2), (3) from Definition 2.1. The meaning of arrows is
described in (4). This figure is analogous to [3, Figure 9] and [10, Figure 2], however, note that
we do not use the notation “↠” for the reflexive-transitive closure.
The following propositions make the definitions of the classes DCR2 , DCR3 more explicit:
Proposition 1. An ARS (A, →) belongs to the class DCR2 if and only if there exist binary
relations →0 ⊆ A × A and →1 ⊆ A × A such that → = (→0 ∪ →1 ) and the following 3 conditions∗
hold, where for i = 0, 1, →=i and →i denote the reflexive closure of →i and the reflexivetransitive closure of →i on A respectively:=
1. ∀a, b, c ∈ A ((a →0 b ∧ a →0 c) ⇒ ∃d ∈ A (b →=0 d ∧ c →0 d))′′∗∗
2. ∀a, b, c ∈ A ((a →0 b ∧ a →1 c) ⇒ ∃b′ , d ∈ A (b →=1 b ∧ b →0 d ∧ c →0 d))

3. ∀a, b, c ∈ A ((a →1 b ∧ a →1 c) ⇒

′
= ′′
′′
∗
∗ ′
′′
′′
∗
∃b′ , b′′ , c′ , c′′ , d ∈ A (b →∗0 b′ ∧ b′ →=1 b ∧ b →0 d ∧ c →0 c ∧ c →1 c ∧ c →0 d)).

Proof. Follows immediately from Definition 2.1 by assuming that γ = 2 and taking into accountsymmetry of the cases α = 0, β = 1 and α = 1, β = 0.
Proposition 2. An ARS (A, →) belongs to the class DCR3 if and only if there exist relations→0 , →1 , →2 ⊆ A × A such that → = (→0 ∪ →1 ∪ →2 ) and the next 6 conditions hold, where– for i = 0, 1, 2, →=i denotes the reflexive closure of →i on A
– for i = 0, 1, 2, →∗i denotes the reflexive-transitive closure of →i on A
– →∗01 denotes the reflexive-transitive closure of →0 ∪ →1 on A:=
1. ∀a, b, c ∈ A ((a →0 b ∧ a →0 c) ⇒ ∃d ∈ A (b →=0 d ∧ c →0 d))

32

On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems

I. Ivanov′′∗∗
2. ∀a, b, c ∈ A ((a →0 b ∧ a →1 c) ⇒ ∃b′ , d ∈ A (b →=1 b ∧ b →0 d ∧ c →0 d))

3. ∀a, b, c ∈ A ((a →1 b ∧ a →1 c) ⇒

′′
′′
∗
∗ ′
′
= ′′
′′
∗
∃b′ , b′′ , c′ , c′′ , d ∈ A (b →∗0 b′ ∧ b′ →=1 b ∧ b →0 d ∧ c →0 c ∧ c →1 c ∧ c →0 d)).

′′∗∗4. ∀a, b, c ∈ A ((a →0 b ∧ a →2 c) ⇒ ∃b′ , d ∈ A (b →=2 b ∧ b →01 d ∧ c →01 d))
′′
′′
∗
∗
5. ∀a, b, c ∈ A ((a →1 b ∧ a →2 c) ⇒ ∃b′ , b′′ , d ∈ A (b →∗0 b′ ∧ b′ →=2 b ∧ b →01 d ∧ c →01 d))

6. ∀a, b, c ∈ A ((a →2 b ∧ a →2 c) ⇒

′′
′′
∗
∗
′
′
= ′′
′′
∗
∃b′ , b′′ , c′ , c′′ , d ∈ A (b →∗01 b′ ∧ b′ →=2 b ∧ b →01 d ∧ c →01 c ∧ c →2 c ∧ c →01 d)).

Proof. Follows from Definition 2.1 by assuming that γ = 3 and taking into account symmetryof the cases (α, β) ∈ {(0, 1), (1, 0)}, (α, β) ∈ {(0, 2), (2, 0)}, and (α, β) ∈ {(1, 2), (2, 1)}.

3

Main Result

Let R denote the set of real numbers and 2R denote the power set of R.
Let Pf (R) denote the set of all finite subsets of R.
Remark 3.1. The set R is used here for concreteness and simplicity. In the example given
below it can be replaced with any other uncountable set.
Example 1. Let (E, →E ) be an ARS, where E = {0, 1, 2, 3, 4, 5, 6, 7, 8} × 2R × 2R × 2R and→E is a binary relation on E such that for every (n, A, B, C), (n′ , A′ , B ′ , C ′ ) ∈ E a rewrite step(n, A, B, C) →E (n′ , A′ , B ′ , C ′ ) holds if and only if one of the following 9 conditions holds:
1. n = 0 ∧ A = ∅ ∧ B = ∅ ∧ C = ∅ ∧ n′ = 1 ∧ A′ ∈ Pf (R) ∧ B ′ = ∅ ∧ C ′ = ∅2. n = 1 ∧ A ∈ Pf (R) ∧ B = ∅ ∧ C = ∅ ∧ n′ = 2 ∧ A′ = A ∧ B ′ = ∅ ∧ C ′ = ∅3. n = 2 ∧ A ∈ Pf (R) ∧ B = ∅ ∧ C = ∅ ∧ n′ = 3 ∧ A′ = A ∧ B ′ ∈ Pf (R) ∧ C ′ = ∅4. n = 3 ∧ A ∈ Pf (R) ∧ B ∈ Pf (R) ∧ C = ∅ ∧ n′ = 4 ∧ A′ = A ∧ B ′ = B ∧ C ′ = ∅5. n = 4 ∧ A ∈ Pf (R) ∧ B ∈ Pf (R) ∧ C = ∅ ∧ n′ = 5 ∧ A′ = A ∧ B ′ = B ∧ C ′ ∈ Pf (R)
6. n = 5 ∧ A ∈ Pf (R) ∧ B ∈ Pf (R) ∧ C ∈ Pf (R) ∧ n′ = 6 ∧ A′ = A ∧ B ′ = B ∧ C ′ = C
7. n = 6 ∧ A ∈ Pf (R) ∧ B ∈ Pf (R) ∧ C ∈ Pf (R) ∧ n′ = 7 ∧ A′ = A ∪ B ∪ C ∧ B ′ = A′ ∧ C ′ = A′
8. n = 7 ∧ A ∈ Pf (R) ∧ B = A ∧ C = A ∧ n′ = 8 ∧ A′ = A ∧ B ′ = A′ ∧ C ′ = A′
9. n = 8 ∧ A ∈ Pf (R) ∧ B = A ∧ C = A ∧ n′ = 7 ∧ A ⊂ A′ ∧ A′ ∈ Pf (R) ∧ B ′ = A′ ∧ C ′ = A′ .

Theorem 1. The ARS (E, →E ) defined in Example 1 is confluent, but it does not belong to
the class DCR2 .

33

On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems

I. Ivanov

Proof. A machine-checked proof of a formalized version of Theorem 1 in Isabelle proof assistantis available in the supplementary material for this paper [5, lines 1142–1145, theorem thm 1].
More specifically, the formal proof shows that (E, →E ) is a confluent ARS, but there is nopair of relations →0 ⊆ E × E and →1 ⊆ E × E such that →E = (→0 ∪ →1 ) and →0 , →1 satisfy
the conditions 1-3 of Proposition 1.
Instructions on re-checking the formal proof using Isabelle 2023 software are included in the
supplementary material [5].
Semi-formally, the construction of the ARS in Example 1 is based on viewing the set E asa union of 9 “layers” (where a layer consists of elements of the form (n, A, B, C) for a fixedn ∈ {0, 1, ..., 8}) and joining elements of the mentioned layers in accordance with the pattern
illustrated in Figure 2: elements with uncountably many direct successors are succeeded byelements with a single direct successor, elements with a single direct successor are succeeded byelements with uncountably many successors. Reduction sequences of elements with n ∈ {0, ..., 5}
only diverge, but their continuations using elements with n ∈ {6, 7, 8} can converge. Details of
the definition of →E ensure that (E, →E ) is confluent, but does not have the cofinality property.
The main steps of the proof of Theorem 1 can be described as follows. First, it is assumed
that there exist →0 ⊆ E×E and →1 ⊆ E×E such that →E = (→0 ∪ →1 ) and →0 , →1 satisfy theconditions 1-3 of Proposition 1. Then using the condition 1 of Proposition 1 and the definition
of →E it can be shown that any element of E has no more than one direct successor w.r.t.
→0 ([5, formal lemma lem rE diamsubr un]). Note that this implies that the set of elements
reachable from any given element using →0 is at most countable. Using this fact it can beshown [5, formal lemma lem rE one] that the relation →0 does not contain rewrite steps of theform (n, A, B, C) →0 (n′ , A′ , B ′ , C ′ ), where n ∈ {0, 2, 4} (note that such elements (n, A, B, C)
have uncountably many direct successors w.r.t. →E ). Then all such rewrite steps belong to→1 . Using this fact a contradiction with the condition 3 of Proposition 1 can be obtained.
Remark 3.2. Reviewers Jörg Endrullis, Femke van Raamsdonk, and Jan Willem Klop in theirreview of the initial version of this paper proposed the following simplification of the example ofa confluent ARS outside of the class DCR2 :(A, →), where A = {1, 2, 3} × Pf in (R) and → is defined by the following rules:(1, P ) → (2, P ⊎ {p, q})(2, P ) → (3, P )(3, P ) → (2, P ⊎ {p})for all p, q ∈ R\P with p ̸= q.
Theorem 2. The ARS (E, →E ) defined in Example 1 belongs to the class DCR3 .
Proof. A machine-checked proof of a formalized version of Theorem 2 in Isabelle proof assistantis available in the supplementary material for this paper [5, lines 1147–1150, theorem thm 2].
More specifically, the formal proof shows that the following binary relations →i on E satisfy
the equality →E = (→0 ∪ →1 ∪ →2 ) and the conditions 1-6 of Proposition 2:• →0 = {((n, A, B, C), (n′ , A′ , B ′ , C ′ )) ∈ →E | n ∈ {1, 3, 5, 6, 7}}• →1 = {((n, A, B, C), (n′ , A′ , B ′ , C ′ )) ∈ →E | n ∈ {4, 8}}• →2 = {((n, A, B, C), (n′ , A′ , B ′ , C ′ )) ∈ →E | n ∈ {0, 2}}• →01 =→0 ∪ →1 .

34

On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systemsbb

I. Ivanovbb

uncountably many
direct successors
b
b

b

b

b

b

one direct successor
b

b

b

b

b

b

b

b

b

b

b

b

b

b

uncountably many
direct successorsb

Figure 2: Illustration of the main rewrite pattern used in the ARS (E, →E ) from Example 1.

Remark 3.3. Theorems 1 and 2 together imply that the answer to [3, Open Problem 6.4] isaﬃrmative.

References[1] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL.
volume 8558 of Lecture Notes in Computer Science, pages 111–127, 2014.
[2] Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing diagrams with two labels arecomplete for confluence of countable systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), pages 14:1–14:15, 2018.
https://doi.org/10.4230/LIPIcs.FSCD.2018.14.
[3] Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing diagrams for confluence andcommutation. Logical Methods in Computer Science, 16:23:1–23:25, 2020.
https://doi.org/10.23638/LMCS-16(1:23)2020.
[4] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, 1980.
[5] Ievgen Ivanov. Supplementary material for this paper. https://doi.org/10.5281/zenodo.
11571490 .
[6] Ievgen Ivanov. On Newman’s lemma and non-termination. In CEUR-WS.org, volume 3624, pages
14–24, 2024.
[7] Elliott Mendelson. Introduction to Mathematical Logic. CRC Press, 2015.
[8] Maxwell Herman Alexander Newman. On theories with a combinatorial definition of “equivalence”.
Annals of mathematics, pages 223–243, 1942.
[9] Chuangjie Xu Nicolai Kraus, Fredrik Nordvall Forsberg. Type-theoretic approaches to ordinals.
Theoretical computer science, 957, 2023.
[10] Vincent Van Oostrom. Confluence by decreasing diagrams. Theoretical computer science,
126(2):259–280, 1994.

35

Orthogonality of Generalized Term Rewriting Systems∗
Salvador Lucas
DSIC & VRAIN, Universitat Politècnica de València, Spainslucas@dsic.upv.es
Abstract
We introduce the notion of V-orthogonality for Generalized Term Rewriting Systems(GTRSs), which generalize Conditional Term Rewriting Systems by (i) restricting rewritings on arguments of function symbols and (ii) allowing for more general conditions inrules, namely, atoms defined by a set of Horn clauses. The usual left-linearity requirement
for rules is relaxed. However, besides the absence of proper conditional critical pairs, theinfeasibility of the conditional variable pairs introduced by conditional rules is also required. We prove that V-orthogonal GTRSs are confluent. This new confluence criterion
has been implemented in the confluence tool CONFident improving its ability to deal with
context-sensitive and conditional term rewriting systems. We briefly report on this.

1

Introduction

For Term Rewriting Systems (TRSs), orthogonality is a syntactic criterion guaranteeing confluence by requiring (i) left-linearity of rules and (ii) the absence of critical pairs [4, Definition
3.1.1]. In this paper we extend this approach to Generalized Term Rewriting Systems (GTRSs[6]) R = (F, Π, µ, H, R), where F is a signature of function symbols; Π is a signature of predicate symbols, including → and →∗ ; µ is a replacement map, i.e., a mapping such that, forall k-ary function symbols f ∈ F, µ(f ) ⊆ {1, . . . , k} is the set of active arguments on which
rewriting steps are allowed [5]; H is a (possibly empty) set of definite Horn clauses A ⇐ c,where the predicate symbol of A is not → or →∗ ; and R is a set of rewrite rules ` → r ⇐ csuch that ` ∈/ X [6, Definition 51]. In both cases, c is a sequence of atoms.
Example 1. Consider the GTRS R = (F, Π, µ⊥ , H, R), where F = {0, s}, Π = {→, →∗ , ≥,peven, odd, zero}, µ⊥ (f ) = ∅ for all f ∈ F, H = {(1), (2), (3), (4), (5)}, and R = {(6)}, with:x≥0s(x) ≥ s(y) ⇐peven(x) ⇐odd(x) ⇐ x →∗ s(0)

(1)

x≥y

zero(x) ⇐ x →∗ 0(2)

x →∗ s(s(0)) (3)s(s(x)) → x ⇐ x ≥ s(0)

(4)

(5)
(6)

Predicate ≥ is defined by the Horn clauses (1) and (2); clauses (3), (4), and (5) define tests tocheck whether a number (in Peano notation) is positive and even (peven), odd, or zero.
The FO-theory of a GTRS R is R = {(Rf), (Co)} ∪ {(Pr)f,i | f ∈ F, i ∈ µ(f )} ∪ {(HC)α |α ∈ H ∪ R}, where (see Table 1), (Rf) expresses reflexivity of many-step rewriting; (Co)expresses compatibility of one-step and many-step rewriting; for each k-ary function symbol fand i ∈ µ(f ), (Pr)f,i enables the propagation of rewriting steps in the i-th immediate active
subterm t|i of a term t with root symbol f ; finally, for each Horn clause α ∈ H ∪ R, (HC)α
provides the usual implicative form.
∗ Partially
supportedby
MCIN/AEI
project
PID2021-122830OB-C42
fundedby
MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe” and by the grant
CIPROM/2022/6 funded by Generalitat Valenciana.

36

Orthogonality of Generalized Term Rewriting Systems

Salvador Lucas

Table 1: Generic sentences of the first-order theory of a GTRS
Label
Sentence(Rf)(∀x) x →∗ x
(Co)(∀x, y, z) x → y ∧ y →∗ z ⇒ x →∗ z(Pr)f,i(∀x1 , . . . , xk , yi ) xi → yi ⇒ f (x1 , . . . , xi , . . . , xk ) → f (x1 , . . . , yi , . . . , xk )(HC)A⇐A1 ,...,An (∀x1 , . . . , xp ) A1 ∧ · · · ∧ An ⇒ A
where x1 , . . . , xp are the variables occurring in A1 , . . . , An and A

Example 2. We have R = {(Rf), (Co), (HC)(1) , (HC)(2) , (HC)(3) , (HC)(4) , (HC)(5) , (HC)(6) }for R in Example 1. Note that no propagation rule is necessary as µ⊥ (f ) = ∅ for all f ∈ F.
For all terms s and t, we write s →R t (resp. s →∗R t) iff R ` s → t (resp. R ` s →∗t). A GTRS R is (locally) confluent (resp. terminating) iff →R is (locally) confluent (resp.
terminating). A sequence of atoms A1 , . . . , An is R-feasible (or just feasible if no confusion
arises) if there is a substitution σ such that, for all 1 ≤ i ≤ n, R ` σ(Ai ) holds. A rule
` → r ⇐ c is feasible if c is feasible. Only feasible rules contribute to →R -rewriting steps andhence to confluence. As in [8, Definition 6.1], rules ` → r ⇐ c in GTRSs are classified according
to the distribution of variables: type 1, if Var(r) ∪ Var(c) ⊆ Var(`); type 2, if Var(r) ⊆ Var(`);
type 3, if Var(r) ⊆ Var(`) ∪ Var(c); and type 4, otherwise. A rule of type n is often called ann-rule. A GTRS R is called an n-GTRS if all its rules are of type n; if R contains at least one
n-rule which is not an m-rule for some m < n, then we say that R is a proper n-GTRS.

2

V-orthogonality of GTRSs

In the following, we deal with conditional pairs, π : hs, ti ⇐ c, where s and t are terms and c isa sequence of atomic conditions; π is trivial if s = t; it is R-(in)feasible if c is.
Definition 1 (Conditional critical and variable pairs of a GTRS [6, Def. 59]). Let R be a GTRS,
and α : ` → r ⇐ c, α0 : `0 → r0 ⇐ c0 be variable disjoint rules of R (rename if necessary).
• Let p ∈ PosµF (`) be a nonvariable active position of ` such that `|p and `0 unify with mgu θ.
Then, hθ(`[r0 ]p ), θ(r)i ⇐ θ(c), θ(c0 ), labelled πα,p,α0 , is a conditional critical pair (CCP).
If p = Λ and α and α0 are renamed versions of the same rule, then πα,p,α0 is an improper
CCP; otherwise, it is a proper CCP. Let pCCP(R) be the set of feasible proper CCPs of
R. Let iCCP(R) be the set of feasible improper CCPs of proper 3- or 4-rules in R.
• Let p ∈ Posµx (`) be an active position of a variable x in `, and x0 be a fresh variable.
Then, h`[x0 ]p , ri ⇐ x → x0 , c, labelled πα,x,p , is a conditional variable pair (CVP). Let
CVP(α) be the set of feasible CVPs of a rule α.
Our next definition introduces V-orthogonality of GTRSs R. For unconditional rules ` → r
in R, the requirement of left-linearity is weakened to benefit from replacement restrictions andthe consideration of CVPs: for unconditional rules, we require that active variables occur atmost once in the left-hand sides and that they remain active in the right-hand sides. On theother hand, besides requiring that only trivial and proper critical pairs are present, we also
require the infeasibility of conditional variable pairs for proper conditional rules.

37Orthogonality of Generalized Term Rewriting Systems

Salvador Lucas

Definition 2 (V-orthogonal GTRS). Let R = (F, Π, µ, H, R) be a GTRS such that:
1. for all unconditional rules ` → r ∈ R, and all active variables x ∈ Varµ (`) in `, (a) x
occurs nowhere else in ` and (b) x is not frozen in r;
2. all feasible improper CCPs π ∈ iCCP(R) are trivial; and3. for all rules α : ` → r ⇐ c with c nonempty there is no feasible CVP: CVP(α) = ∅.
If pCCP(R) = ∅, then R is called V -orthogonal. If for all π ∈ pCCP(R), π is a trivial overlay,
then R is called almost V -orthogonal. If for all π ∈ pCCP(R), π is trivial, then R is called
weakly V -orthogonal.
V-orthogonal GTRSs are almost V-orthogonal, hence weakly V-orthogonal. For TRSs,
Definition 2 and (almost, weak) orthogonality coincide. And (almost, weakly) orthogonal 2CTRSs modulo infeasibility [10, Definition 2] (properly including (weakly) orthogonal 2-CTRSs[9, Definition 7.1.10]) are (weakly) V-orthogonal. The GTRS R in Example 1 is V-orthogonal.

3

Confluence of weakly V-orthogonal GTRSs

Two positions p and q are disjoint (written p k q [9, page 39]) if p 6≤ q and q 6≤ p; otherwise,
we write p 6 k q. Given a position p and a set of positions P , we write p k P if p k p0 for all
p0 ∈ P . Given sets of positions P and Q, we write P k Q if for all p ∈ P , p k Q (equivalently
q k P for all q ∈ Q). As before, we write p 6 k P (resp. P 6 k Q) if p k P (resp. P k Q) does nothold. Given a position p and a set of positions Q, let A(p, Q) = {q ∈ Q | q < p} be positions
in Q (strictly) above p, and B(p, Q) = {q ∈ Q | p < q} be positions in Q (strictly) below p.
Note that p ∈/ B(p, Q) and p k p0 implies B(p, Q) k B(p0 , Q). We say that P is a set of mutually
disjoint positions if positions in P are pairwise disjoint: for all p, p0 ∈ P , p 6= p0 implies p k p0 .
Proposition 3. Let p be a position and Q be a set of mutually disjoint positions. Then, (1)A(p, Q) 6= ∅ implies that A(p, Q) = {q} is a singleton; (2) if p ∈/ Q, then A(p, Q) = B(p, Q) = ∅implies p k Q; and (3) it is not possible to simultaneously have A(p, Q) 6= ∅ and B(p, Q) 6= ∅.
Rewriting with GTRSs R has a position-based view [6, Proposition 58]: s →R t iff there
is p ∈ Posµ (s) and ` → r ⇐ c ∈ R such that (i) s|p = σ(`) for some substitution σ, (ii)for all A ∈ c, R ` σ(A) holds, and (iii) t = s[σ(r)]p . Accordingly, given a term s, a set
P = {p1 , . . . , pn } ⊆ Posµ (s) of disjoint (active) positions in s, for some n ≥ 0, rules αi : `i →ri ⇐ ci ∈ R and substitutions σi , 1 ≤ i ≤ n, such that s|pi = σi (`i ) and σ(ci ) holds, we writePs −→R t if t = s[σ1 (r1 )]p1 · · · [σn (rn )]pn (also s →k R t, or even s →k t, if no confusion arises).

Proposition 4. Let R = (F, Π, µ, H, R) be a weakly V-orthogonal GTRSs. For all terms
k t and s →k t0 , there is u such that t →k u and t0 →k u.
s, t, t0 ∈ T (F, X ), if s →P

P0

Proof. Let s ∈ T (F, X ) and P, P 0 ⊆ Posµ (s) be such that s −→R t and s −→R t0 for someterms t, t0 . Let P = {p1 , . . . , pm } and P 0 = {p01 , . . . , p0n } for some m, n > 0 be nonempty setsof mutually disjoint redex positions of s. Thus, there are (pairwise variable disjoint) rules
αi : `i → ri ⇐ ci for all 1 ≤ i ≤ m and αj0 : `0j → rj0 ⇐ c0j for all 1 ≤ j ≤ n such thats = s[σ(`1 )]p1 · · · [σ(`m )]pm = s[σ(`01 )]p01 · · · [σ(`0n )]p0n and thent = s[σ(r1 )]p1 · · · [σ(rm )]pm

and t0 = s[σ(r10 )]p01 · · · [σ(rn0 )]p0n

38

(7)

Orthogonality of Generalized Term Rewriting Systems

Salvador Lucas

Since P and P 0 are sets of pairwise disjoint redex positions, the order in which replacementsin (7) are made is not important. We partition P as P = A ] B ] E ] D, where A = {p ∈P | B(p, P 0 ) 6= ∅} is the subset of positions in P which are strictly above some positions of P 0(and hence not below any position in P 0 , due to Proposition 3.(3)); B = {p ∈ P | A(p, P 0 ) 6= ∅}is the subset of positions in P which are strictly below positions of P 0 ; E = P ∩ P 0 , and
D = P − (A ∪ B ∪ E) = {p ∈ P − P 0 | A(p, P 0 ) = ∅ ∧ B(p, P 0 ) = ∅} is the set of positions of
P which are disjoint from P 0 (Proposition 3(2)). Proposition 3(3) guarantees that A ∩ B = ∅.
Note that, since P is mutually disjoint, A, B, D, and E are pairwise mutually disjoint.
1. If p ∈ E, then p ∈ P ∩ P 0 and s|p = σ(`) = σ(`0 ) for some (variable disjoint) rules
α : ` → r ⇐ c and α0 : `0 → r0 ⇐ c0 , where both σ(c) and σ(c0 ) are satisfied. Thus, ` and `0
overlap at the root position Λ, i.e., ` and `0 unify with mgu θ, defining a (feasible) conditional(overlay) critical pair π : hθ(`)[θ(r0 )]Λ , θ(r)i ⇐ θ(c), θ(c0 ), i.e., π : hθ(r0 ), θ(r)i ⇐ θ(c), θ(c0 ).
Also, t|p = σ(r) and t0 |p = σ(r0 ). By Definition 2, whether proper or improper, π is trivial.
Then, t0 |p = σ(r0 ) = σ(r) = t|p , see the diagram in Figure 1(1).
2. If p ∈ A, then for all p0 ∈ B(p, P 0 ) ⊆ P 0 , p0 = p.q 0 for some nonempty position q 0 . Thus,00B(p, P 0 ) = p.{q10 , . . . , qm
} for some m ≥ 1 and nonempty positions q10 , . . . , qm
. We have0s|p = σ(`) = σ(`)[σ(`01 )]q10 · · · [σ(`0k )]qm

for some substitution σ and rules α : ` → r ⇐ c and αi0 : `0i → ri0 ⇐ ci for 1 ≤ i ≤ m suchthat σ(c) and σ(c0i ) hold for all 1 ≤ i ≤ m. Let Var(`) = {x1 , . . . , xk } and, for each 1 ≤ j ≤ k,
Vj = P osxj (`) be the set of positions of ` where xj occurs. We also let Vjµ = Vj ∩ Posµ (`) beµ
the (possibly empty) subset of active positions of xj in ` and V j = Vj ∩ Posµ (`) = Vj − Vjµbe the (possibly empty) subset of frozen positions of xj in `. Then, ` = `[x1 ]V1 · · · [xk ]Vk =`[x1 ]V1µ [x1 ]V µ · · · [xk ]Vkµ [xk ]V µ and we can write
1

k

s|p

=

s|p

−→α

s|p

{Λ}

0
{q10 ,...,qm}−−−−−−→Rσ(`) = `[σ(x1 )]V1µ [σ(x1 )]V µ · · · [σ(xk )]Vkµ [σ(xk )]V µ(8)σ(r) = t|p

(9)

1

k

0
0
0 = t |pσ(`)[σ(r10 )]q10 · · · [σ(rm
)]qm

(10)

We consider cases 2.a and 2.b:
2.a. No rule αi overlaps α, i.e., for all 1 ≤ i ≤ m, qi0 ∈/ PosF (`). Thus, Varµ (`) 6= ∅ andthere is a variable index mapping ν : {1, . . . , m} → {1, . . . , k} such that for all 1 ≤ i ≤ m, qi0 isµ
below an active position of a variable xν(i) in `, i.e., qi0 = ui .u0i for some ui ∈ Vν(i)and active
0
0
0
0
0
0
0
0
position ui . Let Q = {q1 , . . . , qm }. We can partition Q as Q = Q1 ] · · · ] Qk where, for all
1 ≤ j ≤ k, Q0j = {q 0 ∈ Q0 | u ≤ q 0 for some u ∈ Vjµ } collects the positions in Q0 which are
below a position of an occurrence of variable xj in `. Define the substitution σ 0 to be such that
Q0j

σ(xj ) −→R σ 0 (xj ) for all 1 ≤ j ≤ k. We distinguish two cases:• If α is an unconditional rule ` → r, then, by item 1.(a) in Definition 2, for all 1 ≤ j ≤ k,either (I) Vjµ = ∅ and hence Q0j = ∅ and σ 0 (xj ) = σ(xj ); or (II) Vjµ = {uj } is a singletonµand then V j = ∅ and uj ≤ Q0j . Hence, (10) can be written as follows:s|p{q 0 ,...,q 0 }m−−1−−−−→R`[σ 0 (x1 )]V1µ [σ 0 (x1 )]V µ · · · [σ 0 (xk )]Vkµ [σ 0 (xk )]V µ = t0 |p
1

k

(11)

for all 1 ≤ i ≤ m, let Wν(i)Sm be the (possibly empty) set of positions of xν(i) in r: Wν(i) =P osxν(i) (r). Let W = i=1 p.Wν(i) = PosX (r). By item 1.(b) of Definition 2, for all

39

Orthogonality of Generalized Term Rewriting Systems

{Λ}

s|p

/ t|p

{Λ}

s|p

{Λ}

1. p ∈ E{q1 ,...,qn }

{Λ}

{Λ}


t0 |p0

W0

/ t|p
0
0
{qν+1
,...,qm
}



u
t0 |p
2.(b) p ∈ A{q1 ,...,qn }/ t|p0s|p {qν 0 +1 ,...,qn }/ut0 |p03.(b) p ∈ B

t0 |p

s|p0

/ t|p0{Λ}

0{q10 ,...,qm}W

 {Λ} /ut0 |p2.(a) p ∈ A

u

s|p0

s|p

/ t|p

0
{q10 ,...,qm
}


t0 |p

Salvador Lucas

{Λ}

/ u

3.(a) p ∈ B

{Λ}

{Λ}

/ t|p

/u

4. p ∈ D

Figure 1: Different cases in the proof of Proposition 4
1 ≤ i ≤ m, xi does not occur frozen in r. Hence, W = PosµX (r) is a set of disjoint active
variable positions of r. Therefore,
t|p
t0 |p

=
=

W

σ(r) = r[σ(x1 )]W1 · · · [σ(xk )]Wk −→R r[σ 0 (x1 )]W1 · · · [σ 0 (xk )]Wk = u(12)`[σ 0 (x1 )]V1µ [σ 0 (x1 )]V µ · · · [σ 0 (xk )]Vkµ [σ 0 (xk )]V µ −→α = u

(13)

{Λ}

1

k

The parallel rewriting step (12) is possible because (10) is possible. The rewriting step(13) is possible due to (I) and (II) above. Overall, we obtain diagram 2.(a) in Figure 1.
• If α is a conditional rule ` → r ⇐ c, and xj ∈ Vjµ for some 1 ≤ j ≤ k such that Q0j 6= ∅,then, by item (3) in Definition 2, the CVP h`[x0j ]uj , ri ⇐ xj → x0j , c for a fresh variable x0j
is infeasible. Since, due to (9), σ(c) holds it must be σ(xj ) 6→R σ(x0j ), which contradicts
Q0jthat σ(xj ) −→R σ 0 (xj ) due to (11). Thus, the peak is not possible.
2.b. If some αi overlaps α, i.e., qi0 ∈ PosF (`), then without loss of generality, there is ν, 1 ≤ ν ≤000m partitioning {q10 , . . . , qm
} into {q10 , . . . , qν0 }, representing critical peaks, and {qν+1, . . . , qm},
representing variable peaks. Accordingly, one of the following two conditions hold: for all
1 ≤ i ≤ ν, qi0 ∈ PosF (`), i.e., `|qi0 and `0 unify with mgu θi and there is a conditional criticalpair πi : hσ(`)[σ(ri0 )]qi0 , θi (r)i ⇐ θi (c), θi (c0i ). Since σ(c) and σ(c0i ) hold, πi is feasible, i.e.,
πi ∈ pCCP(R). By strong orthogonality, πi is trivial for all 1 ≤ i ≤ ν. Hence,t|p= σ(r) = σ(`)[σ(r10 )]q10 = · · · = σ(`)[σ(rν0 )]qν000= σ(`)[σ(r10 )]q10 · · · [σ(rν0 )]qν0 [σ(`0ν+1 )]qν+1· · · [σ(`0m )]qm

0
0
{qν+1
,...,qm}−−−−−−−→Rt0 |pand we obtain the diagram 2.(b) in Figure 1.
3. If p ∈ B, then, by Proposition 3(1), A(p, P 0 ) = {p0 } returns the (only) position p0 ∈ P 0 which
is above p. Then, B 0 = B(p0 , P ) is the set of positions in P which are below p0 . By reasoning as
in the previous item, we obtain diagrams 3.(a) and 3.(b) in Figure 1.
{p}

4. If p ∈ D, then s|p −→α t|p but, since p k P 0 , t0 |p = s|p , see diagram 4 in Figure 1.
Proposition 4 proves the diamond property [1, Definition 2.7.8] of →k R , which implies strong
confluence of →R [1, Definition 2.7.3]. Since →R ⊆ →k R ⊆ →∗R , by [1, Corollary 2.7.7], we have:40Orthogonality of Generalized Term Rewriting Systems

Salvador Lucas

Theorem 5. Weakly V -orthogonal GTRSs are confluent.
The V-orthogonal GTRS R in Example 1 is conflluent.
Application to CS-TRSs. A Context-Sensitive Term Rewriting System (CS-TRS) R =(F, µ, R), where R is a set of unconditional rules [5], can be seen as a GTRS R = (F, Π, µ, H, R),
where Π = {→, →∗ } and H is empty. When applied to CS-TRSs, Definition 2 collapses into
the requirement (1) for unconditional rules, as (2) and (3) concern conditional rules only.
Example 3. Consider the following CS-TRS R from COPS (1336.trs):f(x, x) → plus(plus(x, x), x)plus(x, y) →plus(y, x)

Since all variables in the left-hand sides of rules are frozen, R is V-orthogonal and confluent.

Left-linear CS-TRSs R without µ-critical pairs (i.e., critical pairs in CP(R) whose critical
position is active, i.e., they coincide with pCCP(R)) and such that for all ` → r in R and
active variable x in ` the variable occurs nowhere else in ` and is not frozen in r, are called µorthogonal [7, Definition 35]. V-orthogonal CS-TRSs properly include µ-orthogonal CS-TRSs.
For instance, R in Example 3 is V-orthogonal but not µ-orthogonal.
Application to Conditional Term Rewriting Systems. A CTRS R = (F, R), with R
a set of rules ` → r ⇐ s1 ≈ t1 , . . . , sn ≈ tn for a predicate symbol ≈, can be seen as a
GTRS R = (F, Π, µ> , H, R), where Π = {→, →∗ , ≈}, µ> (f ) = {1, . . . , k} for all k-ary symbols
f ∈ F (i.e., no replacement restriction is considered), and H depends on the (fixed) evaluation
semantics (join, oriented, or semi-equational, see, e.g., [9, Definition 7.1.3]) for the conditionss ≈ t in rules. Accordingly, H is either {(J)}, or {(O)}, or {(SE1 ), (SE2 ), (SE3 )}, see [6, Figure2]. Since no replacement restriction is considered, when applied to CTRSs, requirement (1) in
Definition 2 just becomes left-linearity (of unconditional rules).
Example 4. The following (non-terminating) 2-CTRS R:
a →

b

c

→

f(x, x) → x ⇐ h(b, y) ≈ h(x, g(y)), y ≈ cg(c)is not (almost, weakly) orthogonal [9, Definition 7.1.10], as it is not left-linear due to the conditional rule. Thus, the usual results guaranteeing confluence of (weakly) orthogonal CTRSs(see, e.g., [9, Section 7.4]) do not apply. However, the unconditional rules are left-linear,pCCP(R) = ∅, and the only improper CCP obtained from the conditional (2-)rule is trivial. The two CVPs, f(x0 , x) → x ⇐ x → x0 , h(b, y) ≈ h(x, g(y)), y ≈ c and f(x, x0 ) →x ⇐ x → x0 , h(b, y) ≈ h(x, g(y)), y ≈ c are infeasible: if a substitution σ would satisfy the(common) conditional part then σ(x) →R σ(x0 ) holds. However, σ(h(b, y)) = h(b, σ(y)) →∗Rh(σ(x), g(σ(y))) = σ(h(x, g(y))) requires b = σ(x), which contradicts reducibility of σ(x).
Therefore, R is almost V -orthogonal and hence confluent.
V -orthogonality, alone, does not subsume existing results for orthogonal CTRSs.

Example 5. The following orthogonal 3-CTRS R [11, Example 4.4]
a → b

b → c
k(x) → j(x)f(x) → g(x, y) ⇐ x ≈ i(y)h(x) → i(y) ⇐ x ≈ j(y)is confluent by [11, Corollary 4.7]. However, R is not weakly V -orthogonal: the improper CCP
hi(y), i(y 0 )i ⇐ x ≈ j(y), x ≈ j(y 0 ) obtained from the last rule is feasible and not trivial.

Such results, though, require additional restrictions on the conditional rules (e.g., a particular evaluation semantics for the conditional part [2], or conditions of a given shape [11]).

41

Orthogonality of Generalized Term Rewriting Systems

4

Salvador Lucas

Implementation

The results in this paper were implemented as part of the confluence tool CONFident to prepare its participation in the 2023 edition of the Confluence Competition, CoCo 20231 . CONFident and ConfCSR participated in the CSR category of CoCo 2023, where CS-TRSs and
CS-CTRSs are mixed (there were 176 CS-TRSs and 287 CS-CTRSs). Since ConfCSR does nothandle CS-CTRSs (whose confluence is (dis)proved by CONFident by using the results in thispaper together with [6, 3], as CS-CTRSs are particular GTRSs [6, Section 7.3]), the following
table reproduces the information for CS-TRSs extracted in [3, Table 10 (left)] for the CoCo2023 full run benchmarks set (full details in [3, Section 8]):Tool
ConfCSR
CONFident 2024

Yes
28
49

No Maybe
83
65
83
44

Solved
111
132

Total
176
176

For instance, the CS-TRS R in Example 3 was solved by using the results in this paper.2
Acknoledgements.

I thank Miguel Vı́tores for implementing these results in CONFident.

References[1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press,
1998.
[2] Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. J.
Comput. Syst. Sci., 32(3):323–362, 1986.
[3] Raúl Gutiérrez, Salvador Lucas, and Miguel Vı́tores. Proving Confluence in the Confluence Framework with CONFident. Fundamenta Informaticae, to appear, 2024.
[4] J. W. Klop. Chapter 1: Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaurn,
editors, Handbook of Logic in Computer Science, pages 1–116. Oxford University Press, 1992.
[5] Salvador Lucas. Context-sensitive Rewriting. ACM Comput. Surv., 53(4):78:1–78:36, 2020.
[6] Salvador Lucas. Local confluence of conditional and generalized term rewriting systems. Journalof Logical and Algebraic Methods in Programming, 136:paper 100926, pages 1–23, 2024.
[7] Salvador Lucas, Miguel Vı́tores, and Raúl Gutiérrez. Proving and disproving confluence of contextsensitive rewriting. Journal of Logical and Algebraic Methods in Programming, 126:100749, 2022.
[8] Aart Middeldorp and Erik Hamoen. Completeness results for basic narrowing. Appl. Algebra Eng.
Commun. Comput., 5:213–253, 1994.
[9] Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002.
[10] Christian Sternagel and Thomas Sternagel. Certifying confluence of almost orthogonal ctrss via
exact tree automata completion. In Delia Kesner and Brigitte Pientka, editors, 1st International
Conference on Formal Structures for Computation and Deduction, FSCD 2016 Proceedings inInformatics (LIPIcs), pages 29:1–29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
[11] Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-Confluence of Conditional Rewrite Systems
with Extra Variables in Right-Hand Sides. In Jieh Hsiang, editor, Rewriting Techniques andApplications, 6th International Conference, RTA-95, Proceedings, volume 914 of Lecture Notes in
Computer Science, pages 179–193. Springer, 1995.

1 https://project-coco.uibk.ac.at/2023/
2 The report produced by CONFident for CoCo 2023 displays “strong orthogonality” rather than Vorthogonality, see http://cops.uibk.ac.at/results/2023/CSR/CONFident/1336.trs/615314450.txt.

42

Second-order Church-Rosser modulo, without normalization
Thiago Felicissimo
Université Paris-Saclay, INRIA, Deducteam, Laboratoire de Méthodes Formelles, ENS Paris-Saclay
thiago.felicissimo@inria.fr
Abstract
We investigate criteria for proving Church-Rosser modulo of second-order rewrite systems
without relying on normalization.

1

Introduction

Rewriting modulo is an alternative to standard rewriting in which one considers not only
rewriting rules l 7−→ r ∈ R but also undirected equations t ≈ u ∈ E, allowing to handle theories
defined by axioms that cannot be oriented in a well-behaved manner, such as commutativity. In
this setting, the Church-Rosser property must be adapted into Church-Rosser modulo, statingthat t (−→ ∪ ←− ∪ ≃)∗ u implies t −→˜ ∗ ◦ ≃ ◦ ∗ ←−˜ u, where ≃ is the congruence generated
by E, −→ is the rewrite relation generated by R, and −→˜ is a relation that can be −→ [9], or≃ ◦ −→, or something in between [10] depending on the considered variant of this definition.
Unfortunately, most criteria for Church-Rosser modulo rely on normalization [9, 10, 13, 6], posing a challenge in an ongoing line of study [2] to extend Dedukti [5], a rewriting-based frameworkfor defining type theories, with rewriting modulo. Indeed, confluence proofs for dependent typetheories are usually carried out on untyped terms, for which normalization does not hold due torules such as β-reduction. The situation is made worse by the fact that type theories rely not on
first- but second-order rewriting, for which criteria for Church-Rosser modulo are much rarer.
Example 1. Consider the following second-order rewrite system modulo, defining (a fragmentof) the conversion of a type theory with an addition satisfying commutativity and assocativity.
Function symbols are written in blue, and metavariables in typewriter font. We would like toshow this example (or a variant of it) to be Church-Rosser modulo.1+(t, 0) ≈ t+(t, S(u)) ≈ S(+(t, u))+(t, u) ≈ +(u, t)+(+(t, u), v) ≈ +(t, +(u, v))

Nrec (0, p0, xy.pS{x, y}) 7−→ p0@(λ(x.t{x}), u) 7−→ t{u}Nrec (S(n), p0, xy.pS{x, y}) 7−→ pS{n, Nrec (n, p0, xy.pS{x, y})}In this work, we investigate criteria for proving Church-Rosser modulo of second-order rewrite
systems without relying on normalization. We start by proposing a first criterion, which relies
on a notion of unblocked term. We then discuss a second criterion, which can be shown almost
directly from a well-known result. The proofs not given here can be found in a technical report [7].

2Preliminaries

We work in the setting of (untyped) second-order rewriting.2 An arity is a natural number n
and a binding arity is a list of natural numbers (n1 , . . . , nk ). Given a set V of variables x, y, . . . ,1 Among other things, this is needed to establish the injectivity of Π-types: Π(A , x.A ) ≡ Π(A′ , x.A′ ) should
12
12
imply Ai ≡ A′i . This is then used to establish subject reduction of β-reduction.
2 This can be seen as Hamana’s Second-order Computational Systems [8], or a simply-typed version of
Klop’s Combinatory Reduction Systems (CRSs) [12] with a single base type, or Nipkow’s Pattern Rewrite

43Second-order Church-Rosser modulo, without normalization

Felicissimo

a set M of metavariables t, u, x, . . . equipped with arities, and a set F of (function) symbols
f, g, . . . equipped with binding arities, we define the terms by the following grammar, where wewrite |⃗x| for the number k of variables in a list of variables ⃗x = x1 . . . xk . Here, the (simple) arity
arity(x) = k of x specifies that it takes k arguments, and the binding arity arity(f ) = (n1 , . . . , nk )of f specifies that it takes k arguments and binds ni variables ⃗xi in its i-th argument ti . GivenF ′ ⊆ F, we write T (F ′ ) for the set of terms containing only symbols in F ′ .
t, u, v ::= | x| x{t1 , . . . , tk }| f (⃗x1 .t1 , . . . , ⃗xk .tk )x∈Vx ∈ M with arity(x) = kf ∈Fwith arity(f ) = (n1 , . . . , nk ) and |⃗xi | = ni

We write fv(t) for the set of free variables of t and mv(t) for its set of metavariables. We
often abbreviate t1 , . . . , tk as ⃗t, and ⃗x1 .t1 , . . . , ⃗xk .tk as t. A substitution σ is a set of pairs eitherof the form t/x or ⃗x.t/x where arity(x) = |⃗x|. We write t[σ] for the application of σ to t, theinteresting cases being x[σ] = t if t/x ∈ σ and x{⃗t}[σ] = u[⃗t[σ]/⃗x] if ⃗x.u/x ∈ σ.
A term t is said to be a ⃗x-pattern if fv(t) ⊆ ⃗x and all metavariables occurrences are of theform x{⃗x, ⃗y } where ⃗y are the variables bound between the root of the term and this occurrenceof x3 . A pattern is then just a ε-pattern, where ε is the empty list.
A rewrite system R is a set of rewrite rules l 7−→ r, where l is a pattern headed by a symbol
and mv(r) ⊆ mv(l) and fv(r) = ∅ (we already have fv(l) = ∅ from the definition of pattern). An
equational system E is a set of equations t ≈ u, where t, u are both patterns.4 Given a rewrite system R, we write −→ for the rewrite relation generated by R, and given an equational system E wewrite ≃ for the congruence on terms generated by E. We write FR ⊆ F for the symbols appearing
in some left-hand side of R, and FE ⊆ F for the symbols appearing in some equation of E.
A rewrite system modulo is a pair (R, E), and we write ≡ for the least equivalence relation
containing −→ and ≃. As previously mentioned, there are many different definitions of ChurchRosser modulo in the literature, so here we will say that (R, E) is weak (resp. strong) ChurchRosser modulo when t ≡ u implies t (≃ ◦ −→)∗ ◦ ≃ ◦ ∗ (←− ◦ ≃) u (resp. t −→∗ ◦ ≃ ◦ ∗ ←− u).
A context C is a linear pattern on distinguished metavariables □1 , □2 , . . . called holes. Givena context C with k holes and t = ⃗x1 .t1 , . . . , ⃗xk .tk with arity(□i ) = |⃗xi | for all i, we write C[t]for C[⃗x1 .t1 /□1 , . . . , ⃗xk .tk /□k ].
Finally, we will also consider the definition of orthogonal rewriting =⇒ (also known as developements, or simultaneous reduction [3]), given by the following rules. Here we write ⃗t1 =⇒ ⃗t2 when⃗ti = ti,1 , . . . , ti,k and t1,j =⇒ t2,j , and t1 =⇒ t2 when ti = ⃗x1 .ti,1 , . . . , ⃗xk .ti,k and t1,j =⇒ t2,j ,and σ1 =⇒ σ2 when dom(σ1 ) = dom(σ2 ) and t1 =⇒ t2 whenever ti /x ∈ σi or ⃗x.ti /x ∈ σi .
σ =⇒ σ ′l 7−→ r ∈ R
mv(l) = dom(σ) l[σ] =⇒ r[σ ′ ]3t =⇒ t′f (t) =⇒ f (t′ )⃗t =⇒ ⃗t′x{⃗t} =⇒ x{⃗t′ }x =⇒ x

The first criterion

In order to explain our criterion and the intuition behind it, it is instructive to start with thefollowing simple criterion for abstract rewriting. Recall that an abstract rewrite system modulo
is given by a set A equipped with a binary relation ≻ and an equivalence relation ∼.
Systems (PRSs) [13] over a single base type but with only function symbols of order at most two and variablesof order at most one. In particular, this allows us to use results developed for any of these formalisms.
3 Compared with Miller’s original definition, we require patterns to be fully applied.
4 Note that we allow equations such as +(n, 0) ≈ n, in which one of the sides is a metavariable.

44Second-order Church-Rosser modulo, without normalization

Felicissimo

Definition 1 (Unblocking subset of A). Given an abstract rewrite system modulo, we say thata subset U ⊆ A is unblocking for it if:(A) For all a ∈ A there is some b ∈ U with a ∼ b.

(B) For all a, a′ ∈ A and b ∈ U with b ∼ a ≻ a′ we have b ≻ b′ ∼ a′ for some b′ ∈ A.

Condition (B) intuitively states that in elements b ∈ U redexes are maximally unblockedwith respect to ∼, so that if b ∼ a, then any redex that is available in a is also available in b.
(A) then imposes that for every ∼ equivalence class one can always find an element in U.
An interesting consequence of having an unblocking subset U is that we do not need to search
the whole ∼ equivalence class for redexes, but instead we can just appeal to (A) to obtain aterm in which all redexes are available. This motivates us to define the relation ▷U by a ▷U b iffa ∼ c ≻ b for some c ∈ U. We then have the following easy result — in the statement, we thinkof ≻ as orthogonal rewriting, which is why supposing the diamond property is reasonable.
Proposition 1. Suppose that ≻ satisfies the diamond property and that we have an unblocking∗
subset U ⊆ A. Then a (≻ ∪ ≺ ∪ ∼) b implies a ▷∗U ◦ ∼ ◦ ∗U ◁ b.
The main insight of our criterion is then that, under suitable conditions (satisfied for instanceby Example 1), we can find an unblocking subset of terms. The intuition is that the only two
ways that a redex can be blocked in Example 1 is if (1) some collapsable term is inserted in the
middle of the redex (as in @(+(λ(x.t), 0), u), where we have +(x, 0) ≃ x), or (2) some symbolin E matched by a rule left-hand side is not maximally exposed (as in Nrec (+(x, S(y)), p, xy.q),
where S could be exposed using +(x, S(y)) ≃ S(+(x, y))). This motivates the following definition:
Definition 2 (Unblocked terms). A context E is an E-fragment of t if E ∈ T (FE ) and E[u] isa subterm of t for some u. A term t is said to be unblocked if, for all E-fragments E of t:(1) E ≃ □i implies E = □i .

(2) E ≃ f (t) with f ∈ FE ∩ FR implies E = f (t′ ) with t ≃ t′ .
Let us now state the assumptions of our criterion:(i) Equations t1 ≈ t2 ∈ E are linear, and we have mv(t1 ) = mv(t2 ).

(ii) Symbols in FE have a binding arity of the form (0, . . . , 0), the list being possibly empty.

(iii) For every context E ∈ T (FE ), there is some unblocked E ′ ∈ T (FE ) with E ≃ E ′ .
(iv) R is left-linear and no left-hand side is headed by a symbol in FE ∩ FR .
(v) Orthogonal rewriting (=⇒) with R satisfies the diamond property.

The goal of the rest of this section is then to show the following theorem, where we write−→
˜ for the relation defined by t −→˜ t′ iff t ≃ u −→ t′ for some unblocked u.

Theorem 1. Suppose (i)-(v). Then t ≡ u implies t −→˜ ∗ ◦ ≃ ◦ ∗ ←−˜ u for all t, u. In particular,(R, E) is weak Church-Rosser modulo.
Before showing the proof of Theorem 1, let us see how it can be applied to Example 1.
Conditions (i), (ii) and (iv) can be directly verified, whereas (v) follows from the fact that R is
orthogonal [14, Theorem 4.8]. To show (iii), let us first note that each context E ∈ T (FE ) canbe put in a normal-form. Indeed, writing ⟨⃗t⟩ for +(t1 , . . . +(tk−1 , tk ) . . . ) or 0 when ⃗t is empty,
then for each context E ∈ T (FE ) we have E ≃ Sk (⟨□1 , . . . , □n ⟩) for some unique k when E has
n holes. We can easily see that this normal form is unblocked, showing (iii).

45

Second-order Church-Rosser modulo, without normalization

Felicissimo

Proof of Theorem 1
To prove Theorem 1, we set out to show that unblocked terms satisfy properties (A) and (B)of Definition 1 for the abstract rewrite system modulo defined by =⇒ and ≃, which will beachieved by Propositions 2 and 3 respectively, and then apply Proposition 1.
A central tool of our proof is the fact that every term t can be decomposed as t = E[⃗t] where
E is a context with E ∈ T (FE ), and none of the terms in ⃗t is headed by a symbol in FE . We
call E[⃗t] the E-decomposition of t, which is unique modulo renaming of E. A main property ofE-decompositions is that E-conversions can be split along them, in the sense of the following
lemma. Let us write t1 ∼= t2 when we have ti = x or ti = x{⃗vi } and ⃗v1 ≃ ⃗v2 or ti = f (vi ) andv1 ≃ v2 . Let us then write ⃗t1 ∼= ⃗t2 for its pointwise extension to the elements of ⃗ti .
Lemma 1 (Splitting of an E-conversion). Suppose (i), (ii), and t1 ≃ t2 for some t1 , t2 . Writing
E i [⃗ui ] for the E-decomposition of ti , we then must have E 1 ≃ E 2 and ⃗u1 ∼= ⃗u2 .
Proof. By induction on t1 ≃ t2 . For the case ti = ui [σ] with u1 ≈ u2 ∈ E we crucially rely on
the fact that equations are linear, which ensures that matching is completely local.
Lemma 2. Suppose (i), (ii) and that we have t1 ≃ t2 with t1 an unblocked term and t2 a term
not headed by a symbol in FE . Then we have t1 ∼= t2 .
Proof. We consider the E-decompositions ti = E i [⃗ui ] and apply Lemma 1 to get E 1 ≃ E 2 and⃗u1 ∼= ⃗u2 . But because t2 is not of the form f (t) for some f ∈ FE , we must have E 2 = □, andbecause t1 is unblocked we get E 1 = □, so we conclude ⃗ui = ti and thus t1 ∼= t2 .
We can now show that the set of unblocking terms satisfies property (A) of Definition 1.
Proposition 2. Suppose (i)-(iii). For each t, there is some unblocked term u with t ≃ u.
Proof. By induction on t. Case t = x is trivial. Cases t = x{⃗t} and t = f (t) with f ̸∈ FE follow
directly by the ih. For t headed by a symbol in E, consider its decomposition t = E[⃗t]. By ih we′have ⃗u unblocked with ⃗t ≃ ⃗u, so by Lemma 2 we have ⃗t ∼= ⃗u. Finally, by (iii) we get E ∈ T (FE )′′′unblocked with E ≃ E , and so E [⃗u] is unblocked and E [⃗u] ≃ t.
To show that the set of unblocking terms satisfies property (B) of Definition 1 we now only
need the following technical lemma, shown by induction on t1 and using Lemma 2.
Lemma 3. Suppose (i)-(iv), and t1 [σ] ≃ t2 with t2 unblocked and t1 ∈ T (FR ) a linear ⃗x-patternand dom(σ) = mv(t1 ). Then we have t2 = t1 [σ ′ ] for some σ ′ ≃ σ.
In the following, let us write ρ(t =⇒ u) for the number of redexes contracted in t =⇒ u (evenif there might be many derivations of t =⇒ u, the relevant one can be inferred from the context).
Proposition 3. Suppose (i)-(v). If u is unblocked and u ≃ t =⇒ t′ then u =⇒ u′ ≃ t′ andρ(t =⇒ t′ ) = ρ(u =⇒ u′ ).
Proof. By induction on t =⇒ t′ . Almost all cases are either trivial or follow directly by applying
Lemma 2 and the ih, and case l[σ] =⇒ r[σ ′ ] also uses Lemma 3. The case f (t) =⇒ f (t′ ) is moreinteresting, and follows using Lemma 2 when f ̸∈ FE , or using Lemma 1 when f ∈ FE .
Corollary 1. Suppose (i)-(v). If u is unblocked and u ≃ t −→ t′ then u −→ u′ ≃ t′ .
We can now prove Theorem 1. Let us write t =⇒˜ u when t ≃ t′ =⇒ u with some t′ unblocked.

46

Second-order Church-Rosser modulo, without normalization

Felicissimo

Proof of Theorem 1. By Propositions 2 and 3, the set of unblocked terms is unblocking for =⇒and ≃. So by Proposition 1, and the fact that ≡ equals (=⇒ ∪ ⇐= ∪ ≃)∗ , we get that ≡ is
included in =⇒˜ ∗ ◦ ≃ ◦ ∗ ⇐=.
˜ To conclude it now suffices to replace the =⇒˜ by −→.
˜ To dothis, we first show that =⇒˜ is included in −→˜ ∗ ◦ ≃ using Corollary 1, and then we show that=⇒˜ ∗ ◦ ≃ is included in −→˜ ∗ ◦ ≃ by induction on =⇒˜ ∗.
Before concluding this section, let us mention that Theorem 1 can probably be strengthen.
More precisely, we think the requirement that mv(t1 ) = mv(t2 ) in (i) can be dropped, and thatit might be possible to weaken (v) to only require R to be confluent. Assumption (ii) also does
not seem to be essential, and was made here to simplify proofs, because all our use cases satisfy
it. On the other hand, all linearity assumptions are essential in our proof.

4

The second criterion

We now discuss an alternative and much easier criterion, which follows almost directly froma well-known result. In the following, let us write CP± (R1 , R2 ) for the set of critical pairs
between rules of R1 and R2 (see for instance [13] for a definition), and CP(R) for CP± (R, R).
Moreover, given E for which both sides of all equations are headed by symbols and have the same
metavariables5 , let us write E ± for the rewrite system E ∪ E −1 , and note that we have ≃E =−→∗E ± .
Then, given a second-order rewrite system modulo (R ∪ S, E), consider the assumptions:(a) R ∪ S is left-linear(b) For all equations t ≈ u ∈ E, we have t, u linear and headed by symbols, and mv(t) = mv(u)(c) R is confluent(d) (S, E) is strong Church-Rosser modulo(e) CP± (R, S) = ∅ and CP± (R, E ± ) = ∅Theorem 2. Suppose (a)-(e). Then (R ∪ S, E) is strong Church-Rosser modulo.
So to apply Theorem 2 we still have to prove strong Church-Rosser modulo of a smaller system.
The point is that in some cases of interest this smaller system can be strongly-normalizing,enabling the use of criteria that rely on this property. Let us see an example of this.
Example 2. Consider a version of Example 1 in which equations +(t, 0) ≈ t and +(t, S(u)) ≈S(+(t, u)) are removed from E, and in which we consider an additional rewrite system S given by
S := +(t, 0) 7−→ t,+(t, S(u)) 7−→ S(+(t, u)),+(0, t) 7−→ t,+(S(u), t) 7−→ S(+(t, u))Then conditions (a), (b) and (e) can be directly verified, while (c) follows by orthogonality and(d) follows by [13, Theorem 5.11]6 , using the fact that −→S ◦ ≃ is strongly normalizing andthat CP± (E ± , S) ∪ CP(S) ⊆−→!S ◦ ≃E ◦ !S ←−, where −→! denotes reduction to a normal form.
Let us now move to the proof of Theorem 2. As previously mentioned, it can be shown
almost directly from a well-known result, more precisely the following:

Theorem 3 (Shown locally in the proof of Theorem 6.8 in [15]). If R and S are left-linear
Pattern Rewrite Systems (PRSs) with CP± (R, S) = ∅ then they commute.

5 This extra condition on E is important for the definition to make sense. For instance, if E := {+(x, 0) ≈ x},then E ∪ E −1 does not define a rewrite system, as left-hand sides of rewrite rules should be headed by symbols.
6 Actually, [13, Theorem 5.11] is a criterion for confluence modulo, but by [3, Exercise 14.3.7] in this case thisis equivalent to strong Church-Rosser modulo, given that S is strongly normalizing.

47

Second-order Church-Rosser modulo, without normalization

Felicissimo

Proof of Theorem 2. Let us start with the following claim:
Claim 1. We have ≃E ◦ ∗RS ←− ◦ −→∗S ◦ ≃E ⊆−→∗S ◦ ≃E ◦ ∗RS ←−.
Proof of Claim 1. First of all, because (S, E) is strong Church-Rosser modulo, it is easy to seethat it suffices to prove ∗RS ←− ◦ −→∗S ◦ ≃E ⊆−→∗S ◦ ≃E ◦ ∗RS ←−. To do this, we now showthat t nRS ←− ◦ −→∗S ◦ ≃E u implies t −→∗S ◦ ≃E ◦ ∗RS ←− u by induction on n, the base casebeing trivial. For the induction step, we have t RS ←− t′ nRS ←− ◦ −→∗S ◦ ≃E u, so by ih we
get t RS ←− t′ −→∗S ◦ ≃E ◦ ∗RS ←− u. We now do a case analysis on t RS ←− t′ . For the caset R ←− t′ this follows because R commutes with S and E ± (by Theorem 3) and the fact that≃=−→∗E ± . For the case t S ←− t′ this follows because (S, E) is strong Church-Rosser modulo.
We now proceed with the proof of Theorem 2. We have ≡ equal to (−→RS ∪ RS ←− ∪ ≃E )∗ ,nso we prove the theorem by showing that t (−→RS ∪ RS ←− ∪ ≃E ) u implies t −→∗RS ◦ ≃E∗
◦ RS ←− u by induction on n. The base case is trivial, and for the induction step we havent (−→RS ∪ RS ←− ∪ ≃E ) u′ (−→RS ∪ RS ←− ∪ ≃E ) u, and by ih we have t −→∗RS ◦ ≃E∗′
◦ RS ←− u . We conclude by a case analysis on u′ (−→RS ∪ RS ←− ∪ ≃E ) u. Case u′ RS ←− uis trivial. Cases u′ −→S u and u′ ≃E u follow by Claim 1, and case u′ −→R u follows because
R commutes with S and E ± (by Theorem 3) and with itself (by confluence of R).

5

Discussion

In this work, we discussed two criteria for proving Church-Rosser modulo without normalization.
As previously mentioned, Theorem 2 can be shown almost directly from the fact that twoleft-linear PRSs with no critical pairs between them commute, so it might not be original (maybe
it was already clear for others that it could be derived)7 . However, until finding Theorems 1
and 2, it was unclear for us how to prove Church-Rosser modulo for second-order systems with
non-terminating rules, and we think that this problem should be more discussed in the literature.
With Theorem 2 in hand, showing this property can be possible by isolating a terminating
subsystem (S, E), proving it strong Church-Rosser modulo with the criteria available in theliterature (such as [13, Theorem 5.11]), and trying to verify the other hypotheses of Theorem 2 (asillustrated in Example 2). Because of this, we consider important to document here the existenceof Theorem 2 and the strategy of how it can be applied, which will certainly be useful in the future
for showing Church-Rosser modulo in an upcoming version of Dedukti with rewriting modulo [2].
A natural question is then how the two criteria compare. First of all, both of them require
equations to be linear and rewrite rules to be left-linear, two important limitations, but which
seem reasonable: indeed, non-terminating higher-order rules (such as β-reduction) are known
to interact badly with non-left-linearity (see Klop’s countexample [11])8 . Then, some of theother hypotheses seem difficult to compare, and indeed each of our examples (Examples 1 and 2)
only works with one of the two criteria. However, looking closer at the examples, we remark an
interesting point: the unblocked terms in Example 1 turn out to be exactly the normal forms
for the system S in Example 2, so the move from Example 1 to Example 2 replaces the search
for an unblocked term by rewriting with S. The latter option seems more desirable, as it yields
the strong variant of Church-Rosser modulo, instead of just the weak. It is an open question for
us whether there are interesting examples that can be covered by Theorem 1, but which do not
admit a variant covered by Theorem 2, or if the second criterion is always more useful in practice.
7 Let us mention that a similar result is given by Blanqui in [4, Theorem 15], yet it is neither stronger nor
weaker than ours (e.g., it only shows confluence modulo, which is weaker than strong Church-Rosser modulo).
8 An alternative is to consider a setting with confinement to avoid interactions between the higher-order rules
and the equations, as done in [1]. Unfortunately, this would forbid interesting examples like Examples 1 and 2.

48

Second-order Church-Rosser modulo, without normalization

Felicissimo

References[1] Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu. Untyped Confluence In
Dependent Type Theories. working paper or preprint, April 2017.
[2] Bruno Barras, Thiago Felicissimo, and Theo Winterhalter. Towards a logical framework modulo
rewriting and equational theories. In 30th International Conference on Types for Proofs andPrograms (TYPES 2024). https://types2024.itu.dk/abstracts.pdf#section.0.40.
[3] Marc Bezem, Jan Willem Klop, and Roel de Vrijer. Term rewriting systems. 2003.
[4] Frédéric Blanqui. Rewriting modulo in deduction modulo. In Robert Nieuwenhuis, editor, Rewriting
Techniques and Applications, pages 395–409, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.
[5] Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, and François Thiré. A
modular construction of type theories. Logical Methods in Computer Science, 2023.
[6] Alexandre Boudet and Evelyne Contejean. About the confluence of equational pattern rewrite
systems. In Claude Kirchner and Hélène Kirchner, editors, Automated Deduction — CADE-15,
pages 88–102, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.
[7] Thiago Felicissimo. Second-order church-rosser modulo, without normalization. Technical report,
2024. Can be found at http://www.lsv.fr/∼felicissimo/.
[8] Makoto Hamana. Complete algebraic semantics for second-order rewriting systems based on abstract
syntax with variable binding. Mathematical Structures in Computer Science, 32(4):542–573, 2022.
[9] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems:
Abstract properties and applications to term rewriting systems. Journal of the ACM (JACM),
1980.
[10] Jean-Pierre Jouannaud and Hélene Kirchner. Completion of a set of rules modulo a set of equations.
In 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1984.
[11] Jan Willem Klop. Combinatory reduction systems. PhD thesis, Rijksuniversiteit Utrecht, 1963.
[12] Jan Willem Klop, Vincent Van Oostrom, and Femke Van Raamsdonk. Combinatory reduction
systems: introduction and survey. Theoretical computer science, 121(1-2):279–308, 1993.
[13] Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoreticalcomputer science, 192(1):3–29, 1998.
[14] Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. In International Conference
on Typed Lambda Calculi and Applications, pages 306–317. Springer, 1993.
[15] Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: The
higher-order case. Technical report, 1994. http://www.javakade.nl/research/ps/ISRL-94-5.ps.

49

Rule Removal for Confluence∗
Nao Hirokawa1 and Kiraku Shintani2
1

JAIST, Nomi, Japan
hirokawa@jaist.ac.jp
2
Japans.kiraku@gmail.com
Abstract
We show how rule removal criteria for confluence can be derived from compositional
confluence criteria.

1Introduction

Rule removal for confluence is a method to remove unnecessary rules from term rewrite systems(TRSs). The method is characterized as a criterion that identifies an equi-confluent subsystem
S of a TRS R. Here a TRS S is a subsystem of R if S ⊆ R, and R and S are equi-confluent if
confluence of R is equivalent to confluence of S. Confluence criteria often demand terminationor severe syntactic conditions for TRSs. Therefore, rule removal can improve applicability ofconfluence criteria and automated confluence analysis may benefit from this method. However,techniques for rule removal still remain to be explored. Up to our knowledge, the following
trivial criterion is the only known result.
Theorem 1 ([7, 9]). A TRS R and a subsystem S of R are equi-confluent if R ⊆ →∗S .
Example 2. Consider the TRS R:
1 : ((S ◦ x) ◦ y) ◦ z → (x ◦ z) ◦ (y ◦ z)

2 : (K ◦ x) ◦ y → x

3 : ((S ◦ K) ◦ K) ◦ x → x

For the subsystem S = {1, 2} of R the relation ((S ◦ K) ◦ K) ◦ x →∗S x holds. According
to Theorem 1, the TRSs R and S are equi-confluent. Since S is orthogonal, S is confluent.
Hence, R is confluent.
In this note we show how to obtain rule removal criteria. Our idea is to exploit compositional
confluence criteria [6, 7, 10]. Here a compositional criterion means a sufficient condition thatconfluence of a subsystem implies confluence of the original rewrite system. For instance,
consider the following compositional criterion:
Theorem 3 ([7, Corollary 9]). Suppose that S is a subsystem of a TRS R with R ⊆ ↔∗S . If S
is confluent then R is confluent.
Unfortunately, the converse does not hold (consider, e.g., R = {a → b, a → c, b → c} andS = {a → b, a → c}). However, if the converse is somehow guaranteed, the criterion can beused as a rule removal method. In the next section, we present a condition for the converse.
The condition is combinable with any compositional confluence criterion. Using the fact, wedemonstrate rule removal based on compositional versions of orthogonality, rule labeling, andKnuth and Bendix’ criterion (Sections 3, 4, and 5). Throughout the note, we assume familiarity
with term rewriting and the notions of parallel/extended critical pair [1, 3, 5, 11]. The contentsof Sections 2 and 3this note are partly based on our recent publication [10].
∗ Supported by JSPS KAKENHI Grant Number JP22K11900.

50

Rule Removal for Confluence2

Hirokawa and Shintani

A Condition for the Converse

Let R be a TRS and S a subsystem of R. We show that if R↾S ⊆ →∗S then confluence ofR implies confluence of S. Here R↾S stands for the TRS {ℓ → r ∈ R | Fun(ℓ) ⊆ Fun(S)},and Fun(ℓ) and Fun(S) for the sets of all function symbols in ℓ and in S, respectively. The
following auxiliary lemma explains the role of the condition R↾S ⊆ →∗S .
Lemma 1. Suppose R↾S ⊆ →∗S .
(1) If s →R t and s ∈ T (Fun(S), V) then s →∗S t and t ∈ T (Fun(S), V)(2) If s →∗R t and s ∈ T (Fun(S), V) then s →∗S t.
As a consequence of Lemma 1(2), confluence of R carries over to confluence of S, when
the inclusion R↾S ⊆ →∗S holds and the signature of S is Fun(S). The restriction against thesignature of S can be lifted by the fact that confluence is preserved under signature extensions:
Proposition 4. A TRS S is confluent if and only if the implicationt S∗ ← s →∗S u =⇒ t →∗S · S∗ ← uholds for all terms s, t, u ∈ T (Fun(S), V).
Proof. Immediate from the modularity of confluence [13].
Theorem 5 ([10, Theorem 8.3]). Let R be a TRS and S a subsystem with R↾S ⊆ →∗S . If R
is confluent then S is confluent.
Proof. Suppose that R is confluent. It is enough to show the implication in Proposition 4 forall s, t, u ∈ T (Fun(S), V). Suppose t S∗ ← s →∗S u. By confluence of R we have t →∗R v R∗ ← ufor some v. Therefore, Lemma 1(2) yields t →∗S v S∗ ← u.
Theorem 5 enables us to use Theorem 3 as a rule removal method.
Example 6. We show the confluence of the TRS R:
1 : f(x) → x

2 : f(f(x)) → f(x)3 : g(x, x) → g(f(x), f(x))

For the subsystem S = {1, 2} the inclusion R ⊆ ↔∗S holds. Because Fun(S) = {f}, we obtain
R↾S = {1, 2} = S. Thus, R↾S ⊆ →∗S holds. Therefore, R and S are equi-confluent. Since S is
terminating and all critical pairs are joinable, Knuth and Bendix’ criterion applies. Thus, S isconfluent, and hence R is confluent.

3

A Generalization of Orthogonality

In this section we illustrate rule removal based on parallel critical pairs [3]. There is a compositional confluence criterion that originates from orthogonality (see [10, Section 5]), and it
employs a subsystem that can close all parallel critical pairs.
Let t be a term and let P be a set of (pairwise) parallel positions in t. By t[up ]p∈P wedenote the term that results from replacing in t the subterm at p by a term up for all p ∈ P .
P

We write s −−→7 [ t if the parallel step s −−→7 [ t contracts redexes at positions in P .

51

Rule Removal for Confluence

Hirokawa and Shintani

Definition 7. Let R and S be TRSs, ℓ → r a variant of an S-rule, and {ℓp → rp }p∈P a familyϵof variants of R-rules, where P is a set of positions. A local peak (ℓσ)[rp σ]p∈P R ←−7 [ ℓσ →− S rσis called a parallel critical peak between R and S if the following conditions hold:• P is a non-empty set of parallel function positions in ℓ;• none of rules ℓ → r and ℓp → rp for p ∈ P shares a variable with other rules;• σ is a most general unifier of {ℓp ≈ (ℓ|p )}p∈P ; and• if P = {ϵ} then ℓϵ → rϵ is not a variant of ℓ → r.
PϵWhen t R ←−7[ s→− S u is a parallel critical peak, the pair (t, u) is called a parallel critical pairbetween R and S. The set of all parallel critical pairs between R and R is denoted by PCP(R).
Theorem 8 ([10, Theorem 5.4]). Let R be a left-linear TRS and S a subsystem of R with
PCP(R) ⊆ ↔∗S . If S is confluent then R is confluent.
Theorem 8 coincides with weak orthogonality when S = ∅, and generalizes Theorem 3 forleft-linear TRSs as the inclusions PCP(R) ⊆ ↔∗R ⊆ ↔∗S hold.
Example 9. Consider the left-linear TRS R:
1 : ((S ◦ x) ◦ y) ◦ z → (x ◦ z) ◦ (y ◦ z)

2 : (K ◦ x) ◦ y → x 3 : I ◦ x → x 4 : I → (S ◦ K) ◦ K

Let S = {1, 2}. The TRS R admits only one parallel critical pair, and it is joinable by S-steps:
{1}

I◦x

=

((S ◦ K) ◦ K) ◦ x

R

S

ϵ
R

(K ◦ x) ◦ (K ◦ x)

Sx

Because of Fun(S) = {◦, S, K} we obtain R↾S = {1, 2} = S. Thus, according to Theorems 5
and 8, the TRSs R and S are equi-confluent. The latter TRS S is orthogonal, so it is confluent.
Hence, the confluence of R follows. Note that the combination of Theorem 3 and Theorem 5 is
not available for R because no proper subsystem S of R satisfies R ⊆ ↔∗S and R↾S ⊆ →∗S .

4

Rule Labeling

Rule labeling [8, 15] is a powerful confluence method for left-linear TRSs and its compositionalversion is known [10]. Let R be a TRS. Labeling functions are functions from R to N. Givena labeling function ϕ and an integer k, we write Rϕ,k for the TRS {α ∈ R | ϕ(α) ⩽ k}. The
rewrite relation of Rϕ,k is referred to as →ϕ,k . Note that Rϕ,−1 = ∅ as ϕ(α) ⩾ 0. Suppose ϕPand ψ are labeling functions and k, m ∈ N. A peak t ϕ,k ←−7 [ s →ψ,m u is (ψ, ϕ)-decreasing if
∗

∗

P′

max{m,n}−1ϕ,k∗t ←−→ · −−
7→
[ = · ←−−−−−−−→ v = ←−7 [− · ←−−→ u
k−1

ψ,m

m−1

and Var(v, P ′ ) ⊆ Var(s, P ) for some v and set P ′ of parallel positions in v. Here ↔i stands forthe union of ϕ,i ← and →ψ,i , and Var(w, Q) for the union of Var(w|p ) for all p ∈ Q.
Theorem 10 ([10, Theorem 6.5]). Let R be a left-linear TRS and ϕ, ψ labeling functions for R
with Rϕ,0 = Rψ,0 =: S. Assume that the following conditions hold for all (k, m) ∈ N2 \ {(0, 0)}:52

Rule Removal for Confluence

Hirokawa and Shintani
ϵ• Every parallel critical peak of form t ←−7 [− s −−−→ u is (ψ, ϕ)-decreasing.
ϕ,k

ψ,m
ϵ

• Every parallel critical peak of form t ←−7−
[ s −−→ u is (ϕ, ψ)-decreasing.
ψ,m

ϕ,k

If S is confluent then R is confluent.

It is known that Theorem 10 subsumes Theorem 8 and the parallel closedness results by
Huet [4] and Toyama [12, 14], see [10]. We now use this powerful theorem for rule removal.
Example 11. We show the confluence of the left-linear TRS R:
1 : s(x) + y → s(x + y)

3 : (x + y) + z → x + (y + z)

2 : x + s(y) → s(x + y)

4:5:

∞ → s(∞)

d(x) → x + x

6 : d(s(x)) → s(s(d(x)))

Define the labeling functions ϕ and ψ as follows:ϕ(1) = ϕ(2) = ϕ(3) = 0

ϕ(4) = ϕ(5) = 1

ϕ(6) = 2

ψ(1) = ψ(2) = ψ(3) = 0

ψ(4) = ψ(5) = 1

ψ(6) = 2

Then Rϕ,0 = Rψ,0 = {1, 2, 3} := S and the decreasingness conditions in Theorem 10 are
satisfied. For instance, the parallel critical peak between rules 5 and 6 admits the diagram:d(s(x))

=

{ϵ}

ϕ, 1

ψ, 0

s(x + s(x))

s(s(x + x))

ψ, 0

{1}

=

s(x) + s(x)ϵψ, 2s(s(d(x)))ϕ, 1Because Var(s(s(x + x))), {1}) = {x} = Var(d(s(x)), {ϵ}), the peak is (ψ, ϕ)-decreasing. Since
Fun(S) = {s, +}, we obtain R↾S = S ⊆ →∗S . Therefore, by Theorems 5 and 10 the TRSs R and
S are equi-confluent. Since S is terminating and all critical pairs are joinable, the confluenceof S is shown by Knuth and Bendix’ criterion. Hence, R is confluent.

5

A Generalization of Knuth and Bendix’ Criterion

Finally, we illustrate rule removal based on the generalization of Knuth and Bendix’ criterion [6],which is available for non-left-linear TRSs. Given a TRS R, we write R◦ for the extended TRS{ℓ◦ → r | ℓ → r ∈ R}. Here ℓ◦ stands for an arbitrary but fixed linear term that admits avariable substitution σ with ℓ◦ σ = ℓ. TRSs R and S are strongly non-overlapping if there isno overlap between R◦ and S ◦ . For example, the TRSs {f(x, x) → a} and {g(x) → x} arestrongly non-overlapping, and the TRSs {f(x, x) → a} and {f(s(x), x) → b} are not because
f(x, x)◦ = f(x1 , x2 ) and f(s(x), x)◦ = f(s(x3 ), x4 ) are unifiable. When →∗S · →R · →∗S is
terminating, the pair of TRSs R and S, denoted by R/S, is called relatively terminating.
Definition 12 ([5]). Let R and S be TRSs and let ℓ1 → r1 and ℓ2 → r2 be variants of R-rules
having no common variables. Suppose that the following conditions hold:• p is a function position in ℓ2 ;• σ is a substitution in a complete set of S-unifiers of ℓ1 and ℓ2 |p ; and• if p = ϵ then ℓ1 → r1 is not a variant of ℓ2 → r2 .

53

Rule Removal for Confluence

Hirokawa and Shintani

Then the pair ((ℓ2 σ)[r1 σ]p , r2 σ) is called an extended S-critical pair of R. The set of all
extended S-critical pairs of R is denoted by CPS (R).
Theorem 13 ([6, Theorem 2]). Let R and S be strongly non-overlapping TRSs such that R/S
is terminating and CPS (R) ⊆ ↓R∪S . If S is confluent then R ∪ S is confluent.
When S = ∅, the theorem coincides with Knuth and Bendix’ criterion.
Example 14. We show the confluence of the non-left-linear TRS [6, Example 10]:1:2:eq(s(n), x : xs, x : ys) → eq(n, xs, ys)eq(n, xs, xs) → T

3:4:nats → 0 : inc(nats)inc(x : xs) → s(x) : inc(xs)

Let R = {1, 2} and S = {3, 4}. The TRSs R and S are strongly non-overlapping, and thetermination of R/S is shown by, e.g., the termination tool TTT2. Except for the symmetricversion, the TRS R admits the only one S-critical pair originating from eq(s(n), x : xs, x : xs),
and it is joinable by R ∪ S:

eq(n, xs, xs)ϵReq(s(n), x : xs, x : xs)

R∪S

ϵ
R

T

Since Fun(S) = {0, s, :, nat, inc}, we obtain (R ∪ S)↾S = {3, 4} = S. Therefore, the equiconfluence of R ∪ S and S follows by Theorems 5 and 13. As S is orthogonal, S is confluent.
Hence, the original TRS R ∪ S is confluent.

6

Conclusion

We have presented how rule removal criteria can be derived from compositional confluence
criteria. We are currently preparing a next version of the confluence tool Hakusan [10], whereconfluence is analyzed by successive application of rule removal criteria. Experimental data
based on the tool will be reported during the workshop. As we have seen, Theorem 5 is a key
for rule removal. We anticipate that applicability of the theorem is improved by incorporating
modularity results such as layer systems [2].

References[1] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
doi:10.1017/CBO9781139172752.
[2] B. Felgenhauer, A. Middeldorp, H. Zankl, and V. van Oostrom. Layer systems for proving confluence. ACM Trans. Comput. Logic, 16(2):1–32, 2015. doi:10.1145/2710017.
[3] B. Gramlich. Confluence without termination via parallel critical pairs. In Proceedings of 21stInternational Colloquium on Trees in Algebra and Programming, volume 1059 of LNCS, pages
211–225, 1996. doi:10.1007/3-540-61064-2_39.
[4] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems.
Journal of the ACM, 27(4):797–821, 1980. doi:10.1145/322217.322230.
[5] 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. doi:10.1137/0215084.

54

Rule Removal for Confluence

Hirokawa and Shintani[6] D. Klein and N. Hirokawa. Confluence of non-left-linear TRSs via relative termination. In Proceedings of 18th International Conference on Logic Programming and Automated Reasoning, volume7180 of LNCS, pages 258–273, 2012. doi:10.1007/978-3-642-28717-6_21.
[7] J. Nagele, B. Felgenhauer, and A. Middeldorp. Improving automatic confluence analysis of rewrite
systems by redundant rules. In Proceedings of 26th International Conference on Rewriting Techniques and Applications, volume 36 of LIPIcs, pages 257–268, 2015. doi:10.4230/LIPIcs.RTA.
2015.257.
[8] V. van Oostrom. Confluence by decreasing diagrams, converted. In Proceedings of 19th International Conference on Rewriting Techniques and Applications, volume 5117 of LNCS, pages 306–320,
2008. doi:10.1007/978-3-540-70590-1_21.
[9] K. Shintani and N. Hirokawa. CoLL: A confluence tool for left-linear term rewrite systems. In
Proceedings of 25th International Conference on Automated Deduction, volume 9195 of LNCS
(LNAI), pages 127–136, 2015. doi:10.1007/978-3-319-21401-6_8.
[10] K. Shintani and N. Hirokawa. Compositional confluence criteria. Logical Methods in Computer
Science, 20:6:1–6:28, 2024. doi:10.46298/lmcs-20(1:6)2024.
[11] Terese.
Term Rewriting Systems.
Cambridge University Press, 2003.
doi:10.1017/
S095679680400526X.
[12] Y. Toyama. On the Church–Rosser property of term rewriting systems. In NTT ECL Technical
Report, volume No. 17672. NTT, 1981. Japanese.
[13] Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journalof the ACM, 34(1):128–143, 1987. doi:10.1145/7531.7534.
[14] Y. Toyama. Commutativity of term rewriting systems. In Programming of Future Generation
Computers II, pages 393–407. North-Holland, 1988.
[15] H. Zankl, B. Felgenhauer, and A. Middeldorp. Labelings for decreasing diagrams. Journal ofAutomated Reasoning, 54(2):101–133, 2015. doi:10.1007/s10817-014-9316-y.

55

Confluence by the Z-property for De Bruijn’s λ-calculus
with nameless dummies, based on PLFA∗
Vincent van Oostrom
University of Sussex, School of Engineering and Informatics, Brighton, UK
Vincent.van-Oostrom@sussex.ac.uk
Abstract
We discuss the Agda formalisation of a proof of confluence of the untyped λβ-calculus,
more precisely, of the Z-property for De Bruijn’s λ-calculus notation with nameless dummies, based on the latter’s formalisation in Programming Language Foundations in Agda.

Introduction We consider confluence of the rewrite system →β of the λβ-calculus [3].
A sufficient condition for a rewrite system → to be confluent is the Z-property, the existenceof a map • on its objects such that if a → b then b ↠ a• ↠ b• . The Z-property originateswith Loader [14, Section 4.1] for the λβ-calculus with the Gross–Knuth bullet map, and with
Dehornoy [9] for self-distributivity with the full distribution bullet map. See [15] for more on
it and on its theory, e.g. that it is not necessary for confluence.
In [15, Remark 52][10, Conclusions] we claimed that the proof of confluence of →β by meansof the Z-property given there was (a bit) shorter than the proof of the same due to Takahashi [18]via the angle property, the existence of a map • on the objects of → together with a rewrite
system −→◦ with → ⊆ −→◦ ⊆ ↠ and such that if a −→◦ b then b −→◦ a• [19, 15].
Remark. In the same paper we showed [15, Lemma 8] that the Z-property and the angle
property are equivalent. That the proof using the former is (a bit) shorter nonetheless is dueto that it dispenses with introducing the auxiliary rewrite system −→;◦ the •-map suffices.

Here we investigate that claim specialised to a formalisation of the λ-calculus, in particular to the formalisation of it in Agda in Programming Language Foundations in Agda [20].
There, in the module Confluence, a proof of confluence of De Bruijn’s λ-calculus with namelessdummies [7] was formalised via the angle property. We present an alternative formalisation1 ofconfluence via the Z-property; it again is (a bit) shorter than the one via the angle property.
Our alternative formalisation is based on the October 2021 snapshot2 of [20]; it may replace its
Confluence module but is still based on its modules Untyped (formalising De Bruijn’s λ-calculus
with nameless dummies) and Substitution (formalising the so-called Substitution Lemma).
We first describe and comment on the key ingredients of the Agda code from [20] we took
as the basis of our formalisation, the objects and steps of the rewrite system, and motivate why
we did so. We then do the same for our supplementary code, the alternative formalisation ofConfluence, split into: (i) supplementary code (50 loc) showing the system to be a term rewrite
system, (ii) code (65 loc) for the Z-property, and (iii) code (25 loc) for inferring confluence fromZ, supplemented with comments on design decisions. We assume knowledge of rewriting [19]and the λ-calculus [3] with nameless dummies [7].

∗ This work is licensed under the Creative Commons Attribution 4.0 International License L M. The Agda
code was developed in the 1st week of October 2021 based on the then-current version of Programming Language
Foundations in Agda [20] on a MacBook Pro 2019 with Agda 2.6.1.1, Emacs 26.3.
1 HTML source at http://www.javakade.nl/research/agda/plfa.part2.ConfluenceZ4.html (external hyperlinks
do not work; see PLFA) and pure Agda code at http://www.javakade.nl/research/agda/ConfluenceZ4.agda.
2 That snapshot already had the proof via the angle property of the 2022 version of [20], instead of the Tait–
Martin-Löf proof via the diamond property found in its 2020 version, i.e. based on the existence of a rewrite
system −→◦ with → ⊆ −→◦ ⊆ ↠, such that for a −→◦ b and a −→◦ c there is a d with b −→◦ d and c −→
◦ d.

56

Confluence by Z in Agda

V. van Oostrom

Figure 1: Church numeral 2 with names, nameless and scopes (left), and factoring 2 2 →β 4 (right)
Objects of the rewrite system The objects of the rewrite system are the λ-terms with
nameless dummies of [7], obtained by restricting generalised such terms [5, 12] t ::= 0 | St | λt | t t
by requiring t in St to be an index, a unary natural number generated from 0 and S only. Figure 1(left) exemplifies the correspondence between named [3] and nameless [7] (better: uni -named) λterms for the Church numeral 2:=λλ(S0) ((S0) 0) (we employ the notational conventions of [3]).
It is a matter of hygiene to factor a notion for open λ-terms through the same for closed
λ-terms, e.g. it is hygienic to define an open term M to be solvable [3] if its closure M̂ is, i.e.
if M̂ P⃗ =β I for some P⃗ . The formalisation in Untyped follows suit and carves out from theabove λ-terms the closed ones [2, 16] by means of the inference rules (to be read bottom–up):

Here the scoping judgment i ⊢ t asserts that t is a λ-term having i as upper bound on its freeindices, in particular 0 ⊢ t asserts t is closed. See [16, example 3] for a derivation showing 2 isindeed closed. Scoping judgments are implemented in the module Untyped of [20], there split
into separate judgments for indices i and λ-terms t built from them by means of abstraction(λ) and application (@). As is good engineering practice, we reuse it for our formalisation.
Remark. The reason for calling i ⊢ t a scoping judgment in [20] is that making the scopes of
λ-abstractions explicit [12, 16] as boxes, as done in Figure 1 for the Church numeral 2, makes it
clear that each S represents an end-of-scope of, and each 0 a reference to, its λ-abstraction. The
notion of binding for named λ-terms is recovered for nameless λ-terms by the context-free notionof matching parentheses along paths of the abstract syntax tree of the λ-term, viewing each λ asan opening parenthesis ( and each end-of-scope S or reference 0 as a closing parenthesis ) [12].
A box is formed by an abstraction together with its matching end-of-scopes and references.
Design. Since in the λβ-calculus terms are constructed just from abstractions and applications,in the literature [3] one usually abstains from formalising the concept of a symbol / signature [19]to construct terms from. The formalisation in the module Untyped follows suit. For applied
λ-calculi this design choice leads to redundancy, e.g. an inference rule for each construct.
Steps of the rewrite system The →β -steps are generated by closing the β-rule scheme [7]:β : (λt) s → t[s]under contexts, where t[s] denotes substitution of s for the free occurrences of 0 in t; it must
be hygienic in that it should preserve scoping: if i ⊢ (λt) s, i.e. if Si ⊢ t and i ⊢ s, then i ⊢ t[s].

57Confluence by Z in Agda

V. van Oostrom

Figure 2: Alternative substitution (left), scope extrusion (middle) and minimal lifting (right)
Contracting (λt) s can be split into two phases. In the first phase the λ together with its
box are removed and each 0 on it is replaced by s, see Figure 1 (right). This yields a generalised
λ-term, upon which the second phase extrudes any offending scopes, to yield the λ-term t[s].
Contracting (λt) s to t[s] in the module Untyped of [20] factors through subst-zero yielding
a parallel substitution σ mapping 0 7→ s and Si 7→ i implementing the first phase, with thesecond lifting phase brought about during the parallel substitution process t[s] = tσ via subst.3
That subst satisfies the so-called Substitution Lemma [3] is shown in the module Substitutionof [20]. Since our code is modular in it, we reuse also that module.
Remark. The Substitution Lemma is unavoidable in any proof of confluence as it captures theresolution of the critical peak of the β-rule arising from nested redex-patterns (λy.(λx.M ) N )) L:(λy.M [x := N ]) L ← (λy.(λx.M ) N )) L → ((λx.M ) N )[y := L] = (λx.M [y := L])(N [y := L])
in a canonical way by means of a valley, having the Substitution Lemma (SL) in its middle:(λy.M [x := N ]) L → M [x := N ][y := L] =SL M [y := L][x := N [y := L]] ← (λx.M [y := L])(N [y := L])Design. To allow for an algebraic proof of the Substitution Lemma, the module Substitutionof [20] first defines the basic substitution operations corresponding to the explicit substitution
operators of [17], based on [1] but having laws that are complete w.r.t. De Bruijn algebras in thesense that explicit substitution expressions are equivalent iff they are provably equal by meansof the laws. Then these operations are linked to substitutions, the algebraic laws are proven to
hold for substitutions, and finally the Substitution Lemma is proven using the algebraic laws.
The result of taking that indirect approach is that the module Substitution is largish. As itessentially only provides (both to [20] and to our code) the Substitution Lemma subst-commute,it should be feasible and interesting to replace it by a smaller module on a different basis.
E.g., [13] employs only 2 operations, substitution (subst rec) and lifting (lift rec), and 6
laws governing their interaction to formalise the Substitution Lemma in Coq. That development
can be seen as implementing t[s] as t[s]0 followed by maximal scope extrusion as sketched above,
defined in [16], and repeated here in Figure 2. We formalised4 the Substitution Lemma forgeneralised λ-terms in Coq, based on minimal scope extrusion, only extruding scopes as far asneeded to make β-redexes visible [12]. Somewhat surprisingly Huet’s 6 laws still hold.
Design. In the module Untyped of [20] steps are generated as in [3] via the compatible closure,via clauses conventionally called ζ for abstraction and ξ1 and ξ2 for (the arguments of) application. Already here the absence of a signature leads to redundancy (between ξ1 and ξ2 ). The
redundancy will be worse for applied λ-calculi having larger signatures.
3 Now lifting the substitution into a box top–down via its λ, instead of bottom–up via an S as earlier.
4 HTML at http://www.javakade.nl/research/coq/ConfluencebyZofGeneralisedLocalDeBruijninCoq.html.

58

Confluence by Z in Agda

V. van Oostrom

app-cong : ∀{Γ } {K L M N : Γ ⊢ ⋆} → K —↠ L → M —↠ N → K · M —↠ L · N
rew-rew : ∀{Γ } {M N : Γ , ⋆ ⊢ ⋆ } {K L : Γ ⊢ ⋆ }→ M —↠ N→ K —↠ L-------------------→ M [ K ] —↠ N [ L ]Figure 3: Closure of reduction under application (app-cong) and substitution (rew-rew)Term rewrite system To say that we have a term rewrite system [19] is to say that steps (andreductions) are closed under contexts and substitutions [19]. We supplemented the results in [20]with the remaining ones needed to show that, with the main ones being closure of reduction
under application (app-cong) and under substitution (rew-rew), displayed in Figure 3. The 50 loc
needed for it constitute Part I of our formalisation and confirm sanity of the module Untyped.
Remark. For rew-rew, we first showed closure of steps under substitution (stp-subst) after which
we pointwise extended the definition of many-step reduction —↠ to many-step reduction ofsubstitutions —↠s and showed the latter to be closed under term-contexts trm-subst, finallyallowing us to show reductions are closed under substitution for rew-rew, all missing from [20].
Design. Since in the λ-calculus there is only a single rule β, one usually abstains from formalising the concept of a rule, instead giving the corresponding ad hoc rule scheme directly(one can think of the scheme as obtained from the rule by taking all its substitution instances).
Since in the module Untyped there is only one such rule scheme, conventionally [3] called β,this is manageable. However, for applied λ-calculi this would again lead to redundancy.
It should be feasible and interesting to give an alternative formalisation of the untyped λcalculus in [20] as a higher-order term rewrite systems [19, Chapter 9], proceeding in the spiritof [19, Chapter 8] and [6] via a signature of both function and rule symbols, with (multi )steps
simply being terms over that signature, so-called proofterms.
Z To establish the Z-property for →β we follow the approach pioneered by Loader [14] withkey properties outlined in [15, Sections 3.3.1, 3.4] for orthogonal term rewrite systems. We takeas bullet map • the full development map [15, Definition 42], recursively mapping a term M to
the target obtained by contracting all β-redexes in M ; its Agda code is presented in Figure 4.
Remark. For the history of this bullet map for the λ-calculus, going back to Gross, Knuth,
and Takahashi among others, see [4, 15].
Design. I initially tried formalising the Z-property for the full superdevelopment [15, Definition 42] bullet map going back to Aczel, van Raamsdonk and others, cf. [11], inside–out
contracting β-redexes starting from M , but failed. (Defining the full superdevelopment map
was unproblematic but I failed to use it.) It should be of interest to have a single generic proof
that can be instantiated to both the full development and superdevelopment bullet maps.
• : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A(‘ x)• = ‘ x(λλ M)• = λλ (M •)((λλ M) · N)• = M • [ N • ](M · N)• = (M •) ·(N •)Figure 4: Full-development bullet map •59

Confluence by Z in Agda

V. van Oostrom

The Agda code for the four key properties below, taken from [15, Sections 3.3.1, 3.4]5 , with
the Z-property the conjunction of (upperbound) and (monotonic), fitting on one page (Figure 5)
bears witness to the simplicity of the proof of confluence via the Z-property. These 65 locconstitute Part II of the formalisation, its core, the rest being generic / boilerplate code.
(extensive) M ↠β M • (• gives an upperbound);(upperbound) if M →β N then N ↠β M • (• gives an upperbound on all 1-step reducts); ••(rhss) (M • )σ ↠β (M σ )• (applying • to whole exceeds applying it to parts (of the rhs)); and(monotonic) if M →β N then M • ↠β N • (• is monotonic with respect to reduction).

Remark. Each property may be shown either by induction on the term M (and then distinguishing cases on steps (proofterms) M →β N possible from M ) or by induction on M →β N
(and then distinguishing cases on the possible shapes of M ). This choice is largely immaterial.
Here we found it convenient to prove the properties (extensive) and (rhhs) by induction on theterm M , and the properties (upperbound) and (monotonic) by induction on M →β N .
Confluence That the Z-property entails confluence, holds abstractly [15, 8]. We arbitrarily
chose to formalise the first proof of it in [15, Lemma 51], factoring confluence through the Strip
Lemma [3, 20] strip, and that through an easy recombination of (extensive), (upperbound) and(rew-monotonic), the lifting of (monotonic) from steps to reductions. Combining the trivial
formalisation of this final part with that of Parts I,II yields some 140 loc6 confirming our claim.
Conclusion Upon sending comments on the module Confluence to the authors of [20] in thesummer of 2021, Jeremy Siek challenged me to formalise the comments myself. Since for a longtime I had wanted to learn some Agda and in October of that year I had some time on myhands, I then took up the challenge resulting in the current alternative formalisation of thatmodule. It closely followed the pen-and-paper proof [15] and confirmed my comments (that themodule Confluence could be simplified by basing it on the Z-property; its core is only 65 loc).
Formalising was surprisingly smooth (taking a full week only; not knowing Agda), helped bythat the code in [20] is well-explained and modularised, allowing for easy reuse and adaptation.
Accordingly, the proofs of the key properties in Figure 5 are by direct inductions on terms andsteps (proofterms), mostly making use of properties in the modules Untyped and Substitution.
Design. Having renaming and substitution and parallel substitution causes redundancy in [20].
Whether one can easily formalise a proof of confluence of the λ-calculus is often used as alitmus test for proof assistants so formalisations abound [11]. When starting the endeavour I
was not aware of other formalisations of confluence via the Z-property in Agda. At IWC 2023,
I learned from Riccardo Treglia that he had supervised the student project in 2019/2020 of Andrea Laretto on formalising the Church–Rosser theorem for the λ-calculus in Agda (not relyingon [20]). I have tried to initiate a discussion, but that has not materialised yet. The authorsof [20] still have to react to both the original comments and the subsequent formalisation, andthe improvements suggested to the untyped λ-calculus and its confluence mostly still apply.

5 The (rhss) property here is the one which was intended in [15, Lemma 44(Rhs)]. The property (Rhs)•
given there, that M (σ ) reduces to (M σ )• , is correct in it being a trivial consequence of (extensive) and (rhss).
•
However, (Rhs) did not capture the idea that the result ((M • )(σ ) ) of applying the bullet map to the parts (Mσand σ) of the right-hand side of the term rewrite rule (M ) reduces to the result ((M σ )• ) of applying the bullet
map to right-hand side. Consequently, the property (Rhs) given there is too weak to be useful.
6 Of which 50 loc show the λ-calculus in the module Untyped is a term rewrite system so belong in thatmodule, leaving 90 loc for confluence itself in the module Untyped.

60

Confluence by Z in Agda

V. van Oostrom

References[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional
Programming, 1(4):375–416, 1991. doi:10.1017/S0956796800000186.
[2] T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive
types. In Computer Science Logic (CSL ’99), Madrid, 1999, volume 1683 of Lecture Notes in
Computer Science, pages 453–468. Springer, 1999. doi:10.1007/3-540-48168-0\_32.
[3] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103. North-Holland,
Amsterdam, 2nd revised edition, 1984.
[4] H.P. Barendregt, J. Bergstra, J.W. Klop, and H. Volken. Degrees, reductions and representability
in the lambda calculus. Preprint 22, Utrecht University, Department of Mathematics, 1976. URL:
https://dspace.library.uu.nl/handle/1874/15119.
[5] R.S. Bird and R.A. Paterson. de Bruijn notation as a nested datatype. Journal of Functional
Programming, 9(1):77–91, 1999. doi:10.1017/S0956796899003366.
[6] H.J.S. Bruggink. Equivalence of Reductions in Higher-Order Rewriting. PhD thesis, Utrecht
University, 2008. URL: https://dspace.library.uu.nl/handle/1874/27575.
[7] N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem. Indagationes Mathematicae(Proceedings), 75(5):381–392, 1972. doi:10.1016/1385-7258(72)90034-0.
[8] F.L.C. de Moura and L.O. Rezende. A formalization of the (compositional) Z property. Conferenceon Intelligent Computer Mathematics, 2021. URL: http://flaviomoura.info/files/fmm21.pdf.
[9] P. Dehornoy. Braids and Self-Distributivity, volume 192 of Progress in Mathematics. Birkhäuser,
2000.
[10] P. Dehornoy and V. van Oostrom. Z; proving confluence by monotonic single-step upperboundfunctions. In Logical Models of Reasoning and Computation (LMRC-08), Moscow, 2008. URL:
http://www.javakade.nl/research/talk/lmrc060508.pdf.
[11] B. Felgenhauer, J. Nagele, V. van Oostrom, and C. Sternagel. The Z property. Archive of Formal
Proofs, June 2016. URL: https://www.isa-afp.org/entries/Rewriting_Z.shtml.
[12] D. Hendriks and V. van Oostrom. λ. In Proceedings of CADE 19, volume 2741 of Lecture Notes
in Artificial Intelligence, pages 136–150. Springer, 2003. doi:10.1007/978-3-540-45085-6_11.
[13] G. Huet. Residual theory in λ-calculus: a formal development. Journal of Functional Programming,
4(3):371–394, July 1994. doi:10.1017/S0956796800001106.
[14] R. Loader. Notes on simply typed lambda calculus. ECS-LFCS- 98-381, Laboratory forFoundations of Computer Science, The University of Edinburgh, February 1998. URL: http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/.
[15] V. van Oostrom. Z; syntax-free developments. In 6th Conference on Formal Structures for Computation and Deduction (FSCD 2021), Buenos Aires, volume 195 of LIPIcs, pages 24:1–24:22.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.24.
[16] V. van Oostrom, K.J. van de Looij, and M. Zwitserlood. Lambdascope. In Workshop on Algebra
and Logic on Programming Systems, Kyoto, page 9 pp., April 2004. URL: http://www.javakade.
nl/research/pdf/lambdascope.pdf.
[17] S. Schäfer, G. Smolka, and T. Tebbi. Completeness and decidability of de Bruijn substitution
algebra in Coq. In Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP2015), India, pages 67–73. ACM, 2015. doi:10.1145/2676724.2693163.
[18] M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120–127, April
1995. doi:10.1006/inco.1995.1057.
[19] Terese. Term Rewriting Systems. Cambridge University Press, 2003.
[20] P. Wadler, W. Kokke, and J.G. Siek. Programming Language Foundations in Agda. 2024. http://
plfa.inf.ed.ac.uk/20.07/, http://plfa.inf.ed.ac.uk/22.08/, http://plfa.inf.ed.ac.uk/.

61

Confluence by Z in Agda

V. van Oostrom

extensive : ∀ {Γ A} → (M : Γ ⊢ A) → M —↠ M •extensive (‘ ) = ■extensive (λλ M) = abs-cong (extensive M)
extensive ((λλ M) · N) = —→〈 β 〉 rew-rew (extensive M) (extensive N)
extensive (‘ · N) = appR-cong (extensive N)
extensive (L · M · N) = app-cong (extensive (L · M)) (extensive N)
upperbound : ∀ {Γ } → {M N : Γ ⊢ ⋆}→ M —→ N-------→ N —↠ M •upperbound { } {λλ } (ζ ϕ) = abs-cong (upperbound ϕ)upperbound { } {(‘ ) · } { } (ξ 2 ϕ) = appR-cong (upperbound ϕ)upperbound { } {(λλ ) · M} {((λλ ) · M)} (ξ 1 (ζ ϕ)) = —→〈 β 〉 rew-rew (upperbound ϕ) (extensive M)
upperbound { } {(λλ L) · } {.((λλ L) · )} (ξ 2 ϕ) = —→〈 β 〉 rew-rew (extensive L) (upperbound ϕ)upperbound { } {(λλ L) · M} {.(subst (subst-zero M) L)} β = rew-rew (extensive L) (extensive M)
upperbound { } { · · M} {.( · M)} (ξ 1 ϕ) = app-cong (upperbound ϕ) (extensive M)
upperbound { } {K · L · } {.( · · )} (ξ 2 ϕ) = app-cong (extensive (K · L)) (upperbound ϕ)rhss : ∀{Γ ∆} (M : Γ ⊢ ⋆) {σ τ : Subst Γ ∆} → ((x : Γ ∋ ⋆) → τ x ≡ σ x •)----------------------------→ subst τ (M •) —↠ (subst σ M)•
rhss (‘ x) eq rewrite (eq x) = ■rhss (λλ M) eq = abs-cong (rhss M (exts-bullet eq))
rhss ((‘ x) · M) {σ} eq rewrite (eq x) = —↠-trans(appR-cong (rhss M eq)) (app-bullet (σ x) (subst σ M)) where{- auxiliary rhs/monotonicity lemma for application -}app-bullet : ∀{Γ } (L M : Γ ⊢ ⋆) → L • · M • —↠ (L · M)•
app-bullet (‘ ) = ■app-bullet (λλ ) = ( —→〈 β 〉 ■)app-bullet ( · ) = ■rhss ((λλ L) · M) {τ = τ } eq rewrite (sym (subst-commute {N = L •} {M •} {τ })) =rew-rew (rhss L (exts-bullet eq)) (rhss M eq)
rhss (K · L · M) eq = app-cong (rhss (K · L) eq) (rhss M eq)
monotonic : ∀{Γ } → {M N : Γ ⊢ ⋆}→ M —→ N---------→ M • —↠ N •monotonic (ζ ϕ) = abs-cong (monotonic ϕ)monotonic { } {(‘ ) · } {(‘ ) · } (ξ 2 ϕ) = appR-cong (monotonic ϕ)monotonic {Γ } {(λλ M) · N} {.(subst (subst-zero N) M)} β = rhss M bullet-zero where{- bullet commutes with lifting terms to substitutions -}bullet-zero : (x : Γ , ⋆ ∋ ⋆) → subst-zero (N •) x ≡ subst-zero N x •bullet-zero Z = reflbullet-zero (S x) = reflmonotonic { } {(λλ ) · } {(λλ ) · } (ξ 1 (ζ ϕ)) = rew-rew (monotonic ϕ) ( ■)monotonic { } {(λλ M) · } {.((λλ M) · )} (ξ 2 ϕ) = rew-rew (M • ■) (monotonic ϕ)monotonic { } { · · } {(λλ ) · } (ξ 1 ϕ) = —↠-trans (appL-cong (monotonic ϕ)) ( —→〈 β 〉monotonic { } { · · } {(‘ ) · } (ξ 1 ϕ) = appL-cong (monotonic ϕ)monotonic { } { · · } { · · } (ξ 1 ϕ) = appL-cong (monotonic ϕ)monotonic { } { · · } { · · } (ξ 2 ϕ) = appR-cong (monotonic ϕ)■)

Figure 5: Key properties (extensive,upperbound,rhss,monotonic) for confluence of λ-calculus by Z

62

Confluence Competition 2024Rául Gutiérrez1 , Aart Middeldorp2 , Naoki Nishida3 ,Teppei Saito4 , and René Thiemann2
1

Universidad Politécnica de Madrid, Madrid, Spain
Department of Computer Science, University of Innsbruck, Austria
3
Department of Computing and Software Systems, Nagoya University, Japan
4
School of Information Science, JAIST, Japan2

The next few pages in these proceedings contain the descriptions of the tools participating in
the 13th Confluence Competition (CoCo 2024). 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 [2]. This year there were 14 tools(listed in order of registration) participating in 11 categories (listed in order of first appearancein CoCo):
TRS

CTRS

GCR

UNR

UNC

NFP

COM

INF

SRS

CSR LCTRS✓

crest
Hakusan

✓

✓
✓

Moca
✓

CO3
CONFident

✓

✓

✓

✓

✓

✓

infChecker
✓

AGCP
ACP

✓

CeTA

⋆

CSI

✓

FORT-h✓FORTify

⋆

✓

✓

✓

✓
⋆

✓

✓

✓

✓

✓

✓

✓

✓

⋆

⋆

⋆

⋆

⋆

✓
⋆

⋆
✓

✓

CRaris✓NaTTThis year CoCo adopted the new ARI1 format for input problems. In addition, there is new
category (LCTRS) about confluence of logically constrained rewrite systems [1], with two newtools (crest and CRaris). Tools producing certifiable output in a specific category team up with acertifier and participate as combination in that category. The certifiers in CoCo 2024 are CeTA
and FORTify. The latter teamed up with FORT-h. The former with ACP, CSI and Hakusan in
the SRS and TRS categories, with ACP in the COM category, and with Moca in the INF category.
The winning (for combined YES/NO answers) tools2 of CoCo 2023 participated as demonstration tools, to provide a benchmark to measure progress. The live run of CoCo 2024 on
1 https://project-coco.uibk.ac.at/ARI/
2 They are not listed in the table but see http://project-coco.uibk.ac.at/2023/results.php.

63Confluence Competition 2024

CoCo SCStarExec [3] can be viewed at http://cocograph.uibk.ac.at/2024.html. Further information
about CoCo 2024, including a description of the categories and detailed results, can be obtained
from http://project-coco.uibk.ac.at/2024/.
Acknowledgements The CoCo steering committee is grateful to Nao Hirokawa and Fabian
Mitterwallner for their support.

References[1] Cynthia Kop and Naoki Nishida. Term Rewriting with Logical Constraints. In Proc. 9th International
Symposium on Frontiers of Combining Systems, volume 8152 of LNCS (LNAI), pages 343–358, 2013.
doi: 10.1007/978-3-642-40885-4 24.
[2] Aart Middeldorp, Julian Nagele, and Kiraku Shintani. CoCo 2019: Report on the Eighth Confluence Competition. International Journal on Software Tools for Technology Transfer, 2021.
doi: 10.1007/s10009-021-00620-4.
[3] Aaron Stump, Geoff Sutcliffe, and Cesare 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.

64

CoCo 2024 Participant: crest 0.8∗
Jonas Schöpf and Aart Middeldorp
Department of Computer Science, University of Innsbruck, Innsbruck, Austria{jonas.schoepf,aart.middeldorp}@uibk.ac.at

The Constrained REwriting Software Tool (crest, for short) is a tool for automaticallyproving (non-)confluence of logically constrained rewrite systems (LCTRSs). LCTRSs are an
extension of term rewrite systems (TRSs) where rules are equipped with constraints. These
must be satisfied in order for a rule to be applied. Analysis methods for plain TRSs cannot beapplied in this setting, hence special techniques, adapted for LCTRSs, are used.
The development of crest started in the beginning of 2023 as part of the ARI project1 andinitial experiments were presented at CADE-29 in 2023 [3]. More information and executablesof crest can be found at
http://cl-informatik.uibk.ac.at/software/crest/
Currently, crest supports (non-)confluence [2, 3, 4] and limited (non-)termination analysis [2, 1].
The confluence methods mostly rely on closure properties of (parallel) critical pairs. In particular confluence analysis via (weak) orthogonality [2], strong closedness [3], (almost) parallel
closedness [3], (almost) development closedness [4], closure of parallel critical pairs [4] or joinable
critical pairs of terminating LCTRSs [5] is implemented. Moreover, non-confluence is shown by
finding a witness for two different normal forms originating from the same peak.
Input problems in the new ARI format are accepted.2 However, crest extends the format
slightly, e.g. by allowing theory symbols, which are only available in the SMT-LIB logic ofquantifier-free bit-vector arithmetic.3 Also most variable sort annotations, which are mandatory in the LCTRS format, can be omitted due to the implemented type inference algorithm.
Reasoning about the theory part of an LCTRS is utilized via the SMT solver Z3.4
Our tool crest participates in the LCTRS category of CoCo 2024.

References[1] Cynthia Kop. Termination of LCTRSs. CoRR, abs/1601.03206, 2016. doi: https://doi.org/10.
48550/ARXIV.1601.03206.
[2] Cynthia Kop and Naoki Nishida. Term rewriting with logical constraints. In Pascal Fontaine,
Christophe Ringeissen, and Renate A. Schmidt, editors, Proc. 9th International Symposium on
Frontiers of Combining Systems, volume 8152 of Lecture Notes in Artificial Intelligence, pages
343–358, 2013. doi: https://doi.org/10.1007/978-3-642-40885-4_24.
[3] Jonas Schöpf and Aart Middeldorp. Confluence criteria for logically constrained rewrite systems.
In Brigitte Pientka and Cesare Tinelli, editors, Proc. 29th International Conference on AutomatedDeduction, volume 14132 of Lecture Notes in Artificial Intelligence, pages 474–490, 2023. doi:
https://doi.org/10.1007/978-3-031-38499-8_27.
∗ This research is funded by the Austrian Science Fund (FWF) project I 5943-N.
1 https://ari-informatik.uibk.ac.at/
2 https://project-coco.uibk.ac.at/ARI/lctrs.php
3 https://smt-lib.org/logics-all.shtml#QF_BV
4 https://www.microsoft.com/en-us/research/project/z3-3/65

CoCo 2024 Participant: crest 0.8

Schöpf, Middeldorp[4] Jonas Schöpf, Fabian Mitterwallner, and Aart Middeldorp. Confluence of logically constrained
rewrite systems revisited. CoRR, abs/2402.13552, 2024. doi: https://doi.org/10.48550/ARXIV.
2402.13552.
[5] Sarah Winkler and Aart Middeldorp. Completion for logically constrained rewriting. In Hélène
Kirchner, editor, Proc. 3rd International Conference on Formal Structures for Computation and
Deduction, volume 108 of Leibniz International Proceedings in Informatics, pages 30:1–30:18, 2018.
doi: https://doi.org/10.4230/LIPIcs.FSCD.2018.30.

66

Hakusan 0.11: A Confluence Tool
Fuyuki Kawano, Nao Hirokawa, and Kiraku Shintani
JAIST, Japan{f-kawano,hirokawa}@jaist.ac.jp, s.kiraku@gmail.com

Hakusan (https://www.jaist.ac.jp/project/saigawa/) is a confluence tool for left-linear
term rewrite systems (TRSs). It analyzes confluence by successive application of rule removal
criteria [6, 4] based on rule labeling [5, 8] and critical pair systems [3]. Confluence proofs ofHakusan are now verifiable by CeTA [7], see [2].
With a small example we illustrate confluence analysis in our tool. Let R be a TRS andS ⊆ R a subsystem of R. We write PCPS(R, S) for the parallel critical pair system given byϵ{s → t, s → u | t R ←−7 [ s→− R u is a parallel critical peak but not t ←→∗S u}. Moreover, we writeR↾S for the TRS {ℓ → r ∈ R | Fun(ℓ) ⊆ Fun(S)}.
Theorem 1 ([4]). Let R be a left-linear TRS and S ⊆ R. If every parallel critical pair of R is
joinable, PCPS(R, S)/R is terminating, and R↾S ⊆ →∗S then R and S are equi-confluent.
Example 1. Consider the left-linear TRS R:
1 : s(p(x)) → p(s(x))

2 : p(s(x)) → x

3 : ∞ → s(∞)

We show the confluence of R by using the rule removal criteria based on parallel critical pairsystem and rule labeling.
(i) The TRS R admits two parallel critical peaks and the corresponding critical pairs join:s(p(s(x)))

ϵ

s(x)

p(s(p(x)))
p(s(s(x)))

p(p(s(x)))

ϵ

p(x)

Let S = {3}. The parallel critical pair system PCPS(R, S) consists of the four rules:s(p(s(x))) → s(x)p(s(p(x))) → p(p(s(x)))

s(p(s(x))) → p(s(s(x)))

p(s(p(x))) → p(x)By taking the linear polynomial interpretation A on N withsA (n) = 2npA (n) = n + 1∞A = 0

the inclusions PCPS(R, S) ⊆ >A and R ⊆ ⩾A hold. Thus, PCPS(R, S)/R is terminating.
As Fun(S) = {s, ∞} implies R↾S = {3} = S, we obtain R↾S ⊆ →∗S . Therefore, byTheorem 1 the TRSs R and S are equi-confluent.
(ii) As S admits no parallel critical peaks, the rule removal criterion based on rule labeling [4]proves the equi-confluence of S and ∅.
(iii) The empty TRS ∅ is trivially confluent.
Hence the original TRS R is confluent.
As a final remark, our tool employs the SMT solver Z3 [1] for automating the compositional
confluence criteria and the reduction method.

67

References[1] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of 12th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963
of LNCS, pages 337–340, 2008. The website of Z3 is: https://github.com/Z3Prover/z3. doi:
10.1007/978-3-540-78800-3_24.
[2] N. Hirokawa, D. Kim, K. Shintani, and R. Thiemann. Certification of confluence- and commutationproofs via parallel critical pairs. In Proceedings of the 13th ACM SIGPLAN International Conference
on Certified Programs and Proofs, pages 147–161, 2024. doi:10.1145/3636501.3636949.
[3] N. Hirokawa and A. Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47:481–501, 2011. doi:10.1007/s10817-011-9238-x.
[4] N. Hirokawa and K. Shintani. Rule removal for confluence. In Proceedings of 13th International
Workshop on Confluence, 2024. In this proceedings.
[5] V. van Oostrom. Confluence by decreasing diagrams, converted. In Proceedings of 19th International
Conference on Rewriting Techniques and Applications, volume 5117 of LNCS, pages 306–320, 2008.
doi:10.1007/978-3-540-70590-1_21.
[6] K. Shintani and N. Hirokawa. Compositional confluence criteria. Logical Methods in Computer
Science, 20:6:1–6:28, 2024. doi:10.46298/lmcs-20(1:6)2024.
[7] R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In Proceedingsof the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of
LNCS, pages 452–468, 2009.
[8] H. Zankl, B. Felgenhauer, and A. Middeldorp. Labelings for decreasing diagrams. Journal ofAutomated Reasoning, 54(2):101–133, 2015. doi:10.1007/s10817-014-9316-y.

68

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

Overview 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 ARI format, the tool
outputs YES if its infeasibility is proved, and MAYBE otherwise.
New feature This version of Moca can generate certifiable infeasibility proofs in the CPF 3
format. Using this feature, Moca forms a coalition with the certifier CeTA to give new certified
proofs to a number of problems in the infeasibility category.
Techniques Moca implements maximal ordered completion [7] together with approximation
techniques [4], the generalized split-if encoding [1, 4] (akin to unraveling [3, 2]), and inlining forconditional rewrite rules [6]. With a 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 ̸≈ s(x)By applying the split-if encoding the problem reduces to the word problem of deciding T ̸≈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

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:
x−0≈x

0−x≈0

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

f(x − x, y) ≈ T

Now maximal ordered completion builds up the finite ground-complete presentation R of theapproximated equational system:x−0→xf(0, y) → T

0−x→0f(s(x), x) → F

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

Since T↓R ̸= F↓R holds, infeasibility of the conversion x − x ↔∗ s(x) is concluded.

69

References[1] K. Claessen and N. Smallbone. Efficient Encodings of First-Order Horn Formulas in Equational
Logic. In Proc. 9th IJCAR, LNCS 10900, pages 388–404, 2018.
[2] K. Gmeiner, N. Nishida and B. Gramlich. Proving Confluence of Conditional Term Rewriting
Systems via Unravelings In Proc. 2nd IWC, pages 35–41, 2013.
[3] M. Marchiori. Unravelings and Ultra-Properties. In Proc. 5th ALP, LNCS 1139, pages 107–21,
1996.
[4] Y. Oi. Refutation by Completion and Approximations. Master’s thesis, JAIST, 2019.
[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] 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.
[7] S. Winkler and G. Moser. MædMax: A Maximal Ordered Completion Tool. In Proc. 9th IJCAR,LNCS 10900, pages 472–480, 2018.

70

CO3 (Version 2.5)
Naoki Nishida and Misaki Kojima
Nagoya University, Nagoya, Japannishida@i.nagoya-u.ac.jp k-misaki@nagoya-u.jp

CO3, a converter for proving confluence of conditional TRSs,1 tries to prove confluenceof conditional term rewrite systems (CTRSs, for short) by using a transformational approach(cf. [6]). The tool first transforms a given weakly-left-linear (WLL, for short) 3-DCTRS into
an unconditional term rewrite system (TRS, for short) by using Uconf [2], a variant of theunraveling U [8], 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 [7, 3] to prove infeasibility of a condition
w.r.t. a CTRS has been implemented [4]. The approach is applicable to syntactically deterministic CTRSs that are operationally terminating and ultra-right-linear w.r.t. the optimized
unraveling. To prove infeasibility of a condition c, the tool first proves confluence, and thenlinearizes c if failed to prove confluence; then, the tool computes and simplifies a narrowing
tree for c, and examines the emptiness of the narrowing tree. Since version 2.2, CO3 accepts
both join and semi-equational CTRSs, and transforms them into equivalent DCTRSs to prove
confluence or infeasibility [5].
This version has a new disproof criterion for confluence of CTRSs. A CTRS is trivially nonconfluent if there exist a (possibly unconditional) critical pair ⟨s, t⟩ ⇐ c of R and a substitution θsuch that θ satisfies c and sθ, tθ are different constructor terms of R. To find such a substitution
θ, we implemented the following sufficient condition for ⟨s, t⟩ ⇐ s1 ≈ t1 , . . . , sk ≈ tk : Thereexists some i ∈ {1, . . . , k} such that si θ →=R′ ti θ, si θ, ti θ are constructor terms of R, and for allj ∈ {1, . . . , i − 1, i + 1, . . . , n}, sj θ →ε,R′ tj θ, where R′ = {ℓ → r | ℓ → r ⇐ c ∈ R, c = ϵ}. This
criterion works for, e.g., 251.ari and 319.ari in ARI-COPS2 (262.trs and 330.trs, resp.,
in COPS3 ).
Example 1. Consider the 3-DCTRS 251.trs:plus(0, y) → yplus(s(x), y) → plus(x, s(y))
R251 =

f(x, y) → z ⇐ plus(x, y) ↠ plus(z, z ′ )The (conditional) critical pairs of R251 are⟨z, w⟩ ⇐ plus(x, y) ↠ plus(z, z ′ ), plus(x, y) ↠ plus(w, w′ )The first condition plus(x, y) ↠ plus(z, z ′ ) is satisfied by the substitution θ1 = {z 7→ x, z ′ 7→ y},which does not instantiate the second condition plus(x, y) ↠ plus(w, w′ ). The second conditionis satisfied by the second rule of R251 by means of the substitution θ2 = {x 7→ s(x′ ), w 7→
x′ , w′ 7→ y}: plus(x, y)θ2 →R251 plus(w, w′ )θ2 . The composed substitution θ = {z 7→ s(x′ ), z ′ 7→y, x 7→ s(x′ ), w 7→ x′ , w′ 7→ y} is a constructor substitution satisfying the conditional part ofthe critical pair. For the composed substitution θ, zθ and wθ are not joinable because they are
different constructor terms. Therefore, θ is a witness disproving confluence of R251 .
1 http://www.trs.css.i.nagoya-u.ac.jp/co3/
2 https://ari-cops.uibk.ac.at/ARI/
3 https://ari-cops.uibk.ac.at/COPS/

71

CO3

Nishida and Kojima

References[1] K. Gmeiner, B. Gramlich, and F. Schernhammer. On soundness conditions for unraveling deterministic conditional rewrite systems. In A. Tiwari, editor, Proceedings of the 23rd International
Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics, pages 193–208, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012.
[2] K. Gmeiner, N. Nishida, and B. Gramlich. Proving confluence of conditional term rewriting systems
via unravelings. In N. Hirokawa and V. van Oostrom, editors, Proceedings of the 2nd International
Workshop on Confluence, pages 35–39, 2013.
[3] Y. Maeda, N. Nishida, M. Sakai, and T. Kobayashi. Extending narrowing trees to basic narrowing
in term rewriting. IEICE Technical Report SS2018-39, Vol. 118, No. 385, pp. 73–78, the Instituteof Electronics, Information and Communication Engineers, 2019 (in Japanese).
[4] N. Nishida. CO3 (Version 2.1). In M. Ayala-Rinćon and S. Mimram, editors, Proceedings of the
9th International Workshop on Confluence, page 67, 2020.
[5] N. Nishida. CO3 (Version 2.2). In S. Mimram and C. Rocha, editors, Proceedings of the 10th
International Workshop on Confluence, page 61, 2021.
[6] N. Nishida, T. Kuroda, and K. Gmeiner. CO3 (Version 1.3). In B. Accattoli and A. Tiwari, editors,
Proceedings of the 5th International Workshop on Confluence, page 74, 2016.
[7] N. Nishida and Y. Maeda. Narrowing trees for syntactically deterministic conditional term rewriting systems. In H. Kirchner, editor, Proceedings of the 3rd International Conference on Formal
Structures for Computation and Deduction, volume 108 of Leibniz International Proceedings inInformatics, pages 26:1–26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018.
[8] E. Ohlebusch. Termination of logic programs: Transformational methods revisited. Applicable
Algebra in Engineering, Communication and Computing, 12(1/2):73–116, 2001.

72

CONFident at the 2024 Confluence Competition∗
Miguel Vı́tores2 , 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, Spain
mvitvic@posgrado.upv.esslucas@dsic.upv.es1Overview

CONFident 2.0 is a tool which is able to prove confluence of TRSs, CS-TRSs, CTRSs and
CS-CTRSs. The tool is available here:
http://zenon.dsic.upv.es/confident/.
It is written in Haskell implementing the Confluence Framework: we consider two types of problems: confluence problems and joinability problems. Confluence problems encapsulate the different variants of rewrite systems. Joinability problems
encapsulate any possible type of critical pair generated by rewrite systems.
 processors are partial functions that are applied to problems. Our processors encapsulatetechniques for simplification, modular decomposition, problem transformation and directconfluence/joinability checks.

We implement these processors using the logical approach presented in [1, 3, 7] and mechanizing them by external tools like MU-TERM [3], infChecker [1], AGES [2], Prover9 and Mace4 [9]and Barcelogic1 .
Although CONFident 2.0 is the same as last year’s, there were results submitted to conferences or journals before this publication and accepted afterwards. Latest description of thetool can be found now in [4]. Furthermore, a newly documented technique based on the notionof V-orthogonality is presented in [6]. V-orthogonal Generalized Term Rewriting Systems areconfluent. For V-orthogonality, the usual left-linearity requirement for rules is relaxed. However, besides the absence of proper conditional critical pairs, the infeasibility of the conditionalvariable pairs introduced by conditional rules is also required.

References[1] R. Gutiérrez and S. Lucas. Automatically Proving and Disproving Feasibility Conditions. In
N. Peltier and V. Sofronie-Stokkermans, editor, Proc. of IJCAR’2020, LNCS 12167:416–435.
Springer, 2020.
[2] 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.
∗ Partially supported by grants PID2021-122830OB-C42 and PID2021-122830OB-C44 funded by
MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe” and by the grant
CIPROM/2022/6 funded by Generalitat Valenciana.
1 https://barcelogic.com/

73infChecker2.0

Gutiérrez, R. and Lucas, S.

[3] R. Gutiérrez and S. Lucas. MU-TERM: Verify Termination Properties Automatically (System
Description). In N. Peltier and V. Sofronie-Stokkermans, editor, Proc. of IJCAR’2020, LNCS
12167:436–447. Springer, 2020.
[4] R. Gutiérrez. and S. Lucas Proving Confluence in the Confluence Framework with CONFident.
Fundamenta Informaticae, 193, to appear 2024.
[5] R. Gutiérrez, M. Vı́tores and S. Lucas. Confluence Framework: Proving Confluence with CONFident. In A. Villanueva, editor, Proc. of LOPSTR’2022, LNCS 13474:24–43. Springer, 2022.
[6] S. Lucas. Orthogonality of Generalized Term Rewriting Systems. Proc. of IWC’2024, to appear,2024.
[7] S. Lucas. Proving semantic properties as first-order satisfiability. Artificial Intelligence 277, paper
103174, 24 pages, 2019.
[8] S. Lucas and R. Gutiérrez. Use of Logical Models for Proving Infeasibility in Term Rewriting.
Information Processing Letters, 136:90–95, 2018.
[9] W. McCune. Prover9 and Mace4. [online]. Available at https://www.cs.unm.edu/~mccune/mace4/.

274infChecker at the 2024 Confluence Competition∗Raúl Gutiérrez1 , Salvador Lucas2 , and Miguel Vı́tores2
1

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

infChecker is a tool for checking (in)feasibility of sequences of rewrite and relations with respect
to first-order theories, called goals [3]. infChecker participates in the INF category at the
Confluence Competition but it is also used as as a external tool in CONFident, which participatesin several categories in the Competition. In 2024, we participate with the same version as in
2023.
The tool is available here:
http://zenon.dsic.upv.es/infChecker/.
It is written in Haskell implementing the Feasibility Framework: we consider f-problems that are form by a theory and and goal. In the competition, goals
only contain reachability conditions.
 processors are partial functions that are applied to problems. Our processors encapsulatetechniques for simplification, splitting, satisfiability and provability.

Some processors are mechanized using external tools like AGES [2], Prover9 and Mace4 [4].
Latest description of the tool can be found in [1].

References[1] R. Gutiérrez and S. Lucas. Automatically Proving and Disproving Feasibility Conditions. In
N. Peltier and V. Sofronie-Stokkermans, editor, Proc. of IJCAR’2020, LNCS 12167:416–435.
Springer, 2020.
[2] 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.
[3] S. Lucas and R. Gutiérrez. Use of Logical Models for Proving Infeasibility in Term Rewriting.
Information Processing Letters, 136:90–95, 2018.
[4] W. McCune. Prover9 and Mace4. [online]. Available at https://www.cs.unm.edu/~mccune/mace4/.

∗ Partially supported by grants PID2021-122830OB-C42 and PID2021-122830OB-C44 funded by
MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe” and by the grant
CIPROM/2022/6 funded by Generalitat Valenciana.

75

AGCP: System Description for CoCo 2024
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. In this year, no new ground (non-)confluence criterion has
been incorporated from the one submitted for CoCo 2023. Below we provide a brief overview
of AGCP.
AGCP is written in Standard ML of New Jersey (SML/NJ). AGCP proves ground confluenceof 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 ground confluence 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].

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

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

ACP (Automated Confluence Prover) is a tool for proving confluence and some related
properties of (conditional) term rewriting systems. In this year, we have revised methodsfor (dis)proving the UNR property employed in our prover, whose deails are described in [4].
Also, some revision has been done for generating some proofs in CPF format. Below we provide
a brief overview of ACP.
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 supports proving the UNC property (unique normal form property w.r.t. conversion) and the commutation property of term
rewriting systems. The ingredients of the former property have been appeared in [2, 5]. Our(dis)proofs of commutation are based on a development closed criterion [6] and a simple searchfor counter examples.
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] T. Aoto. Proving uniqueness of normal forms w.r.t. reduction of term rewriting systems. submitted,
2024.
[5] 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.
[6] J. Yoshida, T. Aoto, and Y. Toyama. Automating confluence check of term rewriting systems.
Computer Software, 26(2):76–92, 2009.

77

CoCo 2024 Participant: CeTA 3.1
Dohan Kim1 , Christina Kirk1 , Teppei Saito2 , and René Thiemann1
1

2

University of Innsbruck, Austria
Japan Advanced Institute of Science and Technology, JapanThe tool CeTA [1] 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. Below, we present the relevant changes fromlast year’s version (2.45) to this year’s version (3.1). 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 CeTA 3.1 several new term orderings have been added. These can be used in nonjoinability proofs as discrimination pairs, or in infeasibility proofs as co-rewrite pairs. This
includes CoWPO and WPO, also in combination with non-strongly normalizing orders suchas polynomial interpretations with negative coefficients [2]. Moreover, the monotonic semantic
path order and the generalized WPO have become available [3].
For non-joinability proofs [4] for terms s and t we further support the technique of showingthat both s and t only reach a finite set of terms, and that these sets are disjoint.
One of the big differences is the switch to CPF 3, which has the following benefits:• Joining sequences for various confluence and commutation criteria now have a uniform
format. One of the possibilities is to provide just the intermediate terms, without having
to explicitly specify the positions or the applied rules of each rewrite step. Moreover,whenever the join allows arbitrary many steps s →∗ t, then the intermediate terms can beconnected by parallel rewrite steps.
• Rules and terms can be indexed, a technique to reduce the size of certificates. For instancein a modular decomposition it suffices to state that the system is split into rules (A), (B),(E) and rules (C), (D), without having to fully spell out these five rules again.
• Several redundant CPF 2 elements have been removed. For instance, the longish<polynomial><sum><polynomial><variable>1</variable></polynomial><polynomial><coefficient><integer>2</integer></coefficient></polynomial></sum></polynomial>in CPF 2 is just <sum><variable>1</variable><integer>2</integer></sum> in CPF 3
in order to specify the polynomial x1 + 2.

78

References[1] 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 Lecture
Notes in Computer Science, pages 452–468, 2009. doi: 10.1007/978-3-642-03359-9_31.
[2] Akihisa Yamada. Term Orderings for Non-reachability of (Conditional) Rewriting. In Proc. 11th
International Joint Conference, IJCAR 2022, volume 13385 of Lecture Notes in Computer Science,
pages 248–267, 2022. doi: 10.1007/978-3-031-10769-6_15.
[3] Teppei Saito and Nao Hirokawa. Weighted Path Orders Are Semantic Path Orders. In Proc. 14th
International Symposium on Frontiers of Combining Systems, Frocos 2023, volume 14279 of Lecture
Notes in Computer Science, pages 63–80, 2023. doi: 10.1007/978-3-031-43369-6_4.
[4] Takahito Aoto. Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering.
In Proc. 9th International Symposium on Frontiers of Combining Systems, Frocos 2013, volume 8152
of Lecture Notes in Computer Science, pages 311–326, 2013. doi: 10.1007/978-3-642-40885-4_22.

79

CoCo 2024 Participant: CSI 1.2.7
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]. CSI can also produce certificates for confluence
results, which are checked by CeTA.
CSI participates in the following CoCo 2024 categories: NFP, SRS, TRS, UNC and UNR.
Additionally, it participates together with CeTA in the SRS and TRS categories, providing certified
YES/NO answers. In 2023 CSI won the NFP, TRS and SRS categories and came second in the
UNC and UNR categories.
CSI uses the conversion tool1 to transform ARI problems into COPS problems.

References[1] Bertram Felgenhauer. Confluence for Term Rewriting: Theory and Automation. PhD thesis,
University of Innsbruck, 2015.
[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 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] Harald Zankl. Challenges in Automation of Rewriting. Habilitation thesis, University of Innsbruck,2014.

1 https://project-coco.uibk.ac.at/ARI/#conversion

80

CoCo 2024 Participant: FORT-h 2.1
Fabian Mitterwallner and Aart Middeldorp
Department of Computer Science, University of Innsbruck, Austria
fabian.mitterwallner@uibk.ac.at, aart.middeldorp@uibk.ac.at

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]. FORT-h is areimplementation of the tool FORT [4], but is based on a new variant of the decision procedure,
described in [2], 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. More
importantly, it can produce certificates for the YES/NO answers. These certificates can thenbe verified by FORTify, an independent Haskell program that is code-generated from theformalization of the decision procedure in the proof assistant Isabelle/HOL.
A command-line version of FORT-h can be downloaded fromhttp://fortissimo.uibk.ac.at/fort(ify)/
FORT-h participates in the following CoCo 2024 categories: COM, GCR, NFP, TRS, UNC, andUNR. In all six categories it additionally participates together with FORTify [3] to produce
certified YES/NO answers. In 2023 FORT-h had the most YES answers in the UNR category.
Moreover, it won the RELIABILITY1 category.
FORT-h 2.1 accepts input problems in ARI2 format.

References[1] Max Dauchet and Sophie Tison. The Theory of Ground Rewrite Systems is Decidable. In Proc. 5thIEEE Symposium on Logic in Computer Science, pages 242–248, 1990. doi: 10.1109/LICS.1990.113750.
[2] Aart Middeldorp, Alexander Lochmann, and Fabian Mitterwallner. First-Order Theory of Rewriting
for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. Journalof Automated Reasoning, 67(14):1–76, 2023. doi: 10.1007/s10817-023-09661-7.
[3] Fabian Mitterwallner and Aart Middeldorp. CoCo 2024 Participant: FORTify 2.0. In Proc. 13th
International Workshop on Confluence, 2024. This volume.
[4] Franziska Rapp and Aart Middeldorp. FORT 2.0. In Proc. 9th International Joint Conference on
Automated Reasoning, volume 10900 of LNCS (LNAI), pages 81–88, 2018. doi: 10.1007/978-3-31994205-6 6.

1 https://project-coco.uibk.ac.at/2023/results.php#certification
2 https://project-coco.uibk.ac.at/ARI/81

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

The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite
systems. The decision procedure goes back to Dauchet and Tison [1]. In this theory confluencerelated properties on ground terms are easily expressible. An extension of the theory to multiple
rewrite systems, as well as the decision procedure, has been formalized in Isabelle/HOL [2–4].
The code generation facilities of Isabelle then give rise to the certifier FORTify which checks
certificate constructed by FORT-h [6]. FORTify takes as input an answer (YES/NO), a formula,a list of TRSs, and a certificate proving that the formula holds (does not hold) for the given
TRSs. It then checks the integrity and validity of the certificate. A command-line version of thetool can be downloaded fromhttps://fortissimo.uibk.ac.at/fort(ify)/
We refer to the recent article [5] for a detailed description of FORTify.
This year FORTify participates, together with FORT-h, in the following CoCo 2024 categories:
COM, GCR, NFP, TRS, UNC, and UNR.

References[1] Max Dauchet and Sophie Tison. The Theory of Ground Rewrite Systems is Decidable. In Proc. 5thIEEE Symposium on Logic in Computer Science, pages 242–248, 1990. doi: 10.1109/LICS.1990.113750.
[2] Alexander Lochmann. Reducing Rewrite Properties to Properties on Ground Terms, 2022. https://isa-afp.org/entries/Rewrite_Properties_Reduction.html, Formal proof development.
[3] Alexander Lochmann and Bertram Felgenhauer. First-Order Theory of Rewriting. Archive ofFormal Proofs, 2022. https://isa-afp.org/entries/FO_Theory_Rewriting.html, Formal proof
development.
[4] Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, and Thomas
Sternagel. Regular Tree Relations. Archive of Formal Proofs, 2021. https://www.isa-afp.org/
entries/Regular_Tree_Relations.html, Formal proof development.
[5] Aart Middeldorp, Alexander Lochmann, and Fabian Mitterwallner. First-Order Theory of Rewriting
for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. Journalof Automated Reasoning, 67(14):1–76, 2023. doi: 10.1007/s10817-023-09661-7.
[6] Fabian Mitterwallner and Aart Middeldorp. CoCo 2024 Participant: FORT-h 2.1. In Proc. 13th
International Workshop on Confluence, 2024. This volume.

82

CRaris: CR checker for LCTRSs in ARI Style
Naoki Nishida and Misaki Kojima
Nagoya University, Nagoya, Japannishida@i.nagoya-u.ac.jp k-misaki@nagoya-u.jp

CRaris, a CR checker for LCTRSs in ARI style,1 is a tool to prove confluence of logicallyconstrained term rewrite systems (LCTRSs, for short) [4] written in ARI format [1].2 The tool
is based on Crisys2, constrained rewriting induction system (version 2),3 and receives LCTRSs
written in ARI format only to prove confluence, while crisys2 has many functions to e.g., solve
all-path reachability problems [2]. To prove confluence of LCTRSs, the tool uses the following
criteria:• weak orthogonality [4], and• termination and joinability of critical pairs [6].
To prove termination, the tool uses the DP framework for LCTRSs [3] without any interpretation method, together with a criterion for LCTRSs with bitvector arithmetics [5].
The critical pairs of two constrained rewrite rules ρ1 : ℓ1 → r1 [φ1 ] and ρ2 : ℓ2 → r2 [φ2 ]with distinct variables (i.e., Var (ℓ1 , r1 , φ1 ) ∩ Var (ℓ2 , r2 , φ2 ) = ∅) are all tuples ⟨s, t, ϕ⟩ suchthat a non-variable subterm ℓ1 |p of ℓ1 at a position p is unifiable with ℓ2 , “p ̸= ε, ρ1 ̸= ρ2
up to variable renaming, or Var (r1 ) ⊆ Var (ℓ1 )”, the most general unifier γ of ℓ1 |p and ℓ2
respects variables of both ρ1 and ρ2 , i.e., γ(x) is either a value or a variable for all variables x
in Var (φ1 , φ2 ) ∪ (Var (r1 , r2 ) \ Var (ℓ1 , ℓ2 )), (φ1 ∧ φ2 )γ is satisfiable, s = r1 γ, t = (ℓ1 [r2 ]p )γ, and
ϕ = (φ1 ∧ φ2 )γ. The set of critical pairs of an LCTRS R is denoted by CP (R), which includes
all critical pairs of two rules in R ∪ Rcalc . A critical pair ⟨s, t, ϕ⟩ is called trivial if s [ϕ] ∼ t [ϕ].
An LCTRS R is called weakly orthogonal if R is left-linear and all critical pairs of R are trivial.
Theorem 1 ([4]). A weakly orthogonal LCTRS is confluent.
A critical pair ⟨s, t, ϕ⟩ is called joinable if (⟨s, t⟩ [ϕ]) →∗R (⟨s′ , t′ ⟩ [ϕ′ ]) and s′ [ϕ′ ] ∼ t′ [ϕ′ ].
Theorem 2 ([6]). A terminating LCTRS is confluent if all its critical pairs are joinable.
Instead of joinability of critical pairs, the tool uses a much simpler sufficient condition.
Proposition 3. A critical pair ⟨s, s, ϕ⟩ is trivial and thus joinable.
We use “s = t” as a sufficient condition for triviality of ⟨s, s, ϕ⟩.

References[1] T. Aoto, N. Hirokawa, D. Kim, M. Kojima, A. Middeldorp, F. Mitterwallner, N. Nishida, T. Saito,
J. Schöpf, K. Shintani, R. Thiemann, and A. Yamada. A new format for rewrite systems. In
C. Chenavier and S. Winkler, editors, Proceedings of the 12th International Workshop on Confluence, pages 32–37, 2023.
1 http://www.trs.css.i.nagoya-u.ac.jp/craris/
2 https://project-coco.uibk.ac.at/ARI/lctrs.php
3 https://www.trs.cm.is.nagoya-u.ac.jp/crisys/

83

CRarisNishida and Kojima[2] M. Kojima and N. Nishida. Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. Journal of Logical and Algebraic Methods in Programming,
135:1–19, 2023.
[3] C. Kop. Termination of LCTRSs. In Proceedings of the 13th International Workshop on Termination, pages 1–5, 2013.
[4] C. Kop and N. Nishida. Term rewriting with logical constraints. In P. Fontaine, C. Ringeissen, and
R. A. Schmidt, editors, Proceedings of the 9th International Symposium on Frontiers of Combining
Systems, volume 8152 of Lecture Notes in Artificial Intelligence, pages 343–358, Springer, 2013.
[5] A. Matsumi, N. Nishida, M. Kojima, and D. Shin. On singleton self-loop removal for terminationof LCTRSs with bit-vector arithmetic. In A. Yamada, editor, Proceedings of the 19th International
Workshop on Termination, pages 1–6, 2023.
[6] J. Schöpf and A. Middeldorp. Confluence criteria for logically constrained rewrite systems. In
B. Pientka and C. Tinelli, editors, Proceedings of the 29th International Conference on AutomatedDeduction, volume 14132 of Lecture Notes in Computer Science, pages 474–490, Springer, 2023.

84