Расчет конструкций

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

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

Общие черты

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

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

Использование

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

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

Основы расчета конструкций

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

Условия

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

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

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

e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e

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

доказательства , которые представляют собой термины, типами которых являются предложения ;
предложения , которые также известны как малые типы ;
предикаты — функции, возвращающие предложения;
большие типы , которые являются типами предикатов ( $\mathbf {P}$ является примером крупного типа);
$\mathbf {T}$ сам по себе, что является типом больших типов.

Суждения

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

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

,

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

Если переменные

x_{1},x_{2},\ldots

имеют соответственно типы

A_{1},A_{2},\ldots

, то срок

t

имеет тип

B

.

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

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

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

,

что означает

если

\Gamma \vdash A:B

является действительным суждением, то таковым является и

\Gamma '\vdash C:D

.

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

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

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

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

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

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

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

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

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

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

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

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

логические значения: $\forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A$
естественный: $\forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow A\Rightarrow A$
Продукт $A\times B$: $A\wedge B$
Непересекающийся союз $A+B$: $A\vee B$

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

См. также

Ссылки

^ Исчисление индуктивных конструкций и основные стандартные библиотеки: Datatypes и Logic.
^ Коканд, Тьерри; Галье, Жан Х. (июль 1990 г.). «Доказательство сильной нормализации теории конструкций с использованием интерпретации типа Крипке» . Технические отчеты (СНГ) : 14.
^ «Стандартная библиотека | Помощник по проверке Coq» . coq.inria.fr . Проверено 8 августа 2020 г.

Источники

Коканд, Тьерри ; Юэ, Жерар (1988). «Строительный расчет» (PDF) . Информация и вычисления . 76 (2–3): 95–120. дои : 10.1016/0890-5401(88)90005-3 .
- Также имеется в свободном доступе онлайн: Коканд, Тьерри; Юэ, Жерар (1986). Расчет конструкций (Технический отчет). ИНРИА , Центр Рокенкур. 530.
  Обратите внимание, что терминология довольно разная. Например, ( $\forall x:A.B$ ) пишется [ x : A ] B .
Бандер, М.В.; Селдин, Джонатан П. (2004). «Варианты основного расчета конструкций» . CiteSeer ^х: 10.1.1.88.9497 .
Фраде, Мария Жуан (2009). «Исчисление индуктивных конструкций» (PDF) . Архивировано из оригинала (обсуждение) 29 мая 2014 г. Проверено 03 марта 2013 г.
Юэ, Жерар (1988). «Принципы индукции, формализованные в расчете конструкций» (PDF) . Ин Фучи, К.; Ниват, М. (ред.). Программирование компьютеров будущего поколения . Северная Голландия. стр. 205–216. ISBN 0444704108 . Архивировано из оригинала (PDF) 1 июля 2015 г. — Заявление КоК

[1] Исчисление индуктивных конструкций и основные стандартные библиотеки: Datatypes и Logic.

[2] Коканд, Тьерри; Галье, Жан Х. (июль 1990 г.). «Доказательство сильной нормализации теории конструкций с использованием интерпретации типа Крипке» . Технические отчеты (СНГ) : 14.

[3] «Стандартная библиотека | Помощник по проверке Coq» . coq.inria.fr . Проверено 8 августа 2020 г.

[1]

[2]

[3]