Editing Church–Rosser theorem (section)

==Pure untyped lambda calculus==
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 <math>( \lambda x . t) s</math> is contracted by the substitution <math> t [ x := s]</math>. If β-reduction is denoted by <math> \rightarrow_\beta </math> and its reflexive, transitive closure by <math> \twoheadrightarrow_\beta </math> then the Church–Rosser theorem is that:{{sfnp|Barendregt|1984|p=53–54}}
:<math>\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</math>

A consequence of this property is that two terms equal in <math>\lambda\beta</math> must reduce to a common term:{{sfnp|Barendregt|1984|p=54}}
:<math>\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</math>

The theorem also applies to η-reduction, in which a subterm <math>\lambda x.Sx</math> is replaced by <math>S</math>. It also applies to βη-reduction, the union of the two reduction rules.

===Proof===
For β-reduction, one proof method originates from [[William W. Tait]] and [[Per Martin-Löf]].{{sfnp|Barendregt|1984|p=59-62}} Say that a binary relation <math> \rightarrow </math> satisfies the diamond property if:
:<math>\forall M, N_1, N_2 \in \Lambda: \text{if}\ M\rightarrow N_1 \ \text{and}\ M\rightarrow N_2 \ \text{then}\ \exists X\in \Lambda: N_1\rightarrow X \ \text{and}\ N_2\rightarrow X</math>

Then the Church–Rosser property is the statement that <math> \twoheadrightarrow_\beta </math> satisfies the diamond property. We introduce a new reduction <math> \rightarrow_{\|} </math> whose reflexive transitive closure is <math> \twoheadrightarrow_\beta </math> and which satisfies the diamond property. By induction on the number of steps in the reduction, it thus follows that <math> \twoheadrightarrow_\beta </math> satisfies the diamond property.

The relation <math> \rightarrow_{\|} </math> has the formation rules:
*<math>M \rightarrow_{\|} M</math>
*If <math>M \rightarrow_{\|} M'</math> and <math>N \rightarrow_{\|} N'</math> then <math>\lambda x.M \rightarrow_{\|} \lambda x.M'</math> and <math>MN \rightarrow_{\|} M'N'</math> and <math>(\lambda x. M)N \rightarrow_{\|} M'[x:=N']</math>

The η-reduction rule can be proved to be Church–Rosser directly. Then, it can be proved that β-reduction and η-reduction commute in the sense that:{{sfnp|Barendregt|1984|p=64–65}}
:If <math>M \rightarrow_\beta N_1</math> and <math>M \rightarrow_\eta N_2</math> then there exists a term <math>X</math> such that <math>N_1 \rightarrow_\eta X</math> and <math>N_2\rightarrow_\beta X</math>.

Hence we can conclude that βη-reduction is Church–Rosser.{{sfnp|Barendregt|1984|p=66}}