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

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

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

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

$(\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$.

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

$\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}$, где $n\geq 0$ и $m\geq 1$.

Любое другое снижение представляет собой внутреннюю бета-редукцию.

– Нормальная форма это термин, который не содержит бета-редекса. т.е. это не может быть уменьшено дальше. — Нормальная форма головы это термин, который не содержит бета-редекса в положении головы, т. е. который не может быть дополнительно уменьшен за счет уменьшения головы. При рассмотрении простого лямбда-исчисления (т. е. без добавления константных или функциональных символов, которые должны быть сокращены с помощью дополнительного правила дельты), головными нормальными формами являются члены следующей формы:

$\lambda x_{1}\ldots \lambda x_{n}.xM_{1}M_{2}\ldots M_{m}$, где $x$ это переменная, $n\geq 0$ и $m\geq 0$.

Нормальная форма головы не всегда является нормальной формой, потому что применяемые аргументы $M_{j}$ не обязательно должен быть нормальным. Однако верно и обратное: любая нормальная форма также является нормальной формой головы. Фактически нормальные формы — это именно главные нормальные формы, в которых подтермы $M_{j}$ сами по себе являются нормальными формами. Это дает индуктивное синтаксическое описание нормальных форм.

Существует также понятие нормальной формы слабой головы : термин в нормальной форме слабой головы — это либо термин в нормальной форме головы, либо лямбда-абстракция. Это означает, что редекс может появиться внутри лямбда-тела.

Стратегии сокращения

В общем, данный терм может содержать несколько редексов, следовательно, может быть применено несколько различных бета-сокращений. Мы можем указать стратегию , чтобы выбрать, какой редекс уменьшить.

• Сокращение нормального порядка — это стратегия, при которой постоянно применяется правило бета-редукции положения головы до тех пор, пока такие редукции больше не станут невозможны. В этот момент результирующий член находится в нормальной форме головы. Затем продолжают применять уменьшение головы в подтерминах. $M_{j}$, слева направо. Другими словами, сокращение в нормальном порядке — это стратегия, которая всегда сначала уменьшает самый левый и самый внешний редекс.
• Напротив, при аппликативной редукции сначала применяются внутренние редукции, а затем применяется редукция напора только тогда, когда внутренние редукции больше невозможны.

Приведение к нормальному порядку является полным в том смысле, что если терм имеет головную нормальную форму, то приведение к нормальному порядку в конечном итоге достигнет ее. Согласно синтаксическому описанию нормальных форм, приведенному выше, это влечет за собой то же утверждение для «полностью» нормальной формы (это теорема стандартизации ). Напротив, аппликативное понижение порядка может не прекратиться, даже если термин имеет нормальную форму. Например, используя аппликативное приведение порядка, возможна следующая последовательность приведений:

${\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}}$

Но при использовании приведения к нормальному порядку та же самая отправная точка быстро приводится к нормальной форме:

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

$\rightarrow z$

Синота Строки директора — это один из методов, с помощью которого можно оптимизировать вычислительную сложность бета-снижения.

См. также

• Лямбда-исчисление
• Нормальная форма (значения)