Перегляд вихідного коду сторінки Числення конструкцій

'''Числення конструкцій''' ({{Lang-en|calculus of constructions, CoC}})&nbsp;— [[теорія типів]] на основі [[Поліморфізм (програмування)|поліморфного]] [[Лямбда-числення|λ-числення]] вищого порядку із [[Залежний тип|залежними типами]], розроблена {{Нп|Тьєррі Коканом|Тьєррі Коканом|ru|Кокан, Тьерри}} і {{Нп|Жерар Юе|Жераром Юе|en|Gérard Huet}} 1986 року. Міститься у вищій точці [[лямбда-куб]]а [[Генк Барендрегт|Барендрегта]], є найширшою зі систем, що входять до нього&nbsp;— <math>\lambda P\omega</math>. Може застосовуватись як основа для побудови типізованої мови програмування і як система [[Конструктивізм (математика)|конструктивних]] [[Криза основ математики|основ математики]].

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

Серед варіантів числення&nbsp;— числення індуктивних конструкцій<ref>[https://coq.inria.fr/distrib/current/refman/language/cic.html Исчисление индуктивных конструкций] {{Webarchive|url=https://web.archive.org/web/20200610014646/https://coq.inria.fr/distrib/current/refman/language/cic.html |date=2020-06-10 }}, и в базовых стандартных библиотеках Coq: [https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html <code>Datatypes</code>] {{Webarchive|url=https://web.archive.org/web/20200610014635/https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html |date=2020-06-10 }} and [https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html <code>Logic</code>] {{Webarchive|url=https://web.archive.org/web/20200610014635/https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html |date=2020-06-10 }}.</ref> (використовує [[Інтуїціоністська теорія типів|індуктивні типи]]), числення коіндуктивних конструкцій (із застосуванням [[Коіндукція|коіндукції]]), предикативне числення індуктивних конструкцій (усуває деяку частину [[Непредикативність (математика)|непредикативності]]).

З погляду [[Відповідність Каррі — Говарда|відповідності Каррі&nbsp;— Говарда]] числення конструкцій встановлює взаємозв'язок між залежними типами та доведеннями у [[Числення секвенцій|секвенційному]] інтуїціоністському [[Логіка першого порядку|численні предикатів]].

== Структура ==

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

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

Іншими словами, синтаксис терму, якщо записати його за допомогою [[Нотація Бекуса — Наура|BNF]], такий:

: <math>e ::= \mathbf{T} \mid \mathbf{P} \mid x \mid e \, e \mid \lambda x\mathbin{:}e.e\mid \forall x\mathbin{:}e.e</math>

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

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

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

: <math> x_1:A_1, x_2:A_2, \ldots \vdash t:B</math>

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

: Якщо змінні <math>x_1, x_2, \ldots</math> мають типи <math>A_1, A_2, \ldots</math>, то терм <math>t</math> має тип <math>B</math>.

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

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

: <math> {\Gamma \vdash A:B} \over {\Gamma' \vdash C:D} </math>

це означає:

: Якщо <math> \Gamma \vdash A:B </math> є валідним судженням, то <math> \Gamma' \vdash C:D </math>

=== Правила виведення для числення конструкцій ===
'''1''' . <math> {{} \over {} \Gamma \vdash P : T} </math>

'''2''' . <math> {\Gamma \vdash A : K \over 
{\Gamma, x:A \vdash x : A}} </math>

'''3''' . <math> {\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}} </math>

'''4''' . <math> {\Gamma \vdash M : (\forall x:A . B)\qquad\qquad\Gamma
\vdash N : A \over 
{\Gamma \vdash M N : B[x := N]}} </math>

'''5''' . <math> {\Gamma \vdash M : A \qquad \qquad A =_\beta B \qquad \qquad \Gamma \vdash B : K 
\over {\Gamma \vdash M : B}} </math>

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

: <math>
\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}
</math>

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

; Булівські значення
: <math>\forall A: P . A \Rightarrow A \Rightarrow A</math>
; Натуральні числа
: <math>\forall A:P . 
(A \Rightarrow A) \Rightarrow (A \Rightarrow A)</math>
; Добуток <math>A \times B</math>
: <math>A \wedge B</math>
; Виключне об'єднання (запис із варіантами) <math>A + B</math>
: <math>A \vee B</math>

Зверніть увагу на те, що булівські та числові значення визначаються способом, аналогічним [[Кодування Чорча|кодуванню Чорча]]. Однак додаткові проблеми виникають через екстенсіональність тверджень та іррелевантність{{Уточнити}} доведень<ref>{{Cite web|url=http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html|title=Standard Library {{!}} The Coq Proof Assistant<!-- Заголовок добавлен ботом -->|accessdate=2020-06-24|archivedate=2011-07-21|archiveurl=https://web.archive.org/web/20110721010122/http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html|deadurl=no}} {{Webarchive|url=https://web.archive.org/web/20110721010122/http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html |date=2011-07-21 }}</ref>.

== Примітки ==
{{Reflist}}
{{Бібліоінформація}}
{{Типи даних}}
[[Категорія:Теорія типів]]
[[Категорія:Лямбда-числення]]