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

Эта статья посвящена способу избежать именования связанных переменных в лямбда-исчислении. Альтернативный синтаксис лямбда-выражений см. в нотации Де Брёйна .

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

• Термин λ 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). См. следующий рисунок, где папки окрашены в цвет, а ссылки показаны стрелками.

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

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

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

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

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

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

1. найти экземпляры переменных n ₁ , n ₂ , ..., nk _{которые} в M, связаны λ в λ M ,
2. уменьшить свободные переменные M , чтобы они соответствовали удалению внешнего λ-связующего, и
3. замените n ₁ , n ₂ , ..., nk _, на 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 ₂ ..., где Mi _— замена i-й свободной переменной. Операцию увеличения на шаге 3 иногда называют сдвигом и пишут ↑ ^к где k — натуральное число, указывающее на величину увеличения переменных, и определяется формулой

$\uparrow ^{k}=(k+1).(k+2)....$

Например, ↑ ⁰ — это замена идентичности, оставляющая термин неизменным. Конечный список термов M ₁ . M ₂ ... M _n сокращает замену M ₁ . M ₂ ... M _n .(n+1).(n+2)... оставляя без изменений все переменные, большие n. Применение замены s к терму M записывается M [ s ]. Композиция двух замен s ₁ и s ₂ записывается как s ₁ s ₂ и определяется формулой

( М ₁ . М ₂ ...) s знак равно М ₁ [ s ]. М ₂ [ с ]...

удовлетворение собственности

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

и замена определяется следующим образом:

${\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.s'])\\&{\text{where }}s'=s\uparrow ^{1}\end{aligned}}$

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

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

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

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

Альтернативный способ просмотра индексов де Брёйна — это уровни де Брёйна, которые индексируют переменные снизу стека, а не сверху. Это устраняет необходимость переиндексации свободных переменных, например, при ослаблении контекста, тогда как индексы де Брёйна устраняют необходимость переиндексации связанных переменных, например, когда подстановка закрытого выражения в другой контекст.

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

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

Рассуждая о метатеоретических свойствах дедуктивной системы в помощнике по доказательству , иногда желательно ограничиться представлениями первого порядка и иметь возможность называть или переименовывать предположения. Локально безымянный подход использует смешанное представление переменных — индексы де Брейна для связанных переменных и имена для свободных переменных — которое может извлечь выгоду из α-канонической формы индексированных терминов де Брейна, когда это необходимо.

Соглашение о переменных Барендрегта

Соглашение о переменных Барендрегта это соглашение, обычно используемое в доказательствах и определениях, где предполагается, что:

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

В общем контексте индуктивного определения невозможно применить α-преобразование, необходимое для преобразования индуктивного определения, использующего соглашение, в определение, в котором соглашение не используется, поскольку переменная может появляться как в обязательной, так и в необязательной позиции. -обязательное положение в правиле. Принцип индукции справедлив, если каждое правило удовлетворяет следующим двум условиям:

• правило эквивариантно в смысле номинальной логики, то есть его действительность не меняется при переименовании переменных.
• Если исходить из посылок правила, то переменные в обязательных позициях в правиле различны и свободны в заключении.

См. также

• Обозначение де Брейна для λ-термов.
• Комбинаторная логика — более существенный способ устранения имен переменных.