In
mathematics and
theoretical computer science, the
Church–Rosser theorem states that, when applying
reduction rules to
terms in the
lambda calculus, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions. The theorem was proved in 1936 by
Alonzo Church and
J. Barkley Rosser, after whom it is named.