Curry-Howard korrespondance

Curry-Howard korrespondancen ( Curry-Howard isomorphism , engelsk formulæ-as-types fortolkning ) er en observerbar strukturel ækvivalens mellem matematiske beviser og programmer , der kan formaliseres som en isomorfi mellem logiske systemer og maskinskrevne calculi.

Haskell Curry [1] og William Howard2] , at konstruktionen af konstruktivt bevis ligner beskrivelsen af beregninger, og udsagn om konstruktiv logik ligner i deres struktur de typer af beregnede udtryk - programmer til en computer . Tidlige manifestationer af denne forbindelse er Brouwer-Heiting-Kolmogorov-fortolkningen (1925), som definerer den intuitionistiske logiks semantik gennem beregning af beviser, og realiserbarhedsteorien Kleene (1945).

Curry-Howard korrespondance i den moderne opfattelse er ikke begrænset til nogen logik eller type system. For eksempel svarer propositionslogik til en simpelt skrevet λ-regning , andenordens svarer til en λ-regning og prædikatregning svarer til en λ-regning med afhængige typer .

Inden for rammerne af Curry-Howard isomorfismen betragtes følgende strukturelle elementer som ækvivalente:

Logiske systemer	Programmeringssprog
udmelding	Type
Bevis for erklæringen $P$	Term (udtryk) type $P$
Udsagnet kan bevises $P$	Type beboet $P$
implikation $P\Rightarrow Q$	funktionel type $P\rightarrow Q$
Konjunktion $P\land Q$	Artwork type (par) $P\ gange Q$
Disjunktion $P\lor Q$	Sumtype (diskrimineret forening) $P+Q$
Ægte formel	enkelt type
Falsk formel	Tom type ( ) $\bot$
Universal kvantifier $\for alle$	Afhængig produkttype ( -type) $\Pi$
Eksistens kvantifier $\eksisterer$	Afhængig sumtype ( -type) $\Sigma$

Det enkleste eksempel på Curry-Howard-korrespondancen er en isomorfi mellem en simpel maskinskrevet λ-regning og et stykke intuitionistisk propositionel logik , der kun omfatter implikation . For eksempel svarer en type i en simpel maskinskrevet lambdaregning til en proposition af propositionel logik. For at bevise denne erklæring er det nødvendigt at konstruere et udtryk af den specificerede type (hvis dette kan gøres, så siger de om typen, at det er beboet eller beboet ), i dette tilfælde kan du præsentere det ønskede udtryk: , og det betyder, at tautologien er bevist. $(P\rightarrow Q\rightarrow R)\rightarrow (P\rightarrow Q)\rightarrow P\rightarrow R$ $(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$ $\lambda fgx\rightarrow fx(gx)$ $(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$

Brugen af Curry-Howard isomorfisme har gjort det muligt at skabe en hel klasse af funktionelle programmeringssprog, hvis runtime-miljø også er et automatisk bevissystem , såsom Coq , Agda og Epigram .

Noter

↑ Curry, HB, Feys, R. Combinatory Logic Vol. I. - Amsterdam : Nord-Holland , 1958.
↑ Howard, WA Formler-som-typer-begrebet om konstruktion // Til HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. - Boston: Academic Press , 1980. - s. 479-490 .

Litteratur

Pierce, Benjamin C. Typer og programmeringssprog. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Oversættelse til russisk: Pierce B. Skriver på programmeringssprog. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .