Обозначение де Брёйна - De Bruijn notation

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

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

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

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

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

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

${displaystyle {egin{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 _{eta } M[v:=N]}$

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

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

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

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

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

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

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

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

Смотрите также

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

использованная литература

1. Де Брёйн, Николаас Говерт (1980). «Обзор проекта АВТОМАТ». В Хиндли Дж. Р. и Селдин Дж. П. (ред.). Х. Б. Карри: Очерки комбинаторной логики, лямбда-исчисления и формализма. Академическая пресса. С. 29–61. ISBN  978-0-12-349050-6. OCLC  6305265.
2. Камареддин, Файруз (2001). «Обзор классических обозначений и обозначений Де Брейна для λ-исчисления и систем чистых типов». Логика и вычисления. 11 (3): 363–394. CiteSeerX  10.1.1.29.3756. Дои:10.1093 / logcom / 11.3.363. ISSN  0955-792X. Пример со страницы 384.
3. Камареддин, Файруз; Недерпелт, Роб (1996). «Полезная λ-запись». Теоретическая информатика. 155: 85–109. Дои:10.1016/0304-3975(95)00101-8. ISSN  0304-3975.
4. Де Лью, Б.-Дж. (1995). «Обобщения в λ-исчислении и теории его типов». Дипломная работа, Университет Глазго. .