# 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.