Eelmises peatükis nägime, et igale tüübisüsteemile vastab loogika. Nüüd uurime, mis on Idris 2 keelele vastav loogika ning kuidas selles tõestusi teha saab.
Tõestamise aluseks on puhtad, täielikud funktsioonid. Kui programmeerijale on antud võimalus jääda lõpmatusse tsükklisse või sulgeda programm erindiga, siis pole meil vajalikku garantiid, et eeldusest järeldub järeldus. See on ka põhjus, miks paljusid praktilisi programmeerimiskeeli ei saa kasutada tõestamiseks. Seevastu, Idris toetab puhtaid ja täielikke funktsioone.
Suurim erinevus Curry-Howardi vastavuse teoreetilise käsitluse ja selle rakendusel Idrises on kontekstide käsituluses. Teoorias saime kontekstide üle ise otsustada defineerides oma suva järgi kontekstidega tegelevaid reegleid. Idrises on kontekste muutvad reeglid sisse-ehitatud ja järgnevate reeglite lisamine käib viisil, kus kontekstid ei muutu.
Esmalt vaatame sisseehitatud reegleid, kus otsustes on kontekstid. Need reeglid on Idrise loogika peamiseks tööriistaks – funktsioonitüüp a -> b ehk täpsemalt (x : a) -> b.
Funktsioonitüübile vastab loogikas implikatsioon. Sõltuvaid tüüpe võimaldavale funktsioonitüübile (x : a) -> b vastab aga hoopis predikaatloogika üldsuskvantor ∀ x∈ A. B
Üldsuskvantori väljaviimise ehk funktsioonirakenduse reegel, nimetame seda näiteks E→, võtab avaldised f : (x: a) -> b ja e : a ning järeldab nendest f e : b[x->e]. Seda kõike iga konteksti Γ jaoks.
Idrises pole sellel reeglil tegelikut eraldi nime — saame sellele viidata kui funktsioonirakenduse termile f e vastavale reeglile.
Teine sisseehitatud reegel on üldsuskvantori ehk funktsiooni sissetoomise reegel, mida võime nimetada I→. Reeglist näeme, kuidas skoobis olevad funktsiooniparameetrid koos oma tüüpidega satuvad konteksti.
Ülejäänud sisulised reeglid saame luua andmestruktuuride loomise abil, kus sissetoomise reeglid tulevad konstruktorite tüübist ja väljaviimise reeglid vastava struktuuri mustrisobitusest.
Nägime, et loogikareeglitel on eeldused ja järeldus. Ning ka seda, et (mitme parameetriga) funktsioonil on eeldus(ed) ja järeldus. Seetõttu võime tänu sellele reeglile funktsioonist f tüübiga T1 → T2 → … → Tn → Tr mõelda kui reeglist
ehk
Järgnevalt vaatame, kuidas defineerida konnektiivid: konjunktsioon, disjunktsioon, tõesus, väärsus ja eituse. Samas tuletame meelde, mis tüüpi väärtusi defineerivad andmestruktuurid nagu paarid, tüüpide summad jne.
Konjunktsiooni defineerimiseks andmestruktuurina, peame konstruktoriks võtma konjunktsiooni sissetoomise reegli. Väljaviimise reeglile vastav tõestus tuleneb mustrisobituse avaldisest.
Pane tähele, et loodud konjunktsiooni andmestruktuurile on sisuliselt sama mis paari andmestruktuur Idrise standardteegis.
Disjunktsiooni defineerimiseks andmestruktuurina, peame konstruktoriks võtma mõlemad disjunktsiooni sissetoomise reeglid. Väljaviimise reeglile vastav tõestus tuleneb jälle mustrisobituse avaldisest.
Pane tähele, et loodud konjunktsiooni andmestruktuurile on sisuliselt sama mis Idrise standardteegis olev Either.
Tõesuse ja vääruse saame sammuti ise defineerida. Aga ka need on juba Idrise standardteegis olemas. Tõesusele vastab tüüp Unit ehk (), millel on konstruktor MkUnit ehk (). Väärusele vastab tüüp Void, millel konstruktorid puuduvad. Tüübil Void on aga vääruse väljaviimisele vastav funktsioon absurdity.
Nagu konstruktiivsele loogikas tavaks, saab eituse konnektiivi defineerida läbi implikatsiooni väärusesse. Seega oleme katnud lausearvutuse osa. Aga nägime ka, et väärtusest sõltuv funktsioonitüüp on üldsuskvantor. See tähendab, et predikaatloogikast on puudu vaid olemasolukvantor. Selline struktuur on standardteegi moodulis Data.DPair.
Näiteks saame võtta väite, et leiduvad viiest suuremad naturaalarvud. Sellist väidet kodeerib näiteks Idrise tüüp
Exists (\ x: Nat. x>5 = True). Selle väite tõestamiseks peame pakkuma välja mingi arvu y ja siis näitama, et kehtib y>5 = True. Näiteks on sobiv arv 6 ja sellele vastav tõestus Refl. Ehk saame kirjutada järgnevalt.
| 1bigNum : Exists (\x:Nat => x>5 = True) 2bigNum = Evidence 6 Refl |
Esiteks paneme tähele, et jällegi on sarnasus paaridega: tüübil on üks konstruktor, millel on kaks argumenti. Lisaks, andmestruktuuril on väljad fst ja snd. Aga erinevalt tavalistest paaridest on tegemist sõltuvate paaridega, kus paari esimese komponendi valik kitsendab, mida teise komponendina saab kasutada. Selliseid sõltuvaid paare saame kasutada ka paaride implementatsioonina. Vaata järgmist koodilõiku.
| 1myPair : Type -> Type -> Type 2myPair a b = Exists (\x:a => b) 3 4test : myPair Char String 5test = Evidence 'x' "Hello!" |
Seega, kui tingimus parameetrist ei sõltu, saame tavalise paari. Siiski leidub erinevus paaride ja selle olemasolukvantori implementatsiooni vahel. Nimelt, Exists on mõeldud tõestuste kirjutamiseks ja seetõttu on paari esimene komponenti lubatud kasutada vaid tüübikontrolli ajal. Programmi käivitamise ajaks on paari esimese komponent unustatud.
| Main> test.snd "Hello!" Main> test.fst Error: ... |