Лямбда-куб
Ля́мбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт. Дальнейшие обобщения лямбда-куба можно получить, рассматривая чистую систему типов.
Структура λ-куба
В системах λ-куба переменные относят к одному из двух сортов: [math]\displaystyle{ \ast }[/math] или [math]\displaystyle{ \Box }[/math]. Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание [math]\displaystyle{ A:B:C }[/math] читается так: элемент [math]\displaystyle{ A }[/math] имеет тип [math]\displaystyle{ B }[/math] и принадлежит сорту [math]\displaystyle{ C }[/math]. Сорт [math]\displaystyle{ \ast }[/math] используется для обычных переменных и термов λ-исчисления, сорт [math]\displaystyle{ \Box }[/math] — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта [math]\displaystyle{ \ast }[/math] и элементы сорта [math]\displaystyle{ \Box }[/math] рассматриваются как пересекающиеся. Например, тип терма [math]\displaystyle{ (\lambda x:\alpha.\,x) :(\alpha\to\alpha):\ast }[/math] может быть записан как элемент более «высокого» сорта [math]\displaystyle{ (\alpha\to\alpha):\ast:\Box }[/math]. Типы сорта [math]\displaystyle{ \Box }[/math] иногда называют родами.
Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта [math]\displaystyle{ s_1 }[/math] зависят от элементов сорта [math]\displaystyle{ s_2 }[/math], если:
- для допустимого выражения [math]\displaystyle{ F[x]:\tau:s_1 }[/math], возможно содержащего переменную [math]\displaystyle{ x:\sigma:s_2 }[/math], мы можем определить лямбда-абстракцию [math]\displaystyle{ (\lambda x:\sigma.\,F[x]):(\sigma\to\tau):s_1 }[/math];
- для функции [math]\displaystyle{ G:(\sigma\to\tau):s_1 }[/math] должно быть допустимо её применение к элементу [math]\displaystyle{ Y:\sigma:s_2 }[/math], при этом результат должен быть элементом типа [math]\displaystyle{ \tau }[/math] сорта [math]\displaystyle{ s_1 }[/math], то есть [math]\displaystyle{ (G\,Y):\tau:s_1 }[/math].
Базовой вершиной куба служит система [math]\displaystyle{ \lambda^\rightarrow }[/math], соответствующая просто типизированному лямбда-исчислению. Термы (элементы сорта [math]\displaystyle{ \ast }[/math]) зависят от термов; типы (элементы сорта [math]\displaystyle{ \Box }[/math]) в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы:
- термы, зависящие от типов: система [math]\displaystyle{ \lambda 2 }[/math] (лямбда-исчисление с полиморфными типами, система F);
- типы, зависящие от типов: система [math]\displaystyle{ \lambda\underline{\omega} }[/math] (лямбда-исчисление с операторами над типами);
- типы, зависящие от термов: система [math]\displaystyle{ \lambda P }[/math] (лямбда-исчисление с зависимыми типами).
Остальные системы представляют собой различные комбинации перечисленных зависимостей. Наиболее богатая система [math]\displaystyle{ \lambda P\omega }[/math] (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций.
Свойства систем λ-куба
Все системы лямбда-куба обладают свойством сильной нормализации: любой допустимый терм (и тип) за конечное число β-редукций приводится к единственной нормальной форме.
Поддержка в языках программирования
Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов.
- Haskell, ML — λ2 (система F)
- В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает [math]\displaystyle{ \lambda\underline{\omega} }[/math] с помощью «type families».
- Coq, Agda — [math]\displaystyle{ \lambda P \omega }[/math] (исчисление конструкций)
Ссылки
- Henk Barendregt, Lambda Calculi with Types (англ.), Handbook of Logic in Computer Science, Volume II, Oxford University Press.
- Simon Peyton Jones and Erik Meijer, 1997. Henk: A Typed Intermediate Language (англ.)
- Lennart Augustsson, 2007. Simpler, Easier! (англ.) Описание реализации систем лямбда-куба на языке Haskell.
- Лямбда-куб на SpbHUG (рус.) с переводом Дениса Москвина раздела о лямбда-кубе из книги Henk Barendregt, Lambda Calculi with Types