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

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

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

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

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

Структура[ред. | ред. код]

Терми[ред. | ред. код]

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

• T — це терм (також його позначають як Type);
• P — це терм (також його позначають як Prop, це — тип, до якого належать усі твердження);
• змінні (x, y, …) — це терми;
• якщо A і B — це терми, то вираз (AB) також є термом;
• якщо A і B — це терми і x — це змінна, то термами є також такі вирази:
  • (λx:A . B),
  • (∀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. великі типи, що є типами для предикатів (P — приклад такого великого типу);
5. 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 }$, і символом K позначено або P, або 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 P:T}}$

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

3 . ${\displaystyle {\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 . ${\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}$

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

Визначення типів даних[ред. | ред. код]

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

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

${\displaystyle \forall A:P.A\Rightarrow A\Rightarrow A}$

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

${\displaystyle \forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)}$

Добуток ${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

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

${\displaystyle A\vee B}$

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

Примітки[ред. | ред. код]

Наука nLab Словники та енциклопедії BabelNet Нормативний контроль Freebase: /m/02wmgl