Peatükk 9 Andmestruktuurid puhtas λ-arvutuses

Eelnevalt nägime, kuidas arvutada konstantidega λ-arvutuses, kus konstantideks võtsime tõeväärtused, täisarvud, paarid ja listid. Nüüd vaatame, kuidas defineerida tõeväärtused, naturaalarvud, paarid ja listid kasutades puhast λ-arvutust. See tähendab, et teoreetilises lähenemises võime konstante ja δ-reduktsioone ignoreerida.

Definitsioonideks valime kombinaatorid: ilma vabade muutujateta termid, mis on normaalkujul. Nii käituvad meie definitsioonid sarnaselt konstantidele — ei tekita juurde vabu muutujaid ega redutseeru selliselt, et me neid ära ei tunne. Tegelikult on võimalik kõik abstraktsioonid kirjeldada S, K ja I kombinaatoritega.

Tõeväärtuste spetsifikatsiooniks võtame tõeväärtuste funktsioonide δ-reduktsioonid, leiame konstantidele vastavad λ-termid ja näitame, et δ-reduktsiooni asemel saame teha β-reduktsioone ja saada sama tulemuse.

9.1 Tõeväärtuste implementatsioon

Tõeväärtuste operatsioonid on spetsifitseeritud järgnevalt.

Sobivate definitsioonide leidmiseks kasutame järgnevat strateegiat: väärtuseks võtame vastava väärtuse mustrisobituse operatsiooni. Tõeväärtuse true mustrisobitus ehk tingimuslause võtab kaks parameetrit, e₁ ja e₂, ning tagastab e₁. Seega võtame true := λ x y.  x. Sarnase argumentatsiooniga võtame false := λ x y.  y. Muud operatsioonid saame programmeerida kasutades teadmist, et tõeväärtused on nendele vastavad tingimuslaused.

Saame näidata, et δ-reduktsioonile vastab mitmesammuline β-reduktsioon.

9.2 Paaride implementatsioon

Paaride operatsioonid on spetsifitseeritud järgnevalt.

Definitsioonide leidmise strateegia on sama mis tõeväärtuste puhul — leiame mustrisobitusele vastava termi. Idrises saab paaride mustrisobitust teostada avaldisega ⁠match MkPair e_1 e_2 with MkPair x y => p. Seega λ-arvutuses võime võtta näiteks pair = λ e₁ e₂ p. p e₁ e₂. Ehk siis paari komponendid antakse ainukesele harule edasi eraldi parameetritena. Siis fst ja snd saame impmeneteerida kasutades mustrisobitus järgnevalt.

Nüüd saame näidata definitsioonide vastavust spetsifikatsioonile.

9.3 Naturaalarvud

Natutaalarvude kohta nõuame, et succ , pred , iszero , add ja mul arvutaks vastavalt järgmise arvu, eelmise arvu, arvu võrdumise nulliga, liitmise ja korrutamise.

Esmalt püüame ehitada nii, et nulli esitab identsusfunktsioon λ x. x ja nullist suuremad arve paarid, mille esimene komponent on false ja teine on ühe võrra väiksem number. Nii on arvude struktuur sarnane Idrise struktuurile aga lisatud on false komponendid. Sellist konstruktsiooni nimetatakse standardnumbriteks.

Saame näidata, et succ , pred ja iszero töötavad korrektselt. Näeme, et pred töötab vaid nullist suuremate arvude korral.

Kui makrode defineerimisel oleks rekursioon lubatud, saaks standardnumbrite liitmise defineerida kui add := λ x y. cond  (iszero  x) y (add  (pred  x)(succ  y)). Hiljem, peatükis 9.5, näeme ühte võimalust, kuidas rekursiooniga hakkama saada. Enne aga vaatame ühte alternatiivset lähenemist — Churchi numbreid.

Numbrite defineerimiseks kasutame funktsiooni termide astendamise notatsiooni. Termide E, E∈ Λ jaoks Eⁿ E′ rakendab funktsiooni E n-korda, alustades argumendist E′. Ehk E⁰ E′ = E′, E¹ E′ = E E′, E² E′ = E (E E′) , E³ E′ = E (E (E E′)) jne. Nüüd saame defineerida Churchi numbrid.

Churchi numbrite intuitsioon on, et arv n tähistab mingi valitud operatsiooni n-kordset tegemist — arv vastab sellele, mitu iteratsiooni tuleb teha. Arvule ühe lisamine tähendab ühe iteratsiooni lisamist. Nulliga võrdumist saab kontrollida nii, et algseisuks võetakse true ja tsüklis muudetakse see false -ks; nulli iteratsiooni puhul jääb seisundiks true ja rohkemate iteratsioonide puhul on tulemus false . Vaata formaalseid β-reduktsioone.

Liitmise, korrutamise ja isegi astendamise saame defineerida järgnevalt. Pane tähele, et astendamise definitsiooni saaks kirjutada veel lühemalt: exp = λ m n. n m.

Vaatame, kuidas term add  m n β-redutseerub naturaalarvude m ja n summaks. Intuitiivselt, kõigepealt tehakse n iteratsiooni ja seejärel veel m iteratsiooni. Korrutamise korrektsuse verifitseerimiseks peame veenduma, et (λ x. fⁿ x )^m x on tõesti sama kui f^mn x. Ehk, intuitiivselt m korda tehakse n iteratsiooni.

Churchi numbrite puhul on keeruliseks ülesandeks hoopis ühe lahutamine. Intuitiivselt, kui meil on arv n ja me saame teha n iteratsiooni aga soovime teha n−1 iteratsiooni. Selle probleemile on kaks standardset lahendust. Esiteks vaatame lahendust, kus meil intuitiivselt on iteratsioonis lisamuutuja — tõeväärtus, mis ütleb, kas me oleme juba ühe maha lahutanud. Vajame abifunktsiooni, mis käituks järgnevalt.

