Лямбда-куб

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
λ-куб. Стрелка вдоль каждого ребра указывает на направление включения; более простая система является частным случаем более сложной.

Ля́мбда-куб (λ-куб) — единообразное графическое описание восьми различных систем типизированного лямбда-исчисления с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт.

Структура λ-куба[править | править исходный текст]

В системах λ-куба переменные относят к одному из двух сортов: \ast или \Box. Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание A:B:C читается так: элемент A имеет тип B и принадлежит сорту C. Сорт \ast используется для обычных переменных и термов λ-исчисления, сорт \Box — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта \ast и элементы сорта \Box рассматриваются как пересекающиеся. Например, тип терма (\lambda x:\alpha.\,x) :(\alpha\to\alpha):\ast может быть записан как элемент более «высокого» сорта (\alpha\to\alpha):\ast:\Box. Типы сорта \Box иногда называют кайндами или видами.

Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта s_1 зависят от элементов сорта s_2, если:

  • для допустимого выражения F[x]:\tau:s_1, возможно содержащего переменную x:\sigma:s_2, мы можем определить лямбда-абстракцию (\lambda x:\sigma.\,F[x]):(\sigma\to\tau):s_1;
  • для функции G:(\sigma\to\tau):s_1 должно быть допустимо её применение к элементу Y:\sigma:s_2, при этом результат должен быть элементом типа \tau сорта s_1, то есть (G\,Y):\tau:s_1.

Базовой вершиной куба служит система \lambda^\rightarrow, соответствующая просто типизированному лямбда-исчислению. Термы (элементы сорта \ast) зависят от термов; типы (элементы сорта \Box) в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы:

  • термы, зависящие от типов: система \lambda 2 (лямбда-исчисление с полиморфными типами, система F);
  • типы, зависящие от типов: система \lambda\underline{\omega} (лямбда-исчисление с операторами над типами);
  • типы, зависящие от термов: система \lambda P (лямбда-исчисление с зависимыми типами).

Остальные системы представляют собой различные комбинации перечисленных зависимостей. Наиболее богатая система \lambda P\omega (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций (англ.).

Свойства систем λ-куба[править | править исходный текст]

Все системы лямбда-куба обладают свойством сильной нормализации (англ.): любой допустимый терм (и тип) за конечное число β-редукций приводится к единственной нормальной форме.

Поддержка в языках программирования[править | править исходный текст]

Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов.

Ссылки[править | править исходный текст]