Математический анализ конструкций
-
Основы конструкционного анализа (CoC)
- CoC — это теория типов, разработанная Тьерри Кокандом, которая может служить как языком программирования, так и основой для математики.
- CoC и его варианты используются в Coq и других инструментах проверки.
-
Общие черты и использование
- CoC является типизированным лямбда-исчислением высшего порядка, которое находится на вершине лямбда-куба Барендрегта.
- В CoC можно определять функции от терминов к терминам и от типов к типам.
- CoC сильно нормализуется и является последовательным.
-
Математический анализ конструкций
- Математический анализ конструкций является продолжением изоморфизма Карри-Говарда, связывающего термины с доказательствами в интуиционистской логике.
- CoC включает в себя пять видов объектов: доказательства, предложения, предикаты, большие типы и T.
-
Суждения и правила вывода
- Математический анализ конструкций позволяет доказывать типизированные суждения.
- Правила вывода для исчисления конструкций включают в себя правила для определения предложений, предикатов, квантификации и лямбда-абстракции.
-
Определение логических операторов и типов данных
- В CoC используется только один логический оператор — ∀.
- Основные типы данных, такие как логические и натуральные значения, могут быть определены в CoC.
-
Дополнительные ресурсы
- В статье также упоминаются другие связанные теории и системы, такие как система чистого типа, лямбда-кубик, система F и теория гомотопических типов.
- Ссылки на источники и рекомендации по изучению CoC также включены в статью.