Beta normal form

In 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 the head position. The normal form of a term, if one exists, is unique. However, a term may have more than one head normal form.

Beta reduction

In the lambda calculus, a beta redex is a term of the form:
A redex is in head position in a term, if has the following shape :
A beta reduction is an application of the following rewrite rule to a beta redex contained in a term:
where is the result of substituting the term for the variable in the term.
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.

Normal forms

A normal form is a term that does not contain any beta redex, i.e. that cannot be further reduced. Some authors may also include η reductions, hence the distinguishing terms beta normal form and beta-eta normal form.
A head normal form is a term that does not contain a beta redex in head position, i.e. that cannot be further reduced by a head reduction. When considering the simple lambda calculus. Weak head normal forms were introduced by Simon Peyton Jones to reflect the form to which functional languages actually evaluate.