Индекс Де Брейна
-
Основы индексов де Брейна
- Индексы де Брейна используются для представления лямбда-терминов без указания имен переменных.
- Термины с индексами де Брейна инвариантны относительно α-преобразования и проверки на синтаксическое равенство.
-
Примеры и применение
- Термин λx.λy.x записывается как λ λ 2 с индексами де Брейна.
- Термин λx.λy.λz.xz (yz) (комбинатор S) равен λ λ λ 3 1 (2 1).
- Термин λz.((λy.y (λx.x)) (λx.z x)) равен λ (λ 1 (λ 1)) (λ 2 1).
-
Формальное определение и операции
- Формально λ-термы с индексами де Брейна имеют синтаксис с круглыми скобками и переменными, привязанными к индексам.
- Подстановка — это операция замены свободных переменных в термине другими членами.
- Операция увеличения переменных называется сдвигом и обозначается как ↑k.
- Композиция подстановок и их применение к терминам описаны в статье.
-
Альтернативы индексам де Брейна
- Именованное представление λ-термов может быть громоздким и неэффективным.
- Уровни де Брейна и альтернативные представления, такие как номинальные методы Питтса и Габбая, могут упростить представление терминов.
- Представления более высокого порядка, где λ-связующее рассматривается как функция, также являются альтернативой.
-
Соглашение о переменах Барендрегта
- Соглашение о переменных Барендрегта используется для упрощения доказательств и определений, где переменные разделены на связанные и свободные.
- Принцип индукции справедлив при соблюдении определенных условий, связанных с эквивариантностью и различием переменных в обязательных и необязательных позициях.
Полный текст статьи: