Previous Up Next

Peatükk 13 λ-termide efektiivne väärtustamine

Redutseerimine on lihtne ja lühike viis väärtustamise defineerimiseks λ-arvutuses. Saame koostada Danvy-stiilis sikk-sakk diagrammi, kuidas redutseerub t0t1, t1t2 jne. Iga iteratsiooni samm jaotatakse term reedeksiks ja kontekstiks. Siis term redutseeritakase ja pannakse tagasi konteksti.

Redutseerimine on praktikas resursimahukas, kuna peame tegelema suurtest termidest otsimise ja nende kopeerimisega. Parem oleks, kui me ei peaks igal sammul termi tagasi kokku panema, vaid saaks leida otse uue reedeksi ja konteksti. Sellist sammu nimetatakse refokusseerimiseks.

Siinjuures on tähtis, et refokusseerimine oleks ka tegelikult efektiivsem kui termi koostamise ja uueks reedeksiks ja kontekstiks jagamise järjestrakendus. Kahjuks λ-termide struktuur ei võimalda väga efektiivset lahendust. Leidub aga alternatiivne formalism, kus redutseerimine ning ka refokuseerimine pole mitte ainult teoreetiliselt efektiivsed vaid selle efektiivsuses on lihtne intuitiivselt veenduda. Järgnevalt vaatamegi seda formalismi, milleks on virtuaalmasinad.

13.1 Virtuaalmasin LVM

Virtuaalmasinad on formalismid, mis väärtustavad efektiivset arvutamist kui λ-arvutus väärtustas lühidust ja omaduste selgust. Virtuaalmasinatel on rohkem komponente aga samas on iga virtuaalmasin samm tehtav konstantse ajaga. Vaatame järgnevalt virtuaalmasinat nimega LVM, mille väärtustaja ja väärtustamsie visualiseerija on saadaval aadressil https://bitbucket.org/kalmera/lvm/

Esmalt vaatame üldpilti ja siis defineerime kõik masina komponendid formaalselt. Suures pildis koosneb LVM definitsiooni järgi programmist P, milleks on instruktsioonide massiiv, ja seisundist S, ehk masina abistruktuuridest. Masin alustab algseisundist S0. Programm arvutuse ajal ei muutu.

Iga seisundi S puhul teame me, et järgmisena täidetav instruktsioon on P[S.pc]. Igas seisundis S saame suvalist instruktsiooni iI käivitada ja jõuda mingisse seisundisse S′. Masin on deterministlik, ehk masin kas alati peatub sellises seisundis või tagastab sama algseisu kohta alati sama lõppseisu. Instruktsiooni rakendamise osalist seost seisundite vahel tähistame Si S′. Järgnevalt defineerime virtuaalmasina täpselt.

Masina LVM seisundid koosnevad järgnevatest struktuuridest. Ehk seisund on viisik järgnevate komponentidega.

Programm saadakse programmiteksti (mis enamasti tuleb failist) parsimisel. Tavajuhul peaks programmi teksti iga instruktsioon olema koodis eraldi real. Lubatud on kasutada ka semikoolonit ‘;’ reavahetuse asemel. Näiteks on programmitekst “PUSH_INT 5; HALT”.

Koodis võivad olla siltide deklaratsioonid kujul “s:”, kus s on sildi nimi. Kui koodis on silt nimega s deklareeritud, siis võib s-i kasutada programmi kohtades, kus oodatakse arvu. Sellisel juhul tähistab s deklaratsioonile järgneva instruktsiooni numbrit. Näiteks programmi “PUSH_INT x; HALT; x: PUSH_INT x’ puhul on tähistab silt x arvu 2. Pane tähele, et silti võib kasutada nii enne kui ka peale selle deklaratsiooni.

Järgenvalt vaatame, mis instruktsioonid virtuaalmasinas leiduvad ja mida need instruktsioonid teevad.

Instruktsioon HALT peateab masina ja jätab seisundi muutmata. Praktikas saab arvutuse tulemuse kohta infot konsooli trükkida aga formaalselt jääb masin lihtsalt antud seisu kinni. Ehk, seisundit, mille järgmiseks seisuks on HALT saame lugeda masina lõppseisundiks. Enamasti loeme arvutust õnnestunuks, kui HALT-ini jõudes on raam ja kutsemagasin tühjad ning magasinis on täpselt üks väärtus — seda loemegi arvutuse tulemuseks. Kuidas aga väärtusi magasini saada?

