|
|
|
|
|
Church-rosser TheoremIn 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.
|
 |
|
| Copyright 2005-2009 OnPedia.com. All Rights Reserved |
|
|