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

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

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

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

Структура

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

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

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

: 

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

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

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

: 

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

: Якщо змінні  мають типи , то терм  має тип .

Допустимі міркування для числення конструкцій можна отримати з набору правил виведення. Надалі символом  позначено послідовність присвоєння типів , і символом K позначено або P, або T. Формула  буде використовуватися для заміни терму  для кожної вільної змінної  у термі .

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

: 

це означає:

: Якщо  є валідним судженням, то 

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

2 . 

3 . 

4 . 

5 . 

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

: 

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

; Булівські значення
: 
; Натуральні числа
: 
; Добуток 
: 
; Виключне об'єднання (запис із варіантами) 
: 

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

Примітки