Instruktsioonid PUSH_INT n, PUSH_BOOL b ja PUSH_NIL lisavad magasini peale vastavalt arvu n, tõeväärtuse b ja tühja listi. Nagu tavaliselt, suurendavad instruktsioonid progammiloendurit ühe võrra.

Funktsioonikutse sees sisaldab raam F funktsiooni argumente. Nende lükkamiseks magasini peale on instruktsuoon LOAD_ARGn, mis paneb magasini peale n-nda argumendi.

Täisarvude aritmeetika jaoks on näiteks instruktsioon ADD, mis võtab magasinist kaks arvu, liidab nad kokku ja paneb summa tagasi magasini peale. Sarnaselt on võimalik täisarve lahutada (instruktsioon SUB), korrutada (instruktsioon MUL), kontrollida täisarvude ning tõeväärtuste võrdsust (instruktsioon EQ) ja kontrollida, kas magasini teine arv on pealmisest arvust ragnelt väiksem (instruktsioon LT). Viimased kaks tekitavad magasini peale tõeväärtuse. Nagu tavaliselt, suurendavad instruktsioonid progammiloendurit ühe võrra.

Tõeväärtustega opereerimiseks on kolm instruktsiooni, mis vastavad konjunktsioonile (instruktsioon AND), disjunktsioonile (instruktsioon OR) ja eitusele (instruktsioon NOT). Need instruktsioonid eeldavad, et argumendid magasinis on tõeväärtused.

Magasiniga opereerimiseks on kolm instruktsiooni. Kahe pealmise magasini vahetamiseks on instruktsioon SWAP. Pealmiste magasini elementide eemaldamiseks on instruktsioon POP n. Pealmisest järgnevate elementide eemaldamiseks on instruktsioon SLIDE n.

Konstantse instruktsiooni juurde minemiseks on instruktsioon JUMPn. See kirjutab programmiloendi üle konstantse väärtusega n. Koodi genereerimisel kasutame argumendina silti, mis esitab sildi deklaratsioonile järgneva instruktsiooni numbrit.

Tingimusavaldiste implementeerimiseks on vaja hüpata vastavalt tingumusele. Selleks on LVM-is instruktsioon JUMP_IF_FALSEl. See instruktsioon on defineeritud kahe juhuga: a) kui magasini peal on “false”, siis hüüppame argumendiga defineeritud instruktsioonile, ja b) kui magasini peal on “true”, siis jätkame järgmise instruktsiooniga.

Nagu nägime instruktsioonist PUSH_NIL, tühi list on väärtus magasinis. Tühja listi äratudmiseks on instruktsioon IS_NIL, mis tühja listi puhul tagastab “true” ja muu väärtuse puhul “false’.

Mittetühja listi puhul on magasinis viit, millele vastab kuhjas paar, kus esimene komponenet on listi pea ja teine komponenet on listi saba. Pane tähele, et listi saba võib olla tühi list või omakorda aadress. Mittetühja listi loomiseks on instruktsioon CONS. Mittetühja listi pea võtmiseks HEAD ja saba võtmiseks TAIL.

Järgnevalt vaatame funtksioonikutsetega seotud instruktsioone. Funtksioonikutse jaoks on vaja kuhja luua arvutuse objekt ehk sulund. Selleks on instruktsioon MK_CLOSUREl, kus l on funktsiooni koodi esimene instruktsioon. Instruktsioon loob uue sulundi objekti funktsiooni sisenemise punkti ja tühja argumentide listiga ning jätab selle aadressi magasini peale.

Sulunditesse salvestatud raam leiab kasutust mitme argumendiga funktsioonide puhul või kui üks funktsioon tagastab omakorda funktsiooni. Nimelt, λ-arvutuses saab substitutsioon tagastada termi, kus on parameeter asendatud argumendiga abstraktsiooni all. Virtuaalmasinas tahame aga just vältida uute termide genereerimist. Seega, salvestame argumendid sulundisse, kuni kõik vajaminevad argumendid on koos et nendega midagi ette võtta.

Funktsiooni väljakutseks on vaja sulundist võtta funktsiooni koodi esimene instruktsioon ja argumentide massiiv ehk raam. Vana programmiloend (+1), raam ja argumentide arv magasinis tuleb panna kutsemagasini peale, et funktsiooni lõpus teaks kuhu tagasi tulla.

