The Church-Rosser theorem reference article from the English Wikipedia on 24-Apr-2004 (provided by Fixed Reference: snapshots of Wikipedia from wikipedia.org)

Church-Rosser theorem

The Church-Rosser theorem states that, in the lambda calculus, a term has at most one normal form. 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.

The theorem was discovered in 1937 by Alonzo Church and J. Barkley Rosser.

See also lambda calculus.

This is the "Church-Rosser theorem" reference article from the English Wikipedia. All text is available under the terms of the GNU Free Documentation License. See also our Disclaimer.