Лямбда-куб

λ-куб. Стрелка вдоль каждого ребра указывает на направление включения; более простая система является частным случаем более сложной.

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

Структура λ-куба

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

Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта $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$, то есть $(GY):\tau :s_1$.

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

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

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

Свойства систем λ-куба

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

Поддержка в языках программирования

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

• Haskell, ML — λ2 (система F)
• В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает $\lambda \underset{\_}{\omega }$ с помощью «type families».
• Coq, Agda — $\lambda P\omega$ (исчисление конструкций)

Ссылки

• Henk Barendregt, Lambda Calculi with TypesШаблон:Ref-en, Handbook of Logic in Computer Science, Volume II, Oxford University Press.
• Simon Peyton Jones and Erik Meijer, 1997. Henk: A Typed Intermediate LanguageШаблон:Ref-en
• Lennart Augustsson, 2007. Simpler, Easier!Шаблон:Ref-en Описание реализации систем лямбда-куба на языке Haskell.
• Лямбда-куб на SpbHUGШаблон:Ref-ru с переводом Дениса Москвина раздела о лямбда-кубе из книги Henk Barendregt, Lambda Calculi with Types