Lisaks on funktsiooni võimalik välja kutsuda ka instruktsiooni TAILCALLn abil. Ainuke erinevus tavalise CALL-ga on, et TAILCALL eeldab, et tegemist on juba kutsutud funktsiooni rekursiivse kutsega, mistõttu kutsemagasinis on juba väärtus. Seega, TAILCALL ei lisa kutsemagasinis uut väärtust vaid uuendab ainult argumentide arvu. See instruktsioon on kasulik rekursiivse funktsiooni rekursiivsel väljakutsel, kui tegemist on kutsega n.n. sabapositsioonis — ehk kutsele sisuliselt järgnev instruktsioon ongi RETURN.

Järgmine instruktsioon, mida vaadata, on TAKEn. See instruktsioon vastutab argumentide paigutamise eest: osa argumente on juba raami peal aga magasinis võib olla veel argumente lisaks. Instruktsioonil on seetõttu kaks juhtu: a) arvutuse alustamiseks on juba piisavalt argumente (>=n) või b) arvutuse jaoks ei ole veel piisavalt argumente (<n). Esimene variant on seega järgnev.

Kui argumente pole piisavalt (n<m+|F|), võime rakendada järgmist reeglit. Sellisel juhul tagastame uue sulundi, kuhu lisatakse olemasolevad argumendid, et selle rakendusel saaks puuduolevaid argumente oodata. Paneme tähele, et hüppame funktsioonikutsest tagasi ning jätame tagastusväärtusena magasini peale viida funktsiooni objektile.

Kui kutsutud funktsioon on valmis (ehk lisaargumente ei ole), võib ta instruktsiooni RETURN abil teda kutsunud funktsiooni tagasi hüpata. Ehk, PC ja raam ennistatakse kutsemagasini pealmisele väärtusele. Pane tähele, et see instruktsioon magasini ei muuda — virtuaalmasina kasutaja võib aga rakendada täiendavaid konventsioone, näiteks et funktsioon jätab oma tagastusväärtuse magasini peale.

Lisaks on variant, et magasinis on veel n lisaargumenti. See tähendab, et kutsutud funktsioon omakorda tagastab mingi funktsiooni ja sellele on sobilik anda veel lisaks argumente. Sellise juhul peame tagastamise asemel mingis mõttes jäljendama instruktusiooni TAILCALL 0 – teeme sabakutse ilma argumente juurde panemata.

Instruktsioonil RETURN on aga ka kolmas vorm, mida kasutatakse laisa väärtustamie jaoks, kui tahame vältida argumentide mitmekordset arvutamist. Aga enne laisa väärtustuse arvutusest tagasitulemist, vaatame, kuidas laisk arvutus genereeritakse ja kuidas see välja kutsutakse. Seega, esiteks on sarnaselt funktsiooni sulundile vaja luua väärtustamata avaldise objekt. Seda tehakse instruktsiooniga MK_THUNKl, mis salvestab raami ja väärtustamise esimese instruktsiooni THUNK objektiks

Vajame THUNK objekte, et nad oleks selgelt eristatavad muudest väärtustest — et kui aadress viitab THUNK-le siis ta on veel väärtustamata ja vastasel juhul on juba väärtustatud. Nii suudame hiljem vältida mitmekordseid arvutusi. Selline väärtustamine algab instruktsiooniga FORCE, mis erineb natuke CALL 0-st. Pane tähele, et kutsemagasini peale lisatakse nüüd nelik, kus viimane komponent on aadress arvutamata väätusele.

Kui aga magasini peal pole aadressi väärtustamata objektile, siis eeldatakse, et objekt on juba väärtustatud ja väärtus salvestatud viidatud aadressile. Sel juhul paneb FORCE magasini peale viidatud väärtuse.

Nüüd oleme siis valmis defineerima instruktsiooni RETURN kolmanda juhu, mis rakendub FORCE-ga kutsumiselt tagasipöördumisel. Ehk juhul, kui kutsemagasin peal on nelik. Sel juhul kirjutame selle kolmanda komponendi poolt viidatud aadressile magasini peal oleva (tagastus-)väärtuse.

13.2 λ-termi tõlkimine LVM programmiks

