Числення конструкцій

Числення конструкцій (англ. calculus of constructions, CoC) — теорія типів на основі поліморфного λ-числення вищого порядку із залежними типами, розроблена Тьєррі Коканом і Жераром Юе 1986 року. Міститься у вищій точці лямбда-куба Барендрегта, є найширшою зі систем, що входять до нього — $\lambda P\omega$. Може застосовуватись як основа для побудови типізованої мови програмування і як система конструктивних основ математики.

Є основою для системи інтерактивного доведення Coq та низки подібних інструментів (зокрема, Matita).

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

З погляду відповідності Каррі — Говарда числення конструкцій встановлює взаємозв'язок між залежними типами та доведеннями у секвенційному інтуїціоністському численні предикатів.

Структура

Терми

Терм у численні конструкцій будується за такими правилами:

• T — це терм (також його позначають як Type);
• P — це терм (також його позначають як Prop, це — тип, до якого належать усі твердження);
• змінні (x, y, …) — це терми;
• якщо A і B — це терми, то вираз (AB) також є термом;
• якщо A і B — це терми і x — це змінна, то термами є також такі вирази:
  • (λx:A . B),
  • (∀x:A . B).

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

$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. великі типи, що є типами для предикатів (P — приклад такого великого типу);
5. 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$, і символом K позначено або P, або T. Формула $B[x:=N]$ буде використовуватися для заміни терму $N$ для кожної вільної змінної $x$ у термі $B$.

Правила виведення записуються в такому форматі:

${\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}$

це означає:

Якщо $\Gamma \vdash A:B$ є валідним судженням, то $\Gamma '\vdash C:D$

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

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

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

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

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

5 . ${\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: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}}$

Визначення типів даних

Числення конструкцій дозволяє визначити базові типи даних, що використовуються в інформатиці:

Булівські значення

$\forall A:P.A\Rightarrow A\Rightarrow A$

Натуральні числа

$\forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)$

Добуток $A\times B$

$A\wedge B$

Виключне об'єднання (запис із варіантами) $A+B$

$A\vee B$

Зверніть увагу на те, що булівські та числові значення визначаються способом, аналогічним кодуванню Чорча. Однак додаткові проблеми виникають через екстенсіональність тверджень та іррелевантність^{[уточнити]} доведень.