Бета-нормальная форма

В лямбда-исчислении термин находится в бета-нормальной форме, если бета-редукция невозможна. Термин находится в бета-эта нормальной форме , если ни бета-редукция, ни эта-редукция невозможны. Термин находится в нормальной форме головы , если в позиции головы нет бета-редекса . Нормальная форма термина, если она существует, уникальна (как следствие теоремы Чёрча – Россера ). Однако термин может иметь более одной головной нормальной формы.

Бета-снижение

В лямбда-исчислении бета-редекс представляет собой термин вида:

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

редекс $r$ находится на руководящей позиции в семестре $t$, если $t$ имеет следующую форму (обратите внимание, что приложение имеет более высокий приоритет, чем абстракция, и что приведенная ниже формула представляет собой лямбда-абстракцию, а не приложение):

$\lambda x_{1}\ldots \lambda x_{n}.\underbrace {(\lambda x.A)M_{1}} _{{\text{the redex }}r}M_{2}\ldots M_{m}$, где $n\geq 0$ и $m\geq 1$.

Бета -редукция — это применение следующего правила перезаписи к бета-редексу, содержащемуся в терме:

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

где $A[x:=M]$ является результатом замены термина $M$ для переменной $x$ в срок $A$.

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

$\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 $n\geq 0$ and $m\geq 1$.

Any other reduction is an internal beta reduction.

A normal form is a term that does not contain any beta redex, i.e. that cannot be further reduced. 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:

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

A head normal form is not always a normal form, because the applied arguments $M_{j}$ need not be normal. However, the converse is true: any normal form is also a head normal form. In fact, the normal forms are exactly the head normal forms in which the subterms $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 in weak head normal form is either a term in head normal form or a lambda abstraction. This means a redex may appear inside a lambda body.

Reduction strategies

In general, a given term can contain several redexes, hence several different beta reductions could be applied. We may specify a strategy to choose which redex to reduce.

• Normal-order reduction is the 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. One then continues applying head reduction in the subterms $M_{j}$, from left to right. Stated otherwise, normal‐order reduction is the strategy that always reduces the left‐most outer‐most redex first.
• By 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. 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:

${\begin{aligned}&(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}$

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

$(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))$

$\rightarrow z$

Sinot's director strings is one method by which the computational complexity of beta reduction can be optimized.

See also

• Lambda calculus
• Normal form (disambiguation)