1 of 14

X International conference�“Information Technology and Implementation” (IT&I-2023)�Kyiv, Ukraine

On Newman’s Lemma and Non-termination

Ievgen, Ivanov, Taras Shevchenko National University of Kyiv�

Dedicated to the tenth anniversary of the Faculty of Information Technology

2 of 14

BASIC DEFINITIONS

An abstract rewriting system (ARS) is a pair (A, →) of a set A and a binary relation → ⊆ A × A
→^* denotes the reflexive transitive closure of →

An element a ∈ A is

reducible, if ∃ a’ ∈ A a → a’
irreducible, if ¬ ( ∃ a’ ∈ A a → a’ )
a normal form of b ∈ A, if ( b →^* a ) ∧ ¬ ( ∃ a’ ∈ A a → a’ )

An ARS (A, →) is

acyclic, if there is no a ∈ A such that a →⁺ a , where →⁺is the transitive closure of →
terminating, if there is no infinite sequence of the form a₁ → a₂ → a₃ → …
confluent, if

∀ a, b, c ∈ A ( a →^* b ∧ a →^* c ⇒ (∃ d ∈ A b →^* d ∧ c →^* d ) )

locally confluent, if

∀ a, b, c ∈ A ( a → b ∧ a → c ⇒ (∃ d ∈ A b →^* d ∧ c →^* d ) )

3 of 14

Reducible elements

Irreducible elements

. . .

Reduction steps

Infinite continuation

Confluent and

terminating

(complete)

Terminating,

not confluent

Not confluent,

not terminating

. . .

Confluent, but

not terminating

. . .

EXAMPLES (ACYCLIC)

4 of 14

Well-known confluence criterion: Newman’s lemma

M. H. A. Newman, On theories with a combinatorial definition of "equivalence", Annals of mathematics 43 (1942) 223-243

Modern formulation:

a terminating ARS is confluent if (and only if) it is locally confluent.

Some other confluence conditions for ARS:

- Hindley-Rosen lemma

- Rosen's requests lemma

- Huet's strong confluence lemma

- De Bruijn’s weak diamond properties

- van Oostrom’s decreasing diagrams

CONFLUENCE CRITERIA

5 of 14

Reducible elements

Irreducible elements

. . .

Reduction steps

Infinite continuation

Acyclic, locally confluent, but not confluent

NEWMAN’S COUNTEREXAMPLE

6 of 14

{0,1,2,…} is a chain �without greatest element

in the sense of the (pre)order →^*

Incomparable minimal upper bounds

of the chain (w.r.t. →*)

. . .

IN ORDER-THEORETIC TERMS

7 of 14

An ARS (A, →) is strictly inductive, if every nonempty chain in the preordered set (A, →^*) has a least upper bound.

Theorem 1. An acyclic strictly inductive ARS with at most countable set of irreducible elements is confluent if and only if it is locally confluent.

Theorem 2 (Strengthened Newman’s counterexample). �There exists an acyclic, strictly inductive, locally confluent ARS that is not confluent.

(any such ARS necessarily has an uncountable set of irreducible elements)

MAIN RESULTS

8 of 14

Reducible elements

Irreducible elements

. . .

Reduction steps

Infinite continuation

Acyclic, strictly inductive, confluent

STRICTLY INDUCTIVE ARS EXAMPLE

9 of 14

An ARS (A, →) where

A = R × R × (ω + 1), where R is the set of real numbers, ω is the first infinite ordinal

(x, y, n) → (x’, y’, n’) if and only if

(n < ω ∧ n’ = n+1 ∧ |x’ – x| < y’/2ⁿ^’∧ 0 < y’ < y) ∨ (n < ω ∧ n’ = ω ∧ x’ = x∧ 0 = y’ < y)

It is acyclic, strictly inductive, locally confluent, but is not confluent.

STRENGTHENED NEWMAN’S COUNTEREXAMPLE

10 of 14

(1/4, 0, ω)

(-1/4, 0, ω)

(0,1,0)

axis

example of a

reducible element

example of an

irreducible element

example of a reduction step

projection of the

boundary of a set of

direct successors

STRENGTHENED NEWMAN’S COUNTEREXAMPLE

11 of 14

(1, 0, ω)

(-1, 0, ω)

(0,1,0)

axis

example of a

reducible element

projection of the

set of normal forms

of (0,1,0)

NORMAL FORMS IN COUNTEREXAMPLE

12 of 14

Let (A, →) be an ARS.

The downward closure of a set B ⊆ A in the preordered set (A, →^*) is the set

{ b’ ∈ A | ∃ b ∈ B b’ →^* b }

A set B ⊆ A is closed in the preordered set (A, →^*), if for every nonempty chain C in �(A, →^*), if C ⊆ B and x is a least upper bound of C in (A, →^*), then x ∈ B

A topology T on the set of irreducible elements of (A, →) is downward-compatible with (A, →), if for every closed set of irreducible elements B (in the sense of T), �the downward closure of B is closed in the preordered set (A, →^*).

DOWNWARD-COMPATIBLE TOPOLOGY

13 of 14

Theorem 3. Let (A, →) be an acyclic strictly inductive locally confluent ARS.

Let IR be the set of all irreducible elements in (A, →).

Let T be a topology on IR that is downward-compatible with (A, →).

Then for any a ∈ A the set of normal forms of a is a connected subset of the space (IR, T).

example of a reducible element

example of a reduction step

example of a reduction sequence

connected set of normal forms of a

LOCAL CONFLUENCE AND CONNECTEDNESS

14 of 14

We have proposed novel results (Theorems 1-3) that can help one to better recognize situations where the local confluence property of ARS is and is not equivalent to the confluence property.

We have formalized Theorems 1-3 in Isabelle proof assistant software using HOL logic.

Theorems 1 and 3 can be generalized to ARS that do not satisfy the acyclicity condition using the notion of quasi-local confluence.

Study of other generalizations of the given results is a subject of further work.

CONCLUSION