Лямбда-куб

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
λ-куб. Стрелка вдоль каждого ребра указывает на направление включения; более простая система является частным случаем более сложной.

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

Структура λ-куба[править | править вики-текст]

В системах λ-куба переменные относят к одному из двух сортов: или . Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание читается так: элемент имеет тип и принадлежит сорту . Сорт используется для обычных переменных и термов λ-исчисления, сорт  — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта и элементы сорта рассматриваются как пересекающиеся. Например, тип терма может быть записан как элемент более «высокого» сорта . Типы сорта иногда называют родами.

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

  • для допустимого выражения , возможно содержащего переменную , мы можем определить лямбда-абстракцию ;
  • для функции должно быть допустимо её применение к элементу , при этом результат должен быть элементом типа сорта , то есть .

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

  • термы, зависящие от типов: система (лямбда-исчисление с полиморфными типами, система F);
  • типы, зависящие от типов: система (лямбда-исчисление с операторами над типами);
  • типы, зависящие от термов: система (лямбда-исчисление с зависимыми типами).

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

Свойства систем λ-куба[править | править вики-текст]

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

Поддержка в языках программирования[править | править вики-текст]

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

Ссылки[править | править вики-текст]