Исчисление конструкций: Теория типов Тьерри Коканда
Calculus of constructions
Калькулус конструкций (CoC): теория типов, созданная Тьерри Кокан. Основа для Coq и других систем доказательства. Математика, программирование, логика.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Теория типов, созданная Тьерри Коканд. В математической логике и информатике, исчисление конструкций (CoC) — это теория типов, разработанная Тьерри Кокандом. Оно может использоваться как в качестве типизированного языка программирования, так и в качестве конструктивного основания для математики. По этой второй причине CoC и его варианты легли в основу Coq и других систем доказательства теорем. Некоторые из его вариантов включают исчисление индуктивных конструкций (которое добавляет индуктивные типы), исчисление (ко)индуктивных конструкций (которое добавляет коиндукцию) и предикативное исчисление индуктивных конструкций (которое устраняет некоторую импредикативность).
Type theory created by Thierry Coquand
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants. Some of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity).
Общие черты
CoC — это ламбда-исчисление высшего порядка, первоначально разработанное Тьерри Коквандом. Оно хорошо известно тем, что занимает верхнюю позицию в кубе лямбда Барендрегта. В CoC можно определять функции от термов к термам, от термов к типам, от типов к типам и от типов к термам. CoC сильно нормализуется и, следовательно, является непротиворечивым.
The CoC is a higher order typed lambda calculus, initially developed by Thierry Coquand. It is well known for being at the top of Barendregt's lambda cube. It is possible within CoC to define functions from terms to terms, as well as terms to types, types to types, and types to terms. The CoC is strongly normalizing, and hence consistent.
Использование
CoC разрабатывался параллельно с системой доказательств Coq. По мере добавления новых возможностей (или устранения потенциальных недостатков) в теорию, они становились доступными в Coq. Варианты CoC используются в других системах доказательств, таких как Matita и Lean.
The CoC has been developed alongside the Coq proof assistant. As features were added (or possible liabilities removed) to the theory, they became available in Coq. Variants of the CoC are used in other proof assistants, such as Matita and Lean.
Основы исчисления конструкций
Калькуль конструкций можно рассматривать как расширение изоморфизма Керри — Ховарда. Изоморфизм Керри — Ховарда сопоставляет терму в просто типизированном лямбда-исчислении каждое доказательство естественной дедукции в интуиционистской пропозициональной логике. Калькуль конструкций расширяет этот изоморфизм на доказательства в полном интуиционистском предикатном исчислении, которое включает доказательства квантифицированных утверждений (которые мы также будем называть "высказываниями").
The calculus of constructions can be considered an extension of the Curry–Howard isomorphism. The Curry–Howard isomorphism associates a term in the simply typed lambda calculus with each natural deduction proof in intuitionistic propositional logic. The calculus of constructions extends this isomorphism to proofs in the full intuitionistic predicate calculus, which includes proofs of quantified statements (which we will also call "propositions").
Правила вывода для исчисления конструкций
1 . - Да. - Да.
2 . - Да. - Да.
3 . - Да. - Да.
4 . - Да. - Да.
5 . - Да. - Да.
6 . - Да. - Да.
1 .
2 .
3 .
4 .
5 .
6 .
Определение логических операторов
В исчислении конструкций очень мало базовых операторов: единственный логический оператор для формирования высказываний — это Однако, этого одного оператора достаточно для определения всех остальных логических операторов:
The calculus of constructions has very few basic operators: the only logical operator for forming propositions is However, this one operator is sufficient to define all the other logical operators: