We give novel confluence criteria and examples that can be used by researchers in computer science and software engineering to better recognize situations where the local confluence property of non-terminating abstract rewriting systems is and is not equivalent to the confluence property. We also describe a formalization of the main results in Isabelle proof assistant software.
Newman’s lemma [
Taking into account usefulness of Newman’s lemma, it is natural to question whether its termination assumption can be relaxed to make the lemma more widely applicable. A formal answer to this question is “yes”: the class of all ARS for which confluence and local confluence are equivalent (the union of classes of confluent and not locally confluent ARS) is wider than the class of all terminating ARS (the remaining question is how to make sure that a given, possibly nonterminating system belongs to the former class). However, in the literature on rewriting systems that mention Newman’s lemma the termination assumption is quite often presented as a necessary condition for the validity of the lemma’s conclusion, e.g.: “The following examples illustrate that the requirement of noetherianity is necessary to prove confluence from local confluence. …’’ [5, paragraph 1.4.2], “… For the relations that are not noetherian, much stronger local hypotheses are necessary to yield confluence.” [2, paragraph 2.2]. In our opinion, such informal statements may unintentionally create an impression that the local confluence property cannot be used in place of the confluence property in any situation where a system under consideration is not terminating (or its termination cannot be established with certainty), although this is not the case.
In this work we give novel results that can help one to better recognize situations where the
local confluence property of abstract rewriting systems is and is not equivalent to the confluence
property. We also describe formalizations of the main theorems (Theorems 1, 2, 3 from Section 4) in
Isabelle proof assistant software [
In this work we will focus on abstract rewriting systems with single reduction relation (without auxiliary labelings of elements or reductions).
We will give novel confluence criteria based on local confluence for special classes of such systems. We will assume that the Axiom of Choice holds and will freely use its corollaries (e.g. Zorn’s lemma).
We will use the following (mostly standard) definitions of basic notions that are consistent with
the terminology used in many works on the rewriting theory [
An abstract rewriting system (ARS) is a pair (X, ) of a set (X) and a binary relation () on it called reduction. We will denote as * the reflexive transitive closure of (on X), and as + the transitive closure of .
An element x X is called reducible (in (X, )), if there exists y X such that x y, and is called irreducible (in (X, )), if it is not reducible in (X, ).
A normal form of an element x X (in an ARS (X, )) is an element y X such that x*y and y is irreducible in (X, ).
An ARS (X, ) has the diamond property, if for all a, b, c X, if a b and a c, then there exists d X such that b d and c d ; is confluent, if for all a, b, c X, if a*b and a*c, then there exists d X such that b*d and c*d ; is locally confluent, if for all a, b, c X, if a b and a c, then there exists d X such that b*d and c*d.
Note that * is a preorder (a binary relation that is reflexive and transitive) and the pair (X,*) can be considered as a preordered set.
If (P, ) is a preordered set, A P and x P, then x is a least element of A (w.r.t. ), if x A and x a for all a A ; x is a greatest element of A (w.r.t. ), if x A and a x for all a A ; x is a minimal element of A (w.r.t. ) , if x A and there is no element y A such that y x and (x y); x is an upper bound of A (in (P, )), if a x for all a A ; x is a least upper bound of A (in (P, )), if x is a least element of the set of all upper bounds of A in (P, ).
In any preordered set (P, ) a subset A X is
a chain, if every x, y A, x y or y x ;
a directed set, if A and for every x, y A there exists u A such that x u and y u ;
closed [
An ARS (X, )
is weakly normalizing, if each element x X has a normal form ;
is countable, if the set X is at most countable, i.e. there exists a total injective function from X
to the set of natural numbers ;
is terminating, if there is no infinite sequence x1x2x3… , where xi X for all i=1, 2, …;
is acyclic, if there is no element x X such that x + x ;
is inductive [
In accordance with Newman’s lemma, any terminating locally confluent ARS is confluent. Any terminating ARS is acyclic, however, generally, an acyclic locally confluent ARS need not be confluent. An example due to Newman [2, Figure 6a] shown in Figure 1(a) below is often used to illustrate the latter fact.
Another widely known example due to Hindley [2, Figure 6b] shows that a finite locally confluent ARS that is not required to be acyclic can be non-confluent.
Newman’s counterexample shown in Figure 1(a) can be formalized as (XNC, NC), where
XNC = {a, b, 0, 1, 2, …}, a = -1, b = -2, and the relation NC is defined as follows: NC = { (2n, a) | n = 0, 1, 2, … } { (2n+1, b) | n = 0, 1, 2, … } { (n, n+1) | n = 0, 1, 2, … }.
The ARS (XNC, NC) is countable, acyclic, inductive, locally confluent, but is not confluent [
However, note that in the preordered set (XNC, (NC )* ) the chain {1, 2, 3, … } has minimal upper bounds (a and b), but has no least upper bound. If the chain {1, 2, 3, … } had a least upper bound (or no upper bounds), the above mentioned explanation of the possibility of inequivalence of local confluence and confluence would not apply. For example, consider an ARS shown in Figure 1(b) that can be formalized as (XNC, NC {(a, b)}). Unlike Newman’s counterexample, it is a strictly inductive ARS, i.e. all nonempty chains in the sense of the preorder generated by the reflexive transitive closure of the reduction relation have least upper bounds. Indeed, in the next section we will show rigorously that any acyclic strictly inductive ARS with at most countable set of irreducible elements is confluent if and only if it is locally confluent. We will also show that countability and acyclicity assumptions here are important and cannot be simply omitted from this proposition. Besides, Newman’s counterexample implies that strict inductivity cannot be weakened to inductivity in this proposition since (XNC, NC) is acyclic, inductive, has a finite set of irreducible elements, is locally confluent, but is not confluent. These results complement Newman’s lemma and clarify the limits of usefulness of the local confluence property as a condition in confluence criteria.
Below we give formulations and proofs of the main results. One can assume that a background theory for understanding them is ZFC.
Theorem 1. Let (X, ) be an acyclic strictly inductive ARS such that the set of all its irreducible elements is at most countable.
Then (X, ) is confluent if and only if (X, ) is locally confluent.
Proof.
Any confluent ARS is locally confluent, so it is sufficient to show that if (X, ) is locally confluent, then (X, ) is confluent.
Assume that the ARS (X, ) is locally confluent. Note that since the ARS (X, ) is acyclic, the relation * on X is antisymmetric: if x*y and y*x, then x = y (otherwise, x + x which contradicts acyclicity). Then (X, *) is not only a preordered set, but is a partially ordered set (poset).
Let us introduce the following notation: IR is the set of all irreducible elements of (X, ) ; NF(x), where x X, is set of all normal forms of x ; ND is the set of all x X such that the set NF(x) contains at least two distinct elements.
Let us show that (X, ) is a weakly normalizing ARS. Let x X and U = { y X | x * y }. It is
straightforward to show that since (X, ) is a strictly inductive acyclic ARS, the set U, considered as
an induced subposet of (X, *), is a nonempty inductive poset [
Now let us show that for each xND and bIR there exists yND such that x*y and b NF(y). Let us denote U = { y X | x * y } and D ={ y U | y * b }. Denote as the relation * (UU). Then (U, ) is a (nonempty) induced subposet of (X, *).
Let us fix xND and bIR and consider the following 2 cases.
Case 1: x * b does not hold. Then for y = x we have yND, x*y and b NF(y).
Case 2: x * b holds. Since xND, the set NF(x)\{b} is nonempty. Let m be some element of NF(x)\{b}. Then x* m, so m U. Note that m D since otherwise, m*b, and also mIR, whence m = b which contradicts the fact that m NF(x)\{b}. Thus m U\D. Let E = D { y X | y * m }. It is straightforward to check that E is a closed set in the poset (U, ) (in the sense of Section 2). Moreover, x E (because x*b and x*m), so E . Then it is straightforward to check that (E, (EE)) is a nonempty inductive poset (i.e. a poset where every nonempty chain has an upper bound), so by Zorn’s lemma, E has a maximal element xmax with respect to the order (EE). Then xmax E, so xmax* b and xmax * m. Then we have xmax b and xmax m, because otherwise, b*m or m*b holds, whence b = m since bIR and mIR, which contradicts the fact that m NF(x)\{b}. Then xmax + b and xmax + m, so there exist e1, e2 X such that xmax e1 * b and xmax e2 * m. Since (X, ) is a locally confluent ARS, there exists dX such that e1 * d and e2 * d.
Let us show that e2 ND.
- Suppose that e2 ND. Note that e2 * m and m IR, so m NF(e2). Since (X, ) is weakly normalizing (as we have shown above) and e2 ND, NF(e2) is a singleton set, so NF(e2) = {m}. Moreover, e2 * d and NF(d) , so m NF(d). Then x * xmax e1 * b, and e1 * d * m, so e1 E. Then xmax e1 and e1 E. Since xmax is maximal in E with respect to E E, we have xmax = e1. Then xmax xmax and we get a contradiction with the theorem’s assumption that (X, ) is an acyclic ARS.
Thus e2 ND. Let us show that b NF(e2).
- Suppose that b NF(e2). Then x * xmax e2 * b and e2 * m, so e2 E. Then xmax e2 and e2 E. Since xmax is maximal in E with respect to E E, we have xmax = e2. Then xmax xmax and we get a contradiction with the theorem’s assumption that (X, ) is an acyclic ARS.
Note that x * xmax e2, so there exists y = e2 ND such that x*y and b NF(y). We conclude that indeed, for each xND and bIR there exists yND such that x*y and b NF(y).
Now let us show by contradiction that ND = . Suppose that ND . Then IR is a nonempty, at most countable set (IR is at most countable by theorem’s assumption), so IR is an image of a total function on the set of all non-negative integers N0 = { 0, 1, 2, … }, so there exists an infinite sequence fn X, n = 0, 1, 2, … such that IR = { fi | iN0 } (note that elements in the sequence fn , n = 0, 1, 2, … can repeat). As we have shown above, for each xND and bIR there exists yND such that x*y and b NF(y). Then for each xND and iN0 there exists yND such that x*y and fi NF(y). Then since ND , by the principle of dependent choice there exists an infinite sequence gn ND, n=0,1,2,… such that for each n=0,1,2,…, gn*gn+1 and fn NF(gn+1). Then the set { gn | nN0 } is a 17 non-empty chain in the poset (X, *), so it has a least upper bound in (X, *) since (X, ) is a strictly inductive ARS. Denote as u the least upper bound of { gn | nN0 } in the poset (X, *). As we have shown above, (X, ) is a weakly normalizing ARS, so NF(u) . Let m be some element of NF(u).Then m IR, so there exists kN0 such that m = fk . Note that gk+1 * u (since u is an upper bound of the set { gn | nN0 }) and u*m, so gk+1*m. Then m NF(gk+1), since m IR. On the other hand, m = fk NF(gk+1) by the definition of the sequence gn , n = 0, 1, 2, …, so we have a contradiction: mNF(gk+1) and mNF(gk+1). Thus the assumption ND is false and we conclude that ND = .
Since ND = , each xX has at most one normal form in the ARS (X, ). As we have shown above, (X, ) is a weakly normalizing ARS, so each xX has exactly one normal form. This straightforwardly implies that the ARS (X, ) is confluent.
Note that - the ARS shown in Figure 1(a) does not satisfy the assumptions of Theorem 1: although it is inductive, it is not strictly inductive ; - the ARS shown in Figure 1(b) satisfies the assumptions of Theorem 1.
Corollary 1. Let (X, ) be an acyclic strictly inductive ARS where each element has at most countable set of normal forms. Then (X, ) is confluent if and only if (X, ) is locally confluent.
Proof.
Any confluent ARS is locally confluent, so it is sufficient to show that if (X, ) is locally confluent, then (X, ) is confluent.
Assume that the ARS (X, ) is locally confluent. Let a, b, c X, a*b, and a*c. Let U = { u X | a * u }. It is straightforward to check that (U, (UU)) is an acyclic strictly inductive locally confluent ARS, where each irreducible element is a normal form of a in (X, ). Since the set of normal forms of a in (X, ) is at most countable, the ARS (U, (UU)) is confluent by Theorem 1. Note that a, b, c U, so there exists d U X such that (b, d) and (c, d) belong to the reflexive transitive closure of (UU), so b*d and c*d.
Thus we conclude that (X, ) is confluent.
Corollary 2. Let (X, ) be a countable acyclic ARS such that for every infinite reduction sequence x1 x2 x3 … the set {x1, x2, x3, … } has a least upper bound in the poset (X,*). Then (X, ) is confluent if and only if (X, ) is locally confluent.
Proof.
Note that since (X, ) is acyclic, (X,*) is indeed a poset (not just a preordered set).
Let us check that (X, ) is a strictly inductive ARS. Let C be a nonempty chain in the poset
(X,*). Let c0 be some element of C (it exists since C is nonempty). Let C be a binary relation on C
such that for all x, y C, x C y if and only if x*y (note that * is considered as a binary relation
of X, but C is a binary relation on C X). Note that the ARS (C, C) has the diamond property,
because whenever a, b, c C, a C b, and a C c, we have b*c or c*b (since C is a chain in the
poset (X,*)), and in either case there exists d {c, b} C such that bC d and cC d . Also,
(C, C) is a countable ARS, because (X, ) is a countable ARS. Since any ARS with diamond
property is confluent [5, Remark 1.2.3] and any countable confluent ARS has the cofinality property
[
Note that if the set B is finite, it is a nonempty finite chain in the poset (X,*), so it has a greatest element which is its least upper bound, and if B is an infinite set, then x1 x2 x3 … is an infinite reduction sequence, so B has a least upper bound in the poset (X,*) by assumption. Thus in any case there exists u X such that u is a least upper bound of B in (X,*).
Note that u is an upper bound of C in (X,*), because for each c C there exists y B such that c * y and y * u. Moreover, u is a least upper bound of C, because if x is an upper bound of C in (X,*), then for each y B there exists c A C such that such that y * c * x, so x is an upper bound of B in (X,*), whence u * x. Thus C has a least upper bound in (X,*).
We conclude that (X, ) is a strictly inductive ARS. Moreover, it is acyclic by assumption. Since (X, ) is a countable ARS, the set X is (at most) countable, so the set of irreducible elements in (X, ) is (at most) countable. Then (X, ) is confluent if and only if (X, ) is locally confluent by Theorem 1.
Hindley’s counterexample [2, Figure 6b] shows that the acyclicity assumption cannot be simply omitted from the statement of Theorem 1, e.g. the ARS
({ 0, 1, 2, 3 }, { (1, 0), (2, 3), (1, 2), (2, 1) }) is strictly inductive, has a finite set of irreducible elements, is locally confluent, but is not confluent.
The following result shows that the countability assumption also cannot be simply omitted from the statement of Theorem 1. The corresponding ARS is illustrated in Figure 2. We call it a strengthened Newman’s counterexample, because the usual Newman’s counterexample (Figure 1(a)) is inductive, but is not strictly inductive.
Theorem 2 (Strengthened Newman’s counterexample).
Let P = R R ( + 1), where R is the set of real numbers and is the first infinite ordinal. Let be a binary relation on P such that (x, y, n) (x, y, m) if and only if one of the following two conditions holds: 1. n < and m = n + 1 and | x – x | < y/2m and 0 < y < y ; 2. n < and m = and x = x and 0 = y < y .
Then (P, ) is an acyclic, strictly inductive, locally confluent ARS that is not confluent.
Proof.
Since (x, y, n) (x, y, m) implies that n < m, the relation (x, y, n) + (x, y, n) does not hold for any (x, y, n) P, so the ARS (P, ) is acyclic.
It is straightforward to show that (x, y, n) + (x, y, m) if and only if one of the following two conditions holds: (T1) n < and m < and n < m and | x – x | < y/2n – y/2m-1 + y/2m and 0 < y < y ; (T2) n < and m = and | x – x | < y/2n and 0 = y < y .
Then the ARS (P, ) is not confluent, because if a = (0, 2, 0), b = (-1, 0, ), c = (1, 0, ), then a + b and a + c by (T2), however, by the definition of , the elements b and c are irreducible, and since they are distinct, the relations b*d and c*d cannot both hold for any d P.
Let us check that the ARS (P, ) is locally confluent.
Let a = (x1, y1, n), b = (x2, y2, m), c = (x3, y3, k) P be elements such that ab and a c. Then the definition of implies that n < . Let d = (x1, 0, ).
Consider the following cases.
- If m < , then | x2 – x1 | < y2/2m and y2 > 0, because (x1, y1, n) = a b = (x2, y2, m), whence b = (x2, y2, m) + (x1, 0, ) = d by (T2). - If m = , then x2 = x1 and y2 = 0, because (x1, y1, n) = a b = (x2, y2, m), whence b = (x2, y2, m) = (x1, 0, ) = d.
In both cases we have b*d. Similarly, consider the following cases.
- If k < , then | x3 – x1 | < y3/2k and y3 > 0, because (x1, y1, n) = a c = (x3, y3, k), whence c = (x3, y3, k) + (x1, 0, ) = d by (T2). - If k = , then x3 = x1 and y3 = 0, because (x1, y1, n) = a c = (x3, y3, k), whence c = (x3, y3, k) = (x1, 0, ) = d.
In both cases we have c*d. Thus both b*d and c*d hold.
Since a, b, c are arbitrary, we conclude that (P, ) is a locally confluent ARS.
Finally, let us check that the ARS (P, ) is strictly inductive.
Let C be a nonempty chain in the poset (P, *) and let
N = { n < | x y (x, y, n) C } .
Consider the following three cases.
Case 1: there exist x1, y1 R such that (x1, y1, ) C. Then using (T1), (T2) is straightforward to check that (x1, y1, ) is a greatest element in C with respect to *, so it is a least upper bound of C in (P, *).
Case 2: the set N is finite and (x, y, ) C for all x, y R. Then the set N is nonempty (since C is nonempty). Let km be the greatest element of N and x1, y1 R be elements such that (x1, y1, km) C. Then using (T1), (T2) it is straightforward to check that (x1, y1, km) is a greatest element in C with respect to *, so it is a least upper bound of C in (P, *).
Case 3: the set N is infinite and (x, y, ) C for all x, y R. Let
Y = { y R | x n < (x, y, n) C } .
Note that if k0 is the least element of N and x0, y0 are such that (x0, y0, k0) C, then y y0 for all y Y. This implies that the set Y is empty or bounded from above. Then let ym be a positive real number such that y ym for all y Y. This implies that whenever n < , m < , (x, y, n) C, and (x, y, n) + (x, y, m), the following holds:
| x – x | < y/2n – y/2m-1 + y/2m y/2n – y/2m = y (1/2n – 1/2m) ym (1/2n – 1/2m).
Then since C is a chain in (P, *), the following inequality holds all (x, y, n), (x, y, m) C such that n < and m < :
| x – x | ym | 1/2n – 1/2m |.
Let us fix some bijection f : N0 N, where N0 = {0, 1, 2, …} is the set of non-negative integers (such a bijection exists since N is infinite and at most countable). Note that the definition of N implies that for each i N0 the set { xR | yR (x, y, f(i)) C } is nonempty. Then let us fix some function g: N0 R such that for each i N0 there exists yR such that (g(i), y, f(i)) C.
Let us check that g(0), g(1), g(2), … is a Cauchy sequence of real numbers. Let be a positive real number, i.e. > 0. Note that the set { i N0 | f(i) 2ym/ } is finite, so there is some natural number M such that for all i N0, f(i) 2ym/ implies i < M. Moreover, whenever i, j N0 and i > M, j > M, there exist y, y R such that
(g(i), y, f(i)) C and (g(j), y, f(j)) C, where f(i) < and f(j) < , so
| g(j) – g(i) | ym | 1/2f(i) – 1/2f(j) | ym max{1/2f(i), 1/2f(j)} ym /(2ym) < .
Since > 0 is arbitrary, we conclude that g(0), g(1), g(2), … is a Cauchy sequence of real numbers.
Then the sequence g(0), g(1), g(2), … is convergent in R and has a limit that we will denote as xs. Let us check that (xs, 0, ) is a least upper bound of C.
Firstly, let us check that (xs, 0, ) is an upper bound of C in (P, *).
Let (x, y, n) C. The assumption of the Case 3 implies that n < . Then n N. Since N is infinite, there is some m N such that m > n. Let x, y R be elements such that (x, y, m) C. Since C is a chain in (P, *) and m > n, we have (x, y, n) + (x, y, m). Then 0 < y < y. Note that the set { i N0 | f(i) m } is finite, so there is some natural number M such that for all i N0, if f(i) m holds, then i < M.
Let us check that for all i N0, if i M, then | g(i) – x | y/2m. Let i N0 and i M. Then f(i) > m. Since f(i) N, there exist y0 R such that (g(i), y0, f(i)) C. Since C is a chain in (P, *) and f(i) > m, we have (x, y, m) + (g(i), y0, f(i)). Then (T1) implies that f(i) 1, 0 y0 y, and Note that so | g(i) – x | y/2m. Thus whenever i M, the inequality | g(i) – x | y/2m holds. Then holds for all integer i M, so the limit xs of the sequence g(0), g(1), g(2), … satisfies the inequality | g(i) – x | < y/2m – y/2f(i)-1 + y0/2f(i).
y0/2f(i) 2y/2f(i) = y/2f(i)-1, x – y/2m g(i) x + y/2m, x – y/2m xs x + y/2m .
| x – x | < y/2n – y/2m-1 + y/2m Moreover, because (x, y, n) + (x, y, m), from (T1) we have:
| xs – x | | xs – x | + | x – x | < y/2m + y/2n – y/2m-1 + y/2m y/2n.
Then | x – x | < y/2n, and also y > 0, so from (T2) we have (x, y, n) + (xs, 0, ). Since (x, y, n) C is arbitrary, we conclude that (xs, 0, ) is an upper bound of C.
Now let us check that (xs, 0, ) is least among upper bounds of C in (P, *).
Let (x1, y1, l) P be an upper bound of C in (P, *). Then n l for all n N, and since N is infinite, it is not bounded from above by any natural number, so l = . Then since C is nonempty, from (T2) it follows that y1 = 0 and for all (x, y, n) C, | x1 – x | < y/2n.
Let us check that x1 is a limit of the sequence g(0), g(1), g(2), … Let be a positive real number, i.e. > 0. Since the set { i N0 | f(i) 2ym/ } is finite, there is some natural number M such that for all i N0, f(i) 2ym/ implies i < M. Moreover, whenever i N0 and i M, there exists yR such that (g(i), y, f(i)) C, where f(i) < , so y Y and | x1 – g(i) | < y/2f(i) ym /(2ym) < .
Since > 0 is arbitrary, x1 is a limit of the sequence g(0), g(1), g(2), …, and since this sequence converges to xs, we have x1 = xs and (x1, y1, l) = (xs, 0, ). Since (x1, y1, l) is arbitrary, we conclude that (xs, 0, ) is a least upper bound of C in (P, *).
Note that in the ARS (P, ) given in the statement of Theorem 2, reducible elements have the form (x, y, n), where y > 0 and n < , and the items (T1), (T2) in the proof of Theorem 2 imply that for any such a reducible element (x, y, n) the set of its normal forms is { (x, 0, ) | |x – x| < y/2n }, and the latter is isomorphic to a real interval that is a connected subset of R in the sense of the standard topology on R (see an illustration in Figure 3). This observation motivates the result described below (Theorem 3 illustrated in Figure 4).
For any preordered set (P, ) and a set A P , the downward closure of A in (P, ) is the set { y P | a A y a }.
Given an ARS (X, ), we will say that a topology T on the set of all irreducible elements of (X, ) is downward-compatible with (X, ), if for any closed set A in the sense of T, the downward closure of A in the preordered set (X, *) is closed in the sense of Section 2.
Theorem 3. Let (X, ) be an acyclic strictly inductive locally confluent ARS and T be a topology on the set of all irreducible elements of (X, ) that is downward-compatible with (X, ).
Then for each x X, the set of all normal forms of x in (X, ) is a connected subset of the topological space ({x X | x is irreducible in (X, ) }, T).
Proof. Let us denote as IR the set of all irreducible elements of (X, ). For each x X denote: - U(x) = { y X | x*y } ; - U*(x) is the poset ( U(x), * (U(x)U(x)) ) ; - NF(x) is the set of all normal forms of x in (X, ).
Since (X, ) is an acyclic strictly inductive ARS, one can show that (X, ) is weakly normalizing using the same argument as in the proof of Theorem 1 (i.e. using Zorn’s lemma).
Let us fix x X. Note that NF(x) . Suppose that NF(x) is not a connected subset of the topological space (IR, T). Then there exist sets O1, O2 IR that are open in the sense of T and such that NF(x) O1 O2, O1 O2 NF(x) = , O1 NF(x) , and O2 NF(x) .
Let A = NF(x)\O1 and B = NF(x)\O2. Then A B = NF(x), A B = , A , and B . ;;
Figure 3: Illustration of the set of normal forms of a reducible element in the Strengthened Newman’s counterexample (Theorem 2).
Note that NF(x) U(x), so A, B U(x). Let D1 be the downward closure of A in U*(x) and D2 be the downward closure of B in U*(x).
Since T is downward-compatible with (X, ), the downward closures of the sets IR\O1, IR\O2 in (X, *) are closed in (X, *) (in the sense of Section 2). Then it is straightforward to check that D1 and D2 are closed in U*(x) (in the sense of Section 2).
Since x U(x), A, B NF(x), and A, B , we have x D1 and x D2, so D1 D2 . However, note that D1 D2 NF(x) = , because for each y D1 D2 NF(x) we have NF(y) = {y}, NF(y) A , and NF(y) B , whence y A B = .
As we have mentioned above, (X, ) is weakly normalizing, so for each y U(x) we have NF(y) , and also NF(y) NF(x) = A B, so NF(y) A or NF(y) B , whence y D1 D2. Thus U(x) D1 D2, and also D1, D2 U(x), so D1 D2 = U(x).
Note that A D2 = , because whenever y D2, there exists b B such that y*b, so if y is irreducible in (X, ), then y = b A (because A B = ), and if y is reducible in (X, ), then y A. Similarly, we have B D1 = .
Let us define a binary relation on U(x) such that for all y1, y2 U(x):
y1 y2 (y1 * y2 or (y1 D1 and y2 A) or (y1 D2 and y2 B) )
Using the facts that D1, D2 are closed, A D2 = and B D1 = and strict inductivity of the ARS (X, ), it is straightforward to show that is a preorder on U(x), and, moreover, every nonempty chain in the preordered set (U(x), ) has a least upper bound.
Let us fix some elements a0 A, b0 B (they exist, because A, B ). It is straightforward to check that for all y U(x), y a0 or y b0.
Let D = { y U(x) | y a0 and y b0 }. Then D is closed in (U(x), ) in the sense of Section 2 and D since x D. Then since (U(x), ) has a least upper bound for every nonempty chain, using Zorn’s lemma (like in Theorem 1) we conclude that D has some maximal element with respect to . Let us denote it as d. Then d U(x), d a0 and d b0. Since the relation is defined as a disjunction of 3 conditions (y1 * y2 or (y1 D1 and y2 A) or (y1 D2 and y2 B) ), the conjunction “d a0 and d b0” can be reduced to a disjunction of 9 conditions: “d * a0 and d * b0”, “(d D1 and a0 A) and d * b0 “, and so on. It is straightforward to check that each of these cases leads to a contradiction (e.g. if d * a0 and d * b0, then using local confluence of (X, ) we can obtain a contradiction with maximality of d in D with respect to like in a similar situation in the proof of Theorem 1). Then the assumption that NF(x) is not a connected subset of (IR, T) is false.
We conclude that the set of all normal forms of x in (X, ) is a connected subset of (IR, T).
We formalized Theorems 1-3 from Section 4 in Isabelle proof assistant [
The statement of a formalized version of Theorem 1 in NLNT has the following form (here the symbol denotes a reduction relation): theorem thm_1: fixes X assumes "X, is ACYCLIC ARS" and "X, is S.I.ARS"
and "{xX. x is IRREDUCIBLE in X,} is AT MOST COUNTABLE" shows "(X, is CONFLUENT ARS) = (X, is L.CONFLUENT ARS)"
The formal notions ACYCLIC ARS, S.I.ARS (i.e. a strictly inductive ARS), IRREDUCIBLE, CONFLUENT ARS, L.CONFLUENT ARS (i.e. a locally confluent ARS) are defined in the theory GNL.thy.
The statement of a formalized version of Theorem 2 in NLNT has the following form: theorem thm_2: fixes P :: "(real real enat) set" and :: "(real real enat) (real real enat) bool" assumes "P = {x::real. True} {y::real. True} {n::enat. True}" and " (x::real) (y::real) (n::enat) (x'::real) (y'::real) (m::enat).
(x, y, n) (x', y', m) = ( ( n < m = n + 1 | x' – x | < y' / 2^(the_enat m) 0 < y' y' < y )
( n < m = x' = x 0 = y' y' < y ) )" shows "(P, is ACYCLIC ARS) (P, is S.I.ARS) (P, is L.CONFLUENT ARS) ( (P, is CONFLUENT ARS))" The statement of a formalized version of Theorem 3 in NLNT has the following form: where "(f is DW-COMPATIBLE with X,) ( bij_betw f { n::'n. True } { xX. x is IRREDUCIBLE in X, } (A::('n set). closed A --> ({ y X. aA. ^** y (f a) } is c-CLOSED in X,(^**))) )" theorem thm_3: fixes X :: "'a set" and :: "'a 'a bool" and f :: "'n::topological_space 'a" assumes "X, is ACYCLIC ARS" and "X, is S.I.ARS" and "X, is L.CONFLUENT ARS" and "f is DW-COMPATIBLE with X," shows " x X. connected { n::'n. (f n) is N.F. of x in X, }"
The formal notions c-CLOSED (a closed subset of a preordered set) and N.F. (normal form) are defined in the theory GNL.thy.
We have proposed novel results (Theorems 1-3 in Section 4) that can help one to better recognize
situations where the local confluence property of abstract rewriting systems is and is not equivalent to
the confluence property. We have formalized Theorems 1-3 in Isabelle proof assistant software using
HOL logic. Note that Theorems 1 and 3 can be generalized to ARS that do not satisfy the acyclicity
condition using the notion of quasi-local confluence proposed in [