| 释义 |
Church-Rosser Theorem Church-Rosser theorem[¦chərch ¦rȯs·ər ¦thir·əm] (mathematics) If for a lambda expression there is a terminating reduction sequence yielding a reduced form B, then the leftmost reduction sequence will yield a reduced form that is equivalent to B up to renaming. Church-Rosser Theorem (theory)A property of a reduction system that states thatif an expression can be reduced by zero or more reductionsteps to either expression M or expression N then there existssome other expression to which both M and N can be reduced.This implies that there is a unique normal form for anyexpression since M and N cannot be different normal formsbecause the theorem says they can be reduced to some otherexpression and normal forms are irreducible by definition. Itdoes not imply that a normal form is reachable, only that ifreduction terminates it will reach a unique normal form. |