Sellist spetsifikatsiooni rahuldab järgmine definitsioon.

Reduktsiooni (prefn f)ⁿ (false,x) ↠ (false,fⁿ x) tõestame induktsiooniga üle naturaalarvu n. Vaatame baasjuhtu n=0 ja induktsiooni sammu n=n′+1.

Siis saame defineerida eelmise arvu leidmise operaatori pred .

Seega oleme andnud ühe naturaalarvude implementatsiooni kasutades paari ja tõeväärtust. Teine variant on implementeerida viivitus naturaalarvude paariga, mille mõlemad komponendid on alguses nullid. Iga iteratsioon kopeerib paari teise komponendi esimeseks ja suurendab teiset komponenti ühe võrra — nii on paari esimene komponent alati peale esimest iteratsiooni ühe võrra väiksem. Peale iteratsioone tagastatakse paari esimene komponent.

Esmalt tõestamie induktsiooniga, et f-i n-kordsel rakendamisel paarile pair  m m+1 on tulemuseks (pair  m+n m+n+1). Induktsiooni baas kehtib triviaalselt kuna f⁰ (pair  m m+1) = pair  m m+1. Induktsiooni sammu kehtivust tõestab järgnev reduktsioon.

Nüüd saame hõlpsasti näidata, et pred  0 redutseerub väärtuseks 0 ja pred  n+1 redutseerub väärtuseks n.

9.4 Listid

Listide kohta on jägnevad δ-reduktsioonireegild.

Sarnaselt naturaalarvudele, on siin võimalik kaks lähenemist. Esiteks võime lähtuda listi mingist fold-funktsioonist ja implementeerida null, hd ja tl kasutades seda fold-i. Teine võimalus oleks kasutada paare ja tõeväärtueseid — teades ette, et fold-i puudumisel on paljude funktsioonide implementeerimiseks vaja rekursioon.

Vaatame esmalt põgusalt listide implementatsiooni, mis on tuletatud listide foldr funktsioonist.

Nüüd saame implementeerida konstandid null ja hd.

Listi saba leidmine kasutades fold funktsioone on võimalik aga parajalt tülikas. Definitsioonid tulevad pikad ja korrektsuse näitamine võtab palju samme. Seetõttu piirdume siin Idrise koodiga, mis arvutavad listi saba kasutade ⁠foldr või ⁠foldl.

Teine võimalus listifunktsioone defineerida on läbi paaride ja tõeväärtuste.

Nüüd saame näidata, et meie definitsioonid vastavad spetsifikatsioonile kasutades β-reduktsiooni.

Sellised definitsioonid ei võimalda meil aga defineerida rekursiivset foldr funktsiooni. Järgmisena vaatamegi, kuidas toetada rekursiivset käitumist.

9.5 Püsipunktid

Termi M nimetatakse püsipunktikombinaatoriks kui kehtib

Tuntuim püsipunktikombinaator on Haskell Curry “paradoksaalne” kombinaator

Saame näidata, et Y on püsipunktikombinaator.

Pane tähele, et tõestuse viimase sammuna tuleb β-ekspansioon, mitte β-reduktsioon. Seetõttu on mõnevõrra raskendatud Y e-ks ekspandeerutava termi äratundmine suurema termi sees — kui meil oleks mingi konkreetne term e. Seetõttu võib olla kasulik kasutada hoopis “tugevat” püsipunkti kombinaatorit Θ.

Kombinaatori Θ kohta saame tõestada tugevama väite, et Θ e  →_β  e (Θ e).

Püsipunktikombinaatoreid saab kasutada rekursiivsete funktsioonide defineerimiseks. Võtame näiteks standardnumbrite (naturaalarvude) liitmise. Rekursiivse väljakutse jaoks lisame definitsiooni esimese parameetri ja rakendame funktsiooni püsipunktikombinaatorile.

Tõestame näiteks ka liitmise korrektsust, s.t, et add m n redutseerub avaldiseks m+n. Tõestuseks kasutame induktsiooni ja alustame baasjuhust m=0, kus kasutame add-i definitsiooni järel püsipunktikombinaatori võrdust Y f =_β f (Y f), teadmist iszero 0 ↠_β true ja cond true e₁ e₂ ↠_β e₁.

Jätkame induktsiooni sammu m=m′+1 tõestusega, kus kasutame add-i definitsiooni järel püsipunktikombinaatori võrdust Y f =_β f (Y f), teadmist iszero m+1 ↠_β false , teadmist pred m+1 ↠_β m, teadmist succ n ↠_β n+1, teadmist cond false e₁ e₂ ↠_β e₂ ning induktsiooni hüpoteesi ∀ k, add m k ↠_β m+k.

Sarnaselt liitmisoperatsioonile add saame kõik rekursiivsed definitsioonid kirjutada mitterekursiivselt, kasutades mõnda püsipunktioperaatorit. Üldine muster on, et funktsioonile tuleb lisada esimene parameeter ja sellega asendada kõik rekursiivsed väljakutsed. Nii saame funktsiooni, mis töötab soovitud viisil kuni rekursiivse väljakutseni. Kuidas aga anda funktsioonile see esimene argument? Seda teeb püsipunktioperaator. Ehk kui soovime defineerida funktsiooni, mis käitub nagu võrdus f = λx y z. … (f a b c) … siis piisab meil see defineerida mitterekursiivse makrona f := Y (λf’ x y z. … (f’ a b c) …).