Source : Free On-Line Dictionary of Computing
Weak Head Normal Form
(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)