Система чистого типа
-
Основы теории доказательств и типов
- Система чистых типов (PTS) — это форма типизированного лямбда-исчисления с произвольным количеством видов и зависимостей.
- PTS обобщает лямбда-куб Барендрегта и может затушевывать различие между типами и терминами.
-
История и развитие
- PTS были независимо представлены Стефано Берарди и Яном Терлоу в 1988 и 1989 годах соответственно.
- Герман Гейверс расширил PTS, назвав его L-кубом, и распространил на него соответствие Карри-Говарда.
- Дж. Барт и другие добавили оператор двойного отрицания, чтобы получить классические системы чистого типа (CPTS).
- Тийн Боргуис представил модальные системы чистых типов (MPTS) в 1998 году.
-
Гипотеза Барендрегта-Гейверса-Клопа
- Гипотеза касается свойства сильной нормализации всех известных систем чистых типов.
- Это свойство называется гипотезой Барендрегта-Гейверса-Клопа и является нерешенной проблемой в области.
-
Определение системы чистых типов
- Система чистых типов состоит из набора разновидностей (S), набора аксиом (A) и набора правил (R).
- Правила ввода текста включают аксиомы и правила, такие как начало, ослабление, продукт, заявка, абстракция и преобразование.
-
Примеры языков программирования с PTS
- Некоторые языки программирования, такие как ШАЛФЕЙ, Тысячелистник и Хенк 2000, используют PTS.
-
Дополнительные сведения
- В статье упоминаются система U как пример несогласованной PTS и λμ-calculus с другим подходом к управлению типами.
- Также есть рекомендации по дальнейшему чтению и внешние ссылки.
Полный текст статьи: