Curry-Howardi vastavus

Curry-Howardi vastavus ehk Curry-Howardi isomorfism on informaatikas ja matemaatilise loogika tõestusteooria valdkonnas otsene seos arvutiprogrammide ja matemaatiliste tõestuste vahel. Nimelt on see tähelepanek, et mõisted informaatikas on üksüheses vastavuses mõistetega matemaatilises loogikas.

See on üldistus süntaktilisest analoogiast formaalloogika ja arvutusmudelite vahel, mida kirjeldasid esmakordselt matemaatik Haskell Curry ja loogik William Alvin Howard.Vastavuse olemasolu tegi esmakordselt selgeks . Näiteks sektsioon 4.6, lk. 53 Gert Smolka and Jan Schwinghammer (2007-8), Lecture Notes in Semantics Idee on seotud ühe intuistionistliku loogika tõlgendusega, mida on kirjeldanud ka mitmetes formuleeringutes L. E. J. Brouwer, Arend Heyting ja Andrei Kolmogorov (nimelt Brouweri-Heytingi-Kolmogorovi tõlgendus)Brouwer–Heyting–Kolmogorovi tõlgendust kutsutakse ka "tõestusetõlgenduseks": lk. 161 Juliette Kennedy, Roman Kossak, eds. 2011. Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies  ning Stephen Kleene. Kui kaasata kategooriateooria vastavuse kolmandaks liikmeks, lisatakse sellele ka Joachim Lambeki nimi.

 Alged, ulatus ja tagajärjed 
Curry-Howardi vastavus tuleneb mitmest tähelepanekust:

 1934. aastal pani Curry tähele samasusi kombinaatorloogika ja intuitsionistliku loogika vahel.
 1958. aastal pani ta tähele samasusi kombinaatorloogika ja Hilberti stiilis deduktsioonisüsteemide vahel.
 1969. aastal pani Howard tähele, et üht kõrgetasemelist tõestussüsteemi võib intuitsionistlikult tõlgendada otseselt kui lambda-arvutust.

Curry-Howardi vastavus on tähelepanek, et tõestussüsteemide ja arvutussüsteemide vahel eksisteerib isomorfism, ning see väidab, et neid kahte formalismide perekonda võib lugeda samasteks. Nõnda ilmneb üldistus, et tõestus on programm, ning valem, mida see tõestab, on selle programmi tüüp. See tähendab, et funktsiooni tagastusväärtuse tüüp on analoogne loogilisele teoreemile, hüpoteesid on analoogsed funktsiooni argumentidele, ning programm selle funktsiooni arvutamiseks on analoogne teoreemi tõestusele. See annab loogilise programmeerimise keeltele tugeva aluse: nimelt võib tõestuseid esitada kui programme (eriti kui lambda-terme), ning tõestuseid on võimalik käitada.

Läbi vastavuse sündisid mitmed teaduslikud avastused, sealhulgas uus klass formaalseid süsteeme, mis käituvad samaaegselt kui tõestussüsteemid ja tüübitud funktsionaalsed programmeerimiskeeled. Nende hulka kuuluvad Per Martin-Löfi intuitsionistlik tüübiteooria ja Thierry Coquandi konstruktsioonide arvutus. Nende süsteemide diskursuses on tõestused tavalised objektid, ning tõestuste omadused avalduvad samamoodi, nagu programmidel. Seda uurimisvaldkonda kutsutakse tavaliselt kaasaegseks tüübiteooriaks.

Need tüübitud lambda-arvutused on pannud aluse tõestusassistentide tarkvarale, milles on tõestusi võimalik programmidena formaliseerida, kontrollida ja käitada. Teises suunas on võimalik kasutada programmi, et luua tõestus, mis kinnitaks programmi korrektset toimimist ning loogilist täielikkust.

 Üldine formuleering 
Üldisemas formuleeringus viitab Curry-Howardi vastavus vastavusele formaalsete tõestussüsteemide ja arvutusmudelite tüübisüsteemide vahel. Tegelikkuses jaotub see kaheks erinevaks vastavuseks, millest üks eksisteerib valemite ja tüüpide tasemel, mis ei sõltu tõestussüsteemi ja arvutusmudeli valikust, ning teine eksisteerib tõestuste ja programmide tasemel, mis seevastu sõltub nende valikust.

Valemite ja tüüpide tasemel käitub implikatsioon nagu funktsioonitüüp, konjunktsioon nagu "korrutistüüp" (mida tuntakse kui ennik, struktuur, järjend, või sõltuvalt keelest mõne muu nimetuse all), disjunktsioon nagu summatüüp (mida tuntakse ka kui ühendit), väär valem nagu tühi tüüp ja tõene valem nagu ühiktüüp (mille ainus liige on nullobjekt). Kvantorid vastavad sõltuva tüübi funktsiooniruumile või korrutistele. Kokkuvõte üldisest formuleeringust on järgnevas tabelis:
Loogika poolProgrammeerimise pooltehetüüptõestustermtehe on tõenetüübil on elementtehe on väärtüübil pole elementeüldisuskvantorüldistatud korrutistüüp (Π-tüüp)olemasolukvantorüldistatud summatüüp (Σ-tüüp)implikatsioonfunktsioonitüüpkonjunktsioonkorrutistüüpdisjunktsioonsummatüüploogiline tõesus ⊤ühiktüüp või top tüüploogiline väärus ⊥tühi tüüp või bottom tüüp
Tõestussüsteemide ja arvutusmudelite tasemel näitab vastavus struktuuride samasust, esmalt Hilberti stiilis deduktsioonisüsteemi (ingl k Hilbert-style deduction system) ja kombinaatorloogika vahel, ning teisalt naturaalse deduktsiooni (ingl k natural deduction) ja lambda-arvutuse vahel. Naturaalse deduktsiooni ja lambda-arvutuse vahel on olemas järgnevad vastavused:
Loogika poolProgrammeerimise poolhüpoteesidvabad muutujadimplikatsiooni elimineerimine (modus ponens)aplikatsioonimplikatsiooni järeldamine alamtõestusestabstraktsioon

 Viited 

 Kirjandus 




 Välislingid 



Kategooria:Informaatika
Kategooria:Loogika