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

В лямбда-исчислении член находится в бета-нормальной форме, если бета-редукция невозможна. ^[1] Термин находится в нормальной форме бета-эта, если невозможно ни бета-уменьшение, ни уменьшение эта . Термин находится в нормальной форме головы, если в положении головы нет бета-редекса .

Бета-сокращение [ править ]

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

${\ Displaystyle (\ mathbf {\ lambda} xA) M}$.

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

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

Снижение беты является применением следующего правила перезаписи данных на бета REDEX , содержащемся в перспективе:

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

где - результат подстановки члена вместо переменной в члене .${\ displaystyle A [x: = M]}$${\displaystyle M}$${\displaystyle x}$${\displaystyle A}$

Головка снижение беты является снижение беты применяется в положении головы, то есть, в следующей форме:

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

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

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

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

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

Существует дополнительное понятие слабой нормальной формы заголовка (whnf) : термин находится в whnf, если это не приложение, и он не начинается с константы или символа функции. находится в WHNF, потому что это абстракция. не входит в whnf, потому что начинается с символа функции, а именно .${\displaystyle \mathbf {\lambda } x.M}$${\displaystyle 1+2}$${\displaystyle +}$

Стратегии сокращения [ править ]

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

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

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

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

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

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

${\displaystyle \rightarrow z}$

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

См. Также [ править ]

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

Ссылки [ править ]