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

^[1] В математической логике и информатике исчисление конструкций ( CoC ) — это теория типов, созданная Тьерри Кокандом . Она может служить как типизированным языком программирования , так и конструктивной основой для математики . По этой второй причине CoC и его варианты стали основой для Coq и других помощников доказательства .

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

CoC — это типизированное лямбда-исчисление высшего порядка , изначально разработанное Тьерри Кокандом . Оно хорошо известно тем, что находится на вершине лямбда-куба Барендрегта . В CoC можно определять функции от термов к термовам, а также термов к типам, типов к типам и типов к термовам.

CoC является строго нормализующим и, следовательно, последовательным . ^[1]

CoC был разработан вместе с помощником по доказательству Coq . По мере добавления функций (или устранения возможных обязательств) к теории они стали доступны в Coq.

Варианты CoC используются в других помощниках по проверке доказательств, таких как Matita и Lean .

Исчисление конструкций можно считать расширением изоморфизма Карри–Ховарда . Изоморфизм Карри–Ховарда связывает термин в просто типизированном лямбда-исчислении с каждым доказательством естественного вывода в интуиционистской пропозициональной логике . Исчисление конструкций расширяет этот изоморфизм до доказательств в полном интуиционистском предикатном исчислении , которое включает доказательства квантифицированных утверждений (которые мы также будем называть «предложениями»).

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

• ${\displaystyle \mathbf {T} }$— это термин (также называемый типом );
• ${\displaystyle \mathbf {P} }$является термином (также называемым prop , типом всех предложений);
• Переменные ( ) — это термины;${\displaystyle x,y,\ldots}$
• Если и являются терминами, то также является ;${\displaystyle А}$${\displaystyle Б}$${\displaystyle (AB)}$
• Если и являются терминами, а — переменной, то следующие также являются терминами:${\displaystyle А}$${\displaystyle Б}$${\displaystyle x}$
  • ${\displaystyle (\лямбда x:AB)}$,
  • ${\displaystyle (\forall x:AB)}$.

Другими словами, синтаксис термина в форме Бэкуса-Наура выглядит следующим образом:

${\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. большие типы , которые являются типами предикатов ( является примером большого типа);${\displaystyle \mathbf {P} }$
5. ${\displaystyle \mathbf {T} }$сам по себе, который является типом больших типов.

Как и в случае с нетипизированным лямбда-исчислением, исчисление конструкций использует базовое понятие эквивалентности терминов, известное как -эквивалентность. Это отражает значение -абстракции:${\displaystyle \beta }$${\displaystyle \lambda }$

• ${\displaystyle (\lambda x:A.B)N=_{\beta }B(x:=N)}$

${\displaystyle \beta }$-эквивалентность — это отношение конгруэнтности для исчисления конструкций в том смысле, что

• Если и , то .${\displaystyle A=_{\beta }B}$${\displaystyle M=_{\beta }N}$${\displaystyle AM=_{\beta }BN}$

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

${\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 }$${\displaystyle A,B,C,D}$${\displaystyle K,L}$${\displaystyle \mathbf {P} }$${\displaystyle \mathbf {T} }$${\displaystyle B[x:=N]}$${\displaystyle N}$ ${\displaystyle x}$${\displaystyle B}$

Правило вывода записывается в виде

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

что означает

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

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

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

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

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

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

6 . ${\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:\mathbf {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}$

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

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

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

Натуралы

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

Продукт${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

Несвязное объединение${\displaystyle A+B}$

${\displaystyle A\vee B}$

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

• Чистая типизированная система
• Лямбда-куб
• Система F
• Зависимый тип
• Интуиционистская теория типов
• Теория гомотопического типа