Calculul constructiilor

Calculul construcțiilor ( CoC ) este o teorie a tipurilor bazată pe un λ-calcul polimorf de ordin superior cu tipuri dependente , dezvoltat de Thierry Cocan și Gerard Huet în 1986. Este situat în cel mai înalt punct al cubului lambda Barendregt , fiind cel mai larg dintre sistemele sale constitutive - . Poate fi folosit ca bază pentru construirea unui limbaj de programare tipizat și ca sistem de baze constructive pentru matematică . $\lambda P\omega$

Folosit ca bază pentru sistemul interactiv de dovezi Coq și o serie de instrumente similare (inclusiv Matita ).

Printre opțiunile de calcul se numără calculul construcțiilor inductive [1] (folosește tipuri inductive ), calculul construcțiilor co-inductive (folosind coinducția ), calculul predicativ al construcțiilor inductive (elimină o parte din non-predicativitatea ).

În ceea ce privește corespondența Curry-Howard , calculul de construcție stabilește relația dintre tipurile dependente și dovezi în calculul predicat intuiționist secvențial .

Structura

Băi

Un termen în calculul construcțiilor este construit conform următoarelor reguli:

T este un termen (denumit și Tip );
P este un termen (denumit și Prop , acesta este tipul la care se referă toate declarațiile);
Variabilele ( x , y , …) sunt termeni;
Dacă A și B sunt termeni, atunci expresia ( A B ) este de asemenea un termen;
Dacă A și B sunt termeni și x este o variabilă, atunci următoarele expresii sunt și termeni:
- ( λx : A. B ) ,
- (∀x : A . B).

Cu alte cuvinte, sintaxa unui termen, atunci când este scris folosind BNF , este:

e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}ee\mid \forall x{\mathbin { :}}ee

Calculul de construcție folosește cinci tipuri de obiecte:

dovezi care au tipul anumitor afirmatii ;
aserţiuni , numite şi tipuri mici ;
predicate , care sunt funcții care returnează aserțiuni ;
tipuri mari care sunt tipuri pentru predicate ( P este un exemplu de tip atât de mare);
T ca atare, care este tipul căruia îi aparțin tipurile mari.

Hotărârile

Calculul de construcție permite să se dovedească judecăți despre tipuri .

x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B

poate fi citit ca o implicație:

Dacă variabilele sunt de tip , atunci termenul este de tip .

x_{1},x_{2},\ldots

A_{1},A_{2},\ldots

t

B

Propozițiile valide pentru calculul construcției pot fi derivate dintr-un set de reguli de inferență. În cele ce urmează, folosim simbolul pentru a desemna o secvență de atribuiri de tip , iar K pentru a desemna fie P , fie T. Formula va fi folosită pentru a înlocui termenul pentru fiecare variabilă liberă din termen . $\Gamma$ $x_{1}:A_{1},x_{2}:A_{2},\ldots$ $B[x:=N]$ $N$ $X$ $B$

Regulile de inferență sunt scrise în următorul format:

{\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}

inseamna:

Dacă este o propoziție validă, atunci

\Gamma \vdash A:B

\Gamma '\vdash C:D

Reguli de inferență pentru calculul construcției

1 . ${{} \over {}\Gamma \vdash P:T)$

2 . ${\Gamma \vdash A:K \over {\Gamma,x:A\vdash x:A)}$

3 . ${\Gamma,x:A\vdash B:K\qquad \qquad \Gamma,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:AN):(\forall x: AB):K}}$

4 . ${\Gamma \vdash M:(\forall x:AB)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}$

5 . ${\Gamma \vdash M:A\qquad \qquad A=_{\beta}B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B)}$

Definiția operatorilor logici

Calculul de construcție include un număr foarte mic de operatori de bază: singurul operator logic pentru formarea enunțurilor . Cu toate acestea, această declarație este suficientă pentru a defini toți ceilalți operatori logici: $\pentru toți$

{\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:AB&(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)&\\\există x:AB&\equiv &\forall C:P.(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}

Definirea tipurilor de date

Calculul de construcție vă permite să definiți tipurile de date de bază utilizate în informatică:

Valori booleene

\forall A:PA\Rightarrow A\Rightarrow A

numere întregi

\forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)

Muncă

A\ori B

A\penă B

Unire exclusivă (notație variantă)

A+B

A\vee B

Rețineți că valorile booleene și numerice sunt definite într-un mod similar cu codarea Bisericii . Cu toate acestea, probleme suplimentare apar din extensialitatea enunțurilor și din irelevanță[ clarifica ] dovezi [2] .

Note

↑ Calculus of Inductive Constructions Arhivat la 10 iunie 2020 la Wayback Machine și în Coq Core Standard Libraries: Arhivat la 10 iunie 2020 la Wayback Machine și arhivat la 10 iunie 2020 la Wayback Machine .Datatypes Logic
↑ Biblioteca standard | Asistentul Coq Proof . Preluat la 24 iunie 2020. Arhivat din original la 21 iulie 2011. (nedefinit)