The normal form of a term, if one exists, is unique (as a corollary of the Church–Rosser theorem).
has the following shape (note that application has higher priority than abstraction, and that the formula below is meant to be a lambda-abstraction, not an application): A beta reduction is an application of the following rewrite rule to a beta redex contained in a term: where
A normal form is a term that does not contain any beta redex,[3][5] i.e. that cannot be further reduced.
without the addition of constant or function symbols, meant to be reduced by additional delta rule), head normal forms are the terms of the following shape: A head normal form is not always a normal form,[5] because the applied arguments
This gives an inductive syntactic description of normal forms.
[6] This means a redex may appear inside a lambda body.
In general, a given term can contain several redexes, hence several different beta reductions could be applied.
Normal-order reduction is complete, in the sense that if a term has a head normal form, then normal-order reduction will eventually reach it.
By contrast, applicative order reduction may not terminate, even when the term has a normal form.