Расчет конструкций - Calculus of constructions

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

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

Общие черты

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

CoC - это сильно нормализующий, хотя доказать это свойство в рамках CoC невозможно, поскольку оно предполагает согласованность, которая Теорема Гёделя о неполноте невозможно доказать изнутри самой системы.

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

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

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

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

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

Условия

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

• ${\displaystyle \mathbf {T} }$ это термин (также называемый Тип);
• ${\displaystyle \mathbf {P} }$ это термин (также называемый Опора, тип всех предложений);
• Переменные (${\displaystyle x,y,\ldots }$) являются терминами;
• Если ${\displaystyle A}$ и ${\displaystyle B}$ термины, то так ${\displaystyle (AB)}$;
• Если ${\displaystyle A}$ и ${\displaystyle B}$ условия и ${\displaystyle x}$ является переменной, то следующие термины также:
  • ${\displaystyle (\lambda x:A.B)}$,
  • ${\displaystyle (\forall 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. большие типы, которые являются типами предикатов (${\displaystyle \mathbf {P} }$ пример большого шрифта);
5. ${\displaystyle \mathbf {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 }$; ${\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 {\Gamma \vdash A:B} \over {\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 {{} \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}$

Naturals

${\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
• Зависимый тип
• Интуиционистская теория типов
• Теория гомотопического типа

Рекомендации

1. Исчисление индуктивных конструкций, и базовые стандартные библиотеки: Типы данных и Логика.
2. "Стандартная библиотека | Помощник по проверке Coq". coq.inria.fr. Получено 2020-08-08.

• Кокванд, Тьерри; Юэ, Жерар (1988). «Исчисление конструкций» (PDF). Информация и вычисления. 76 (2–3): 95–120. Дои:10.1016/0890-5401(88)90005-3.
  • Также доступны в свободном доступе в Интернете: Коканд, Тьерри; Юэ, Жерар (1986). Исчисление конструкций (Технический отчет). INRIA, Центр де Роккенкур. 530.
    Обратите внимание, что терминология несколько иная. Например, (${\displaystyle \forall x:A.B}$) написано [Икс : А] B.
• Bunder, M. W .; Селдин, Джонатан П. (2004). «Варианты основного исчисления конструкций». CiteSeerX  10.1.1.88.9497.
• Frade, Мария Жоао (2009). «Исчисление индуктивных конструкций» (PDF). Архивировано из оригинал (разговаривать) на 2014-05-29. Получено 2013-03-03.
• Юэ, Жерар (1988). «Принципы индукции, формализованные в исчислении конструкций» (PDF). In Fuchi, K .; Ниват, М. (ред.). Программирование компьютеров будущего поколения. Северная Голландия. С. 205–216. ISBN  0444704108. - Приложение CoC