Peatükk 16 Curry-Howard vastavus λ-arvutuses

Funktsionaalsete programmide ja matemaatiliste tõestuste vahelist seost kutsutakse Haskell Curry ja William Alvin Howardi järgi Curry-Howard’i vastavuseks. Vastavus tuleneb struktuursetest sarnasusest formaalsete loogikate ja tüübisüsteemi abil kirja pandud arvutusmudelite vahel.

Hiljem vaatame, mida saame üle kanda programmeerimisest loogikasse ja loogikast programmeerimisse.

Oleme juba vaadanud üht näidet tüübisüsteemist: lihtsalt tüübitud λ-arvutust. Nüüd vaatame lausearvutust ja paneme tähele sarnasusi tüübisüsteemiga. Sarnased lauserarvutuse definitsioonid on olnud Tartu Ülikooli kursustes Loogika arvutiteaduses ja Diskreetne matemaatika I.

Loomuliku tuletuse iga konnektiiviga (∧, ∨, ⊃, …) on seotud kaht liiki reegleid: sissetoomise reeglid ja väljaviimise reeglid. Sissetoomise reeglites esineb konnektiiv järelduses ja vastab küsimusele: ”kuidas näidata konnektiiviga väite tõesust”. Väljaviimise reeglid esineb konnektiiv eelduses ja vastab küsimusele: ”kuidas kasutada konnektiiviga väidet”.

Gentzen-i stiilis loomulikus tuletuses kasutatakse otsusteks sekventse on kujul: Γ ⊢ P, kus P on loogika valem ja Γ on kontekst ehk (kohalike) hüpoteeside hulk.

Sõltumata valemist kehtib hüpoteesi aksioom, mis ütleb et kontekstis olevad väited on tõesed. Pane tähele, tegemist on lihtsa tautoloogiaga: kui eeldame P, siis saame väita P.

Tihti algab arutelu küsimusega, kas valem P kehtib ilma hüpoteesideta ehk tühjas kontekstis. S.t. proovime tõestada väidet  ⊢ P.

Edasi näitame vajalike konnektiivide (P ⊃ P ∣ P ∧ P ∣ P ∨ P ∣ ⊤ ∣ ⊥ ∣ ¬ P) sissetoomise ja väljaviimise reegleid. Alustame implikatsiooniga P ⊃ P.

Tuletusreegleid saab lugeda alt-üles kui ka ülevalt-alla. Kumb lugemise viis intuitiivsem tundub, on enamasti subjektiivne. Näiteks alt-üles: selleks, et näidata implikatsiooni P₁ ⊃ P₂ kehtimist kontekstis Γ, piisab näidata valemi P₂ kehtimist kontekstis Γ, P₁. Või siis ülevalt-alla: kui kehtib väide P₂ kontekstis Γ, P₁, siis kehtib implikatsioon P₁ ⊃ P₂ kontekstis Γ. Seega, alati on võimalik reegel tekstis formuleerida mõlemat pidi ja edaspidi me õpikus ei kirjuta mõlemat versiooni välja. Seega, implikatsiooni väljaviimise reegel väidab, et kui kehtivad nii implikatsioon P₁ ⊃ P₂ ja valem P₁ kontekstis Γ, siis kehtib ka valem P₂ kontektis kamma.

Sarnaselt implikatsioonile saab anda reeglid konjunktsiooni ja disjunktsiooni jaoks.

Pange tähele, et konjunktsioon ja disjunktsioon on mingis mõttes duaalsed: konjunktsioonil kaks väljaviimise reeglit on sarnased disjunktsiooni sissetoomise reeglitega, kui vahetada eeldused ja järeldused.

Samasugune sarnasus on tegelikult ka konjunktsiooni sissetoomise ja disjunktsiooni väljaviimise reegli vahel. Kuna aga järeldusi võib olla vaid üks, siis tuleb disjunktsiooni väljaviimise reegli jaoks teha lisatööd: kahe järelduse asemel tuleb eeldada, et mõlemast järeldusest järeldub omakorda ühine P₀.

