Обозначение де Брейна

Для представления переменных натуральными числами см. Индекс Де Брейна .

В математической логике нотация Де Брюйна представляет собой синтаксис терминов в исчислении λ, изобретенный голландским математиком Николаасом Говертом де Брейном . Это можно рассматривать как изменение обычного синтаксиса исчисления λ, где аргумент в приложении размещается рядом с соответствующим связующим в функции, а не после тела последней.

Формальное определение

Условия ( $M,N,\ldots$) в обозначениях Де Брюйна являются либо переменными ( $v$), или иметь один из двух префиксов вагонов . Повозка абстрактора , написанная $[v]$, соответствует обычной λ-связующей λ-исчисления , и аппликаторному вагону , записанному $(M)$, соответствует аргументу в приложении по исчислению λ.

$M,N,...::=\ v\ |\ [v]\;M\ |\ (M)\;N$

Термины традиционного синтаксиса можно преобразовать в нотацию Де Брейна, определив индуктивную функцию. ${\mathcal {I}}$ для чего:

${\begin{aligned}{\mathcal {I}}(v)&=v\\{\mathcal {I}}(\lambda v.\ M)&=[v]\;{\mathcal {I}}(M)\\{\mathcal {I}}(M\;N)&=({\mathcal {I}}(N)){\mathcal {I}}(M).\end{aligned}}$

Все операции над λ-термами коммутируют относительно ${\mathcal {I}}$ перевод. Например, обычная β-редукция,

$(\lambda v.\ M)\;N\ \ \longrightarrow _{\beta }\ \ M[v:=N]$

в обозначениях Де Брейна, как и ожидалось,

$(N)\;[v]\;M\ \ \longrightarrow _{\beta }\ \ M[v:=N].$

Особенностью этой записи является то, что вагоны абстрактора и аппликатора β-редексов спарены, как круглые скобки. Например, рассмотрим этапы β-редукции терма $(M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z$, где редексы подчеркнуты:

${\begin{aligned}(M)\;{\underline {(N)\;[u]}}\;(P)\;[v]\;[w]\;(Q)\;z&{\ \longrightarrow _{\beta }\ }(M)\;{\underline {(P[u:=N])\;[v]}}\;[w]\;(Q[u:=N])\;z\\&{\ \longrightarrow _{\beta }\ }{\underline {(M)\;[w]}}\;(Q[u:=N,v:=P[u:=N]])\;z\\&{\ \longrightarrow _{\beta }\ }(Q[u:=N,v:=P[u:=N],w:=M])\;z.\end{aligned}}$

Таким образом, если рассматривать аппликатор как открытую скобку (' (') и абстрактор в виде закрывающей скобки (' ]'), то шаблон в приведенном выше термине будет ' ((](]]'. Де Брейн называл аппликатора и соответствующего ему абстрактора в этой интерпретации партнерами , а вагоны без партнеров — холостяками . Последовательность вагонов, которую он назвал сегментом , хорошо сбалансирована , если все ее вагоны являются партнерами.

нотации

В хорошо сбалансированном сегменте партнерские вагоны могут перемещаться произвольно, и, пока паритет не нарушен, значение термина остается прежним. Например, в приведенном выше примере аппликатор $(M)$ может быть передан его абстрактору $[w]$или от абстрактора к аппликатору. Фактически, все коммутативы и перестановочные преобразования в лямбда-терминах могут быть описаны просто в терминах переупорядочения связанных вагонов с сохранением четности. Таким образом, получается обобщенный примитив преобразования для λ-термов в нотации Де Брейна.

Некоторые свойства λ-термов, которые трудно сформулировать и доказать с использованием традиционных обозначений, легко выразить в обозначениях Де Брейна. Например, в теоретико-типовой ситуации можно легко вычислить канонический класс типов для термина в контексте типизации и переформулировать проблему проверки типов на проверку того, что проверяемый тип является членом этого класса. Нотация де Брёйна также оказалась полезной в исчислениях для явной замены в системах чистых типов .

См. также

• Математические обозначения