Head Normal Form

In the lambda calculus a head normal form is a λ-term that has a top-level abstraction where the body does not have λ-subterms that can have β-reductions applied to them. It may be the case that arguments may have subterms that can be β-reduced. Every normal form λ-term is also a head normal form λ-term.

A β-reduction choice strategy that leads to head normal forms is called head normalising.



W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.