Church–Rosser theorem

In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.

[1] The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser, after whom it is named.

Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem states that the reduction rules of the lambda calculus are confluent.

As a consequence of the theorem, a term in the lambda calculus has at most one normal form, justifying reference to "the normal form" of a given normalizable term.

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. Schroer 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

then the Church–Rosser theorem is that:[3] A consequence of this property is that two terms equal in

must reduce to a common term:[4] The theorem also applies to η-reduction, in which a subterm

It also applies to βη-reduction, the union of the two reduction rules.

For β-reduction, one proof method originates from William W. Tait and Per Martin-Löf.

Then, it can be proved that β-reduction and η-reduction commute in the sense that:[6] Hence we can conclude that βη-reduction is Church–Rosser.

[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).

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