Beta normal form

In lambda calculus, a term is in beta normal form if no beta reduction is possible.^[1] 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 (as a corollary of the Church–Rosser theorem).^[2] 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:^[3][4]

${\displaystyle (\mathbf {\lambda } x.A)M}$.

A redex ${\displaystyle r}$ is in head position in a term ${\displaystyle t}$, if ${\displaystyle t}$ 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):

${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.\underbrace {(\lambda x.A)M_{1}} _{{\text{the redex }}r}M_{2}\ldots M_{m}}$, where ${\displaystyle n\geq 0}$ and ${\displaystyle m\geq 1}$.

A beta reduction is an application of the following rewrite rule to a beta redex contained in a term:

${\displaystyle (\mathbf {\lambda } x.A)M\longrightarrow A[x:=M]}$

where ${\displaystyle A[x:=M]}$ is the result of substituting the term ${\displaystyle M}$ for the variable ${\displaystyle x}$ in the term ${\displaystyle A}$.

A head beta reduction is a beta reduction applied in head position, that is, of the following form:

${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.(\lambda x.A)M_{1}M_{2}\ldots M_{m}\longrightarrow \lambda x_{1}\ldots \lambda x_{n}.A[x:=M_{1}]M_{2}\ldots M_{m}}$, where ${\displaystyle n\geq 0}$ and ${\displaystyle m\geq 1}$.

Any other reduction is an internal beta reduction.

Normal forms

A normal form is a term that does not contain any beta redex,^[3][5] 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 (viz. 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:

${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.xM_{1}M_{2}\ldots M_{m}}$, where ${\displaystyle x}$ is a variable, ${\displaystyle n\geq 0}$ and ${\displaystyle m\geq 0}$.

A head normal form is not always a normal form,^[5] because the applied arguments ${\displaystyle M_{j}}$ need not be normal. However, the converse is true: any normal form is also a head normal form.^[5] In fact, the normal forms are exactly the head normal forms in which the subterms ${\displaystyle M_{j}}$ are themselves normal forms. This gives an inductive syntactic description of normal forms.

There is also the notion of weak head normal form. A λ-term, M, is in weak head normal form in case it is a λ-abstraction, ${\displaystyle M=\mathbf {\lambda } x.N}$ where ${\displaystyle N}$ is any expression, even containing a redex, or it is in head normal form (in the pure lambda calculus, the only head normal forms that are not λ-abstractions are of the form ${\displaystyle xM_{1}M_{2}\ldots M_{m}}$, where ${\displaystyle x}$ is any variable and ${\displaystyle m\geq 0}$).^[6][7] Weak head normal forms were introduced by Simon Peyton Jones to reflect the form to which functional languages actually evaluate.^[7][8]

See also

• Lambda calculus
• Normal form (disambiguation)
• Reduction strategy