Лямбда-куб

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

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

Структура λ-куба

Под зависимостью $F$ от $X$ понимается

• возможность функционального применения $F$ к $X$, то есть $FX$;
• возможность задать соответствующую лямбда-абстракцию: $\lambda X:T\,.\,FX$.

При этом и $F$, и $X$ могут, в зависимости от конкретной системы, являться как термами, так и типами.

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

• термы, зависящие от типов: система $\lambda 2$ (лямбда-исчисление с полиморфными типами);
• типы, зависящие от типов: система $\lambda\underline{\omega}$ (лямбда-исчисление с операторами над типами);
• типы, зависящие от термов: система $\lambda P$ (лямбда-исчисление с зависимыми типами).

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

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

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

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

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

• Haskell, ML — λ2 (System F)
• В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает $\lambda\underline{\omega}$ с помощью "type families".
• Coq, Agda — $\lambda P \omega$ (исчисление конструкций)

Ссылки

• 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