Beta normal form

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.

Beta reduction

In the lambda calculus, a beta redex is a term of the form

Failed to parse (Missing texvc executable; please see math/README to configure.): ((\mathbf{\lambda} x . A(x)) t)

where Failed to parse (Missing texvc executable; please see math/README to configure.): A(x)

is a term (possibly) involving variable Failed to parse (Missing texvc executable; please see math/README to configure.): x

.

A beta reduction is an application of the following rewrite rule to a beta redex

Failed to parse (Missing texvc executable; please see math/README to configure.): ((\mathbf{\lambda} x . A(x)) t) \rightarrow A(t)

where Failed to parse (Missing texvc executable; please see math/README to configure.): A(t)

is the result of substituting the term Failed to parse (Missing texvc executable; please see math/README to configure.): t
for the variable Failed to parse (Missing texvc executable; please see math/README to configure.): x
in the term Failed to parse (Missing texvc executable; please see math/README to configure.): A(x)

.

A beta reduction is in head position if it is of the following form:

• Failed to parse (Missing texvc executable; please see math/README to configure.): \lambda x_0 \ldots \lambda x_{i-1} . (\lambda x_i . A(x_i)) M_1 M_2 \ldots M_n \rightarrow \lambda x_0 \ldots \lambda x_{i-1} . A(M_1) M_2 \ldots M_n

, where Failed to parse (Missing texvc executable; please see math/README to configure.): i \geq 0, n \geq 1 .

Any reduction not in this form is an internal beta reduction.

Reduction strategies

In general, there can be several different beta reductions possible for a given term. Normal-order reduction is the evaluation strategy in which one continually applies the rule for beta reduction in head position until no more such reductions are possible. At that point, the resulting term is in head normal form.

In contrast, in applicative order reduction, one applies the internal reductions first, and then only applies the head reduction when no more internal reductions are possible.

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. In 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:

Failed to parse (Missing texvc executable; please see math/README to configure.): (\mathbf{\lambda} x . z) ((\lambda w. w w w) (\lambda w. w w w))

Failed to parse (Missing texvc executable; please see math/README to configure.): \rightarrow (\lambda x . z) ((\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w))

Failed to parse (Missing texvc executable; please see math/README to configure.): \rightarrow (\lambda x . z) ((\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w))

Failed to parse (Missing texvc executable; please see math/README to configure.): \rightarrow (\lambda x . z) ((\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w))

Failed to parse (Missing texvc executable; please see math/README to configure.): \ldots

But using normal-order reduction, the same starting point reduces quickly to normal form:

Failed to parse (Missing texvc executable; please see math/README to configure.): (\mathbf{\lambda} x . z) ((\lambda w. w w w) (\lambda w. w w w))

Failed to parse (Missing texvc executable; please see math/README to configure.): \rightarrow z

See also

• Lambda calculus
• Normal form