Church–Rosser theorem

In 1936, Alonzo Church and J. Barkley Rosser proved that the theorem holds for β-reduction in the λI-calculus (in which every abstracted variable must appear in the term's body). The proof method is known as "finiteness of developments", and it has additional consequences such as the Standardization Theorem, which relates to a method in which reductions can be performed from left to right to reach a normal form (if one exists). The result for the pure untyped lambda calculus was proved by D. E. Shroer in 1965.[2]

One type of reduction in the pure untyped lambda calculus for which the Church–Rosser theorem applies is β-reduction, in which a subterm of the form ${\displaystyle (\lambda x.t)s}$ is contracted by the substitution ${\displaystyle t[x:=s]}$. If β-reduction is denoted by ${\displaystyle \rightarrow _{\beta }}$ and its reflexive, transitive closure by ${\displaystyle \twoheadrightarrow _{\beta }}$ then the Church–Rosser theorem is that:[3]

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda$ :{\text{if}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{and}}\ M\twoheadrightarrow _{\beta }N_{2}\ {\text{then}}\ \exists X\in \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{and}}\ N_{2}\twoheadrightarrow _{\beta }X}

A consequence of this property is that two terms equal in ${\displaystyle \lambda \beta }$ must reduce to a common term:[4]

${\displaystyle \forall M,N\in \Lambda$ :{\text{if}}\ \lambda \beta \vdash M=N\ {\text{then}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{and}}\ N\twoheadrightarrow _{\beta }X}

The theorem also applies to η-reduction, in which a subterm ${\displaystyle \lambda x.Sx}$ is replaced by ${\displaystyle S}$. It also applies to βη-reduction, the union of the two reduction rules.

A reduction rule that satisfies the Church–Rosser property has the property that every term M can have at most one distinct normal form, as follows: if X and Y are normal forms of M then by the Church–Rosser property, they both reduce to an equal term Z. Both terms are already normal forms so ${\displaystyle X=Z=Y}$.[4]

If a reduction is strongly normalising (there are no infinite reduction paths) then a weak form of the Church–Rosser property implies the full property (see Newman's lemma). The weak property, for a relation ${\displaystyle \rightarrow }$, is:[8]

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda$ :} if ${\displaystyle M\rightarrow N_{1}}$ and ${\displaystyle M\rightarrow N_{2}}$ then there exists a term ${\displaystyle X}$ such that ${\displaystyle N_{1}\twoheadrightarrow X}$ and ${\displaystyle N_{2}\twoheadrightarrow X}$.

The Church–Rosser theorem also holds for many variants of the lambda calculus, such as the simply-typed lambda calculus, many calculi with advanced type systems, and Gordon Plotkin's beta-value calculus. Plotkin also used a Church–Rosser theorem to prove that the evaluation of functional programs (for both lazy evaluation and eager evaluation) is a function from programs to values (a subset of the lambda terms).

In older research papers, a rewriting system is said to be Church–Rosser, or to have the Church–Rosser property, when it is confluent.

• Alama, Jesse (2017). Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy (Fall 2017 ed.). Metaphysics Research Lab, Stanford University.
• Church, Alonzo; Rosser, J. Barkley (May 1936), "Some properties of conversion" (PDF), Transactions of the American Mathematical Society, 39 (3): 472–482, doi:10.2307/1989762, JSTOR 1989762.
• Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103 (Revised ed.), North Holland, Amsterdam, ISBN 0-444-87508-5, archived from the original on 2004-08-23. Errata.