Исчисление конструкций (англ. calculus of constructions, CoC) — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем —
. Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики.
Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов (в том числе Matita[англ.]).
Среди вариантов исчисления — исчисление индуктивных конструкций[1] (использует индуктивные типы), исчисление коиндуктивных конструкций (с применением коиндукции), предикативное исчисление индуктивных конструкций (устраняет некоторую часть непредикативности).
С точки зрения соответствия Карри — Ховарда исчисление конструкций устанавливает взаимосвязь между зависимыми типами и доказательствами в секвенциальном интуиционистском исчислении предикатов.
Структура
Термы
Терм в исчислении конструкций конструируется по следующим правилами:
- T — это терм (так же его обозначают как Type);
- P — это терм (так же его обозначают как Prop, это — тип, к которому относятся все утверждения);
- Переменные (x, y, …) — это термы;
- Если A и B — это термы, то выражение (A B) также является термом;
- Если A и B — это термы и x — это переменная, то нижеследующие выражения также являются термами:
Другими словами, синтаксис терма, если записать его при помощи BNF, следующий:
![{\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78331ca6703e279dde9f74e1ee04ed35fa3b68c1)
Исчисление конструкций использует пять типов объектов:
- доказательства, которые имеют типом те или иные утверждения;
- утверждения, также называемые малыми типами;
- предикаты, являющиеся функциями, возвращающими утверждения;
- большие типы, являющиеся типами для предикатов (P — пример такого большого типа);
- T как таковой, который является типом, к которому относятся большие типы.
Суждения
Исчисление конструкций позволяет доказывать суждения о типах.
![{\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8e7008dd0d3b06110b77e7dab6e23737a59178e)
можно прочесть как импликацию:
- Если переменные
имеют типы
, то терм
имеет тип
.
Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ
чтобы обозначить последовательность присвоений типов
, и K чтобы обозначить либо P либо T. Формула
будет использоваться для замены терма
для каждой свободной переменной
в терме
.
Правила вывода записываются в следующем формате:
![{\displaystyle {\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4aef5197e90b7f5dd04fed1bfd2bd4f1e1156a5b)
это означает:
- Если
является валидным суждением, то ![{\displaystyle \Gamma '\vdash C:D}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3283d4caab1af337a7a820d6bb38ee0caaff9ba8)
Правила вывода для исчисления конструкций
1.
2.
3.
4.
5.
Определение логических операторов
Исчисление конструкций включает в себя совсем небольшое число основных операторов: единственный логический оператор для формирования утверждений
. Однако одного этого оператора достаточно для определения всех других логических операторов:
![{\displaystyle {\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv &\forall C:P.(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:P.(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:P.(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:P.(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1bbe7bac8941af0372f6e44f54276b5d04c6e9e7)
Определение типов данных
Исчисление конструкций позволяет определить базовые типы данных, используемые в информатике:
- Булевы значения
![{\displaystyle \forall A:P.A\Rightarrow A\Rightarrow A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/34ebd8538ed58b315f0c9257afbe7fbcf8db6e71)
- Натуральные числа
![{\displaystyle \forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d14b3d5796b1114c586202c625479179cab461c)
- Произведение
![{\displaystyle A\times B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/65f31ae45b0098f06b5d22c38d317eb097a88fa9)
![{\displaystyle A\wedge B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e86fbe93c98e68dc66cd518c98d5f6a624f5022b)
- Исключающее объединение (запись с вариантами)
![{\displaystyle A+B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4279cdbd3cb8ec4c3423065d9a7d83a82cfc89e3)
![{\displaystyle A\vee B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e4039c1a12cca22bb4df619c295c9a6f8be045f9)
Обратите внимания на то, что булевы и числовые значения определяются способом, аналогичным кодированию Чёрча. Однако дополнительные проблемы возникают из-за экстенсиональности утверждений и иррелевантности[уточнить] доказательств[2].
Примечания