LVM disaini üks otsuseid oli, et funktsiooni defineerimisel alustame tühjast raamist. See tähendab sisuliselt, et vabade muutujate käsitlemine peab olema eksplitsiitne. Ehk siis, kutsuva funktsiooni raam ei lisata automaatselt kutsutava funktsiooni raamiga. Selline käitumine välistab ühe mälulekete allika, kus mälu ei saa vabastada, kuna sellele on viidatud (kutsemagasini salvestatud) raamis, kuigi selle väärtuseni ei vii ükski skoobis olev muutuja. Seetõttu ei pea mitte ainult kogu programm olema kinnine vaid ka kõik sisemised lambdad teha (öeldakse ka “tõsta”) kombinaatoriteks.

Kui programmis leidub (mitmeargumentiline) abstraktsioon (λ x1xn. e), kus leidub vaba muutuja zFVx1xn. e), siis (λ x1xn. e) tuleb programmis asendada termiga ((λ zx1xn. e) z). Nii saame kõik (mitmeargumentised) abstraktsiooid teisendada globaalseteks (mitmeargumentilisteks) funktsioonideks. Lisaks genereerime globaalsete funktsioonide jaoks unikaalsed nimed ja kasutame koodis vaid nimesid.

Lambda-tõstmise tulemusena saime originaalsest termist funktsioonide hulga F ja termi m, nii et funktsiooni kehades ja termis ei leidu λ-abstraktsioone — vaid ainult muutujaid, konstante ja funktsioonirakendusi.

13.2.1 Agar väärtustamine

Agara väärtustamise puhul, käib koodi genereerimine kahe funktsiooni abi. Esitesks funktsioon F, mis teisendab funktsiooni programmikoodiks. Teiseks, funktsioon T, mis teisendab termid programmiks, kasutades sõnastikku ρ. T eeldab, et funktsioonide sisenemiskohad on koodis tähistatud vastava funktsiooni nimelise sildiga. Seevastu sõnastik ρ seab igale funktsiooni parameetrile vastavusse arvu, mitmendal raami indeksil argument leidub.

Selliseid kompileerimise skeeme kirjutame pseudokoodis, kus programmitekst on sõne. Kasutame Pythonile sarnast stringide interpoleerimist, kus, näiteks sõne f“A{B}C” algab A-ga, lõpeb C-ga ja vahepeal on B väärtus (sõnena).

Lisaks kasutame konventsiooni, et kui skeemis on silt s defineeritud ja ka kasutatud, siis selle skeemi rakendamisel oma koodis tuleb selline silt teha unikaalseks. Näiteks kasutada s asemel s1, s2 jne. Silte me ei tee unikaalseks järgmisel juhul.

Funktsioonide kompileeritakse selliselt: esmalt defineeritakse silt funktsiooni nimega, siis TAKE instruktsioon ning seejärel kompileeritakse funktsiooni keha. Funktsiooni keha jaoks on vaja sõnastikku, mis seab vastabusse parameetri xi tema indeksiga i. Ehk, saame defineerida

F(fx1x2 … xn = e) := f{f}:          
 TAKE {n}         
 {T(e, ρ) }         
 RETURN         
          

kus ρ = ∪0<in{xii}.

Funktsiooni puhul kasutame MK_CLOSURE instruktsiooni, mille argumendiks silt funktsiooni nimega. Parameetri korral kasutame LOAD_ARG instruktsiooni, mille argumendiks ρ(x) ehk parameetri indeks. Funktsioonirakenduse puhul kasutame abifunktsiooni C, millel on lisaks parameeter n, mis tähtistab mitu argumenti on käesoleva rakenduse jaoks juba vaadatud. Sisuliselt kompileerime järjest argumendid (vasakult-paremale) ning seejärel funktsiooni ja lõpuks väljakutse instruktsiooniga CALL, millele järgneb argumentide arv.

T(f,ρ):= fMK_CLOSURE {f};″    f ∈  F       
T(x,ρ):= fLOAD_ARG {ρ(x)};″   x ∉  F       
T(e1e2 ,ρ):= T(e2,ρ)+C(e1,ρ,1)          

Funktsioon C on defineeritud (funktsiooni T abil) kui

C(e1e2 ,ρ,n):= T(e2,ρ)+C(e1,ρ,n+1)         
C(e,ρ,n):= T(e,ρ)+fCALL {n};″          

Term t, mis kasutab funktsioone f1, …, fn, teisendatakse programmiks

T(t,∅)+HALT; ″+F(f1)++F(fn).

Konstantide lisamiseks piisab lihtsamal juhul defineerida skeemi juurde kolme väärtuse kompileerimine ja 13 funktsiooni konstandi kompileerimise. Vaata järgnevaid definitsioone.

