Head reduction (untyped)

The notion of head reduction in the untyped \lambda-calculus is defined by the single axiom

 \lambda x_1 \ldots x_n.\; (\lambda x. M)N N_1 \ldots N_m
 		\longrightarrow
 \lambda x_1 \ldots x_n.\; M[N/x] N_1 \ldots N_m

We call (\lambda x. M)N 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 \lambda-abstractions as we can.

Head normal forms

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

 \lambda x_1 \ldots x_n.\; y N_1 \ldots N_m

for n, m >= 0, and a (possibly free) variable y.

Deciding whether a term has a head normal form is undecidable.

Head reduction (untyped)

Head normal forms

See also