Church–Rosser theorem


In mathematics and theoretical computer science, the Church–Rosser theorem states that, when applying reduction rules to terms in some typed variants of the lambda calculus, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying sequences of additional reductions. The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser, after whom it is named.
The theorem is symbolized by the adjacent diagram: If term a can be reduced to both b and c, then there must be a further term d to which both b and c can be reduced.
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.
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 is a function from programs to values.
In older research papers, a rewriting system is said to be Church–Rosser, or to have the Church–Rosser property, when it is confluent.