- Лямбда-куб
-
Ля́мбда-куб (λ-куб) задает единообразное описание восьми различных систем типизированного лямбда-исчисления с явным приписыванием типов (систем, типизированных по Чёрчу). Он организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею лямбда-куба предложил в 1991 году голландский логик и математик Хенк Барендрегт.
Содержание
Структура λ-куба
Под зависимостью от понимается
- возможность функционального применения к , то есть ;
- возможность задать соответствующую лямбда-абстракцию: .
При этом и , и могут, в зависимости от конкретной системы, являться как термами, так и типами.
Базовой вершиной куба служит система , соответствующая просто типизированному лямбда-исчислению. Термы зависят от термов; типы в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы:- термы, зависящие от типов: система (лямбда-исчисление с полиморфными типами);
- типы, зависящие от типов: система (лямбда-исчисление с операторами над типами);
- типы, зависящие от термов: система (лямбда-исчисление с зависимыми типами).
Остальные системы представляют собой различные комбинации перечисленных возможностей. Наиболее богатая система (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций.Свойства систем λ-куба
Все системы лямбда-куба обладают свойством сильной нормализации: любой допустимый терм (и тип) за конечное число β-редукций приводится к (единственной) нормальной форме.
Поддержка в языках программирования
Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов.
- Haskell, ML — λ2 (System F)
- В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает с помощью "type families".
- Coq, Agda — (исчисление конструкций)
Ссылки
- 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
Категория:- Лямбда-исчисление
Wikimedia Foundation. 2010.