Weak Head Normal Form

Weak Head Normal Form

   <reduction, lambda calculus> (WHNF) A {lambda expression} is
   in weak head normal form (WHNF) if it is a {head normal form}
   (HNF) or any {lambda abstraction}.  I.e. the top level is not
   a {redex}.

   The term was coined by {Simon Peyton Jones} to make explicit
   the difference between {head normal form} (HNF) and what
   {graph reduction} systems produce in practice.  A lambda
   abstraction with a reducible body, e.g.

   	\ x . ((\ y . y+x) 2)

   is in WHNF but not HNF.  To reduce this expression to HNF
   would require reduction of the lambda body:

   	(\ y . y+x) 2  -->  2+x

   Reduction to WHNF avoids the {name capture} problem with its
   need for {alpha conversion} of an inner lambda abstraction and
   so is preferred in practical {graph reduction} systems.

   The same principle is often used in {strict} languages such as
   {Scheme} to provide {call-by-name} evaluation by wrapping an
   expression in a lambda abstraction with no arguments:

   	D = delay E = \ () . E

   The value of the expression is obtained by applying it to the
   empty argument list:

   	force D = apply D ()
   		= apply (\ () . E) ()
   		= E

   (1994-10-31)