Science Fair Project Encyclopedia
Church-Rosser theorem
In mathematical logic, the Church-Rosser theorem states that, in the lambda calculus, a term has at most one normal form. More formally, the Church-Rosser property states that the simply typed lambda calculus without η-reduction is confluent.
Specifically, if two different reductions of a term both terminate in normal forms, then the two normal forms will be identical. It is the Church-Rosser theorem that justifies references to "the normal form" of a certain term. This property is also known more generally as confluence.
The theorem was proved in 1937 by Alonzo Church and J. Barkley Rosser.
10-26-2009 08:16:03
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details