Church–Rosser theorem

From Wikipedia, the free encyclopedia

The Church–Rosser theorem states that if there are two distinct reductions starting from the same term in lambda calculus, then there exists a term that is reachable via a (possibly empty) sequence of reductions from both reducts. As a consequence, a term in the lambda calculus has at most one normal form. It is thus the Church–Rosser theorem that justifies references to "the normal form" of a certain term. The theorem was proved in 1937 by Alonzo Church and J. Barkley Rosser.

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 the 1980s, the Church–Rosser theorem was established for extensions of the lambda calculus with features from imperative programming languages.