Ля́мбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт.
В системах λ-куба переменные относят к одному из двух сортов: или . Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание читается так: элемент имеет тип и принадлежит сорту . Сорт используется для обычных переменных и термов λ-исчисления, сорт — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта и элементы сорта рассматриваются как пересекающиеся. Например, тип терма может быть записан как элемент более «высокого» сорта . Типы сорта иногда называют родами.
Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта зависят от элементов сорта , если:
Базовой вершиной куба служит система , соответствующая просто типизированному лямбда-исчислению. Термы (элементы сорта ) зависят от термов; типы (элементы сорта ) в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы:
Остальные системы представляют собой различные комбинации перечисленных зависимостей. Наиболее богатая система (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций .
Все системы лямбда-куба обладают свойством сильной нормализации : любой допустимый терм (и тип) за конечное число β-редукций приводится к единственной нормальной форме.
Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов.
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .