Építőipari kalkulus

A konstrukciószámítás ( CoC ) egy típuselmélet , amely egy magasabb rendű polimorf λ-számításon alapul , függő típusokkal , amelyet Thierry Cocan és Gerard Huet fejlesztett ki 1986-ban. A Barendregt lambda-kocka legmagasabb pontján található , lévén a legszélesebb az alkotórendszerei közül . Használható alapként egy tipizált programozási nyelv felépítéséhez, és a matematika építő alapjainak rendszereként . $\lambda P\omega$

A Coq interaktív bizonyítási rendszer és számos hasonló eszköz (köztük Matita ) alapja .

A számítási lehetőségek között szerepel az induktív konstrukciók számítása [1] ( induktív típusokat használ ), a koinduktív konstrukciók számítása ( koindukciót használva ), az induktív konstrukciók predikatív számítása (kiküszöböli a nem predikativitást ).

A Curry-Howard megfeleltetés szempontjából a konstrukciós kalkulus a szekvenciális intuicionista predikátumszámításban a függő típusok és a bizonyítások közötti kapcsolatot állapítja meg .

Szerkezet

Fürdők

Az építési számításban egy kifejezést a következő szabályok szerint állítunk össze:

T egy kifejezés (más néven típus );
P egy kifejezés (más néven Prop , ez az a típus, amelyre minden utasítás utal);
A változók ( x , y , …) kifejezések;
Ha A és B tagok, akkor az ( A B ) kifejezés is tag;
Ha A és B kifejezések, x pedig változó, akkor a következő kifejezések is tagok:
- (λx : A . B ) ,
- (∀x : A . B).

Más szavakkal, egy kifejezés szintaxisa, ha BNF használatával írják , a következő:

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

A konstrukciós számítás ötféle objektumot használ:

bizonyos állítások típusával rendelkező bizonyítások ;
állítások , más néven kis típusok ;
predikátumok , amelyek olyan függvények, amelyek állításokat adnak vissza ;
nagy típusok , amelyek predikátumok típusai ( P egy ilyen nagy típusra példa);
T mint olyan, amely az a típus, amelyhez a nagy típusok tartoznak.

Ítéletek

A konstrukciós kalkulus lehetővé teszi a típusokra vonatkozó ítéletek bizonyítását .

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

következményként olvasható:

Ha a változók típusúak , akkor a kifejezés típusos .

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

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

t

B

A konstrukciós kalkulusra vonatkozó érvényes javaslatok következtetési szabályokból származtathatók. A következőkben szimbólumot használunk a típus-hozzárendelések sorozatának jelölésére , a K -t pedig P vagy T jelölésére . A képlet a kifejezés minden szabad változójához tartozó kifejezést helyettesíti . $\Gamma$ $x_{1}:A_{1},x_{2}:A_{2},\ldots$ $B[x:=N]$ $N$ $x$ $B$

A következtetési szabályok a következő formátumban vannak megírva:

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

azt jelenti:

Ha érvényes javaslat, akkor

\Gamma \vdash A:B

\Gamma '\vdash C:D

Következtetési szabályok a konstrukciós kalkulushoz

1 . ${\displaystyle {{} \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))$

Logikai operátorok meghatározása

A konstrukciós kalkulus nagyon kevés alapvető operátort tartalmaz: az egyetlen logikai operátor az utasítások képzéséhez . Ez az állítás azonban önmagában elegendő az összes többi logikai operátor meghatározásához: $\mindenkinek$

{\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)&\\\ létezik x:AB&\egyenértékű &\minden C:P.(\minden x:A.(B\Rightarrow C))\Rightarrow C&\end{tömb}}

Adattípusok meghatározása

A konstrukciós kalkulus lehetővé teszi a számítástechnikában használt alapvető adattípusok meghatározását:

Logikai értékek

\forall A:PA\Rightarrow A\Rightarrow A

Egész számok

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

Munka

A\-szer B

A\ék B

Kizárólagos csatlakozás (változatjelölés)

A+B

A\vee B

Vegye figyelembe, hogy a logikai és a numerikus értékek az egyházi kódoláshoz hasonló módon vannak meghatározva . További problémák merülnek fel azonban az állítások kiterjedtségéből és irrelevánsságából[ pontosítani ] bizonyíték [2] .

Jegyzetek

↑ Induktív konstrukciók kalkulusa archiválva 2020. június 10-én a Wayback Machine -nél és a Coq Core Standard Libraries-ben: 2020. június 10-én a Wayback Machine -nél és 2020. június 10-én archiválva a Wayback Machine -nél .Datatypes Logic
↑ Standard Library | A Coq Proof Assistant . Letöltve: 2020. június 24. Az eredetiből archiválva : 2011. július 21. (határozatlan)