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

Эта статья требует внимания специалиста по информатике . Пожалуйста , добавьте причину в или разговоре параметр для этого шаблона , чтобы объяснить проблему с статьей. WikiProject Computer science может помочь нанять эксперта. ( Ноябрь 2008 г. )

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

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

Общие черты [ править ]

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

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

Использование [ править ]

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

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

Основы исчисления конструкций [ править ]

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

Условия [ править ]

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

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

Ссылки [ править ]