Ля́мбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт. Дальнейшие обобщения лямбда-куба можно получить, рассматривая чистую систему типов.
Структура λ-куба В системах λ-куба переменные относят к одному из двух сортов: или . Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание читается так: элемент имеет тип и принадлежит сорту . Сорт используется для обычных переменных и термов λ-исчисления, сорт — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта и элементы сорта рассматриваются как пересекающиеся. Например, тип терма может быть записан как элемент более «высокого» сорта . Типы сорта иногда называют родами.
Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта зависят от элементов сорта , если: для допустимого выражения , возможно содержащего переменную , мы можем определить лямбда-абстракцию ; для функции должно быть допустимо её применение к элементу , при этом результат должен быть элементом типа сорта , то есть .
Базовой вершиной куба служит система , соответствующая просто типизированному лямбда-исчислению. Термы (элементы сорта ) зависят от термов; типы (элементы сорта ) в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы: термы, зависящие от типов: система (лямбда-исчисление с полиморфными типами, система F); типы, зависящие от типов: система (лямбда-исчисление с операторами над типами); типы, зависящие от термов: система (лямбда-исчисление с зависимыми типами).
Остальные системы представляют собой различные комбинации перечисленных зависимостей. Наиболее богатая система (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций.
Свойства систем λ-куба
Все системы лямбда-куба обладают свойством : любой допустимый терм (и тип) за конечное число β-редукций приводится к единственной нормальной форме.
Поддержка в языках программирования Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов. Haskell, ML — λ2 (система F) В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает с помощью «type families». Coq, Agda — (исчисление конструкций)
Ссылки 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
Категория:Лямбда-исчисление