T(n,ρ):= fPUSH_INT {n}; ″          
T(b,ρ):= fPUSH_BOOL {b}; ″          
T(nil,ρ):= fPUSH_NIL; ″          
C(add,ρ,2):= ‶ADD; ″          
C(sub,ρ,2):= ‶SUB; ″          
C(mul,ρ,2):= ‶MUL; ″          
C(not,ρ,1):= ‶NOT; ″          
C(null,ρ,1):= ‶IS_NIL; ″          
C(iszero,ρ,1):= ‶PUSH_INT 0; EQ; ″          
C(cons,ρ,2):= ‶PAIR; ″          
C(hd,ρ,1):= ‶FST; ″          
C(tl,ρ,1):= ‶SND; ″          
C(pair,ρ,2):= ‶PAIR; ″          
C(fst,ρ,1):= ‶FST; ″          
C(snd,ρ,1):= ‶SND; ″          

Tingimusoperaatoriga peame agara väärtustamise puhul rohkem vaeva nägema, et vältida mõlema haru väärtustamist. Seetõttu ei saa kasutada tavalist argumentide skeemi. Peame koodist leidma kolmele argumendile cond -i rakendamised ja tõlkima järgneva skeemi abil.

T(condbte,ρ) := f{T(b,ρ)}          
  JUMP_IF_ZERO else          
  {T(t,ρ)}          
  JUMP end          
  else:          
  {T(e,ρ)}          
  end:          
          
C(condbte,ρ,n) := T(condbte,ρ)+fCALL {n};″          

Selliste definitsioonide puhul ei saa konstante kasutada koos osalise rakendamisega, kuna skeem tõlgib konstandid vaid juhul, kui neile on rakendatud täpselt õige arv argumente. Seda puudujääki on aga lihtne lahendada abifunktsioone kasutades. Näiteks, saame kasutada skeemi

T(add,ρ) := fMK_CLOSUREadd; ″

kus programmitekstis on defineeritud funktsioon

add: TAKE 2; LOAD_ARG 1; LOAD_ARG 0; ADD; RETURN;

Kuigi defineeritud skeem on praktiliselt mõistlik kuna annab meile termi struktuurile lähedase programmi, on see problemaatiline. Nimelt, antud skeem ei järgi rangelt aplikatiivset järjekorda — võib juhtuda, et mõned argumendid väärtustatakse liiga vara. Täpselt aplikatiivjärjekorra saamiseks peame argumente siiski ükshaaval edastama. Selline kood annab segasema programmiteksti. Vaata järgnevat, alternatiivset, koodi.

T(e1e2,ρ):= T(e1,ρ)+T(e2,ρ)+SWAP; CALL 1;″          

Sellisel juhul väärtustame enne funktsiooni, seejärel argumendi ning siis teostame funktsioonikutse.

13.2.2 Agara väärtustamise näited

Kompileerime termi (λ x. mulxx) (add 2 3). Esimese sammuna loome abstraktsioonist funktsiooni fx = mulxx ning termiks jääb f (add 2 3). Kompileerimisel saame tulemuseks järgneva programmiteksti.

 PUSH_INT 3         
 PUSH_INT 2         
 ADD          
 MK_CLOSURE f         
 CALL 1         
 HALT          
f: TAKE 1         
 LOAD_ARG 0         
 LOAD_ARG 0         
 MUL         
 RETURN          

LVM toetab rekursiooni otse. Seega võime termist üles otsida Y kombinaatori kasutused kujul Y ((λ c1 … ckfx1 … xn. e) c1 … ck) ja muuta need rekursiivse funktsiooni fc1 … ckx1 … xn := e kutseteks. Alternatiivne võimalus on implementeerida Y kombinaator otse LVM-s. Pane tähele, et agaras väärtustamises lõpmatusse tsükklisse minemise vältimiseks peame defineerima kahe argumendiga kombinaatori versiooni Y F X := F (Y F) X.

Y: TAKE 2         
 LOAD_ARG 1         
 LOAD_ARG 0         
 MK_CLOSURE Y         
 CALL 1         
 LOAD_ARG 0         
 CALL 2         
 RETURN          

Seejärel saame implementeerida foldl funktsiooni kui termi YF, kus funktsioon F on λ fgaxs. cond  (nullxs) a (fg (g (hdxs) a)) (tlxs). Sellest termist saame kompileerida järgneva koodi.