Järgmisena vaatame tüüpimisreegleid samaselt tõese väite ⊤ ja samaselt väära väite ⊥ kohta. Samaselt tõesel väitel ⊤ on ainult sissetoomise reegel ja samaselt vääral ⊥vaid väljaviimise reegel. Seetõttu, väidet ⊤ on sissetoomise reegilga triviaalne tõestada aga väidet ⊥ ei ole võimalik tõestada, kuna sissetoomise reeglit ei olegi.

Pane tähele, et samaselt tõesel väitel pole väljaviimise reeglit. Seda polegi vaja, kuna hüpotees ⊤ ei kanna mingit informatsiooni ja seega samaselt tõesusest järeldamine ei anna midagi juurde. Mingit kasu me selise reegli lisamisest ei saaks.

Seevastu, kõige huvitavam nendest reeglitest on vääruse väljaviimine. Kui me oleme jõudnud sellisesse absurdsesse olukorda, kus kontekstis Γ on tõestatav ⊥, siis on kontekstis Γ kõik väited P tõestatavad.

Kasutades väärust ⊥ saame defineerida eituse süntaktilise suhkruna kui ¬ P ≡ P ⊃ ⊥.

Kirjeldatud reeglid annavad intuitsionistliku lausearvutuse IPC. Sõna intuitsionistlik tähendab loogikas seda, et loogika tuleneb konstruktiivsest mõttetegevusest ja mitte objektiivse reaalsuse reeglite avastamisest. Ehk siis tõde on vaid see, mida me saame tõestada. Me ei saa maailmas avastada tõde — ei saa juhtuda olukorda, et mingi asi on tõde aga me ei saa aru, miks see on tõde.

Intuitsionistlikule loogikale vastandub nn. klassikaline loogika, kus kehtib reegel, et iga väide on kas tõene või väär. Seda nimetatakse ka välistatud kolmanda reegliks. Ehk siis klassikalises loogikas kehtib väide A∨ ¬ A. Sama väide ei kehti intuitsionistlikus loogikas, kui me ei tea, kas väide A on tõene või mitte.

Klassikalise loogika saame, kui IPC reeglitele lisame välistatud kolmanda reegeli või sellele samaväärse kahekordse eituse elimineerimise reegeli.

Järgnevalt tõestame, et välistatud kolmanda reeglit kasutades saame tõestada kahekordse eituse elimineerimise. Selleks piisab näidata, et kehtib ¬¬ A⊢ A ilma reeglit E^¬¬ kasutamata. Järgneb tõestuspuu.

Järgnevalt tõestame, et kahekordse eituse elimineerimist kasutades saame tõestada välistatud kolmanda reeglit. Selleks piisab näidata, et kehtib ⊢ A∨ ¬ A ilma reeglit EM kasutamata.

Paneme tähele süntaktilisi sarnasusi vastavate konstruktsioonide ja reeglite vahel. Näiteks Abs ja I^⊂ reeglid, App ja E^⊂ reeglid ning Var ja Hyp reeglid. Kusjuures, loogikas pole “programm” (alati) ilmutatud kujul välja toodud, aga saame selle rekonstrueerida tõestuspuu järgi. Ehk näeme, et implikatsioonile loogikas vastab funktsioonitüüp tüübitud λ-arvutuses.

Sarnaselt eelnevatele vastab konjunktsioonile tüüpide korrutis (ehk paar), disjunktsioonile tüüpide summa ning tõesusele ühiktüüp. Väärusele vastavat konstruktsiooni me veel defineerinud ei ole aga konstantide abil saame defineerida tüübi False ja konstandid absurd_A : False → A iga tüübi A jaoks. Pane tähele, et kuna tüübi False jaoks konstruktoreid pole, siis sellist tüüpi väärtust teha võimalik ei ole.

