Notes on Abstract Reduction Systems

1. Introduction
2. Reduction
3. Properties of reductions
4. Relating termination, normalization and confluence
5. Well-founded induction
6. Proving confluence
- 6.1. Newman's Lemma (Termination and local confluence imply confluence)
  - 6.1.1. Proof
7. References and Further Reading

Change log

UNNUMBERED: notoc

[2022-09-28 Wed] Added theorems equating WFI with termination, and also the proof of Newmann's Lemma.
[2018-08-22 Wed] Added notes on strong induction versus regular induction.
[2018-08-22 Wed] Added notes on Induction on deductions.
[2018-08-22 Wed] Added definition of ``completely simplifies to.''

1 Introduction

This section introduces some basic definitions and results of reduction systems. This material is based on Chapter 1 of "Term Rewriting and All that", Baader and Nipkow (Cambridge University Press 1998).

2 Reduction

2.1 Abstract Reduction system

An abstract reduction system is simply any binary relation $\reducesto$ over a set $A$ of elements. Abstract' means that we make no further assumptions on either the elements of $A$ or the relation $\reducesto$. ``Reduction'' suggests that we are interested in properties motivated by reduction of algebraic expressions, also called terms. Furthermore, the word `system' is justified because the relation $(A,\reducesto)$ immediately defines a transition system with state space (and a set of initial states) $A$, a singleton input alphabet, and a view function that is identity.

2.2 Composition of relations

Let $R\subseteq A\times B$ and $S\subseteq B\times C$. The composition $R;S\subseteq A\times C$ is the relation \[\set{(a,c) \in A\times C \ | \exists b\in B. (a,b)\in R \land (b,c)\in S}\]

2.3 Relations built from Reduction

The basic reduction $\goesto{}$ on $A$ allows us to define other relations on $A$:

