Исчисление конструкций ( англ. calculus of constructions, CoC ) — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами , разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта , являясь наиболее широкой из входящих в него систем — ${\displaystyle \lambda P\omega }$ . Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики .

Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов (в том числе ).

Среди вариантов исчисления — исчисление индуктивных конструкций (использует индуктивные типы ), исчисление коиндуктивных конструкций (с применением коиндукции ), предикативное исчисление индуктивных конструкций (устраняет некоторую часть непредикативности ).

С точки зрения соответствия Карри — Ховарда исчисление конструкций устанавливает взаимосвязь между зависимыми типами и доказательствами в секвенциальном интуиционистском исчислении предикатов .

Структура

Термы

Терм в исчислении конструкций конструируется по следующим правилами:

• T — это терм (так же его обозначают как Type );
• P — это терм (так же его обозначают как Prop , это — тип, к которому относятся все утверждения);
• Переменные ( x , y , …) — это термы;
• Если A и B — это термы, то выражение ( A B ) также является термом;
• Если A и B — это термы и x — это переменная, то нижеследующие выражения также являются термами:
  • (λ x : A . B ),
  • (∀ x : A . B).

Другими словами, синтаксис терма, если записать его при помощи 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}$

Исчисление конструкций использует пять типов объектов:

1. доказательства , которые имеют типом те или иные утверждения ;
2. утверждения , также называемые малыми типами ;
3. предикаты , являющиеся функциями, возвращающими утверждения ;
4. большие типы , являющиеся типами для предикатов ( P — пример такого большого типа);
5. T как таковой, который является типом, к которому относятся большие типы.

Суждения

Исчисление конструкций позволяет доказывать суждения о типах .

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$

можно прочесть как импликацию:

Если переменные ${\displaystyle x_{1},x_{2},\ldots }$ имеют типы ${\displaystyle A_{1},A_{2},\ldots }$ , то терм ${\displaystyle t}$ имеет тип ${\displaystyle B}$ .

Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ ${\displaystyle \Gamma }$ чтобы обозначить последовательность присвоений типов ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$ , и K чтобы обозначить либо P либо T . Формула ${\displaystyle B[x:=N]}$ будет использоваться для замены терма ${\displaystyle N}$ для каждой свободной переменной ${\displaystyle x}$ в терме ${\displaystyle B}$ .

Правила вывода записываются в следующем формате:

${\displaystyle {\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}}$

это означает:

Если ${\displaystyle \Gamma \vdash A:B}$ является валидным суждением, то ${\displaystyle \Gamma '\vdash C:D}$

Правила вывода для исчисления конструкций

1 . ${\displaystyle {{} \over {}\Gamma \vdash P:T}}$

2 . ${\displaystyle {\Gamma \vdash A:K \over {\Gamma ,x:A\vdash x:A}}}$

3 . ${\displaystyle {\Gamma ,x:A\vdash B:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B):K}}}$

4 . ${\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}$

5 . ${\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}$

Определение логических операторов

Исчисление конструкций включает в себя совсем небольшое число основных операторов: единственный логический оператор для формирования утверждений ${\displaystyle \forall }$ . Однако одного этого оператора достаточно для определения всех других логических операторов:

${\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}}}$

Определение типов данных

Исчисление конструкций позволяет определить базовые типы данных, используемые в информатике:

Булевы значения

${\displaystyle \forall A:P.A\Rightarrow A\Rightarrow A}$

Натуральные числа

${\displaystyle \forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)}$

Произведение ${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

Исключающее объединение (запись с вариантами) ${\displaystyle A+B}$

${\displaystyle A\vee B}$

Обратите внимания на то, что булевы и числовые значения определяются способом, аналогичным кодированию Чёрча . Однако дополнительные проблемы возникают из-за экстенсиональности утверждений и иррелевантности ^{[ уточнить ]} доказательств .

Примечания