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 1936 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.
[edit] See also
[edit] References
Alonzo Church and J. Barkley Rosser. Some properties of conversion. Transactions of the American Mathematical Society, vol. 39, No. 3. (May 1936), pp. 472-482.
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
