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.[1]
See on üldistus süntaktilisest analoogiast formaalloogika ja arvutusmudelite vahel, mida kirjeldasid esmakordselt matemaatik Haskell Curry ja loogik William Alvin Howard.[2] Idee on seotud ühe intuistionistliku loogika tõlgendusega, mida on kirjeldanud ka mitmetes formuleeringutes L. E. J. Brouwer, Arend Heyting ja Andrei Kolmogorov (nimelt Brouwer-Heyting-Kolmogorovi tõlgendus)[3] ning Stephen Kleene. Kui kaasata kategooriateooria vastavuse kolmandaks liikmeks, lisatakse sellele ka Joachim Lambeki nimi.[4][5][6]
Alged, ulatus ja tagajärjed
[muuda | muuda lähteteksti]Curry-Howardi vastavus tuleneb mitmest tähelepanekust:
- 1934. aastal pani Curry tähele samasusi kombinaatorloogika ja intuitsionistliku loogika vahel.[7]
- 1958. aastal pani ta tähele samasusi kombinaatorloogika ja Hilberti stiilis deduktsioonisüsteemide vahel.[8]
- 1969. aastal pani Howard tähele, et üht kõrgetasemelist tõestussüsteemi võib intuitsionistlikult tõlgendada otseselt kui lambda-arvutust.[9]
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
[muuda | muuda lähteteksti]Ü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 pool | Programmeerimise pool |
|---|---|
| üldisuskvantor | üldistatud korrutistüüp (Π-tüüp) |
| olemasolukvantor | üldistatud summatüüp (Σ-tüüp) |
| implikatsioon | funktsioonitüüp |
| konjunktsioon | korrutistüüp |
| disjunktsioon | summatüüp |
| tõene valem | ühiktüüp või top tüüp |
| väär valem | 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 pool | Programmeerimise pool |
|---|---|
| hüpoteesid | vabad muutujad |
| implikatsiooni elimineerimine (modus ponens) | aplikatsioon |
| implikatsiooni järeldamine alamtõestusest | abstraktsioon |
Viited
[muuda | muuda lähteteksti]- ↑ Apinis, Kalmer; Vene, Varmo (2023). "Interaktiivne teoreemitõestus" (PDF). Tartu Ülikool. Vaadatud 17. jaanuaril 2024.
- ↑ Vastavuse olemasolu tegi esmakordselt selgeks Howard 1980. Näiteks sektsioon 4.6, lk. 53 Gert Smolka and Jan Schwinghammer (2007-8), Lecture Notes in Semantics
- ↑ 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 ISBN 978-1-107-00804-5
- ↑ Casadio, Claudia; Scott, Philip J. (2021). Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer. Lk 184. ISBN 978-3-030-66545-6.
- ↑ Coecke, Bob; Kissinger, Aleks (2017). Picturing Quantum Processes. Cambridge University Press. Lk 82. ISBN 978-1-107-10422-8.
- ↑ "Computational trilogy". nLab. Vaadatud 29. oktoobril 2023.
- ↑ Curry 1934.
- ↑ Curry & Feys 1958.
- ↑ Howard 1980.
Kirjandus
[muuda | muuda lähteteksti]- Curry, H B (20. september 1934). "Functionality in Combinatory Logic". Proceedings of the National Academy of Sciences of the United States of America. 20 (11): 584–90. Bibcode:1934PNAS...20..584C. DOI:10.1073/pnas.20.11.584. ISSN 0027-8424. PMC 1076489. PMID 16577644.
- Curry, Haskell B; Feys, Robert (1958). Craig, William (toim). Combinatory Logic. Studies in Logic and the Foundations of Mathematics. Kd 1. North-Holland Publishing Company. LCCN a59001593; with two sections by Craig, William; see paragraph 9E
{{cite book}}: CS1 hooldus: postscript (link) - Howard, William A. (september 1980) [original paper manuscript from 1969], "The formulae-as-types notion of construction" (PDF), Seldin, Jonathan P.; Hindley, J. Roger (toim-d), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, lk 479–490, ISBN 978-0-12-349050-6
Välislingid
[muuda | muuda lähteteksti]- Apinis, Kalmer (2021). "LTAT.03.019 Funktsionaalprogrammeerimine: Curry-Howard'i vastavus" (PDF). Tartu Ülikool.
- Wadler, Philip. "Propositions as Types" (Ameerika inglise) – cit. via YouTube.