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

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

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

Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта ${\displaystyle s_{1}}$ зависят от элементов сорта ${\displaystyle s_{2}}$ , если:

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

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

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

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

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

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

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

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

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

Ссылки

• Henk Barendregt, (англ.) , Handbook of Logic in Computer Science, Volume II, Oxford University Press.
• Simon Peyton Jones and Erik Meijer, 1997. (англ.)
• Lennart Augustsson, 2007. (англ.) Описание реализации систем лямбда-куба на языке Haskell.
• (рус.) с переводом Дениса Москвина раздела о лямбда-кубе из книги Henk Barendregt,