Исчисление конструкций

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

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

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

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

Структура

Термы

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

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

Другими словами, синтаксис терма, если записать его при помощи BNF, следующий:

$e::=𝐓\mid 𝐏\mid x\mid ee\mid \lambda x:e.e\mid \mathrm{\forall }x:e.e$

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

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

Суждения

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

$x_1:A_1,x_2:A_2,\dots ⊢t:B$

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

Если переменные $x_1,x_2,\dots$ имеют типы $A_1,A_2,\dots$, то терм $t$ имеет тип $B$.

Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ $\mathrm{\Gamma }$ чтобы обозначить последовательность присвоений типов $x_1:A_1,x_2:A_2,\dots$, и K чтобы обозначить либо P либо T. Формула $B[x:=N]$ будет использоваться для замены терма $N$ для каждой свободной переменной $x$ в терме $B$.

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

$\frac{\mathrm{\Gamma }⊢A:B}{{\mathrm{\Gamma }}^{\prime }⊢C:D}$

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

Если $\mathrm{\Gamma }⊢A:B$ является валидным суждением, то ${\mathrm{\Gamma }}^{\prime }⊢C:D$

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

1. $\frac{}{\mathrm{\Gamma }⊢P:T}$

2. $\frac{\mathrm{\Gamma }⊢A:K}{\mathrm{\Gamma },x:A⊢x:A}$

3. $\frac{\mathrm{\Gamma },x:A⊢B:K\mathrm{\Gamma },x:A⊢N:B}{\mathrm{\Gamma }⊢(\lambda x:A.N):(\mathrm{\forall }x:A.B):K}$

4. $\frac{\mathrm{\Gamma }⊢M:(\mathrm{\forall }x:A.B)\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢MN:B[x:=N]}$

5. $\frac{\mathrm{\Gamma }⊢M:AA{=}_{\beta }B\mathrm{\Gamma }⊢B:K}{\mathrm{\Gamma }⊢M:B}$

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

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

$\begin{array}{cccc}A\Rightarrow B& \equiv & \mathrm{\forall }x:A.B& (x\notin B)\\ A\wedge B& \equiv & \mathrm{\forall }C:P.(A\Rightarrow B\Rightarrow C)\Rightarrow C& \\ A\vee B& \equiv & \mathrm{\forall }C:P.(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C& \\ \mathrm{\neg }A& \equiv & \mathrm{\forall }C:P.(A\Rightarrow C)& \\ \mathrm{\exists }x:A.B& \equiv & \mathrm{\forall }C:P.(\mathrm{\forall }x:A.(B\Rightarrow C))\Rightarrow C& \end{array}$

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

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

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

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

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

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

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

$A\wedge B$

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

$A\vee B$

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