=Paper=
{{Paper
|id=Vol-3909/Paper_37.pdf
|storemode=property
|title=On the Cofinality Property in The Context of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems
|pdfUrl=https://ceur-ws.org/Vol-3909/Paper_37.pdf
|volume=Vol-3909
|authors=Ievgen Ivanov
|dblpUrl=https://dblp.org/rec/conf/iti2/Ivanov24
}}
==On the Cofinality Property in The Context of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems==
https://ceur-ws.org/Vol-3909/Paper_37.pdf
On the cofinality property in the context of the hierarchy
of decreasing Church-Rosser abstract rewriting systems
Ievgen Ivanov1,
1
Taras Shevchenko National University of Kyiv, 64/13, Volodymyrska Street, Kyiv, 01601, Ukraine
Abstract
In the paper we extend a result by J. Endrullis, J.W. Klop, R. Overbeek that implies that an abstract
rewriting system (ARS) with the cofinality property belongs to the class DCR 2 of confluent ARS for which
confluence can be proved with the help of the decreasing diagrams method using the set of labels {0, 1}
ordered in such a way that 0<1. Our extension concerns higher levels of the DCR hierarchy (hierarchy of
decreasing Church-Rosser ARS) and explains why the cofinality property is related to the level 2 in this
hierarchy. A formalized version of a variant of the main result has been machine-checked in Isabelle proof
assistant software using HOL logic.
Keywords
computing, formal methods, abstract rewriting system, confluence, proof assistant1
1. Introduction
This paper concerns the theory of uncountable rewriting systems (that may be abstractly viewed as
directed graphs with uncountably many nodes, so, for example, nodes can form the set of all real
numbers, functions, etc.) that may become a part of foundations of the developing field of formal
methods for cyber-physical systems (systems that integrate computational and physical processes
and, for the purpose of analysis and verification, usually require modeling using combinations of
discrete and continuous mathematical models). In this section we give a background information
and motivation concerning the material given in the rest of the paper.
The widely known Church-Turing thesis [1] that underpins a significant part of theoretical
foundations of modern information technology can be formulated by stating that the informal
concept of effective calculability is captured by the formal concept of computability. Early evidence
in favor of such a conclusion includes proofs of equivalence of three formalizations of effectively
calculable functions obtained in 1930s [2, Section 4.1]: Herbrand-Gödel recursive functions [3],
-definable numerical functions [5]. In particular,
-calculus that now can be considered a part of
theoretical foundations of functional programming. The ideas of the -calculus were initially
presented as a part of larger formal systems by A. Church [6, 7] that were intended to provide a
foundation for mathematical logic based on the concept of a function. The mentioned systems were
soon determined to be inconsistent [2, Section 4.1], but the underlying variant of -calculus turned
out to be consistent. The latter fact followed as a consequence of the Church-Rosser theorem [8] that
was later extended by other researchers and used in the context of the rewriting theory [2, Section
5.2] that studies rewriting systems [9, 10, 11] semi-formally, mathematical models that describe
Information Technology and Implementation (IT&I-2024), November 20-21, 2024, Kyiv, Ukraine
Corresponding author.
ivanov.eugen@gmail.com (I. Ivanov)
0009-0002-1378-0539 (I. Ivanov)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
466
Workshop ISSN 1613-0073
Proceedings
computation or automated reasoning as a sequence of steps that transform an object in accordance
with a set of rules.
In the simplest setting of the abstract rewriting theory [9, 10], an abstract rewriting system (ARS)
is pair (A, →) of a set A of elements and a binary relation → on A. Here → is called a reduction
relation, its elements (pairs (a, b) such that a → b) are reduction steps, and the equivalence relation
generated by → is called a convertibility relation. If there is no b such that a → b, then a is called an
irreducible element. If a →* b, and b is irreducible, then b is called a normal form of a. E.g.,
reduction steps can be considered as steps in a computation or automated reasoning process, and
irreducible elements can be considered as possible results (outcomes) of such processes. The
Church-Rosser (CR) property of an ARS, inspired by the Church-Rosser theorem, expresses a link
between conversion and reduction: for every a, b, c in A, if a * b, then there exists c in A such
that a →* c and b →* c, where is the symmetric closure of →, and * is used to denote the
reflexive transitive closure of a binary relation.
In this context, the confluence property of ARS is equivalent to CR (but is formulated
differently). One of the consequences of the CR property (or confluence) is that every element a in
A has no more than one normal form. This can be interpreted in the context of software
engineering as follows: although there may be many possible computation paths that start from a
(e.g., because of concurrent or otherwise nondeterministic implementation of evaluation, in
particular, for performance reasons), it is not possible that two such paths terminate with two
different outcomes (normal forms). This is a desirable assumption when testing potentially
nondeterministic software that implements such computations.
Methods for checking the CR property for different classes of rewriting systems have been
that was published in 1940s, provides a criterion for checking confluence for strongly normalizing
(terminating) ARS (i.e. for ARS that have no infinite reduction sequences a1 → a2 → ...) that reduces
the problem of checking the confluence property to the problem of checking the local confluence
property (that is frequently simpler to check in specific cases). Subsequent influential works
concerning the CR property / confluence for ARS include the works by B.K. Rosen [13], N.G. de
Bruijn [14], G. Huet [15], J.W. Klop [16], V. van Oostrom [17], and other researchers. One notable
development in this research is the decreasing diagrams method [17, 18] by V. van Oostrom
presented in 1990s and subsequent additions to it published in 2000s [19] that unified a number of
previously known confluence criteria for ARS. This method can be considered [20] as an extension
of the work on confluence criteria [14] by N.G. de Bruijn, done in 1970s in the context of research
concerning Automath (an early formal language and software for automated checking of
correctness of mathematical texts that influenced design of a significant number of subsequent
proof assistants).
To show that an abstract rewriting system (A, →) satisfies the CR property using the decreasing
diagrams method, one is required to select a set of labels, ordered by a some well-founded partial
order, and find a labeled version of (A, →) with labels from the former set that satisfies a condition
reminiscent to the local confluence, but with special constraints on the order between labels of
reduction steps that appear in this condition. Soundness of the method is ensured by a theorem [17,
Theorem 3.7] by V. van Oostrom that implies that whenever there is a labeled version of an ARS
that satisfies the above mentioned requirements, the ARS is confluent. Semi-formally, the class of
all confluent ARS for which confluence can be proved with the help of the decreasing diagrams
method is the class of Decreasing Church-Rosser (DCR) ARS (a rigorous definition can be found in
[17, 18]). An example of application of a variant of this method and related constructions can be
found in [21].
Taking into account that a significant number of previously known confluence criteria can be
considered as straightforward consequences of the decreasing diagrams method, in the work [22]
published in 2018, J. Endrullis, J.W. Klop, R. Overbeek considered a possibility of using the
capability of restricted versions of this method to measure complexity of confluence problems.
467
More specifically, they considered restricted variants of the decreasing diagrams method where
n-1 (for a fixed n) with the usual order on them could be used in a labeling
for establishing confluence of an ARS, and, extending this idea, introduced an ordinal-indexed
hierarchy of subclasses of the class of DCR ARS (shortly, DCR hierarchy) such that, semi-formally,
for each ordinal , the class DCR in this hierarchy consists of confluent ARS for which confluence
can be proved with the help of the decreasing diagrams method using the set of labels { | < }
ordered by the usual order on ordinals (rigorous definitions can be found in [22]). In [22] J.
Endrullis, J.W. Klop, R. Overbeek showed that every ARS that has the cofinality property
(previously considered by J.W. Klop [16]) belongs to the class DCR2 (is at the level 2 of the DCR
hierarchy). In particular, this implies that confluence of any confluent countable ARS (relevant e.g.
for modeling discrete processes) can be shown with the help of the decreasing diagrams method
using the label set {0, 1} with the usual order. The authors of [22] concluded that the size of the
label set is not a suitable measure for complexity of a confluence problem. However, a number of
other questions about the DCR hierarchy remained open, including the question on whether it
collapses already at the level 2.
In 2024 (see [23]) the author of this work obtained a machine-checked proof (in Isabelle proof
assistant [24] using HOL logic) that the DCR hierarchy does not collapse at the level 2. Thus despite
the fact that the label set size is not suitable for measuring complexity of confluence problems for
countable ARS, it still has a certain, not entirely trivial meaning for uncountable ARS. The latter
can be relevant to formal methods applied to cyber-physical systems [25], for ideas on relations
between the rewriting theory and modeling of such systems see [26].
These considerations motivate further investigation of properties of the DCR hierarchy.
In this paper we continue the work [23] and describe a new result (Theorem 3.1 in Section 3
below) that extends the theorem [27, Theorem 4.10] by J. Endrullis, J.W. Klop, R. Overbeek (that
implies that any ARS with the cofinality property belongs to DCR2,). The result proposed in this
paper concerns higher levels of the DCR hierarchy and explains why the cofinality property is
related to the level 2 of this hierarchy. A formalized version of a variant of the main result for finite
levels of the DCR hierarchy has been machine-checked in Isabelle proof assistant software using
HOL logic.
2. Preliminaries
A reader can assume that a background theory for understanding definitions and propositions
given below is von Neumann-Bernays-Gödel set theory [28] with the axiom of global choice and
that a correspondence between non-formalized notions in the paper and formalized notions in
Isabelle/HOL formalization is similar to the one described in [29, 30].
We will denote as , , , the logical negation, conjunction, disjunction, and implication
respectively. To denote that a pair (a, b) is in a binary relation R aRb
a, b) R A, we will use the following notation for any binary relation r AA:
• Fld(r) = { a | b (a, b) r } { b | a (a, b) r } is the field of r
• r -1 = { (b, a) | (a, b) r } is inverse of r
• r + is the transitive closure of r
• r = = r { (a, a) | a A } is the reflexive closure of r on A, if A is clear from the context or is
mentioned explicitly
• r* = r + { (a, a) | a A } is the reflexive transitive closure of r on A, if A is clear from the
context or is mentioned explicitly.
An abstract rewriting system (ARS) is a pair (A,→), where A is a set and → AA is a binary
relation on A (reduction).
An ARS (A, →)
• is confluent, if a, b, c A (a →* b a →* c ( d A b →* d c →* d )
• is countable [22], if there is a surjective function from the set of natural numbers to A
468
• is uncountable, if it is not countable.
An ARS (A, →) has the cofinality property [22], if for every a A there exists a finite or infinite
reduction sequence b0 → b1 → b2 → a = b0 and for every b A such that a →* b there
is an element bi in the above mentioned reduction sequence such that (b, bi) (→)* , where →
denotes → ({ bA | a →* b } { bA | a →* b }), i.e. the restriction of → to { bA | a →* b }.
An ARS (A, →) belongs to the class DCR [22, Definition 15], where is an ordinal, if there exists
an indexed family (→i)iI of binary relations →i AA indexed by ordinals below , i.e. I = {i | i < }
such that → = iI (→i) and for every ordinals , < and elements a, b, c A,
if a → b and a → c, then there exist b, b, c, c, d A that satisfy the following two conditions:
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)* ,
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)* ,
where
• →< denotes the union i< (→i) of relations →i for ordinals i<,
• →<< denotes the union i<i < (→i) of relations →i for ordinals i such that i< or i<,
• upper indices = and * are used to denote, respectively, the reflexive closure and the
reflexive transitive closure of a relation on A.
Known relations between the notions mentioned above include:
1. if , then DCR DCR, i.e. classes DCR form a hierarchy, called here the DCR
hierarchy
2. for every , every ARS in DCR is confluent (follows from [17, Theorem 3.7])
3. for every decreasing Church-Rosser ARS (A, →) [17], [22, Definition 13] there is an ordinal
such that (A, →) belongs to the class DCR (follows from [22, implication (2)])
4. every confluent countable ARS has the cofinality property [16], [22, Theorem 9]
5. a confluent uncountable ARS may or may not have the cofinality property [22, footnote 3]
6. there exists an ARS in DCR1 that does not have a cofinality property [22, footnote 3]
7. every ARS with the cofinality property belongs to DCR2 (follows from [22, Theorem 19])
8. DCR3 \ DCR2 (follows from [23, Theorem 1, Theorem 2]).
To further clarify the above mentioned notions, in Table 2.1 we give a few examples of ARS
(A, →) in the class DCR1 (that are slight modifications of [22, footnote 3]).
Note that an ARS that belongs to DCR for some cannot simultaneously be countable and lack
the cofinality property (by the items 2 and 4 given above).
3. Main result
For any ARS (A, →), (B, →) we will say that:
• (A, →) is weakly connected, if a1 * a2 for all a1, a2 A, where = → →-1
• (B, →) is a subgraph of (A, →), if B A and → →.
If A is a set and A A is a reflexive and transitive relation, the pair (A, ) is a preordered set.
A subset B A is cofinal in a preordered set (A, ), if aA bB a b.
Note that for any ARS (A, →), the pair (A, →*) is a preordered set.
The following theorem is the main result of the paper.
Theorem 3.1. Let (A, →), (B, →) be ARS such that (B, →) is a weakly connected subgraph of
(A, →) and B is a cofinal subset in the preordered set (A, →*).
Then for any nonzero ordinal , if (B, →) belongs to DCR , then (A, →) belongs to DCR+1 .
469
A proof of Theorem 3.1 is given in Section 4 below. A machine-checked proof of a formalized
version of Theorem 3.1 restricted to < is described in Section 6.
Table 2.1
Examples of ARS
No Set A is: Reduction relation → Is ARS (A,→) Does (A, →) have
. on A is: countable ? the cofinality
property ?
1 the set of all the set of all pairs of the Yes Yes
finite subsets form (a, a { x } ), where
of the set of all a A,
natural numbers x is a natural number
2 the set of the set of all pairs of the No Yes
all subsets form (a, a { x } ), where
of the set of all a A,
natural numbers x is a natural number
3 the set of all the set of all pairs of the No No
finite subsets form (a, a { x } ), where
of the set of all a A,
real numbers x is a real number
Remark 3.1. Semi-formally, in the case of finite the theorem can be understood to imply that
for an uncountable, weakly connected, confluent ARS (A, →
its confluence with the help of the decreasing diagrams method, as measured by the size of the
connected subgraph (B, →), where B is cofinal in (A, →*)).
A more detailed interpretation is as follows. Assume that 0<<, corresponds to a positive
integer n, (A, →) is an ARS, and there is a weakly connected subgraph (B, →) of (A, →) such that
• (B, →) is confluent and its confluence can be proved with the help of the decreasing
diagrams method using n B, →) belongs to
DCR
• from any given element a A it is possible to reach some element of B by following
reduction steps in → (this is expressed by the cofinality assumption in Theorem 3.1).
Then (A, →) is a confluent ARS such that its confluence can be proved with the help of the
decreasing diagrams method using n+ A, →) belongs
to DCR+1
Remark 3.2 A, →) belongs to DCR+1
A, →) belongs to DCR
Corollary 3.1. Let be a nonzero ordinal and (A, →) be an ARS. Assume that for every aA
there exists an ARS (B, →) such that
1. (B, →) is a weakly connected subgraph of (A, →),
2. (B, →) belongs to DCR ,
3. B is a cofinal subset in the preordered set (Aa, →a*), where Aa = {b A | a →* b} and
→a = → (Aa Aa).
Then (A, →) belongs to DCR+1.
The proof of Corollary 3.1 is given in Section 5 below.
Example 3.1. As a special case of application of Corollary 3.1 from Theorem 3.1, consider a
situation when (A, →) is an ARS that has the cofinality property.
470
Let a be an arbitrary element of A. Then, by the cofinality property of (A, →), there exists a
(nonempty) finite or infinite reduction sequence b0 → b1 → b2 → I (that is
k} for some non-negative integer k, or the set of all non-negative integers) such that
a = b0 and for every b A such that a →* b we have (b, bi) (→)* for some index i I, where →
is the restriction of → to {bA | a →* b}.
Let B = {bi | i I} and → = { (bi, bi+1) | i I i+1 I }. Then, trivially, (B, →) is an ARS that is a
weakly connected subgraph of (A, →) and that belongs to the class DCR1 (since (B, →) is confluent
and all reduction steps in → can be labeled with 0 for the purpose of proving confluence of (B, →)
with the help of the decreasing diagrams method).
Moreover, B is a cofinal subset in the preordered set (Aa, →a*), where Aa = {bA | a →* b} and
→a = → (Aa Aa), because B {bA | a →* b} and for every b Aa we have bA a →* b, so
for some bi B, (b, bi) (→)*, where
→ = → ( {bA | a →* b} {bA | a →* b} ) = → (Aa Aa) = →a*.
Then by Corollary 3.1, (A, →) belongs to DCR1+1 = DCR2.
Example 3.1 provides an explanation of why the cofinality property is related to the level 2 in
the DCR hierarchy (the cofinality property is formulated in terms of a cofinal reduction sequence
that can be considered as a weakly connected subgraph that belongs to the class DCR1), and
Theorem 3.1 and Corollary 3.1 suggest how its analogs are related to higher levels of the DCR
hierarchy (e.g. DCR3 is indeed a proper superclass of DCR2 by the result of [23]).
4. Proof of Theorem 3.1
Firstly, let us formulate and prove several auxiliary lemmas.
Lemma 4.1. Let be an ordinal, U be a set, and s, r be relations such that
s r U U. Assume that
1) a, b Fld(s) c Fld(s) (a, c) s* (b, c) s*
2) (U, s) is an ARS in the class DCR
3) a Fld(r) b Fld(s) (a, b) r=
4) { b | a Fld(s) (a, b) r \ s } Fld(s)
Then (U, r) is an ARS in the class DCR+1.
Proof.
By the assumption 2, (U, s) is in DCR , so there exists an indexed family (→i)iI of relations
→i UU, where I = {i | i < }, such that s = i I (→i) and for every , < and a, b, c U, if
a → b and a → c, then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)*
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*
where →< denotes i< (→i) and →<< denotes i< i < (→i), and the upper indices = and * are
used to denote, respectively, the reflexive and the reflexive transitive closure of a relation on U.
Let J = {i | i < + 1}. Then I J and J \ I.
Let us introduce an indexed family (→j)jJ of binary relations →j on U, where for each j J,
• →j = →j , if j I
• →j = r \ s , if j J \ I .
Moreover, for any , < +1 let →< denote j< (→j) and →<< denote j< j < (→j).
Since s r and J \ I , we have
r = s (r \ s) = ( i I (→i)) ( j J \ I (→j)) = j J (→j).
Let us show that for every , < +1 and a, b, c U, if a → b and a → c, then there exist b,
b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)* (1)
471
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)* (2)
Let , < +1 and a, b, c U be elements such that a → b and a → c.
Consider the following cases.
Case 1: I and I. Then →< = →< , →<< = →<< , → = → , and → = → , and
there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)*,
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*.
Thus (1) and (2) hold.
Case 2: I and J \ I. Then a → b and (a, c) r \ s, and so (a, b) s and (a, c) r \ s. Then
a, b Fld(s), and from the assumption 4 it follows that c Fld(s). Then from the assumption 1 it
follows that there exists d Fld(s) such that (b, d) s* (c, d) s*. Note that s →<< . Then (1),
(2) hold for b = b = b, c = c = c, and the above mentioned element d.
Case 3: J \ I and I. Then (a, b) r \ s and a → c, and so (a, b) r \ s and (a, c) s. Then
a, c Fld(s), and from the assumption 4 it follows that b Fld(s). Then from the assumption 1 it
follows that there exists d Fld(s) such that (b, d) s* (c, d) s*. Note that s →<< . Then (1),
(2) hold for b = b = b, c = c = c, and the above mentioned element d.
Case 4: J \ I and J \ I. Then (a, b) r \ s and (a, c) r \ s. Then b, c Fld(r). From the
assumption 3 it follows that there exists b Fld(s) such that (b, b) r= ((b, b) s b = b),
because if b Fld(s), then one can take b = b, otherwise b can be obtained from the assumption 3
applied to b and (b, b) s cannot hold. Similarly, from the assumption 3 it follows that there exists
c Fld(s) such that (c, c) r= ((c, c) s c = c). Then (b, b) (r \ s)= and (c, c) (r \ s)=.
Moreover, from the assumption 1 it follows that there exists d Fld(s) such that
(b, d) s* (c, d) s*. Note that s →<< , and, moreover, (b, b) (→)= and
(c, c) (→)=. Then the conditions (1), (2) hold for b = b, c = c, and the mentioned b, c, d.
We conclude that (U, r) is an ARS in the class DCR+1 .
Lemma 4.2. Let be an ordinal, U be a set, and s, r be relations such that
s r U U. Assume that
1) Fld(s) = Fld(r)
2) a, b Fld(s) c Fld(s) (a, c) s* (b, c) s*
3) (U, s) is an ARS in the class DCR
Then (U, r) is an ARS in the class DCR+1.
Proof.
Since Fld(s) = Fld(r) by the assumption 1, we have a Fld(r) b Fld(s) (a, b) r= and
{ b | a Fld(s) (a, b) r \ s } Fld(r) = Fld(s). Then from the assumptions 2, 3 it follows that , U,
s, r satisfy all assumptions of Lemma 4.1. Thus (U, r) is an ARS in DCR+1 by Lemma 4.1.
Lemma 4.3. Let be a nonzero ordinal, U be a set, s, r be relations such that s r U U and
the following conditions hold:
1) a, b Fld(s) c Fld(s) (a, c) s* (b, c) s*
2) (U, s) is an ARS in the class DCR
3) a Fld(r) b Fld(s) (a, b) r*.
Then (U, r) is an ARS in the class DCR+1 .
Proof.
By the assumption 2, (U, s) is in DCR , so there exists an indexed family (→i)iI of relations
→i UU, where I = {i | i < }, such that s = i I (→i) and for every , < and a, b, c U, if
a → b and a → c, then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)*
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*
472
where →< denotes i< (→i) and →<< denotes i< i < (→i), and the upper indices = and * are
used to denote, respectively, the reflexive and the reflexive transitive closure of a relation on U.
For every a Fld(r) denote:
• d(a) is the least non-negative integer such that there exists b Fld(s) such that (a, b) ri
where for i>0, ri ={(a, b) | c0,c1 ci U c0=a ci=b k i-1} (ck, ck+1) r } and
r0 denotes the set {(a, a) | a U}. Note that d(a) is well-defined (i.e. there exists an integer
specified above), because of the assumption 3.
• B(a) = { b | (a, b) r }, i.e. B(a) is the set of direct successors of a w.r.t. r
• H(a) = { b B(a) | c B(a) d(b) d(c) }.
Let us denote:
D = Fld(r) \ Fld(s).
Let us show that H(a) for every a D. If a D, then by the assumption 3, there exists
b Fld(s) such that (a, b) r*, then b D, whence b a and (a, b) r+, so there exists b such that
(a, b) r, then B(a) , which implies that H(a) . Thus H(a) for every a D.
Note that since r U U, for every a D, H(a) is a non-empty subset of U. Then, using the
axiom of choice, there exists a (choice) function h : D → U such that for every a D, h(a) H(a).
Let us denote:
g1 = { (a, h(a)) | a D }.
Let us introduce an indexed family (→i)iI of binary relations →i on U, where I = {i | i < }
(as we have defined above) and for each i I,
• →i = →i g1, if i = 0
• →i = →i , if i I \ {0}.
Note 0 I, because is a nonzero ordinal.
Moreover, for any , < let →< denote j< (→j) and →<< denote j< j < (→j).
Let us denote:
r1 = i I (→i).
Note that although →0 = →0 g1 , no two rewrite steps that belong to →i and g1 respectively
cannot start in the same element: if a →0 b and (c, d) g1, then (a, b) s and c D, so a Fld(s)
and c Fld(s), so a c. Using this fact and the fact the g1 is a functional relation (i.e. if (a, b) g1
and (a, c) g1, then b = c), it is straightforward to check that for every , < and a, b, c U, if
a → b and a → c, then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)*
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*.
Then (U, r1) is an ARS in the class DCR .
Note that (a, b) r for every a D and b H(a), so (a, h(a)) r for every a D, whence g1 r.
Moreover, i I (→i) = s r, so r1 = i I (→i) r. Note that Fld(r) \ Fld(s) = D Fld(g1) Fld(r1),
and s = i I (→i) r1, so Fld(s) Fld(r1). Then Fld(r1) Fld(r). Also Fld(r) Fld(r1), because r1 r,
so Fld(r1) = Fld(r).
Let us show that a Fld(r1) b Fld(s) (a, b) r1* (where the symbol * is used to denote the
reflexive transitive closure of a relation on U specifically). Using the definition of H it is
straightforward to show that for every non-negative integer k, for every a D, if d(a) = k + 1, then
h(k)(a) D, d(h(k)(a)) = 1, and (a, h(k)(a)) g1*, where h(k)(a) = h(h a h is applied k times,
and it is assumed that h (a) = a. Note that for every a D, d(a) > 0, because a Fld(s). Then for
(0)
every a D there exists a D (e.g. h(k)(a)) such that d(a) = 1 and (a, a) g1*.
Let a Fld(r1). If a Fld(s), then for b = a we have b Fld(s) and (a, b) r1*. So consider the
case when a Fld(r1) \ Fld(s). Then a Fld(r) \ Fld(s) = D. Then, as we have shown above, for a
there exists a D such that d(a) = 1 and (a, a) g1*. Then (a, h(a)) r1 and h(a) H(a).
Moreover, since d(a) = 1, there exists b Fld(s) such that (a, b) r. Then b B(a) and d(b) = 0.
473
Note that h(a) H(a), so c B(a) d(h(a)) d(c), and, in particular, d(h(a)) d(b) = 0, whence
d(h(a)) = 0. Then h(a) Fld(s) and (a, a) g1* r1*.
We conclude that
a Fld(r1) b Fld(s) (a, b) r1*.
Let us show that
a, b Fld(r1) c Fld(r1) (a, c) r1* (b, c) r1*.
As we have shown above, a Fld(r1) b Fld(s) (a, b) r1*. Let a, b Fld(r1). Then there exist
a, b Fld(s) such that (a, a) r1* and (b, b) r1*. Then by the assumption 1 applied to a, b,
there exists c Fld(s) such that (a, c) s* (b, c) s*. Since s r1, we have
(a, c) r1* (b, c) r1*
using transitivity of r1* and c Fld(r1). We conclude that
a, b Fld(r1) c Fld(r1) (a, c) r1* (b, c) r1*.
Then all assumptions of Lemma 4.2 hold for , U, r1, r, and we conclude that (U, r) is an ARS in
the class DCR+1 by Lemma 4.2 applied to , U, r1, r.
Lemma 4.4. Let be a nonzero ordinal, U be a set, A U, s, r be relations such that s r A
A, and B = Fld(s). Assume that (B, s) is a weakly connected ARS, B is a cofinal subset in the
preordered set (A, r*), and (U, s) is an ARS in the class DCR .
Then (U, r) is an ARS in the class DCR+1 .
Proof.
Let us show that the assumption 1, 2 of Lemma 4.3 holds for U, s, r.
Firstly, let us show that a, b Fld(s) c Fld(s) (a, c) s* (b, c) s*.
Let a, b Fld(s). Then a, b B, so (a, b) (s s-1)*, because (B, s) is weakly connected.
Moreover, since (U, s) is an ARS in DCR , (U, s) has the Church-Rosser property, so there exists
c U such that (a, c) s* (b, c) s*. Then since a Fld(s), we have c Fld(s). We conclude that
a, b Fld(s) c Fld(s) (a, c) s* (b, c) s*.
We have
a Fld(r) b Fld(s) (a, b) r*,
because B = Fld(s) and B is a cofinal subset in the preordered set (A, r*).
Since (U, s) is an ARS in DCR , we conclude that (U, r) is an ARS in DCR+1 by Lemma 4.3 applied
to , U, s, r.
Lemma 4.5. Let be a nonzero ordinal, U be a set, r, r U U, A U. Assume that (U, r) is an
ARS in the class DCR and r = r {(a, a) | a A}. Then (U, r) is an ARS in the class DCR .
Proof.
Since (U, r) is in DCR, there exists an indexed family (→i)iI of relations →i UU, where
I = {i | i < }, such that r = i I (→i) and for every , < and a, b, c U, if a → b and a → c,
then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)*
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*
where →< denotes i< (→i) and →<< denotes i< i < (→i), and the upper indices = and * are
used to denote, respectively, the reflexive and the reflexive transitive closure of a relation on U.
Let us introduce an indexed family (→i)iI/ of binary relations →i on U, indexed by the same set
I = {i | i < } as (→i)iI , where for each i I, →i = →i {(a, a) | a A}. Then since is a nonzero
ordinal, we have
r = r {(a, a) | a A} = i I (→i).
Let , < and a, b, c U be elements such that a → b and a → c. Let →< denote i<
(→i) and →<< denote i< i < (→i). Then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)* , (3)
(c, c) (→<)* (c, c) (→) (c,d) (→<<)* .
=
(4)
474
Since a → b and a → c, consider the following cases.
Case 1: a = b = c. Then the conditions (3), (4) hold for b = b = c = c = d = a.
Case 2: a = b and a → c. Then the conditions (3), (4) hold for b = b and c = b = c = d = c.
Case 3: a → b and a = c. Then the conditions (3), (4) hold for c = c and b = b = c = d = b.
Case 4: a → b and a → c. Then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)* ,
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*.
Then (3), (4) hold.
We conclude that (U, r) is an ARS in the class DCR by the definition of DCR .
Lemma 4.6. Let be an ordinal, U be a set, r, r U U. Assume that (U, r) is an ARS in the
class DCR and r = r \ {(a, a) | aU}. Then (U, r) is an ARS in the class DCR .
Proof.
Since (U, r) is in DCR, there exists an indexed family (→i)iI of relations →i UU, where
I = {i | i < }, such that r = i I (→i) and for every , < and a, b, c U, if a → b and a → c,
then there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)*
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*
where →< denotes i< (→i) and →<< denotes i< i < (→i), and the upper indices = and * are
used to denote, respectively, the reflexive and the reflexive transitive closure of a relation on U.
Let us introduce an indexed family (→i)iI/ of binary relations →i on U, indexed by the same set
I = {i | i < } as (→i)iI , where for each i I, →i = →i \ {(a, a) | a U}. Then (regardless of whether
I = ) we have
r = r \ {(a, a) | a U} = i I (→i).
Let , < and a, b, c U be elements such that a → b and a → c. Then a → b and a → c,
so there exist b, b, c, c, d U such that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)* ,
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)*.
Let →< denote i< (→i) and →<< denote i< i < (→i). It is straightforward to check that
(b, b) (→<)* (b, b) (→)= (b,d) (→<<)* ,
(c, c) (→<)* (c, c) (→)= (c,d) (→<<)* ,
where the upper indices = and * are used to denote, respectively, the reflexive and the reflexive
transitive closure of a relation on U.
We conclude that (U, r) is an ARS in the class DCR by the definition of DCR .
Lemma 4.7. Let be a nonzero ordinal, U be a set, r, r U U. Assume that (U, r) is an ARS in
the class DCR and {(a, b) r | a b} = {(a, b) r | a b}. Then (U, r) is an ARS in the class DCR .
Proof.
Let r = r \ {(a, a) | a U}. Then
r = {(a, b) r | a b} = {(a, b) r | a b} = r \ {(a, a) | a U} U U.
Then (U, r) is an ARS in DCR by Lemma 4.6, because (U, r) is an ARS in DCR .
Let A = {a | (a, a) r}. Then r, r U U, A U, (U, r) is an ARS in DCR , and
r = r {(a, a) | a A},
so (U, r) is an ARS in DCR by Lemma 4.5 applied to , U, r, r, A.
Lemma 4.8. Let be an ordinal and (A, r), (B, r) be ARS (with a common reduction relation r).
Then (A, r) belongs to the class DCR if and only if (B, r) belongs to the class DCR .
Proof.
Since (A, r), (B, r) are ARS, we have r A A and r B B, whence:
• Fld(r) A, Fld(r) B, r Fld(r) Fld(r)
• if (a, b) r*, then either a, b Fld(r), or a=b.
475
Using these properties it is straightforward to show from the definition of DCR that the following
implications hold:
• if (A, r) or (B, r) belong to DCR, then (Fld(r), r) is an ARS in DCR ,
• if (Fld(r), r) is an ARS in DCR, then (A, r) and (B, r) belong to DCR .
Thus (A, r) belongs to DCR if and only if (B, r) belongs to DCR .
Now we can describe the proof of Theorem 3.1.
Proof of Theorem 3.1.
Assume that (A, →), (B, →) are ARS, (B, →) is a weakly connected subgraph of (A, →) such
that B is a cofinal subset in the preordered set (A, →*). Let us fix a nonzero ordinal and assume
that (B, →) belongs to DCR .
Let us show that (A, →) belongs to DCR+1. Let
r = → {(b, b) | b B},
s = → {(b, b) | b B}.
Since (B, →) belongs to DCR and is a subgraph of (A, →), we have → B B A A, so
(A, →) is an ARS and (A, →) belongs to DCR by Lemma 4.8. Note that s (AA) (BB) = AA
and B A, and s = → {(b, b) | b B}. Then (A, s) belongs to DCR by Lemma 4.5 applied to
, A, →, s, and B.
Note that B Fld(s) Fld(→) B B, because (B, →) is an ARS. Thus B = Fld(s). Moreover,
→ {(b, b) | b B} = s r = → {(b, b) | b B} A A,
because (A, →) is an ARS, → →, and B A. Also,
s = → {(b, b) | b B} B B,
so (B, s) is an ARS. Moreover, from the definition of s it follows that (B, s) is weakly connected,
because (B, →) is weakly connected. Note that B is a cofinal subset in the preordered set (A, (r)*),
because B is a cofinal subset in the preordered set (A, →*) and → r. Thus s, r are relations such
that s r A A, and B = Fld(s), (B, s) is a weakly connected ARS, B is a cofinal subset in the
preordered set (A, (r)*), and (A, s) is an ARS in DCR . By Lemma 4.4 applied to , A, A A, s, r,
we conclude that (A, r) is an ARS in DCR+1 .
Note that r A A and → A A, (A, r) is an ARS in DCR+1 , and from the definition of r it
follows that {(a, b) r | a b} = {(a, b) → | a b}. Then (A, →) belongs to DCR+1 by Lemma 4.7
applied to , A, r, →.
5. Proof of Corollary 3.1
Let be a nonzero ordinal and (A, →) be an ARS.
Assume that for every aA there exists an ARS (B, →) such that
1. (B, →) is a weakly connected subgraph of (A, →),
2. (B, →) belongs to DCR ,
3. B is a cofinal subset in (Aa, →a*), where Aa = {b A | a →* b} and →a = → (Aa Aa).
Let us show that (A, →) belongs to DCR+1.
Firstly, let us show that (A, →) is confluent. Let a, b, c A and a →* b a →* c. Then there
exists an ARS (B, →) such that (B, →) is a weakly connected subgraph of (A, →), and (B, →)
belongs to DCR and B is a cofinal subset in (Aa, →a*). Then (B, →) is confluent. Since a →* b,
either a = b, or there exists a positive integer n and b0, b1 bn A such that
a = b0 → b1 → → bn = b.
In both cases, (a, b) (→a)* and b Aa . Similarly, (a, c) (→a)* and c Aa . Then since B is a
cofinal subset in (Aa, →a*), there exist b, c B such that b →a* b and c →a* c. Since (B, →)
476
weakly connected, (b, c) (→ (→)-1)*. Then since (B, →) is confluent, by the Church-Rosser
property there exists d B A such that (b, d) (→)* and (c, d) (→)*. Then b →a* b →* d
and c →a* c →* d , whence b →* d and c →* d. We conclude that (A, →) is confluent.
Let = → →-1 and let * denote the reflexive transitive closure of on A.
For every a A denote
[a] = { b A | a * b },
→[a] = → ([a] [a]).
Let us show that for every a A, the ARS ([a], →[a]) belongs to DCR+1 .
Let us fix a A. Then there exists ARS (B, →) such that (B, →) is a weakly connected
subgraph of (A, →), and (B, →) belongs to DCR , and B is a cofinal subset in (Aa, →a*).
Note that ([a], →[a]) is an ARS. Also, B [a], because whenever x B, we have x Aa (because
B Aa ), so x A and a →* x, whence x [a]. Then
→ B B [a] [a]
and → → (because (B, →) is subgraph of (A, →)), so
→ → ([a] [a]) = →[a].
Thus B [a] and → →[a] .
We conclude that (B, →) is a subgraph of ([a], →[a]). Moreover, (B, →) is weakly connected.
Let us show that B is a cofinal subset in the preordered set ([a], (→[a])*). Note that B [a].
Let x [a]. Then x A and a * x. As we have shown above, (A, →) is confluent. Then since
a * x, by the Church-Rosser property, there exists y A such that a →* y and x →* y. Then
either a = y, or there exists a positive integer n and y0, y1 yn A such that
a = y0 → y1 → → yn = y.
In both cases, (a, y) (→a)* and y Aa . Since B is a cofinal subset in (Aa, →a*), there exists y B
such that y →a* y. Then x →* y →a* y, so x →* y, and also, a →* y (because B Aa). Then either
x = y, or there exists a positive integer m and y0, y1 ym A such that
x = y0 → y1 → → ym = y,
and, moreover, and y0, y1 ym [a]. Then (x, y) (→[a])* and y B.
We conclude that B is a cofinal subset in ([a], (→[a])*). Then since (B, →) belongs to DCR , by
Theorem 3.1 applied to the ARS ([a], →[a]) and (B, →), the ARS ([a], →[a]) belongs to DCR+1.
We conclude that for every a A, the ARS ([a], →[a]) belongs to DCR+1 .
Note that A = aA [a], and → = aA →[a], and for every a, b A, if Fld(→[a]) Fld(→[b]) ,
then [a] = [b], and for every a A, ([a], →[a]) belongs to DCR+1 . It is straightforward to check that
that these conditions imply that (A, →) belongs to DCR+1 using the definition of DCR+1 .
6. Formalization in proof assistant software
We have formalized a variant of the main result for finite levels of the DCR hierarchy using
Isabelle 2023 proof assistant software and HOL logic.
In this formalization, for a positive integer n and a binary relation r on U , a formal
U, r) belongs to the class DCRn.. The formal
definition of the DCR predicate and the definitions of several auxiliary notions on which the
former depends are given below:
definition L1 :: "(nat 'U rel) nat 'U rel"
where
"L1 g {r. '. (' <) r = g '}"
definition Lv :: "(nat 'U rel) nat nat 'U rel"
477
where
"Lv g {r. '. (' < ' < ) r = g '}"
definition D :: "(nat 'U rel) nat nat ('U 'U 'U 'U) set"
where
"D g = {(b,b',b'',d). (b,b') (L1 g )^* (b',b'') (g )^= (b'',d) (Lv g )^*}"
definition DCR_generating :: "(nat 'U rel) bool"
where
"DCR_generating g ( a b c. (a,b) (g ) (a,c) (g )
---> ( b' b'' c' c'' d. (b,b',b'',d) (D g ) (c,c',c'',d) (D g ) ))"
definition DCR :: "nat 'U rel bool"
where
"DCR n r ( g::(nat 'U rel). DCR_generating g r = { r'. '. ' < n r' = g ' } )"
The statement of a formal version of Theorem 3.1 restricted to < has the form:
theorem thm_1:
fixes r s::"'U rel" and n::nat --"r,s are binary relations"
assumes a0: "n 0"
and a1: "r A A" --"(A,r) is an ARS"
and a2: "s B B" --"(B,s) is an ARS"
and a3: "B A" and a4: "s r" --"(B,s) is a (not necessarily induced) subgraph of (A,r)"
and a5: "b1B. b2B. (b1,b2) (s s^-1)^*" --"(B,s) is weakly connected"
and a6: "aA. bB. (a, b) r^*" --"B is a cofinal set in the preordered set (A,r*)"
and a7: "DCR n s" --"(B,s) is in the class DCR_n"
shows "DCR (n+1) r" --"Then (A,r) is in the class DCR_(n+1)"
7. Conclusions
We have extended a result by J. Endrullis, J.W. Klop, R. Overbeek that implies that an ARS with the
cofinality property belongs to the class DCR2 of confluent ARS for which confluence can be proved
with the help of the decreasing diagrams method using the set of labels {0, 1} ordered in such a way
that 0<1. Our extension (Theorem 3.1 and Corollary 3.1 in Section 3) concerns higher levels of the
DCR hierarchy (e.g. it does not collapse at the level 2 in accordance with [23]) and explains why
the cofinality property is related to the level 2 in this hierarchy (Example 3.1 in Section 3).
A formalized version of a variant of the main result has been machine-checked in Isabelle proof
assistant software using HOL logic.
Further work is required to study the DCR hierarchy and methods for proving confluence and
other properties for not-necessarily-countable rewriting systems in more detail.
Declaration on Generative AI
The author has not employed any Generative AI tools.
References
[1] The Church-Turing Thesis, Stanford Encyclopedia of Philosophy, 2024. URL:
http://plato.stanford.edu/ENTRIES/church-turing .
478
[2] F. Cardone, J.R. Hindley, History of Lambda-calculus and Combinatory Logic, Handbook of the
History of Logic 5 (2006) 723-817.
[3] S.C. Kleene, -definability and recursiveness. Duke Mathematical Journal 2 (1936) 340-353.
[4] A.M. Turing, Computability and -definability. Journal of Symbolic Logic 2 (1937) 153-163.
[5] A. Church, An Unsolvable Problem of Elementary Number Theory, American Journal of
Mathematics 58, no. 2 (1936) 345-363.
[6] A. Church, A set of postulates for the foundation of logic. Annals of Mathematics, Series 2, no.
33 (1932) 346-366.
[7] A. Church, A set of postulates for the foundation of logic (second paper). Annals of
Mathematics, Series 2, no. 34, (1933) 839-864.
[8] A. Church, J.B. Rosser, Some properties of conversion. Transactions of the American
Mathematical Society, no. 39 (1936) 472-482.
[9] Terese, Term Rewriting Systems, Volume 55 of Cambridge Tracts in Theoretical Computer
Science, Cambridge University Press, 2003.
[10] F. Baader, T. Nipkow, Term rewriting and all that, Cambridge University Press, 1999.
[11] P. Malbos, Lectures on Algebraic Rewriting, 2019. URL: http://hal.archives-ouvertes.fr/hal-
02461874 .
[12]
mathematics 43 (1942) 223-243.
[13] B.K. Rosen, Tree manipulating systems and Church-Rosser theorems. Journal of the ACM. Vol.
20, pp. 160-187, 1973.
[14] N.G. de Bruijn, A note on weak diamond properties. Memorandum 78-08, Eindhoven
University of Technology, 1978.
[15] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems,
Journal of the ACM 27, no. 4 (1980) 797-821.
[16] J.W. Klop, Combinatory Reduction Systems, Vol. 127 of Mathematical centre tracts,
Mathematisch Centrum, 1980.
[17] V. van Oostrom, Confluence by decreasing diagrams, Theoretical computer science 126, no. 2
(1994) 259-280.
[18] V. van Oostrom, Confluence for Abstract and Higher-Order Rewriting, Ph.D. thesis, Vrije
Universiteit Amsterdam, 1994.
[19] V. van Oostrom, Confluence by Decreasing Diagrams, Converted, in: Lecture Notes in
Computer Science, vol. 5117, Springer, 2008, pp. 306-320.
[20] J. Endrullis, J.W. Klop, De Bruijn's weak diamond property revisited. Indagationes
Mathematicae 24 (2013) 1050-1072.
[21] N. Hirokawa, A. Middeldorp, C. Sternagel, S. Winkler, Abstract Completion, Formalized,
Logical Methods in Computer Science 15, issue 3, (2019) 19:1-19:42.
[22] J. Endrullis, J. W. Klop, R. Overbeek, Decreasing diagrams with two labels are complete for
confluence of countable systems, in: 3rd International Conference on Formal Structures for
Computation and Deduction (FSCD 2018), 2018, pp. 14:1-14:15.
[23] I. Ivanov, On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting
Systems, in: Proceedings of the 13th International Workshop on Confluence, 2024, pp. 30-35.
[24] Isabelle proof assistant software, 2024. URL: http://isabelle.in.tum.de .
[25] R. Baheti, H. Gill, Cyber-physical systems, The impact of control technology 12 (2011) 161-166.
[26]
International Proceedings in Informatics, volume 260, 2023, pp. 9:1-9:17.
[27] J. Endrullis, J. W. Klop, R. Overbeek, Decreasing diagrams for confluence and commutation,
Logical Methods in Computer Science 16, issue 1 (2020) 23:1-23:25.
[28] A.A. Fraenkel, Y. Bar-Hillel, A. Levy, Foundations of Set Theory, Elsevier, 1973.
[29] A. Krauss, A. Schropp, A mechanized translation from Higher-Order Logic to set theory, in:
Lecture Notes in Computer Science, vol. 6172, Springer, 2010, pp. 323-338.
[30] O. Kuncar, A. Popescu, A consistent foundation for Isabelle/HOL, Journal of Automated
Reasoning 62 (2019) 531-555.
479