Curry-Howardin kirjeenvaihto

Curry-Howard-vastaavuus ( Curry-Howard-isomorfismi , englanninkielinen formulaæ-as-types -tulkinta ) on havaittava rakenteellinen ekvivalenssi matemaattisten todisteiden ja ohjelmien välillä , joka voidaan formalisoida isomorfismina loogisten järjestelmien ja tyypitettyjen laskelmien välillä.

Haskell Curry [1] ja William Howard2] , että todistuksen rakentaminen on samanlaista kuin laskelmien kuvaus ja konstruktiivisen logiikan lausunnot ovat rakenteeltaan samanlaisia kuin tietokoneelle tarkoitettujen laskettujen lausekkeiden tyypit - ohjelmat . Tämän yhteyden varhaisia ilmentymiä ovat Brouwer-Heiting-Kolmogorov-tulkinta (1925), joka määrittelee intuitionistisen logiikan semantiikan todisteiden laskennan avulla, ja Kleenen (1945) realisoituvuusteoria

Curry-Howard-kirjeenvaihto ei nykyajan näkemyksessä rajoitu mihinkään logiikkaan tai tyyppijärjestelmään. Esimerkiksi lauselogiikka vastaa yksinkertaista tyyppiä olevaa λ-laskentaa , toisen asteen λ-laskentaa predikaattilaskenta vastaa λ-laskentaa, jonka tyypit ovat riippuvaisia .

Curry-Howard-isomorfismin puitteissa seuraavia rakenneosia pidetään vastaavina:

Logiikkajärjestelmät	Ohjelmointikielet
lausunto	Tyyppi
Todiste lausunnosta $P$	Termi (lauseke) tyyppi $P$
Väite on todistettavissa $P$	Tyyppi asuttu $P$
seuraamus $P\Rightarrow Q$	toiminnallinen tyyppi $P\rightarrow Q$
Yhteys $P\land Q$	Taideteoksen tyyppi (pareja) $P\times Q$
Disjunktio $P\lor Q$	Summatyyppi (syrjitty liitto) $P+Q$
Todellinen kaava	yksi tyyppi
Väärä kaava	Tyhjä tyyppi ( ) $\bot$
Universaali kvantori $\kaikille$	Riippuva tuotetyyppi ( -tyyppi) $\Pi$
Olemassaolon kvantori $\olemassa$	Riippuva summatyyppi ( -tyyppi) $\Sigma$

Yksinkertaisin esimerkki Curry-Howard-vastaavuudesta on isomorfismi yksinkertaisen tyypin λ-laskennan ja intuitionistisen lauselogiikan välillä , joka sisältää vain implikaatiot . Esimerkiksi tyyppi yksinkertaisessa kirjoitetussa lambda-laskennassa vastaa propositionaalisen logiikan ehdotusta. Tämän väitteen todistamiseksi on tarpeen rakentaa tietyn tyyppinen termi (jos tämä voidaan tehdä, he sanovat tyypistä, että se on asuttu tai asuttu ), tässä tapauksessa voit esittää halutun termin: , ja tämä tarkoittaa, että tautologia on todistettu. $(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))$

Curry-Howard-isomorfismin käyttö on mahdollistanut kokonaisen luokan toiminnallisten ohjelmointikielien luomisen, joiden ajonaikainen ympäristö on myös automaattinen todistusjärjestelmä , kuten Coq , Agda ja Epigram .

Muistiinpanot

↑ Curry, HB, Feys, R. Combinatory Logic Voi. I. - Amsterdam : Pohjois-Hollanti , 1958.
↑ Howard, WA The formulae-as-types concept of construction // To HB Curry: Essays on Combinatory Logic, Lambda Calculus and formalism. - Boston: Academic Press , 1980. - s. 479-490 .

Kirjallisuus

Pierce, Benjamin C. Tyypit ja ohjelmointikielet. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Käännös venäjäksi: Pierce B. Tyypit ohjelmointikielillä. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .