You are here: irt.org | FOLDOC | Church-Rosser Theorem

<*theory*> A property of a reduction system that states that
if an expression can be reduced by zero or more reduction
steps to either expression M or expression N then there exists
some other expression to which both M and N can be reduced.
This implies that there is a unique normal form for any
expression since M and N cannot be different normal forms
because the theorem says they can be reduced to some other
expression and normal forms are irreducible by definition. It
does not imply that a normal form is reachable, only that if
reduction terminates it will reach a unique normal form.

(1995-01-25)

Nearby terms: Church, Alonzo « Church integer « Church of the SubGenius « **Church-Rosser Theorem** » ci » CI$ » CICERO

FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL