Числення конструкцій (англ. calculus of constructions, CoC) — теорія типів на основі поліморфного λ-числення вищого порядку із залежними типами, розроблена [ru] і [en] 1986 року. Міститься у вищій точці лямбда-куба Барендрегта, є найширшою зі систем, що входять до нього — . Може застосовуватись як основа для побудови типізованої мови програмування і як система конструктивних основ математики.
Є основою для системи інтерактивного доведення Coq та низки подібних інструментів (зокрема, [en]).
Серед варіантів числення — числення індуктивних конструкцій (використовує індуктивні типи), числення коіндуктивних конструкцій (із застосуванням коіндукції), предикативне числення індуктивних конструкцій (усуває деяку частину непредикативності).
З погляду відповідності Каррі — Говарда числення конструкцій встановлює взаємозв'язок між залежними типами та доведеннями у секвенційному інтуїціоністському численні предикатів.
Структура
Терми
Терм у численні конструкцій будується за такими правилами:
- 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 .
Визначення логічних операторів
Числення конструкцій включає зовсім невелику кількість основних операторів: єдиний логічний оператор для формування тверджень . Проте одного цього оператора достатньо для визначення всіх інших логічних операторів:
Визначення типів даних
Числення конструкцій дозволяє визначити базові типи даних, що використовуються в інформатиці:
- Булівські значення
- Натуральні числа
- Добуток
- Виключне об'єднання (запис із варіантами)
Зверніть увагу на те, що булівські та числові значення визначаються способом, аналогічним . Однак додаткові проблеми виникають через екстенсіональність тверджень та іррелевантність[] доведень.
Примітки
- Исчисление индуктивных конструкций [ 2020-06-10 у Wayback Machine.], и в базовых стандартных библиотеках Coq:
Datatypes
[ 2020-06-10 у Wayback Machine.] andLogic
[ 2020-06-10 у Wayback Machine.]. - Standard Library | The Coq Proof Assistant. оригіналу за 21 липня 2011. Процитовано 24 червня 2020.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Chislennya konstrukcij angl calculus of constructions CoC teoriya tipiv na osnovi polimorfnogo l chislennya vishogo poryadku iz zalezhnimi tipami rozroblena ru i en 1986 roku Mistitsya u vishij tochci lyambda kuba Barendregta ye najshirshoyu zi sistem sho vhodyat do nogo lPw displaystyle lambda P omega Mozhe zastosovuvatis yak osnova dlya pobudovi tipizovanoyi movi programuvannya i yak sistema konstruktivnih osnov matematiki Ye osnovoyu dlya sistemi interaktivnogo dovedennya Coq ta nizki podibnih instrumentiv zokrema en Sered variantiv chislennya chislennya induktivnih konstrukcij vikoristovuye induktivni tipi chislennya koinduktivnih konstrukcij iz zastosuvannyam koindukciyi predikativne chislennya induktivnih konstrukcij usuvaye deyaku chastinu nepredikativnosti Z poglyadu vidpovidnosti Karri Govarda chislennya konstrukcij vstanovlyuye vzayemozv yazok mizh zalezhnimi tipami ta dovedennyami u sekvencijnomu intuyicionistskomu chislenni predikativ StrukturaTermi Term u chislenni konstrukcij buduyetsya za takimi pravilami T ce term takozh jogo poznachayut yak Type P ce term takozh jogo poznachayut yak Prop ce tip do yakogo nalezhat usi tverdzhennya zminni x y ce termi yaksho A i B ce termi to viraz AB takozh ye termom yaksho A i B ce termi i x ce zminna to termami ye takozh taki virazi lx A B x A B Inshimi slovami sintaksis termu yaksho zapisati jogo za dopomogoyu BNF takij e T P x ee lx e e x e e displaystyle e mathbf T mid mathbf P mid x mid e e mid lambda x mathbin e e mid forall x mathbin e e Chislennya konstrukcij vikoristovuye p yat tipiv ob yektiv dovedennya yaki mayut tipom ti chi inshi tverdzhennya tverdzhennya takozh zvani malimi tipami predikati sho ye funkciyami yaki povertayut tverdzhennya veliki tipi sho ye tipami dlya predikativ P priklad takogo velikogo tipu T yak takij sho ye tipom do yakogo nalezhat veliki tipi Sudzhennya Chislennya konstrukcij dozvolyaye dovoditi sudzhennya pro tipi x1 A1 x2 A2 t B displaystyle x 1 A 1 x 2 A 2 ldots vdash t B mozhna prochitati yak implikaciyu Yaksho zminni x1 x2 displaystyle x 1 x 2 ldots mayut tipi A1 A2 displaystyle A 1 A 2 ldots to term t displaystyle t maye tip B displaystyle B Dopustimi mirkuvannya dlya chislennya konstrukcij mozhna otrimati z naboru pravil vivedennya Nadali simvolom G displaystyle Gamma poznacheno poslidovnist prisvoyennya tipiv x1 A1 x2 A2 displaystyle x 1 A 1 x 2 A 2 ldots i simvolom K poznacheno abo P abo T Formula B x N displaystyle B x N bude vikoristovuvatisya dlya zamini termu N displaystyle N dlya kozhnoyi vilnoyi zminnoyi x displaystyle x u termi B displaystyle B Pravila vivedennya zapisuyutsya v takomu formati G A BG C D displaystyle Gamma vdash A B over Gamma vdash C D ce oznachaye Yaksho G A B displaystyle Gamma vdash A B ye validnim sudzhennyam to G C D displaystyle Gamma vdash C D Pravila vivedennya dlya chislennya konstrukcij 1 G P T displaystyle over Gamma vdash P T 2 G A KG x A x A displaystyle Gamma vdash A K over Gamma x A vdash x A 3 G x A B KG x A N BG lx A N x A B K 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 G M x A B G N AG MN B x N displaystyle Gamma vdash M forall x A B qquad qquad Gamma vdash N A over Gamma vdash MN B x N 5 G M AA bBG B KG M B displaystyle Gamma vdash M A qquad qquad A beta B qquad qquad Gamma vdash B K over Gamma vdash M B Viznachennya logichnih operatoriv Chislennya konstrukcij vklyuchaye zovsim neveliku kilkist osnovnih operatoriv yedinij logichnij operator dlya formuvannya tverdzhen displaystyle forall Prote odnogo cogo operatora dostatno dlya viznachennya vsih inshih logichnih operatoriv A B x A B x B A B C P A B C CA B C P A C B C C A C P A C x A B C P x A B C C displaystyle begin array ccll A Rightarrow B amp equiv amp forall x A B amp x notin B A wedge B amp equiv amp forall C P A Rightarrow B Rightarrow C Rightarrow C amp A vee B amp equiv amp forall C P A Rightarrow C Rightarrow B Rightarrow C Rightarrow C amp neg A amp equiv amp forall C P A Rightarrow C amp exists x A B amp equiv amp forall C P forall x A B Rightarrow C Rightarrow C amp end array Viznachennya tipiv danih Chislennya konstrukcij dozvolyaye viznachiti bazovi tipi danih sho vikoristovuyutsya v informatici Bulivski znachennya A P A A A displaystyle forall A P A Rightarrow A Rightarrow A Naturalni chisla A P A A A A displaystyle forall A P A Rightarrow A Rightarrow A Rightarrow A Dobutok A B displaystyle A times B A B displaystyle A wedge B Viklyuchne ob yednannya zapis iz variantami A B displaystyle A B A B displaystyle A vee B Zvernit uvagu na te sho bulivski ta chislovi znachennya viznachayutsya sposobom analogichnim Odnak dodatkovi problemi vinikayut cherez ekstensionalnist tverdzhen ta irrelevantnist utochniti doveden PrimitkiIschislenie induktivnyh konstrukcij 2020 06 10 u Wayback Machine i v bazovyh standartnyh bibliotekah Coq Datatypes 2020 06 10 u Wayback Machine and Logic 2020 06 10 u Wayback Machine Standard Library The Coq Proof Assistant originalu za 21 lipnya 2011 Procitovano 24 chervnya 2020