Beta normal form: Encyclopedia II - Beta normal form - Beta reduction

Beta normal form - Beta reduction

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

where A(x) is a term (possibly) involving variable x.

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

where A(t) is the result of substituting the term t for the variable x in the term A(x).

A general beta reduction is either a beta reduction in head position, or an internal beta reduction. An internal beta reduction is one of the following cases:

where is a beta-reduction.

where is a beta-reduction.

where is a beta-reduction.

Beta normal form - Reduction strategies

In general, there can be several different beta reductions possible for a given term. Normal-order reduction is the reduction 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:

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

Adapted from the Wikipedia article "Beta reduction", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki