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

IWC 2024

Introduction

Let us recall:Definition
An abstract rewriting system (ARS) is a pair (A, →), where
A is a set→ is a binary relation on A (reduction)
Definition
An ARS (A, →) is terminating, if there is no infinite sequence
a1 → a2 → a3 → ... (where ai ∈ A)

Confluence

Local confluence∀a, b, c ∈ A (a →∗ b ∧a →∗ c ⇒∀a, b, c ∈ A (a → b ∧ a → c ⇒∃d ∈ A (b →∗ d ∧ c →∗ d))∃d ∈ A (b →∗ d ∧ c →∗ d))

A variant of formulation of Newman’s lemma:
A terminating ARS is confluent if(f) it is locally confluent

Theorem (see footnote 1)
Let (A, →) be an ARS that is simultaneously
1countable (the set A is at most countable)2

acyclic (there is no a ∈ A such that a →+ a )3strictly inductive (every nonempty chain in thepreordered set (A, →∗ ) has a least upper bound).

Then (A, →) is confluent iff it is locally confluent.
Note: if one drops any single precondition among 1-3, theabove mentioned statement becomes invalid1 :Newman’s counterexample:
countable + acyclic + inductive (but not strictly inductive)
Hindley’s counterexample:(at most) countable + strictly inductive (but not acyclic)“Strengthened Newman’s counterexample” 1 :uncountable + acyclic + strictly inductive
1

I. Ivanov. On Newman’s lemma and non-termination, CEUR-WS.org
vol.3624, pp. 14–24, 2024

1. Newman’s counterexample

2. Hindley’s counterexample

3. “Strengthened Newman’s counterexample”

Decreasing diagrams
One can overcome limitations of Newman’s lemma using
Van Oostrom’s decreasing diagrams method 2
Semi-formally, to prove that an ARS (A, →) is confluent:12
3

select a set of labels for reduction steps
select a well-founded partial order ≺ on the set of labels
find a labeled version of a (A, →) that satisfies a condition
reminiscent to the local confluence, but with special
constraints on relations between labels of reduction steps.

Rigorously this can be formulated using the notion of adecreasing Church-Rosser (DCR1 ) ARS
A set of labels, an order on it, and an assignment oflabels to rewrite steps can be thought of as
method parameters
2Vincent Van Oostrom. Confluence by decreasing diagrams. Theoreticalcomputer science 126, pp. 259–280, 1994

Questions about decreasing diagrams method
Some general questions (non-formalized):
are method parameters redundant ?
how restrictions imposed on method parameters influencecapability of the method to be used to prove confluence ?

In part, a setting for studying such questions can beformalized using a hierarchy of subclasses of DCR ARS
introduced by J. Endrullis, J.W. Klop, R. Overbeek3
DCR0 ⊆ DCR1 ⊆ DCR2 ⊆ ...
semi-formally, DCRα is the class of confluent ARS forwhich confluence can be proved with the help of thedecreasing 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 {β | β < α}3

J. Endrullis, J.W. Klop, R. Overbeek. Decreasing diagrams with twolabels are complete for confluence of countable systems, In: FSCD 2018, pp.
14:1–14:15, 2018

