Church–Rosser theorem

All roads lead to Rome. Do they? The Church–Rosser theorem says so: it guarantees uniqueness of the normal form, whichever paths we take towards it. Admittedly, in a Turing-complete language we may never reach a normal form at all — but if we do reach one, it is unique: whichever way you go, you arrive precisely in Rome.

If $M$ $\twoheadrightarrow_\beta N$ and $M$ $\twoheadrightarrow_\beta K$, then there is an $L$ such that $N$ $\twoheadrightarrow_\beta L$ and $K$ $\twoheadrightarrow_\beta L$. In other words, $\twoheadrightarrow_\beta$ has the diamond property (confluence):

The proof is best carried out via parallel reduction. We need three reduction operators on terms:

• $\to_\beta$ — ordinary, single-step β-reduction: $M$ $\to_\beta N$ means one redex in $M$ is chosen and contracted (one step — one redex);
• $\Rightarrow$ — parallel reduction: $M$ $\Rightarrow N$ means an arbitrary set of redexes already present in $M$ is contracted (zero, one, two — any number), each at most once, and only the existing ones, not their future copies;
• $\twoheadrightarrow_\beta$ — multi-step reduction (the reflexive-transitive closure of $\to_\beta$): $M$ $\twoheadrightarrow_\beta N$ means there is a chain $M$ $\to_\beta \dots$ $\to_\beta N$ of any length, including zero.

Single-step reduction is a special case of parallel reduction, which in turn is a special case of multi-step reduction:

Why can't the diamond property be proved directly for single-step reduction $\to_\beta$ (fig. 1.1, a)? Redex copying gets in the way. Take a term with two redexes — an outer and an inner one:

Contract the outer redex — the substitution duplicates the inner one: we get $\bigl((\lambda y.y)\,z\bigr)\,\bigl((\lambda y.y)\,z\bigr)$. Contract the inner one — we get $(\lambda x.x\,x)\,z$. The paths have diverged by one step, but they can no longer meet in one step: the second term yields $z\,z$ immediately, while the first needs two steps, one per copy. So the single-step diamond property for $\to_\beta$ is simply false.

Parallel reduction $\Rightarrow$ cures exactly this disease: it contracts all the multiplied copies of a redex at once, in a single tick. For it the diamond property does hold (fig. 1.1, b), and it is proved by Takahashi's trick — via the complete development.

The complete development $M^{*}$ is the term in which all redexes visible in $M$ are contracted simultaneously — the greediest parallel step possible. It is defined by induction on the structure of the term:

The first rule: $x^{*}$ $= x$ — a variable develops into itself.

The second rule: $(\lambda x.P)^{*}$ $= \lambda x.P^{*}$ — the development goes under the abstraction.

The third rule: $(P\,Q)^{*}$ $= P^{*}\,Q^{*}$ if $P\,Q$ is not a redex ($P$ is not an abstraction): the parts are developed independently.

The fourth rule: $\bigl((\lambda x.P)\,Q\bigr)^{*}$ $= P^{*}[x\!:=\!Q^{*}]$ — the redex itself is contracted, and its parts are developed as well.

Let us develop the counterexample term by these rules:

• $\bigl((\lambda x.x\,x)\,((\lambda y.y)\,z)\bigr)^{*}$ $= (x\,x)^{*}[x\!:=\!((\lambda y.y)\,z)^{*}]$ — the whole term is a redex, so the fourth rule fires: the outer redex is contracted and both its parts go into development;
• $(x\,x)^{*}$ $= x^{*}\,x^{*}$ $= x\,x$ — the application $x\,x$ is not a redex: the third rule, then the first for each variable;
• $((\lambda y.y)\,z)^{*}$ $= y^{*}[y\!:=\!z^{*}]$ $= y[y\!:=\!z]$ $= z$ — the inner redex: the fourth rule, then the first twice;
• $(x\,x)[x\!:=\!z]$ $= z\,z$ — it remains to perform the substitution.

