The notion of head reduction in the untyped -calculus is defined by the single axiom
We call a head redex.
In other words, a head reduction can happen at the head of a term, which is the leftmost application that remains after we "peel off" as many -abstractions as we can.
The head normal forms are the untyped terms that are normal forms for head reduction. These are the terms that do not have a redex at head position. As such, they are always of the form
for , and a (possibly free) variable .
Deciding whether a term has a head normal form is undecidable.