Church-Rosser theorems and the lambda (λ) calculus

---

This article is part of a series of articles on the lambda calculus and is also available as a YouTube video.

1. What is the lambda (λ) calculus?
2. Bound vs. free variables in the lambda (λ) calculus
3. Delta (δ) rules in the lambda (λ) calculus
4. Beta (β) reduction in the lambda (λ) calculus
5. Alpha (α) conversion in the lambda (λ) calculus
6. Eta (η) conversion in the lambda (λ) calculus
7. Summary of the lambda calculus (λ) evaluation rules
8. Lambda calculus (λ) reduction orders and normal form
9. (This article) The Church-Rosser theorem and the lambda (λ) calculus

---

We left the previous article discussing reduction orders and normal form with an outstanding question:

• Can two different reduction sequences lead to different normal forms?

Let’s look at one of the Church-Rosser theorems to find out. Alonzo Church and J. Barkley Rosser proved the following in 1936:

Church-Rosser Theorem

\[\text{If }\ E_1\leftrightarrow E_2 \text{ then there exists an expression}\ E \\ \text{such that} \ E_1 \rightarrow E \text{and} E_2 \rightarrow E\]

In plain English: all reduction sequences which do terminate will reach the same result. In other words the answer to the question: can two different reduction sequences lead to different normal forms is a no! All reduction sequences which do terminate which reach the same normal form.

That’s reassuring!

Another important result (also known as the Standardization Theorem) is that:

\[\text{If} \ E_1 \rightarrow E_2 \ \text{and} \ E_2 \ \text{is in normal form, then there exists} \\ \text{a normal order reduction sequence from} \ E_1 \ \text{to} \ E_2\]

Normal order reduction specifies that the leftmost outermost reducible expression should be reduced first. This is the reduction order we explicitly covered in the previous article and the order which leads to lazy evaluation.

That’s it for the series of articles on the lambda calculus. I hope you enjoyed it!