Weak Head Normal Form


Weak Head Normal Form

(reduction, lambda calculus)(WHNF) A lambda expression isin weak head normal form (WHNF) if it is a head normal form(HNF) or any lambda abstraction. I.e. the top level is nota redex.

The term was coined by Simon Peyton Jones to make explicitthe difference between head normal form (HNF) and whatgraph reduction systems produce in practice. A lambdaabstraction with a reducible body, e.g.

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

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

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

Reduction to WHNF avoids the name capture problem with itsneed for alpha conversion of an inner lambda abstraction andso is preferred in practical graph reduction systems.

The same principle is often used in strict languages such asScheme to provide call-by-name evaluation by wrapping anexpression in a lambda abstraction with no arguments:

D = delay E = \\ () . E

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

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