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

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

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

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

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

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

• 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}$

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

У этой статьи есть несколько проблем, помогите их исправить: Стиль этой статьи неэнциклопедичен или нарушает нормы литературного русского языка. Статью следует исправить согласно стилистическим правилам Википедии. (27 сентября 2020) Необходимо проверить качество перевода c неуказанного языка, исправить содержательные и стилистические ошибки. Вы можете помочь улучшить эту статью (см. также рекомендации по переводу). Оригинал не указан. Пожалуйста, укажите его. (27 сентября 2020) Достоверность этой статьи поставлена под сомнение. Необходимо проверить точность фактов и достоверность сведений, изложенных в этой статье. Соответствующую дискуссию можно найти на странице обсуждения. (27 сентября 2020) В этой статье есть формулы, которые необходимо оформить. Пожалуйста, помогите улучшить их отображение. (27 сентября 2020) В статье не хватает ссылок на источники (см. рекомендации по поиску). Информация должна быть проверяема, иначе она может быть удалена. Вы можете отредактировать статью, добавив ссылки на авторитетные источники в виде сносок. (27 сентября 2020) Пожалуйста, после исправления проблемы исключите её из списка параметров. После устранения всех недостатков этот шаблон может быть удалён любым участником.