Notation	Definition	Name/Description
$\goesto{0}$	$\set{(a,a), a\in A}$	Identity
$\goesto{i+1}$	$\goesto{};\goesto{i}$	i+1-fold composition, $i\gt 0$
$\goesto{+}$	$\Union_{i>0} \goesto{i}$	transitive closure
$\goesto{*}$	$\goesto{+} \union \goesto{0}$	reflexive transitive closure
$\goesto{=}$	$\goesto{} \union \goesto{0}$	reflexive closure
$\goesto{-1}$	$\set{(a',a), a\goesto{}a'}$	inverse
$\connected{}$	$\goesto{} \union \goesto{-1}$	symmetric closure
$\connected{+}$	$(\connected{})^{+}$	transitive symmetric closure
$\connected{*}$	$(\connected{})^{*}$	reflexive transitive symmetric closure

2.4 Terminology

$a$ reduces to $a'$ if $a\reducesto a'$.

$a$ is reducible if there is a $a'$ such that $a\goesto{}a'$. Also written $a\goesto{}$.

$a$ simplifies to $a'$ if $a\goesto{*} a'$.

$a$ is in normal form (or is irreducible) if it is not reducible. Also written $a\not\goesto{}$.

$a'$ is a normal form of $a$ if $a$ simplifies to $a'$ and $a'$ is in normal form.

$a$ completely simplifies to $a'$ if $a'$ is a normal form of $a$.

$a$ has a normal form if there is a normal form of $a$.

$a'$ is a direct successor of $a$ if $a\goesto{}a'$.

$a'$ is a successor of $a$ if $a\goesto{+} a'$.

$a$ and $b$ are joinable if for some $c$, $a\goesto{*}c$ and $b\goesto{*}c$. Written $a\downarrow b$.

$a$ and $a'$ are connected if $a\connected{*}a'$.

3 Properties of reductions

Let reduction $(A,\goesto{})$ be an ARS. In the following, unless stated otherwise, all variables are universally quantified.

Church-Rosser: iff $x\connected{*}y$ then $x\downarrow y$.
Confluent: $a\goesto{*}b$ and $a\goesto{*}c$ implies $b\downarrow c$.
Semi-confluent: $a\goesto{}b$ and $a\goesto{*}c$ implies $b\downarrow c$.
Locally-confluent: $a\goesto{}b$ and $a\goesto{}c$ implies $b\downarrow c$.
Normalizing: iff every element simplifies to a normal form.
Terminating: iff there is no infinite chain $a_0\goesto{} a_1\goesto{} \ldots$.
Convergent: iff it is terminating and confluent.

4 Relating termination, normalization and confluence

4.1 Theorem (Termination implies normalizing)

If $\goesto{}$ is terminating, then it is is normalizing.

4.1.1 Proof

Every chain of reduction starting with an element $a$ terminates. The terminal element is a normal form of $a$.

4.2 Theorem (Confluence implies at most one normal form)

If $\goesto{}$ is confluent, then every element has at most one normal form.

4.2.1 Proof

Let $a\simplifiesto{b}$ and $a\simplifiesto{c}$ and let $b$ and $c$ both be normal forms. By confluence, these two normal forms must simplify to a common term $d$. That is $b\simplifiesto{d}$ and $c\simplifiesto{d}$. But since both $b$ and $c$ are normal forms, $b$ can only simplify to $d$ if $d$ is equal to $b$. By a similar reason $d$ also equals $c$. The normal forms $b$ and $c$ are therefore, identical.

4.3 Theorem (Confluence and Normalization imply unique normal form)

If $\goesto{}$ is normalizing and confluent, then every element has a unique normal form.

4.3.1 Proof

Normalization implies that there is at at least one normal form. Confluence implies that there is at most one normal form. Both together imply uniqueness of normal form.

5 Well-founded induction

The principle of Well-founded Induction generalizes the principle of induction on natural numbers to any reduction system that is terminating.

\[ \frac{\forall a\in A. (\forall b\in A. a\goesto{}b \implies P(b)) \implies P(a)}{\forall a\in A. P(a)} \qquad \mbox{WFI} \]

That is, given a reduction $\goesto{}$ on a set $A$, to show a property $P$ is true for all $a$, it is sufficient to prove $P(a)$ assuming $P(b)$ is true for all immediate successors $b$ of $a$.

By taking $A$ to be natural numbers and $a\reducesto b$ to mean $a = b+1$ we get the standard induction principle on natural numbers.

5.1 Theorem (If $\goesto{}$ terminates then WFI holds)

5.1.1 Proof

We prove that if WFI does NOT hold, then $\goesto{}$ is non-terminating.

Assume WFI does not hold. That means the antecedent holds and the consequent doesn't, i.e., $\forall a. P(a)$ is false. Let, for some $a_0$, $P(a_0)$ be false.
Now, the antecedent is a universal statement and is true. So, let's instantiate it for $a_0$ and see what we get:
It's an implication $(\forall b\in A. a_0\goesto{}b \implies P(b)) \implies P(a_0)$.
Since we've assumed $P(a_0)$ is false, the only way the implication is true is if the antecedent of the implication above is false.
So, $\forall b\in A. a_0\goesto{}b \implies P(b)$ is false.
Let $a_1$ be an instance that falsifies the above. So, $a_0\goesto{}a_1 \implies P(a_1)$ is false.
The only way the above formula is false if is $a_0\goesto{}a_1$ and $P(a_1)$ is false.
But now, we can repeat the whole argument with $P(a_1)$, and arrive at an $a_2$ such that $a_1\goesto{}a_2$ and $P(a_2)$ is false.
Doing this ad infinitum, we have a non-terminating sequence $a_0\goesto{}a_1\goesto{}\ldots$.
Hence $(A,\goesto{})$ is non-terminating. QED.

5.2 Theorem (If WFI holds, then $\goesto{}$ terminates)

5.2.1 Proof

Assume WFI.
Pick $P(a)$ to be the predicate ``every chain starting from $a$ terminates.''
Showing that $\goesto{}$ terminates is then the same thing as showing $\forall a. P(a)$.
We claim $\forall a\in A, (\forall b\in A.\ a\goesto{}b \implies P(b)) \implies P(a)$. (Notice that this is just the antecedent of WFI).
Assume an arbitrary $a_0$. To prove the implication $(\forall b\in A.\ a\goesto{}b \implies P(b)) \implies P(a_0)$, we assume $\forall b\in A.\ a\goesto{}b \implies P(b)$ and try to prove $P(a_0)$. The assumption now is that for all immediate successors $b$ of $a_0$, $P(b)$ is true, then $P(a_0)$ is true.
We are now given that every chain from each immediate successor $b$ of $a_0$ terminates. It follows that every chain from $a_0$ terminates. If you're not convinced, assume to the contrary, that there is some chain from $a_0$ not terminating. If $b$ is the immediate successor of $a_0$ in this chain, then the chain from $b$ also does not terminate. But then we've just found a non-terminating chain starting from $b$, an immediate successor of $a_0$. Contradiction.
Hence $P(a_0)$ is true.
Since $a_0$ was arbitrary, it follows that $\forall a\in A\ (\forall b\in A.\ a\goesto{}b$ \implies P(a))$. So we have proved the claim made in Step 4.
Because we assume WFI, we concluded that the consequent $\forall a. P(a)$ is true. But this is the same thing as saying that $\goesto{}$ terminates (Step 3).

5.3 ``Strong'' Induction

The so-called strong induction principle may be stated as follows: \[ \frac{\forall a\in A. (\forall b\in A. a\goesto{+}b \implies P(b)) \implies P(a)}{\forall a\in A. P(a)} \qquad \mbox{WFI (strong)} \]

That is, to show a property $P$ is true for all $a$, it is sufficient to prove $P(a)$ assuming $P(b)$ is true for all successors – immediate or otherwise – $b$ of $a$.

The ``strong'' induction principle on natural numbers is obtained once we realise that the transitive closure of the relation $a=b+1$ is the relation $b < a$.

Despite the nomenclature, the two flavours of induction are in fact equivalent. To see why, note that

1. $\goesto{+}$ is the transitive closure of $\goesto{}$.
2. $\goesto{+}$ is terminating iff $\goesto{}$ is terminating.
3. Thus the induction principle holds for the relation $\goesto{+}$ as well.
4. The transitive closure of $\goesto{+}$ is itself.

5.4 Induction on deductions

You are familiar with the principle of induction on natural numbers, and also perhaps with the principle of structural induction on trees and expression syntax.

You might have also have come across deduction (or inference) systems used for carrying out systematic and formal reasoning.

A deduction system is used to infer judgements. An example of a judgement could be ``today is Tuesday'' or ``1+1=2'', or ``5 is a number'', etc.

A deduction system consists of rules of inference. A rule of inference looks like this:

\[\frac {A_1\quad \ldots \quad A_n}{C}\quad {R}\]

Here, the A's and C are judgements. The A's are antecedents of the rule; C is the consequent. This rule states that if, using the deduction system, we deduce each antecedent $A_i$, $1\leq i\leq n$, then we deduce the consequent $C$. Another way to say this is that we are permitted to infer $C$ only if we already have inferred all the antecedent $A$'s.

An axiom is a rule that may be thought of as an inference rule with no antecedents. Informally, an axiom requires no antecedents, its validity is self evident.

When studying properties of programming languages, we are interested proving properties of all objects deducible in a given deduction system. We do this by applying the principle of induction on the deductions themselves.

The important insight here is that deduction defines a binary relation on judgements. $a\reducesto b$ if $a$ is a consequent of some rule of which $b$ is an antecedent. Thus deduction from the antecdents to a consequent may be alternatively seen as a reduction from the consequent to each of its antecedent. Applying the principle of well-founded induction to this reduction system allows us to prove properties of judgements deduced in the deduction system. To show a property $P$ about all derivable judgements, show that $P(a)$ is true for all axioms $a$ and then show, for each deduction

\[\frac {a_1\quad \ldots \quad a_n}{c}\quad {R}\] assuming $P$ is true for each antecedent $a_1, \ldots, a_n$ then $P(c)$ is true.

6 Proving confluence

$\goesto{}$ is locally confluent if $a\rightarrow b$ and $a\rightarrow c$ implies $b\downarrow c$: if $a$ reduces to two elements $b$ and $c$, then $b$ and $c$ are joinable.

Local confluence is weaker than confluence. That is, confluence implies local confluence (Exercise: prove it), but local confluence does not imply confluence. Examples of the latter fact are given in TRAAT, page 29.

However, if in addition to being locally confluent, an ARS is terminating, then it is confluent.

6.1 Newman's Lemma (Termination and local confluence imply confluence)

If $(A,\goesto{})$ is terminating and locally confluent, then it is confluent.

6.1.1 Proof

Since $(A,\goesto{})$ is terminating, we get to apply WFI on it.
We consider the predicate $P(a)=\forall b, c:\ a\goesto{*}b$ and $a\goesto{*}c$ implies $b\downarrow c$. Confluence is the same this as saying that $\forall a.\ P(a)$.
Let $x$ be an arbitrary element of $A$. Further assume that $x\goesto{*}y$ and $x\goesto{*}z$.
If $x=y$ or $x=z$, then $y\downarrow z$ follows immediately.
Otherwise, $y$ and $z$ are at least one step away from $x$, i.e., $x\goesto{}y_1\goesto{*}y$ and $x\goesto{}z_1\goesto{*}z$.
From local confluence, it follows $y_1\downarrow z_1$. Let's assume they meet at $u$.
By the WFI hypothesis both $y_1$ and $z_1$ satisfy $P$.
Consider $y_1$. $y_1\goesto{*}y$ and $y_1\goesto{*}u$. Hence $y_1\downarrow u$. Assume they meet at $v$.
Consider $z_1$. $z_1\goesto{*}u$ (Step 6). $u\goesto{*}v$ (Step 8). Hence, $z_1\goesto{*}v$. Also, $z_1\goesto{*}z$ (Step 5). By another application of the WFI hypthesis, we have $v\downarrow z$. Let them meet at $w$.
It is now clear that we have $y\goesto{*}v$ (Step 8) and $v\goesto{*}w$ (Step 9), while $z\goesto{*}w$. This just means that $y$ and $z$ are joinable.
We can discharge the assumption $x$ reaches $y$ and $z$ to get the implication $x\goesto{*}y$ and $x\goesto{*}z$ implies $y\downarrow$.
Note that in Step 11, $x$ was arbitrary. If we universally quantifying over $x$, we have $\forall x,y,z\in A, x\goesto{*}y$ and $x\goesto{*} z$ implies $y\downarrow z$. But this is the same thing as saying that $(A,\goesto{})$ is confluent. QED.

If you see the book (TRAAT, p29), there is a nice diagram that visually captures the proof.

7 References and Further Reading

Wolfram's Finally We May Have a Path to the Fundamental Theory of Physics … and It's Beautiful :: Stephen Wolfram's 2020 article where he takes the concept of graph transformation, essentially higher order reductions of Abstract Reduction Systems and explores its connection with Physics. You may also want to read about Wolfram's Physics project: A Class of Models with the Potential to Represent Fundamental Physics.

Notation	Definition	Name/Description
\(\goesto{0}\)	\(\set{(a,a), a\in A}\)	Identity
\(\goesto{i+1}\)	\(\goesto{};\goesto{i}\)	i+1-fold composition, \(i\gt 0\)
\(\goesto{+}\)	\(\Union_{i>0} \goesto{i}\)	transitive closure
\(\goesto{*}\)	\(\goesto{+} \union \goesto{0}\)	reflexive transitive closure
\(\goesto{=}\)	\(\goesto{} \union \goesto{0}\)	reflexive closure
\(\goesto{-1}\)	\(\set{(a',a), a\goesto{}a'}\)	inverse
\(\connected{}\)	\(\goesto{} \union \goesto{-1}\)	symmetric closure
\(\connected{+}\)	\((\connected{})^{+}\)	transitive symmetric closure
\(\connected{*}\)	\((\connected{})^{*}\)	reflexive transitive symmetric closure