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

В математической логике , то обозначение De Бройн является синтаксисом для терминов в Й исчислении изобретенного голландским математиком Де Брёйн . ^[1] Это можно рассматривать как инверсию обычного синтаксиса для λ-исчисления, когда аргумент в приложении помещается рядом с соответствующим связующим элементом в функции, а не после тела последней.

Формальное определение [ править ]

Термины ( ) в нотации Де Брёйна либо являются переменными ( ), либо имеют один из двух префиксов вагона . Реферата вагон , написанная , соответствует обычному Х-связующему из Й исчисления , а аппликатор вагон , написанная , соответствует аргументу в приложении в λ исчислении.${\ displaystyle M, N, \ ldots}$${\ displaystyle v}$${\ displaystyle [v]}$${\ Displaystyle (М)}$

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

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

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

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

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

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

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

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

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

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

Преимущества нотации Де Брёйна [ править ]

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

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

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

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

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