Числення конструкцій () — теорія типів на основі поліморфного λ-числення вищого порядку із залежними типами, розроблена і 1986 року. Міститься у вищій точці лямбда-куба Барендрегта, є найширшою зі систем, що входять до нього — . Може застосовуватись як основа для побудови типізованої мови програмування і як система конструктивних основ математики.
Є основою для системи інтерактивного доведення Coq та низки подібних інструментів (зокрема, ).
Серед варіантів числення — числення індуктивних конструкційИсчисление индуктивных конструкций , и в базовых стандартных библиотеках Coq: Datatypes and Logic . (використовує індуктивні типи), числення коіндуктивних конструкцій (із застосуванням коіндукції), предикативне числення індуктивних конструкцій (усуває деяку частину непредикативності).
З погляду відповідності Каррі — Говарда числення конструкцій встановлює взаємозв'язок між залежними типами та доведеннями у секвенційному інтуїціоністському численні предикатів.
Структура
Терми Терм у численні конструкцій будується за такими правилами:
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 .
Визначення логічних операторів Числення конструкцій включає зовсім невелику кількість основних операторів: єдиний логічний оператор для формування тверджень . Проте одного цього оператора достатньо для визначення всіх інших логічних операторів:
Визначення типів даних Числення конструкцій дозволяє визначити базові типи даних, що використовуються в інформатиці:
Булівські значення
Натуральні числа
Добуток
Виключне об'єднання (запис із варіантами)
Зверніть увагу на те, що булівські та числові значення визначаються способом, аналогічним кодуванню Чорча. Однак додаткові проблеми виникають через екстенсіональність тверджень та іррелевантність доведень .
Примітки