Rigorous definition of DCR the hierarchy
Let γ be an ordinal. For any ordinal α denote ⋎α = {β | β < α}Definition
An ARS (A, →) belongs to the class DCRγ , if there exists anindexed∪ family (→α )α∈(⋎γ) of binary relations on A such that→ = α<γ →α and for every ordinals α, β < γ and for every
a, b, c ∈ A, if
a →α b ∧ a →β c,then there exist b′ , b′′ , c ′ , c ′′ , d ∈ A such that() (∗∗∗=∗′ =′′b 99K b 99K b 99K d ∧ c 99K c ′ 99K c ′′ 99K⋎α{β}⋎α ∪⋎β⋎β{α})⋎β ∪⋎αdHere the following notation is used for any set of ordinals K :)+(∪∪∗=→κ→κ 99K = {(a, a) | a ∈ A}∪
99K = {(a, a) | a ∈ A}∪
Kκ∈KK

κ∈K

abbb

α

⋎α*b′{β} =bβb′′b⋎α ∪ ⋎β *bc*⋎βbc′={α}bc*′′⋎β ∪ ⋎αbd

Definition
A subset B ⊆ A is cofinal in an ARS (A, →), if∀a ∈ A ∃b ∈ B a →∗ b.
An ARS (A, →) has the cofinality property, if for everya ∈ A there exists a finite or infinite reduction sequenceb0 → b1 → b2 → ... with b0 = a such that {b0 , b1 , b2 , ...} iscofinal in (X , → ∩(X × X )), where X = {b ∈ A | a →∗ b}.
J. Endrullis, J.W. Klop, R. Overbeek showed4 thatEvery ARS with the cofinality property is in DCR2 .
For countable ARS, confluence ⇔ cofinality property, so
confluence of a (confluent) countable ARS can always be
proved with the help of the decreasing diagrams method
using the label set {0, 1} ordered in such a way that 0 < 1.
4

J. Endrullis, J.W. Klop, R. Overbeek. Decreasing diagrams with twolabels are complete for confluence of countable systems, In: FSCD 2018, pp.
14:1–14:15, 2018

Proposition
An ARS (A, →) is in DCR2 if and only if there exist binary
relations →0 , →1 ⊆ A × A such that → = (→0 ∪ →1 ) and:=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)).

Problems considered in this talk1

Does there exist an (uncountable) confluent ARS outsideof the class DCR2 ?
The obtained answer is YES.

2

Does the DCR hierarchy collapse at the level 2 ?
The obtained answer is NO.

3How can one extend the theorem about
the DCR2 property of ARS with the cofinality property(by J. Endrullis, J.W. Klop, R. Overbeek) ?
The proposed answer will be described below.

Main results
1Existence of an ARS in the class DCR3 \DCR2

2Cofinal connected subgraph theorem

1. Existence of an ARS in the class DCR3 \DCR2Theorem
DCR3 \DCR2 ̸= ∅This result has been formally verified using
Isabelle proof assistant (using HOL logic).
Formal proof:
http://doi.org/10.5281/zenodo.11571490(formal theorems thm 1, thm 2).

Idea of construction of a confluent ARS outside DCR2

DCR2 case 1

DCR2 case 2

DCR2 case 3

Explicit simplified example
The original example of an ARS in the class DCR3 \DCR2
proposed by the author of this talk and formalized inIsabelle can be found in the paper.
Reviewers J. Endrullis, F. van Raamsdonk, J.W. Klop in
their review of the initial version of the paper proposed thefollowing simplified example of a confluent ARS outside
DCR2 :Example
The ARS ({1, 2, 3} × Pfin (R), →), where Pfin (R) denotes the setof all finite subsets of 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.

2. Cofinal connected subgraph theorem
TheoremLet (A, →), (B, →′ ) be ARS and n be a positive integer.
Assume that:1(B, →′ ) is a (not necessarily induced) subgraph of (A, →)2(B, →′ ) is a weakly connected directed graph3

B is cofinal in the ARS (A, →), i.e. ∀a ∈ A ∃b ∈ B a →∗ b.

Then if (B, →′ ) ∈ DCRn , then (A, →) ∈ DCRn+1 .
E.g., if (A, →) has a cofinal reduction sequenceb0 → b1 → ...., one can take (B, →′ ) to be this sequence:(B, →′ ) is trivially in DCR1 , so (A, →) must be in DCR2 .
This result has been formally verified using
Isabelle proof assistant.

2. Cofinal connected subgraph theorembb(A, →) ∈ DCRn+1bbbbb⇑bbbbbCofinal connected subgraph(B, →′ ) ∈ DCRnbbbbbbbbbbbbbbb

Further work

Further investigation of properties of the DCR hierarchy
Generalization of the decreasing diagrams method
Search for new applications of the rewriting theory