Weak Head Normal Form
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)
(\ y . y+x) 2 --> 2+x
D = delay E = \ () . E
force D = apply D () = apply (\ () . E) () = E