F: TAKE 4         
 LOAD_ARG 3   # xs       
 IS_NIL   # null xs       
 JUMP_IF_FALSE el         
 LOAD_ARG 2   # a       
 JUMP en         
el: LOAD_ARG 3   # xs       
 SND   # tl xs       
 LOAD_ARG 2   # a       
 LOAD_ARG 3   # xs       
 FST   # hd xs       
 LOAD_ARG 1   # g       
 CALL 2   # g (hd xs) a       
 LOAD_ARG 1   # g       
 LOAD_ARG 0   # f       
 TAILCALL 3   # f g (g (hd xs) a) (tl xs)       
en: RETURN         
           

Kasutades foldl-i saame kompileerida foldl (λ ht. consht) nil (cons 1 (cons 2 nil)). Järgmise sammuna loome abstraktsioonist funktsiooni ght = consht. Kompileerimisel saame tulemuseks järgneva programmiteksti. Pane tähele, kuidas koodis on arvutus toimub termi mõttes tagant poolt ette. Arvutus lõpeb peale 85. sammu.

 PUSH_NIL         
 PUSH_INT 2         
 PAIR         
 PUSH_INT 1         
 PAIR         
 PUSH_NIL         
 MK_CLOSURE G         
 MK_CLOSURE F         
 MK_CLOSURE Y         
 CALL 4         
 HALT         
G: TAKE 2         
 LOAD_ARG 0         
 LOAD_ARG 1         
 PAIR         
 RETURN         
Y:          
F:          

13.2.3 Laisk väärtustamine

Laisa väärtustamise olukord on mõnevõrra erinev. Meil on vaja termi väärtustamisele vastavat koodi (T) kui ka koodile laisalt viitavat koodi (T′). Väärtust arvutav kood on väga sarnane agarale väärtustusele. Esimeseks erinevuseks on see, et raamis pole salvestatud otse väärtused vaid hoopis viited väärtustamata koodi — need tuleb väärtustada instruktsiooniga FORCE. Teiseks erinevuseks on parameetrite andmine funktsioonikutsel – me ei arvuta argumente välja vaid anname edasi laisal kujul.

T(f,ρ):= fMK_CLOSURE {f};″    fF       
T(x,ρ):= fLOAD_ARG {ρ(x)}; FORCE;″   xF       
T(ft1tn ,ρ):= T′(tn,ρ)++T′(t1,ρ)+T(f,ρ)+fCALL {n};″          

Väärtustamata (laisale) termile vastav kood on põhimõtteliselt lihtne: loome kuhja peale väärtustamata koodi objekti (instruktsiooniga MK_THUNK) kus viitame koodi väärtustamisele vastavale alamprogrammile. Tehniliselt on selleks on tarvis luua uusi silte ja hüpata üle koodi deklaratsiooni. Erijuhuna, kuna argumendid juba on väärtustamata koodi objektid, saame parameetri puhul sobiva väärtuse otse raamist lugeda.

T′(x,ρ) := fLOAD_ARG {ρ(x)};″    xF       
T′(t,ρ) := fJUMPl         
  c:          
  {T(t,ρ)}         
  RETURN         
  l:          
  MK_THUNK c         
          

Siinkohal oleks sobilik optimisatsioon paigutada väärtustamata avaldiste kood (sildiga c) termi koodi järele koos teiste funktsioonidega. Nii saaksime definitsiooniks võtta T′(t,ρ) := fMK_THUNKc;″.

Konstantidega on olukord sarnane agara väärtustamsiega. Lihtsamal juhul tuleks defineerida skeemi juurde kolme väärtuse kompileerimine ja 13 funktsiooni konstandi kompileerimise. Vaata järgnevaid definitsioone.

T(n,ρ):= fPUSH_INT {n}; ″          
T(b,ρ):= fPUSH_BOOL {b}; ″          
T(nil,ρ):= fPUSH_NIL; ″          
T(addxy,ρ):= T(y,ρ)+T(x,ρ)+ADD; ″          
T(subxy,ρ):= T(y,ρ)+T(x,ρ)+SUB; ″          
T(mulxy,ρ):= T(y,ρ)+T(x,ρ)+MUL; ″          
T(notx,ρ,1):= T(x,ρ)+NOT; ″          
T(nullx,ρ,1):= T(x,ρ)+IS_NIL; ″          
T(iszerox,ρ,1):= T(x,ρ)+PUSH_INT 0; EQ;″          
T(consxy,ρ):= T(y,ρ)+T(x,ρ)+PAIR; ″          
T(hdxy,ρ):= T(y,ρ)+T(x,ρ)+FST; ″          
T(tlxy,ρ):= T(y,ρ)+T(x,ρ)+SND; ″          
T(pairxy,ρ):= T(y,ρ)+T(x,ρ)+PAIR; ″          
T(fstxy,ρ):= T(y,ρ)+T(x,ρ)+FST; ″          
T(sndxy,ρ):= T(y,ρ)+T(x,ρ)+SND; ″          