So $M^{*}$ $= z\,z$: the development has contracted both the outer redex and the inner one — before the latter had a chance to multiply. The whole construction rests on the triangle lemma.

Triangle lemma. The complete development cannot be overtaken: whatever the parallel step $M$ $\Rightarrow N$, exactly one parallel step leads from $N$ to $M^{*}$:

A parallel step is not obliged to contract all the redexes — from a single $M$ the steps $\Rightarrow$ lead to a whole fan of terms, and the complete development is merely the extreme, greediest point of that fan. So the step $N$ $\Rightarrow M^{*}$ is in general a real one; it is a zero step only when everything has already been contracted and $N$ $= M^{*}$.

A reduction that contracts all visible redexes at once, in a single sweep, is called the Gross–Knuth reduction $M$ $\Rightarrow_{\mathrm{GK}} M^{*}$. But it is of no interest to us: it has no variability — from a given term such a step leads to exactly one result. And the Church–Rosser theorem is precisely about variability: the paths $\twoheadrightarrow_\beta$ contract redexes in an arbitrary order, and they cannot be decomposed into rigid Gross–Knuth steps. What is needed is precisely the freedom to contract any subset.

The diamond property follows from the triangle immediately. Suppose $M$ $\Rightarrow N$ and $M$ $\Rightarrow K$. By the triangle lemma $N$ $\Rightarrow M^{*}$ and $K$ $\Rightarrow M^{*}$ — take $L$ $= M^{*}$, and both sides close in one step (fig. 1.2, right). The common point is the same for all: it depends neither on $N$ nor on $K$.

It remains to lift the diamond property from a single parallel step to multi-step reduction (fig. 1.1, c). The inclusions (1.32)$\displaystyle {\to_\beta}$ $\displaystyle \subseteq {\Rightarrow}$ $\displaystyle \subseteq {\twoheadrightarrow_\beta}$ let us read any chain of $\to_\beta$-steps as a chain of $\Rightarrow$-steps and vice versa. So let us write out $M$ $\twoheadrightarrow_\beta N$ and $M$ $\twoheadrightarrow_\beta K$ as two chains of parallel steps, lay them along the sides of a grid and complete it cell by cell — each cell is closed by the diamond property for $\Rightarrow$.

Having filled the whole grid, we obtain at the bottom vertex a term $L$ where both chains converge. All edges of the grid are parallel steps, and ${\Rightarrow}$ $\subseteq {\twoheadrightarrow_\beta}$, so $N$ $\twoheadrightarrow_\beta L$ and $K$ $\twoheadrightarrow_\beta L$. The Church–Rosser theorem is proved.

The Church–Rosser theorem (1.31)$\displaystyle M$ $\displaystyle \twoheadrightarrow_\beta N,\;\; M$ $\displaystyle \twoheadrightarrow_\beta K \;\;$ $\displaystyle \Longrightarrow\;\; \exists L:\; N$ $\displaystyle \twoheadrightarrow_\beta L,\;\; K$ $\displaystyle \twoheadrightarrow_\beta L$ immediately gives the existence of a common reduct: if $M$ $=_\beta N$, there is an $L$ with $M$ $\twoheadrightarrow_\beta L$ and $N$ $\twoheadrightarrow_\beta L$ (induction on the definition of $=_\beta$). Hence the uniqueness of the normal form: a term has at most one β-NF — two paths would meet at a common $L$, and an NF does not reduce further, so $N_1$ $\equiv L$ $\equiv N_2$. Next, reduction to NF: if $N$ is a normal form of $M$, then $M$ $\twoheadrightarrow_\beta N$ (not merely $M$ $=_\beta N$). Finally, consistency: distinct normal forms are not β-equal — e.g. $\mathrm{true}$ and $\mathrm{false}$ — otherwise uniqueness of the NF would fail; this is how term “inequalities” are proved.

The order of contracting redexes, then, does not change the result — only whether the computation terminates and in how many steps. Choosing that order is the job of reduction strategies.