# Beta normal form A lambda term is in * *beta normal form* if no beta reduction is possible * *beta-eta normal form* if neither β or η reduction is possible * *head normal form* if there is no beta-redex in head position *Head Normal Form* (HNF) describes a lambda expression whose top level is either a variable, a data value, a partially applied built-in function, or a lambda abstraction whose body is not reducible. That is, the top level lambda expr is neither a redex nor a lambda abstraction with a reducible body. An expression in HNF may contain redexes in argument postions whereas a normal form may not. 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`