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.

This article is licensed under the GNU Free Documentation License. It uses material from Wikipedia article. Browse Wikipedia for more information.