Лямбда-куб
Лямбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт. Дальнейшие обобщения лямбда-куба можно получить, рассматривая чистую систему типов.
Структура λ-куба
В системах λ-куба переменные относят к одному из двух сортов: ∗ {displaystyle ast } или ◻ {displaystyle Box } . Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание A : B : C {displaystyle A:B:C} читается так: элемент A {displaystyle A} имеет тип B {displaystyle B} и принадлежит сорту C {displaystyle C} . Сорт ∗ {displaystyle ast } используется для обычных переменных и термов λ-исчисления, сорт ◻ {displaystyle Box } — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта ∗ {displaystyle ast } и элементы сорта ◻ {displaystyle Box } рассматриваются как пересекающиеся. Например, тип терма ( λ x : α . x ) : ( α → α ) : ∗ {displaystyle (lambda x:alpha .,x):(alpha o alpha ):ast } может быть записан как элемент более «высокого» сорта ( α → α ) : ∗ : ◻ {displaystyle (alpha o alpha ):ast :Box } . Типы сорта ◻ {displaystyle Box } иногда называют родами.
Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта s 1 {displaystyle s_{1}} зависят от элементов сорта s 2 {displaystyle s_{2}} , если:
- для допустимого выражения F [ x ] : τ : s 1 {displaystyle F[x]: au :s_{1}} , возможно содержащего переменную x : σ : s 2 {displaystyle x:sigma :s_{2}} , мы можем определить лямбда-абстракцию ( λ x : σ . F [ x ] ) : ( σ → τ ) : s 1 {displaystyle (lambda x:sigma .,F[x]):(sigma o au ):s_{1}} ;
- для функции G : ( σ → τ ) : s 1 {displaystyle G:(sigma o au ):s_{1}} должно быть допустимо её применение к элементу Y : σ : s 2 {displaystyle Y:sigma :s_{2}} , при этом результат должен быть элементом типа τ {displaystyle au } сорта s 1 {displaystyle s_{1}} , то есть ( G Y ) : τ : s 1 {displaystyle (G,Y): au :s_{1}} .
Базовой вершиной куба служит система λ → {displaystyle lambda ^{ ightarrow }} , соответствующая просто типизированному лямбда-исчислению. Термы (элементы сорта ∗ {displaystyle ast } ) зависят от термов; типы (элементы сорта ◻ {displaystyle Box } ) в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы:
- термы, зависящие от типов: система λ 2 {displaystyle lambda 2} (лямбда-исчисление с полиморфными типами, система F);
- типы, зависящие от типов: система λ ω _ {displaystyle lambda {underline {omega }}} (лямбда-исчисление с операторами над типами);
- типы, зависящие от термов: система λ P {displaystyle lambda P} (лямбда-исчисление с зависимыми типами).
Остальные системы представляют собой различные комбинации перечисленных зависимостей. Наиболее богатая система λ P ω {displaystyle lambda Pomega } (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций.
Свойства систем λ-куба
Все системы лямбда-куба обладают свойством сильной нормализации: любой допустимый терм (и тип) за конечное число β-редукций приводится к единственной нормальной форме.
Поддержка в языках программирования
Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов.
- Haskell, ML — λ2 (система F)
- В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает λ ω _ {displaystyle lambda {underline {omega }}} с помощью «type families».
- Coq, Agda — λ P ω {displaystyle lambda Pomega } (исчисление конструкций)