
related topics 
{math, number, function} 
{line, north, south} 

The Church–Rosser theorem states that if there are two distinct reductions starting from the same lambda calculus term, then there exists a term that is reachable from each reduct via a (possibly empty) sequence of reductions. This is symbolized by the diagram at right: if term a can be reduced to both b and c, then there must be a further term d (possibly equal to either b or c) to which both b and c can be reduced.
Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem is a theorem of confluence. 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 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 simplytyped lambda calculus, many calculi with advanced type systems, and Gordon Plotkin's betavalue 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).
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.
Full article ▸


related documents 
CoNPcomplete 
Measurable function 
Power associativity 
Prime ideal 
Almost all 
Equivalence class 
Center (group theory) 
Leaf node 
Senary 
Sieve of Eratosthenes 
Ring homomorphism 
CoNP 
Digital Signature Algorithm 
Probability axioms 
Gabriel Lamé 
Integer sequence 
Endomorphism ring 
Mary (programming language) 
Gauss–Legendre algorithm 
Krull dimension 
Sedenion 
Euclidean distance 
Selfsimilarity 
Markov process 
Identity function 
Disjoint sets 
Contextsensitive language 
JUnit 
Galois group 
Timeline of programming languages 
