Русская Википедия:Исчисление конструкций

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Исчисление конструкций (Шаблон:Lang-en) — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — <math>\lambda P\omega</math>. Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики.

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

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

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

Структура

Термы

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

• T — это терм (так же его обозначают как Type);
• P — это терм (так же его обозначают как Prop, это — тип, к которому относятся все утверждения);
• Переменные (x, y, …) — это термы;
• Если A и B — это термы, то выражение (A B) также является термом;
• Если A и B — это термы и x — это переменная, то нижеследующие выражения также являются термами:
  • (λx:A . B),
  • (∀x:A . B).

Другими словами, синтаксис терма, если записать его при помощи BNF, следующий:

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

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

1. доказательства, которые имеют типом те или иные утверждения;
2. утверждения, также называемые малыми типами;
3. предикаты, являющиеся функциями, возвращающими утверждения;
4. большие типы, являющиеся типами для предикатов (P — пример такого большого типа);
5. T как таковой, который является типом, к которому относятся большие типы.

Суждения

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

<math> x_1:A_1, x_2:A_2, \ldots \vdash t:B</math>

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

Если переменные <math>x_1, x_2, \ldots</math> имеют типы <math>A_1, A_2, \ldots</math>, то терм <math>t</math> имеет тип <math>B</math>.

Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ <math>\Gamma</math> чтобы обозначить последовательность присвоений типов <math> x_1:A_1, x_2:A_2, \ldots </math>, и K чтобы обозначить либо P либо T. Формула <math>B[x:=N]</math> будет использоваться для замены терма <math>N</math> для каждой свободной переменной <math>x</math> в терме <math>B</math>.

Правила вывода записываются в следующем формате:

<math> {\Gamma \vdash A:B} \over {\Gamma' \vdash C:D} </math>

это означает:

Если <math> \Gamma \vdash A:B </math> является валидным суждением, то <math> \Gamma' \vdash C:D </math>

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

1. <math> {{} \over {} \Gamma \vdash P : T} </math>

2. <math> {\Gamma \vdash A : K \over {\Gamma, x:A \vdash x : A}} </math>

3. <math> {\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}} </math>

4. <math> {\Gamma \vdash M : (\forall x:A . B)\qquad\qquad\Gamma \vdash N : A \over {\Gamma \vdash M N : B[x := N]}} </math>

5. <math> {\Gamma \vdash M : A \qquad \qquad A =_\beta B \qquad \qquad \Gamma \vdash B : K \over {\Gamma \vdash M : B}} </math>

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

Исчисление конструкций включает в себя совсем небольшое число основных операторов: единственный логический оператор для формирования утверждений <math>\forall</math>. Однако одного этого оператора достаточно для определения всех других логических операторов:

<math>

\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} </math>

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

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

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

<math>\forall A: P . A \Rightarrow A \Rightarrow A</math>

Натуральные числа

<math>\forall A:P .

(A \Rightarrow A) \Rightarrow (A \Rightarrow A)</math>

Произведение <math>A \times B</math>

<math>A \wedge B</math>

Исключающее объединение (запись с вариантами) <math>A + B</math>

<math>A \vee B</math>

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