In this quick post, we will walk through the proof of the Church-Rosser theorem for the untyped lambda calculus. We use the standard Tait-Martin-Löf development, which relies on the notion of parallel reduction.
The Church-Rosser theorem (or confluence) ensures that even if we reduce a term in different orders, we can always find a common term to “meet” at later.
1. The Problem: One-Step Reduction
The standard one-step $\beta$-reduction $\rightarrow_{ \beta}$ does not satisfy the diamond property. If a term $M$ has two redexes, reducing one might destroy or duplicate the other, making it impossible to close the diamond in exactly one step.
For example, consider $M = (\lambda x. x x) ((\lambda y. y) z)$.
- $M \rightarrow_{\beta} (\lambda x. x x) z$
- $M \rightarrow_{\beta} ((\lambda y. y) z) ((\lambda y. y) z)$
To prove confluence for the transitive-reflexive closure $\twoheadrightarrow_{\beta}$, we introduce a middle ground.
2. Parallel Reduction
We define a new relation, parallel reduction ($\Rightarrow$), which allows reducing multiple redexes simultaneously in a single step. It is defined inductively:
- $x \Rightarrow x$
- If $M \Rightarrow M’$, then $\lambda x. M \Rightarrow \lambda x. M’$
- If $M \Rightarrow M’$ and $N \Rightarrow N’$, then $M N \Rightarrow M’ N’$
- If $M \Rightarrow M’$ and $N \Rightarrow N’$, then $(\lambda x. M) N \Rightarrow M’[x := N’]$
Crucially, $\Rightarrow$ sits between $\rightarrow_{\beta}$ and $\twoheadrightarrow_{\beta}$:
$$
\rightarrow_{\beta} ;\subset; \Rightarrow ;\subset; \twoheadrightarrow_{\beta}
$$
3. The Diamond Property for $\Rightarrow$
The core of the proof is showing that $\Rightarrow$ satisfies the diamond property:
If $M \Rightarrow A$ and $M \Rightarrow B$, then there exists some $Z$ such that $A \Rightarrow Z$ and $B \Rightarrow Z$.
To prove this, we define the maximal parallel reduction $M^{\star}$, which reduces all existing redexes in $M$:
- $x^{\star} = x$
- $(\lambda x. M)^{\star} = \lambda x. M^{\star}$
- $(M N)^{\star} = M^{\star} N^{\star}$ (if $M N$ is not a redex)
- $((\lambda x. M) N)^{\star} = M^{\star}[x := N^{\star}]$
By induction on the structure of the proof of $M \Rightarrow A$, one can show that if $M \Rightarrow A$, then $A \Rightarrow M^{\star}$. This immediately closes the diamond:
$$
\begin{CD}
M @>>> A \
@VVV @VVV \
B @>>> M^{\star}
\end{CD}
$$
4. Confluence of $\twoheadrightarrow_{\beta}$
The final step is the Strip Lemma and tiling. Since $\twoheadrightarrow_{\beta}$ is the transitive closure of $\Rightarrow$, and $\Rightarrow$ satisfies the diamond property, we can “tile” any two diverging sequences of reductions to find a common reduct.
If $M \twoheadrightarrow_{\beta} A$ and $M \twoheadrightarrow_{\beta} B$, then there exists $Z$ such that:
$$
A \twoheadrightarrow_{\beta} Z \quad \text{and} \quad B \twoheadrightarrow_{\beta} Z
$$
5. Intuition Recap
- One-step reduction is too “small” to have the diamond property.
- Parallel reduction allows us to reduce everything at once.
- The “maximal” reduction $M^{\star}$ acts as a universal target for any parallel step.
- By tiling these diamonds, we prove that the lambda calculus is confluent.
This result is fundamental: it implies that normal forms are unique if they exist. If $M$ reduces to a normal form, that normal form is the unique “endpoint” of the computation.
peace. da1729