Индекс Де Брёйна

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

• Член λ x . λ y . x , иногда называемый K-комбинатором , записывается как λ λ 2 с индексами Де Брёйна. Связующим элементом для вхождения x является второй λ в области видимости.
• Член λ x . λ y . λ z . x z ( y z ) ( комбинатор S ) с индексами Де Брёйна есть λ λ λ 3 1 (2 1).
• Член λ z . (λ y . y (λ x . x )) (λ x . z x ) равно λ (λ 1 (λ 1)) (λ 2 1). См. Следующую иллюстрацию, на которой папки окрашены, а ссылки показаны стрелками.

Индексы Де Брёйна обычно используются в системах рассуждений более высокого порядка, таких как автоматические средства доказательства теорем и системы логического программирования . ^[2]

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

Формально λ-термы ( M , N , ...), записанные с использованием индексов Де Брёйна, имеют следующий синтаксис (круглые скобки разрешены свободно):

M , N , ... :: = n | M N | λ M

где n - натуральные числа больше 0 - переменные. Переменная n является связанной, если она входит в область действия по крайней мере n связывателей (λ); в остальном это бесплатно . Сайт привязки для переменной n - это n- е связующее, в области действия которого оно находится , начиная с самого внутреннего связующего.

Самая примитивная операция над λ-термами - это подстановка: замена свободных переменных в терме другими термами. Например, в β-редукции (λ M ) N мы должны

1. найти экземпляры переменных n ₁ , n ₂ , ..., n _k в M , которые связаны с λ в λ M ,
2. уменьшить свободные переменные M, чтобы соответствовать удалению внешней λ-связки, и
3. замените n ₁ , n ₂ , ..., n _k на N , соответствующим образом увеличивая количество свободных переменных, встречающихся в N, каждый раз, чтобы соответствовать количеству λ-связующих, при котором соответствующая переменная появляется, когда N заменяет одну из n _я .

Для иллюстрации рассмотрим приложение

(λ λ 4 2 (λ 1 3)) (λ 5 1)

что может соответствовать следующему члену, записанному в обычных обозначениях

(λ x . λ y . z x (λ u . u x )) (λ x . w x ).

После шага 1 мы получаем член λ 4 □ (λ 1 □), в котором переменные, предназначенные для подстановки, заменяются квадратами. Шаг 2 уменьшает свободные переменные, получая λ 3 □ (λ 1 □). Наконец, на шаге 3 мы заменяем поля аргументом, а именно λ 5 1; первый ящик находится под одной связкой, поэтому мы заменяем его на λ 6 1 (что составляет λ 5 1 со свободными переменными, увеличенными на 1); второй находится под двумя связующими, поэтому мы заменим его на λ 7 1. Окончательный результат будет λ 3 (λ 6 1) (λ 1 (λ 7 1)).

Формально подстановка - это неограниченный список замен терминов для свободных переменных, записанный M ₁ . M ₂ ..., где M _i - замена i- й свободной переменной. Операция увеличения на шаге 3 иногда называется сдвигом и записывается как ↑ ^k, где k - натуральное число, указывающее величину увеличения переменных; например, ↑ ⁰ - это подстановка тождества, оставляя термин неизменным.

Применение замены s к члену M записывается M [ s ]. Композиция двух замен s ₁ и s ₂ записывается как s ₁ s ₂ и определяется формулой

M [ s ₁ s ₂ ] = ( M [ s ₁ ]) [ s ₂ ].

Правила применения следующие:

${\displaystyle {\begin{aligned}n[N_{1}\ldots N_{n}\ldots ]=&N_{n}\\(M_{1}\;M_{2})[s]=&(M_{1}[s])(M_{2}[s])\\(\lambda \;M)[s]=&\lambda \;(M[1.1[s'].2[s'].3[s']\ldots ])\\&{\text{where }}s'=s\uparrow ^{1}\end{aligned}}}$

Таким образом, шаги, описанные выше для β-восстановления, более кратко выражаются как:

(λ M ) N → _β M [ N .1.2.3 ...].

Альтернативы индексам Де Брёйна [ править ]

При использовании стандартного «именованного» представления λ-термов, где переменные обрабатываются как метки или строки, необходимо явно обрабатывать α-преобразование при определении любой операции над термами. Стандарт Переменных конвенций ^[3] из Barendregt является одним из такого подхода , при котором применяются α-преобразование по мере необходимости для обеспечения того , чтобы:

1. связанные переменные отличны от свободных переменных, и
2. все связыватели связывают переменные, которые еще не входят в область видимости.

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

Индексы Де Брёйна - не единственное представление λ-термов, которое снимает проблему α-преобразования. Среди именованных представлений номинальные методы Питтса и Габбея представляют собой один из подходов, в котором представление λ-члена рассматривается как класс эквивалентности всех терминов, которые можно переписать в него с использованием перестановок переменных. ^[4] Этот подход используется пакетом номинальных типов данных Isabelle / HOL . ^[5]

Другой распространенной альтернативой является обращение к представлениям более высокого порядка, в которых λ-связка рассматривается как истинная функция. В таких представлениях вопросы α-эквивалентности, подстановки и т. Д. Идентифицируются с теми же операциями в мета-логике .

Рассуждая о метатеоретических свойствах дедуктивной системы в помощнике по доказательству , иногда желательно ограничиться представлениями первого порядка и иметь возможность давать имена или переименовывать предположения. В локально безымянном подходе используется смешанное представление переменных - индексы Де Брёйна для связанных переменных и имена для свободных переменных - которое может извлечь выгоду из α-канонической формы индексированных терминов Де Брёйна, когда это необходимо. ^{[6] [7]}

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

• Обозначения Де Брейны для Й-точки.
• Комбинаторная логика , более важный способ избавиться от имен переменных.

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