Konstruktionsberegning

The calculus of constructions ( CoC ) er en typeteori baseret på en højere ordens polymorf λ-calculus med afhængige typer , udviklet af Thierry Cocan og Gerard Huet i 1986. Den er placeret på det højeste punkt af Barendregt lambda-terningen og er den bredeste af dens konstituerende systemer - . Det kan bruges som grundlag for opbygning af et maskinskrevet programmeringssprog og som et system af konstruktivt grundlag for matematik . $\lambda P\omega$

Brugt som grundlag for det interaktive bevissystem Coq og en række lignende værktøjer (herunder Matita ).

Blandt calculus-mulighederne er calculus for induktive konstruktioner [1] (bruger induktive typer ), calculus for co-induktive konstruktioner (med coinduction ), den prædikative calculus for induktive konstruktioner (eliminerer noget af ikke-prædikativiteten ).

Med hensyn til Curry-Howard-korrespondancen etablerer konstruktionskalkylen forholdet mellem afhængige typer og beviser i den sekventielle intuitionistiske prædikatregning .

Struktur

Bade

Et led i konstruktionsregning er konstrueret efter følgende regler:

T er et udtryk (også omtalt som Type );
P er et udtryk (også kaldet Prop , dette er typen, som alle udsagn refererer til);
Variabler ( x , y , ...) er udtryk;
Hvis A og B er led, så er udtrykket ( A B ) også et led;
Hvis A og B er led, og x er en variabel, så er følgende udtryk også udtryk:
- ( λx : A.B ) , _
- (∀x : A . B).

Med andre ord er syntaksen for et udtryk, når det skrives med BNF ,:

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

Konstruktionsregningen bruger fem typer objekter:

beviser , der har typen af visse udsagn ;
påstande , også kaldet små typer ;
prædikater , som er funktioner, der returnerer påstande ;
store typer , der er typer for prædikater ( P er et eksempel på en så stor type);
T som sådan, som er den type, som de store typer tilhører.

Domme

Konstruktionsregningen giver mulighed for at bevise domme om typer .

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

kan læses som en implikation:

Hvis variablerne er af typen , så er udtrykket af typen .

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

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

t

B

Gyldige forslag til konstruktionskalkylen kan udledes af et sæt slutningsregler. I det følgende bruger vi symbol til at angive en sekvens af typetildelinger , og K til at angive enten P eller T. Formlen vil blive brugt til at erstatte termen for hver fri variabel i termen . $\Gamma$ $x_{1}:A_{1},x_{2}:A_{2},\ldots$ $B[x:=N]$ $N$ $x$ $B$

Inferensregler er skrevet i følgende format:

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

det betyder:

Hvis det er et gyldigt forslag, så

\Gamma \vdash A:B

\Gamma '\vdash C:D

Inferensregler for konstruktionsregning

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))$

Definition af logiske operatorer

Konstruktionsregningen omfatter et meget lille antal grundlæggende operatorer: den eneste logiske operator til dannelse af udsagn . Denne erklæring alene er dog tilstrækkelig til at definere alle andre logiske operatorer: $\for alle$

{\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:AB&(x\notin B)\\A\wedge B&\equiv &\forall C:P.(A\Rightarrow B) \Højrepil C)\Højrepil C&\\A\vee B&\equiv &\forall C:P.(A\Højrepil C)\Højrepil (B\Højrepil C)\Højrepil C&\\\neg A&\equiv &\forall C :P.(A\Rightarrow C)&\\\eksisterer x:AB&\equiv &\forall C:P.(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}

Definition af datatyper

Konstruktionsberegningen giver dig mulighed for at definere de grundlæggende datatyper, der bruges i datalogi:

booleske værdier

\forall A:PA\Rightarrow A\Rightarrow A

Heltal

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

Arbejde

A\ gange B

A\kile B

Eksklusiv joinforbindelse (variant notation)

A+B

A\vee B

Bemærk, at booleske og numeriske værdier er defineret på samme måde som kirkens kodning . Der opstår imidlertid yderligere problemer på grund af udsagnenes ekstensionalitet og irrelevansen[ afklare ] beviser [2] .

Noter

↑ Calculus of Inductive Constructions Arkiveret 10. juni 2020 på Wayback Machine og i Coq Core Standard Libraries: Arkiveret 10. juni 2020 på Wayback Machine og Arkiveret 10. juni 2020 på Wayback Machine .Datatypes Logic
↑ Standardbibliotek | Coq Proof Assistant . Hentet 24. juni 2020. Arkiveret fra originalen 21. juli 2011. (ubestemt)