head normalisation theorem

1 definition found

head normalisation theorem - Free On-line Dictionary of Computing (26 May 2007) :

  head normalisation theorem
  
     Under the typed lambda-calculus, beta/delta reduction of the
     left-most redex (normal order reduction) is guaranteed to
     terminate with a head normal form if one exists.  See also
     Church-Rosser theorem.