Curry-Howard korrespondens

Curry-Howard-korrespondensen ( Curry-Howard isomorphism , engelsk formulæ-as-types interpretation ) är en observerbar strukturell motsvarighet mellan matematiska bevis och program som kan formaliseras som en isomorfism mellan logiska system och maskinskrivna kalkyler.

Haskell Curry [1] och William Howard2] att konstruktionen av konstruktivt bevis liknar beskrivningen av beräkningar, och påståendena om konstruktiv logik liknar i sin struktur de typer av beräknade uttryck - program för en dator . Tidiga manifestationer av detta samband är Brouwer-Heiting-Kolmogorov-tolkningen (1925), som definierar den intuitionistiska logikens semantik genom beräkning av bevis, och realiserbarhetsteorin Kleene (1945).

Curry-Howard-korrespondens i den moderna uppfattningen är inte begränsad till någon logik eller typsystem. Till exempel motsvarar propositionslogik en enkel typad λ-kalkyl , andra ordningens motsvarar en λ-kalkyl och motsvarar en λ-kalkyl med beroende typer .

Inom ramen för Curry-Howard-isomorfismen anses följande strukturella element vara likvärdiga:

Logiska system	Programmeringsspråk
påstående	Sorts
Bevis på uttalandet $P$	Typ av term (uttryck). $P$
Påståendet är bevisbart $P$	Typ bebodd $P$
inblandning $P\Rightarrow Q$	funktionell typ $P\rightarrow Q$
Samband $P\land Q$	Konstverkstyp (par) $P\times Q$
Åtskiljande $P\lor Q$	Summatyp (diskriminerad förening) $P+Q$
Riktig formel	enda typ
Falsk formel	Tom typ ( ) $\bot$
Universell kvantifierare $\för alla$	Beroende produkttyp ( -typ) $\Pi$
Existens kvantifierare $\existerar$	Beroende summatyp ( -typ) $\Sigma$

Det enklaste exemplet på Curry-Howard-korrespondensen är en isomorfism mellan en enkel maskinskriven λ-kalkyl och ett stycke intuitionistisk propositionslogik som endast inkluderar implikation . Till exempel, en typ i en enkel maskinskriven lambda-kalkyl motsvarar en proposition av propositionslogik . För att bevisa detta påstående är det nödvändigt att konstruera en term av den angivna typen (om detta kan göras, då säger de om typen att den är bebodd eller bebodd ), i det här fallet kan du presentera den önskade termen: , och detta betyder att tautologin har bevisats. $(P\högerpil Q\högerpil R)\högerpil (P\högerpil Q)\högerpil P\högerpil 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))$

Användningen av Curry-Howard isomorfism har gjort det möjligt att skapa en hel klass av funktionella programmeringsspråk vars runtime-miljö också är ett automatiskt bevissystem , såsom Coq , Agda och Epigram .

Anteckningar

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

Litteratur

Pierce, Benjamin C. Typer och programmeringsspråk. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Översättning till ryska: Pierce B. Typer i programmeringsspråk. - Dobrosvet , 2012. - 680 sid. — ISBN 978-5-7913-0082-9 .