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.
λx.x is a head normal form.
λx.λy.y is a head normal form.
λx.(λy.y z) is not a normal form.
W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.
Copyright © 2014 Barry Watson. All rights reserved.