Открыть главное меню
λ-куб. Стрелка вдоль каждого ребра указывает на направление включения; более простая система является частным случаем более сложной.

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

Содержание

Структура λ-кубаПравить

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

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

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

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

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

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

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

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

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

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

СсылкиПравить