Tingimusavaliste puhul on seis sarnane nagu argara väärtustamise puhul kuna tingimusavaldis peab ka agaras kontekstis olema laisk.

T(condbte,ρ) := f{T(b,ρ)}          
  JUMP_IF_ZERO else          
  {T(t,ρ)}          
  JUMP end          
  else:          
  {T(e,ρ)}          
  end:          
          

Erinevalt agarast kontekstist, saame cond -i implementeerida ka funktsiooniga, mis sisemiselt kasutab eelmise definitsiooniga sarnast implementatsiooni.

cond: TAKE 3          
  LOAD_ARG 0         
  JUMP_IF_ZERO else          
  LOAD_ARG 1          
  JUMP end          
else: LOAD_ARG 2          
end:           

13.2.4 Laisa väärtustamise näited

Kompileerime termi (λ x. 1) ((λ x. xx) (λ x. xx)) laisa skeemiga. Esimese sammuna loome abstraktsioonist funktsiooni fx = 1 ning ω x = xx ning termiks jääb f (ω ω). Kompileerimisel saame tulemuseks järgneva programmiteksti. Väljakommenteeritud on alternatiivne juht, kus funktsiooniks on identsusfunktsioon. 111ex

 JUMP l1         
c1: JUMP l2          
c2: MK_CLOSURE o          
 RETURN         
l2: MK_THUNK c2         
 MK_CLOSURE o         
 CALL 1         
 RETURN         
l1: MK_THUNK c1         
 MK_CLOSURE f         
 CALL 1         
 HALT         
f: TAKE 1         
# LOAD_ARG 0         
# FORCE         
 PUSH_INT 1         
 RETURN         
o: TAKE 1         
 LOAD_ARG 0         
 LOAD_ARG 0         
 FORCE         
 TAILCALL 1          

Eelneva programmi väärtustamine jõuab peale seitset sammu väärtuseni 1. Alternatiivne programm, millele vastab term (λ x. x) ((λ x. xx) (λ x. xx)), jõuab 17 sammu järel lõpmatu tsükkli esimese iteratsiooni lõppu. Selle järel jõuab arvutus viie sammu möödudes täpselt samasse seisu tagasi.

Järgnevalt vaatame programmi, mis vastab termi (λ x. addxx) (add 1 2) laisale väärtustusele. Kood on järgnev. Kuuendal sammul alustatakse parameetri väärtustamist ehk tehte 1+2 arvutamist. Parameetri teine kasutuskord on 11. sammul. Aga kuna väärtus on juba arvutatud, siis loetakse tulemus mälust. Programm lõpeb 15-ndal sammul tulemusega 6.

  MK_THUNK x         
  MK_CLOSURE F         
  CALL 1         
  HALT         
x: TAKE 0         
  PUSH_INT 1         
  PUSH_INT 2         
  ADD         
  RETURN          
F: TAKE 1         
  LOAD_ARG 0         
  FORCE         
  LOAD_ARG 0         
  FORCE         
  ADD         
  RETURN          

Kuigi see ei pruugi olla kõge optimaalsem lahendus, implementeerime järgnevalt Y kombinaatori LVM-i funktsioonina. Erinevalt agarast väärtustamisest, võime kasutada järgnevar ühe-argumendilist definitsiooni YF := F (YF).

Y: TAKE 1         
 MK_THUNK YF         
 LOAD_ARG 0         
 FORCE         
 CALL 1         
 RETURN         
YF: LOAD_ARG 0         
 MK_CLOSURE Y         
 CALL 1         
 RETURN          

Seejärel saame implementeerida foldl funktsiooni kui termi YF, kus funktsioon F on λ fgaxs. cond  (nullxs) a (fg (g (hdxs) a) (tlxs)). Funktsiooni kehas kasutame skeemi tingimuslause cond arvutamiseks. Sellest termist saame kompileerida järgneva koodi.

