XI INTERNATIONAL CONFERENCE

“INFORMATION TECHNOLOGY AND IMPLEMENTATION” (IT&I-2024)

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

Ievgen, Ivanov

Introduction

• Formal methods¹ - mathematical approaches to specification, development, analysis, verification of

software and systems

• Rewriting theory²: studies properties of rewriting systems – mathematical models that can be used to describe computation or automated reasoning as a sequence of steps that transform an object in accordance with a set of rules, e.g. (1 * 2) * 3 → 2 * 3 → 6

• Confluence of rewriting systems³ - according to the International Workshop on Confluence:

“... Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. ...”

¹ http://fmeurope.org

² http://ifip-tc1.org/wg1-06.php

³ http://cl-informatik.uibk.ac.at/iwc/

2/16

Abstract rewriting systems

An abstract rewriting system (ARS) (A, →) is a pair of

a set (of elements) A

and a binary relation → on A (reduction), elements of → are called reduction steps.

Some possible interpretations of reduction steps:

1. Computation / evaluation steps, e.g. 2 * 3 → 6
2. Reasoning / inference steps
3. State evolution, e.g. x → y means that x and y are states that can be joined by a trajectory
4. Causality, e.g. x → y are events and x causally precedes y

3/16

Interpretations 1, 2 (computation, reasoning)

Consider a concurrent algorithm:

1) Input positive integers A, B, C

2) Run 3 instances of a simple sequential GCD algorithm concurrently on different pairs of shared variables A, B, C:

Thread 1: while (A != B) { if (A < B) B = B - A; else A = A - B; }

Thread 2: while (B != C) { if (B < C) C = C - B; else B = B - C; }

Thread 3: while (A != C) { if (A < C) C = C - A; else A = A - C; }

3) When threads 1-3 exit, output A

How to check if the program (always) computes GCD of A, B,C under a given concurrency assumptions and memory model ?

4/16

Interpretation 3 (state evolution)

ARS (A, →), where

A = [0, + ∝) × (-∝, +∝) is a continuous state space

(y₁, v₁) → (y₂, v₂), if, semi-formally, in a hybrid system given below (y₂, v₂) can be reached from (y₁, v₁)

• either using continuous evolution within one discrete state
• or as a result of a single discrete transition between discrete states that may coincide

5/16

Illustration of a partial run

6/16

State space

7/16

Interpretation 4 (causality)

ARS (A, →), where

A = { (x, t) ∈ R × R | t ≤ 0 }

(x₁, t₁) → (x₂, t₂) iff

t₂ – t₁ > 0 and (t₂ – t₁)² – (x₂ – x₁)² ≥ 0

x, t are space and time coordinates

→ is the strict causal precedence between

events in (1+1) dimensional

Minkowski spacetime restricted to A

For related structures in the context

of distributed computing in computer science:

F. Mattern. On the relativistic structure of

logical time in distributed systems

8/16

Classes of ARS

An ARS (A, →) is

• terminating, if there is no infinite reduction sequence a₁ → a₂ → a₃ → …
• countable, if there is a surjective function from the set of natural numbers to 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 ) )

where →* denotes the reflexive transitive closure of the relation → on A

a

c

b

d

*

*

*

*

a

c

b

d

*

*

Confluence

Local confluence

Note: for terminating ARS, confluence = local confluence (Newman’s lemma),

but in the general case, the local confluence condition is weaker than confluence

9/16

Illustrations of ARS

Reducible elements

. . .

Reduction steps

Infinite continuation

Confluent and

terminating

Terminating,

not confluent

Not confluent,

not terminating

. . .

Confluent, but

not terminating

. . .

. . .

Irreducible elements

10/16

Decreasing diagrams method for proving confluence

One can overcome limitations of Newman’s lemma using

Van Oostrom’s decreasing diagrams method¹

Semi-formally, to prove that an ARS (A,→) is confluent:

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

Rigorously this can be formulated using the notion of a

decreasing Church-Rosser (DCR) ARS

¹ V. van Oostrom. Confluence by decreasing diagrams.

Theoretical computer science 126, pp. 259–280, 1994

a

c

b

d

*

*

=

*

*

=

α

β

<β

α

<β∨<α

<α∨<β

β

<α

means that y can be reached from x

using a finite sequence of

0 or more reduction steps labeled using

labels that satisfy a condition C

*

C

x

y

means that y can be reached from x

using 0 or 1 reduction step labeled using

a label that satisfies a condition C

=

C

x

y

c₂

c₃

b₂

b₃

11/16

DCR hierarchy

J. Endrullis, J.W. Klop, R. Overbeek introduced ¹ a hierarchy of subclasses of DCR ARS:

DCR₀ ⊆ DCR₁ ⊆ DCR₂ ...

Semi-formally, DCR_α is the class of confluent ARS for which confluence can be proved with the help of the decreasing diagrams method using

• a fixed set of labels { β | β<α } ( ordinals less than α )
• a fixed order on them that is a restriction of the usual order on ordinals to {β | β < α}

They also showed that confluence of a (confluent) countable ARS can always be proved with the help of the decreasing diagrams method using the label set {0, 1} ordered in such a way that 0 < 1:

DCR₂ ∩ CNT = CR ∩ CNT

where CR is the class of confluent ARS, CNT is the class of countable ARS

¹ J. Endrullis, J.W. Klop, R. Overbeek. Decreasing diagrams with two

labels are complete for confluence of countable systems. FSCD 2018, P. 14:1–14:15, 2018

12/16

Non-triviality of DCR hierarchy

Does there exist an (uncountable) confluent ARS outside of the class DCR₂ (open problem 32 in [1]) ?

It turns out the answer is YES ² , i.e. the DCR₂ method is incomplete

for proving confluence in the general case, though it is complete for countable ARS.

Moreover, the DCR hierarchy does not collapse at the level 2.

Formal proof in Isabelle proof assistant using HOL logic:

http://doi.org/10.5281/zenodo.11571490

¹ J. Endrullis, J.W. Klop, R. Overbeek. Decreasing diagrams with two

labels are complete for confluence of countable systems. FSCD 2018, P. 14:1–14:15, 2018

² I. Ivanov. On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems, IWC 2024, 2024

13/16

Main result

Theorem. Let (A, →), (B, →′) be ARS such that

1. (B, →′) is a weakly connected subgraph of (A, →)
2. B is a cofinal subset in the preordered set (A, →*), i.e. ∀a ∈ A ∃b ∈B a →* b .
3. Then for any positive integer n (or, more generally, for any non-zero ordinal n), �if (B, →′) belongs to DCR_n , then (A, →) belongs to DCR_n+1.

For example, if (A, →) has a cofinal reduction sequence b₀ → b₁ → …,

one can take (B, → ) to be this sequence:

(B, → ) is trivially in DCR₁, so (A, → ) must be in DCR₂.

This result has been formally verified for all positive integer n using Isabelle proof assistant.

14/16

Formalization in Isabelle

15/16

Further work

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

16/16