Weak Head Normal Form

In the lambda calculus a weak head normal form is a λ-term that is either

• a top-level abstraction which may have λ-subterms in the body that can have β-reductions applied to them, or
• any term that is not β-reducible.

Every head normal form λ-term is also a weak head normal form λ-term.

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

Examples

• λx.x is a weak head normal form.
• λx.(λy.y z) is a weak head normal form.
• λx.x y is not a weak head normal form.

References

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