F: TAKE 4         
 LOAD_ARG 3   # xs       
 FORCE         
 IS_NIL   # null xs       
 JUMP_IF_FALSE el         
 LOAD_ARG 2   # a       
 FORCE         
 JUMP en          
el: MK_THUNK C1   # tl xs       
 MK_THUNK C2   # (g (hd xs) a)       
 LOAD_ARG 1   # g       
 LOAD_ARG 0   # f       
 FORCE         
 TAILCALL 3   # f g (g (hd xs) a)       
C1: LOAD_ARG 3; FORCE; SND; RETURN          
C2:          
en: RETURN         
           

Avaldise g (hdxs) a väärtustamise kood on järgnev.

C2: LOAD_ARG 2   # a       
 MK_THUNK C3   # (hd xs)       
 LOAD_ARG 1   # g       
 FORCE         
 CALL 2   # g (hd xs) a       
 RETURN         
C3: LOAD_ARG 3; FORCE; FST; RETURN          

Sarnaselt agarale väärtustusele saame kasutada laiska skeemi, et kompileerida foldl (λ ht. consht) nil (cons 1 (cons 2 nil)). Arvutus lõpeb peale 120. sammu (agara skeemi järgi kulus 85 sammu).

 MK_THUNK C4         
 MK_THUNK C5         
 MK_THUNK CG         
 MK_THUNK CF         
 MK_CLOSURE Y         
 CALL 4         
 HALT         
C4: PUSH_NIL         
 PUSH_INT 1         
 PAIR         
 PUSH_INT 0          
 PAIR         
 RETURN          
C5: PUSH_NIL         
 RETURN         
CG: MK_CLOSURE G         
 RETURN         
CF: MK_CLOSURE F         
 RETURN         
G: TAKE 2         
 LOAD_ARG 1         
 FORCE         
 LOAD_ARG 0         
 FORCE         
 PAIR         
 RETURN         
Y:          
F:          

13.3 Reduktsioon vs. virtuaalmasinad

Nägime, et reduktsioon on võimalik defineerida mõnede üksikute reeglitega üle termide struktuuri, kus on koleme liiki terme. See on teoreetilisest vaatest mugav ja ülevaatlik.

Samas, kui vaatame aritmeetika implementeerimist Churchi numbrite ja muude andmestruktuuridega, kasvab reduktsioonide arv võrdlemisi suureks juba väikeste konstantidega termide puhul. Konstantide sissetoomine keelde vähendab reduktsioonisammude arvu mingil määral.

Tekib küsimus, kui keerukas on üks redutkstiooni samm. Naiivselt vaadates, tuleb leida reedeks, reedeks redutseerida ja tulemus tagasi konteksti panna. Reedeksi leidmiseks läheb halvimal juhul O(k) tehet, kus k on termipuu kõrgus. Reduktsioon vajab tänu vangistamisele halvimal juhul O(k2) tehet, kuna term võib ruutkeerukusega kasvada. Redutseeritud termi paigutamine konteksti vajab O(k) tehet. Ajaline keerukus tuleneb otse ruumilisest keerukusest, kuna iga samm võib term ruutkeerukusega kasvada.

Seega, samm pikas programmis (suures termis) võtab kauem aega kui lühikeses programmis. On selge, et reduktsioonisammud ei vasta intuitiivselt mingitele baas-sammudele, kuna reduktsiooni keerukus sõltub termi kõrgusest. Vaja oleks leida sammud, mis on arvutatavad konstantse ajaga.

Defineetirud virtuaalmasin LVM puhul ei sõltu ühe instruktsiooni jaoks kuluv aeg programmi suurusest. Instruktsioonid töötavad konstantse ajaga, kui arvestada sellega, et ka instruktsioonide argumendid on konstandid.

Lisaks pole virtuaalmasinas eraldi termi konteksti panemist ega reedeksiks ja kontekstiks jagamist. Programm masina töö jooksul ei muutu. Instruktsiooni rakendamisel toimub implitsiitselt ka refokusseerimine — oleme kohe valmis järgmise instruktsiooni rakendamiseks.

Kokkuvõtteks, igale reduktsioonile vastab konstantne arv konstantset aega võtvaid instruktsioone. Seega, virtuaalmasin näitab, et λ-arvutus (ja funktsionaalne programmeerimine üldiselt) on teoreetiliselt efektiivselt arvutatav. Kuigi LVM pole kindlasti praktikas kõige efektiivsem, saab erinevus olla vaid konstant.


Previous Up Next