The Church-Rosser Theorem

The Church-Rosser Theorem is a fundamental result in lambda calculus.

Understanding the Church-Rosser Theorem

Imagine you are inside a maze with multiple exits:

• • You start from a point $T$.
• You see two different paths to reach a destination:
  • Path 1: $T\twoheadrightarrow T_1$
  • Path 2: $T\twoheadrightarrow T_2$

At first, it might seem like whichever path you take determines your final destination. But the Church-Rosser Theorem assures us that:

No matter which path you choose, there is always a way to navigate through the maze and arrive at the same final destination.

Formally:

In other words, even if you take different routes, there is always a common point inside the maze where the paths reconnect — ensuring that all roads ultimately lead to the same solution.

Visual representation of Church-Rosser

The theorem guarantees a diamond structure for reductions:

No matter which reduction path you follow, they will always converge to a common term $T_3$.

Corollary: Uniqueness of normal forms

A normal form is an expression that cannot be further reduced — it is fully simplified.

This means that no matter how we reduce a term, as long as a normal form exists, we will always reach the same result.

Proof of uniqueness

Suppose that for a given term $T$, there are two different normal forms, $N_1$ and $N_2$. The Church-Rosser Theorem ensures that:

1. We start from $T$:

   $$T\twoheadrightarrow N_1\text{and}T\twoheadrightarrow N_2$$

2. By the Church-Rosser Theorem, both paths must join:

   $$N_1\twoheadrightarrow N\text{and}{N}_2\twoheadrightarrow N$$

3. However, $N_1$ and $N_2$ are normal forms — they cannot be reduced further (or changed):

   $$N_1=N\text{and}{N}_2=N$$

4. This means:

   $$N_1=N_2$$

✅ Conclusion: If a normal form exists, it is unique!