In the lambda calculus, a term is in beta normal form if no beta reduction is possible. A term is in beta-eta normal form if neither a beta reduction nor an eta reduction is possible. A term is in head normal form if there is no beta-redex in head position.
Contents
Beta reduction
In the lambda calculus, a beta redex is a term of the form
where
A redex
A beta reduction is an application of the following rewrite rule to a beta redex contained in a term
where
A head beta reduction is a beta reduction applied in head position, that is, of the following form:
Any other reduction is an internal beta reduction.
A normal form is a term that do not contain any beta redex, ie. that cannot be further reduced. More generally, a head normal form is a term that do not contain a beta redex in head position, ie. that cannot be further reduced by a head reduction. Head normal forms are the terms of the following shape:
It is not always a normal form, because the applied arguments
Reduction strategies
In general, a given term can contain several redexes, hence several different beta reductions can apply. We may specify a strategy to choose which redex to reduce.
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 the syntactic description of normal forms above, this entails the same statement for a “fully” normal form (this is the standardization theorem). By contrast, applicative order reduction may not terminate, even when the term has a normal form. For example, using applicative order reduction, the following sequence of reductions is possible:
But using normal-order reduction, the same starting point reduces quickly to normal form:
Sinot's director strings is one method by which the computational complexity of beta reduction can be optimized.