1. Introduction

On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems

Ievgen Ivanov

0 0 Taras Shevchenko National University of Kyiv , 64/13, Volodymyrska Street, Kyiv, 01601 , Ukraine

466 479

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

eol>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 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 a R b a, b)  R A, we will use the following notation for any binary relation r  AA: • 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 →  AA 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 • 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 →  ({ bA | a →* b }  { bA | a →* b }), i.e. the restriction of → to { bA | a →* b }.

An ARS (A, →) belongs to the class DCR [22, Definition 15], where  is an ordinal, if there exists an indexed family (→i)iI of binary relations →i  AA indexed by ordinals below , i.e. I = {i | i < } such that → = iI (→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 aA bB 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 .

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.

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 aA 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.

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 {bA | 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 = {bA | a →* b} and →a = →  (Aa  Aa), because B  {bA | a →* b} and for every b  Aa we have bA  a →* b, so for some bi  B, (b, bi)  (→)*, where

→ = →  ( {bA | a →* b}  {bA | 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)iI of relations →i  UU, 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)jJ 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)  (→<<)* (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.

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)iI 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(0)(a) = a. Note that for every a  D, d(a) > 0, because a  Fld(s). Then for 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)iI of relations →i  UU, 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)iI/ of binary relations →i on U, indexed by the same set I = {i | i < } as (→i)iI , 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)  (→<<)* , (c, c)  (→<)*  (c, c)  (→)=  (c,d)  (→<<)* . 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) | aU}. Then (U, r) is an ARS in the class DCR .

Proof.

Let us introduce an indexed family (→i)iI/ of binary relations →i on U, indexed by the same set I = {i | i < } as (→i)iI , 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. 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  (AA)  (BB) = AA 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 aA 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, →) 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 = aA [a], and → = aA →[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" 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: "b1B. b2B. (b1,b2)  (s  s^-1)^*" --"(B,s) is weakly connected" and a6: "aA. bB. (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. [1] The Church-Turing Thesis, Stanford Encyclopedia http://plato.stanford.edu/ENTRIES/church-turing . of

Philosophy,

[2]

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]

Church , An Unsolvable Problem of Elementary Number Theory , American Journal of Mathematics 58 , no. 2 ( 1936 ) 345 - 363 .

[6]

Church , A set of postulates for the foundation of logic . Annals of Mathematics, Series 2 , no. 33 ( 1932 ) 346 - 366 .

[7]

Church , A set of postulates for the foundation of logic (second paper) . Annals of Mathematics, Series 2 , no. 34 , ( 1933 ) 839 - 864 .

[8]

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]

Baader , T. Nipkow, Term rewriting and all that , Cambridge University Press, 1999 .

[11]

Malbos , Lectures on Algebraic Rewriting, 2019 . URL: http://hal.archives-ouvertes. fr/hal02461874 . 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]

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]

Endrullis ,

J.W.

Klop , De Bruijn' s weak diamond property revisited . Indagationes Mathematicae 24 ( 2013 ) 1050 - 1072 .

[21]

Hirokawa ,

Middeldorp ,

Sternagel ,

Winkler , Abstract Completion, Formalized, Logical Methods in Computer Science 15, issue

, ( 2019 ) 19 : 1 - 19 : 42 .

[22]

Endrullis ,

J. W.

Klop ,

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]

Baheti ,

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]

Endrullis ,

J. W.

Klop ,

Overbeek , Decreasing diagrams for confluence and commutation , Logical Methods in Computer Science 16, issue 1 ( 2020 ) 23 : 1 - 23 : 25 .

[28]

A.A.

Fraenkel ,

Bar-Hillel , A. Levy , Foundations of Set Theory, Elsevier , 1973 .

[29]

Krauss ,

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]

Kuncar ,

Popescu , A consistent foundation for Isabelle/HOL , Journal of Automated Reasoning 62 ( 2019 ) 531 - 555 .