Лямбда-кубик
-
Определение лямбда-куба
- Лямбда-куб — это система для описания и изучения чистых типов.
- Включает в себя системы λ→, λ2, λω и λC.
- Основана на изоморфизме Карри-Говарда и имеет связь с логикой.
-
Системы в лямбда-кубе
- λ→: самая простая система, не допускает полиморфных типов.
- λ2: позволяет типы, зависящие от терминов, и имеет ограниченную вычислительную мощность.
- λω: чрезвычайно эффективен и является основой для языков программирования.
- λC: сочетает в себе выразительность λP и вычислительную мощность λω, очень мощный.
-
Сравнение с другими системами
- Системный автомат аналогичен λ2, ML-подобные языки находятся между λ→ и λ2.
- Coq основан на расширении λC с линейной иерархией вселенных.
- Системы чистых типов обобщают лямбда-куб, позволяя произвольные сортировки, аксиомы и правила.
-
Общие свойства
- Все системы в кубе обладают свойством Черч-Россер и свойством уменьшения объекта.
- Уникальность типов — если два типа эквивалентны, они должны быть одинаковыми.
- Ни одна система в кубе не является полной по Тьюрингу.
-
Подтипы и дальнейшие расширения
- Подтипы не представлены в кубе, но существуют системы, такие как F<:ω, которые сочетают подтипирование и полиморфизм.
- Лямбда-куб предшествует обобщению в виде фреймворка чистых типов, который включает в себя все углы куба и многие другие системы.
-
Дополнительные представления
- Оливье Риду представил лямбда-куб в виде октаэдра и додекаэдра.
-
Источники и дальнейшее чтение
- Статья содержит ссылки на дополнительные чтения и внешние ссылки.
Полный текст статьи: