church-rosser theorem

1 definition found

church-rosser theorem - Free On-line Dictionary of Computing (26 May 2007) :

  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)