Millest tuleneb aga erinevus, et loogikas pole “programme” aga λ-arvutuses on? Korrektselt tüübitud termid lihtsalt tüübitud λ-arvutuses vastavad tüübikontrolli puule. Seega, miks pole loogikas puule vastavat kodeeringut? Vastus: kuna programmis on tähtis, kumb parameeter tagastada, kuid loogikas pole tähtsust kumma eelduse põhjal midagi järeldatakse. Aga tehniliselt saame loogikat siltidega täiendada — jälgimaks, millisest implikatsioonist aksioom tuleneb.

Järgmisena vaatame, mis on reduktsioonile vastav mehhanism. Meenutame, et β-reduktsiooni reegel oli (λx : τ. e₁) e₂ →_β e₁[x→e₂]. Ehk siis viime implikatsiooni välja kohe peale selle sisse toomist. Saame järgneva sammu loogikas.

Paneme tähele, et Γ, P₁ ⊢ P₂ tõestuses saame teha kõike mis Γ ⊢ P₂ ning lisaks kasutada hüpoteese Γ, P₁, Γ′ ⊢ P₁ iga Γ′ jaoks. Aga kuna näeme puus Σ, et P₁ tõestamiseks piisab kontekstist Γ, siis saab seda tõestada ka kontekstis Γ, Γ′. Seega kui meil on vasakule puule vastav tõestuspuu, siis saame selle abil genereerida valiidse paremale puule vastava tõestuspuu.

Sarnaselt implikatsiooni sissetoomise ja kohese väljaviimise redutseerimisele (β-reduktsiooni vaste) saame defineerida teiste konnektiivide sissetoomise ja väljaviimise reduktsioonid (δ-reduktsioonide vasted). Näiteks toome vaid konjunktsiooni vasaku väljaviimise reeglile vastava redutkstiooni

Kokkuvõtteks paistab, et tüübisüsteemidel ja loogikatel pole sisulisi erinevusi – see ongi Curry-Howard’i vastavus. Vaata järgnevat tabelit.

See tähendab, et iga loogika on tüübisüsteemina kirja pandud arvutusmudel ja iga tüübisüsteemina kirja pandud arvutusmudel on loogika. Meelde tuleb aga jätta, et mitte iga kirjapandav loogika ega arvutusmudel pole kasulik. Järgnevalt vaatamegi neid mittekasulikke juhte.

Näiteks võib tüübisüsteem olla selline, et ainsaks baastüübiks on *. Tulemuseks on tüübisüsteem, mis väga suures osas vastab tüüpimata λ-arvutusele, kus välistatakse vaid olukorrad, kus rakenduse funktsioonikomponent pole tegelikult funktsioon. Sellist tüübisüsteemi tähistatakse näiteks λ_*^→ või ka λ^τ. Kuigi tüübisüsteem võib olla praktikas kasuliks, siis ei ole selle abil võimalik kodeerida huvitavaid väiteid ega nende tõestusi. Ehk, kõik kirjapandavad väited on triviaalselt tõestatavad.

Järgmine näide on tüübisüsteemist, millel on sisseeehitatud püsipunktikombinaator. Seega suvalise tüübi jaoks saame luua mittetermineeruva vastavat tüüpi programmi. Kuigi programmeerijad on sellega rahul siis loogikud ei aktsepteeri lõpmatuid või mittetermineeruvaid tõestusi.

Loogikud kirtsutavad nina ka praktiliste tüübisüsteemide, nagu näiteks Java, peale. Need tüübisüsteemid on põhjendamatult keerukad loogikana kasutamiseks.

Aga võime vaadata ka teises suunas. Klassikaline loogika (näiteks klassikaline predikaatloogika) on kasutuses ja mitmete probleemide lahendamiseks täiesti sobilik tööriist. Samas, sellele vastavas tüübisüsteemis pole kolmanda välistava reeglile (või topelt eituse elimineerimise reeglile) vastavat funktsiooni definitsiooni — reduktsioon sellises süsteemis jääb kinni.

Viimase näitena võtame relevantsusloogikaid, kus on lubatud vaid implikatsioonid a⊃ b kui b tõestamiseks läheb a-d vaja. Selline nõue on aga programmeerijatele enamasti liiga kitsendav, kuna pole, näiteks, tüübidav funktsioon λx y. x.