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

Числення конструкцій (Шаблон:Lang-en) — теорія типів на основі поліморфного λ-числення вищого порядку із залежними типами, розроблена Шаблон:Нп і Шаблон:Нп 1986 року. Міститься у вищій точці лямбда-куба Барендрегта, є найширшою зі систем, що входять до нього — $\lambda P\omega$. Може застосовуватись як основа для побудови типізованої мови програмування і як система конструктивних основ математики.

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

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

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

Структура

Терми

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

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

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

$e::=𝐓\mid 𝐏\mid x\mid ee\mid \lambda x:e.e\mid \mathrm{\forall }x:e.e$

Числення конструкцій використовує п'ять типів об'єктів:

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

Судження

Числення конструкцій дозволяє доводити судження про типи.

$x_1:A_1,x_2:A_2,\dots ⊢t:B$

можна прочитати як імплікацію:

Якщо змінні $x_1,x_2,\dots$ мають типи $A_1,A_2,\dots$, то терм $t$ має тип $B$.

Допустимі міркування для числення конструкцій можна отримати з набору правил виведення. Надалі символом $\mathrm{\Gamma }$ позначено послідовність присвоєння типів $x_1:A_1,x_2:A_2,\dots$, і символом K позначено або P, або T. Формула $B[x:=N]$ буде використовуватися для заміни терму $N$ для кожної вільної змінної $x$ у термі $B$.

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

$\frac{\mathrm{\Gamma }⊢A:B}{{\mathrm{\Gamma }}^{\prime }⊢C:D}$

це означає:

Якщо $\mathrm{\Gamma }⊢A:B$ є валідним судженням, то ${\mathrm{\Gamma }}^{\prime }⊢C:D$

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

1 . $\frac{}{\mathrm{\Gamma }⊢P:T}$

2 . $\frac{\mathrm{\Gamma }⊢A:K}{\mathrm{\Gamma },x:A⊢x:A}$

3 . $\frac{\mathrm{\Gamma },x:A⊢B:K\mathrm{\Gamma },x:A⊢N:B}{\mathrm{\Gamma }⊢(\lambda x:A.N):(\mathrm{\forall }x:A.B):K}$

4 . $\frac{\mathrm{\Gamma }⊢M:(\mathrm{\forall }x:A.B)\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢MN:B[x:=N]}$

5 . $\frac{\mathrm{\Gamma }⊢M:AA{=}_{\beta }B\mathrm{\Gamma }⊢B:K}{\mathrm{\Gamma }⊢M:B}$

Визначення логічних операторів

Числення конструкцій включає зовсім невелику кількість основних операторів: єдиний логічний оператор для формування тверджень $\mathrm{\forall }$ . Проте одного цього оператора достатньо для визначення всіх інших логічних операторів:

$\begin{array}{cccc}A\Rightarrow B& \equiv & \mathrm{\forall }x:A.B& (x\notin B)\\ A\wedge B& \equiv & \mathrm{\forall }C:P.(A\Rightarrow B\Rightarrow C)\Rightarrow C& \\ A\vee B& \equiv & \mathrm{\forall }C:P.(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C& \\ \mathrm{\neg }A& \equiv & \mathrm{\forall }C:P.(A\Rightarrow C)& \\ \mathrm{\exists }x:A.B& \equiv & \mathrm{\forall }C:P.(\mathrm{\forall }x:A.(B\Rightarrow C))\Rightarrow C& \end{array}$

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

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

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

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

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

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

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

$A\wedge B$

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

$A\vee B$

Зверніть увагу на те, що булівські та числові значення визначаються способом, аналогічним кодуванню Чорча. Однак додаткові проблеми виникають через екстенсіональність тверджень та іррелевантністьШаблон:Уточнити доведень.