Suures pildis on puhas λ-arvutus üks minimaalne ja täielik arvutusmudel. Sellistest formaalsetest arvutusmudelitest on λ-arvutus kõige lähedasem tavamõttes programmeerimisele. Lisaks oli see esimene selline mudel. Vaatame nüüd täpsemalt.
Formaalne arvutusmudel on matemaatiline süsteem, kus saab kirjeldab mingit hulka algoritme ja näidata, kuidas selles mudelis antud algoritm antud sisendite puhul väljundini jõuab. Näiteks on lõplikud olekumasinad formaalne arvutusmudel, millega saab arvutada sõne vastavust regulaaravaldisele. Veel üks tuntud formaalne arvutusmudel on Turingi masin, mida kasutatakse arvutatavuse teooria teoreetilistes tõestustes.
Praktikas võib väita, et suvaline konkreetne arvuti on arvutusmudel, aga praktilised arvutid pole minimaalsed ega teoreetilises mõttes täielikud. Lihtsa algoritmi töö üle arutlemine konkreetsel arvutil on väga palju keerukam, kuna arvuti keerukus lisandub algoritmi keerukusele.
Mitteformaalselt võib arvutusmudeliks nimetada ka suvalist progamemerimiskeelt, kui selle keele programmide väärtustamine on piisavalt täpselt defineeritud. Formaalses arutluses on parem kui keel oleks väike ja selge kuid samas lubaks algoritmide kirjeldamist võimalikult lühidalt. Java ja Pythoni kompilaatorites kasutatakse arvutusmudelina vastavat baitkoodi ja virtuaalmasinat.
Puhas λ-arvutus on arvutusmudel, mis koosneb väga vähestest osadest ja väga vähestest reeglitest. Siiski on see täielik — kõik efektiivselt arvutatavad funktsioonid on arvutatavad puhtas λ-arvutuses (Church-Turingi teesi järgi).
Vaatame esmalt üldisemat mudelit — konstantidega λ-arvutust, mis on saadud mingi hulga konstantide lisamisega puhtale λ-arvutusele.
Konstantide idee seisneb selles, et me soovime praktikas kasutada protsessori poolt pakutavaid väärtuseid ja nende operatsioone. Näiteks 64-bitiseid täisarve ja ujukomaarve.
Hiljem näeme, et puhta λ-arvutusega on võimalik implementeerida kõik vajalikud andmestruktuurid ja konstantide kasutamiseks teoreetiline vajadus puudub. Praktikas on muidugi protsessori aritmeetika väga palju kiirem kui selle implementatsioon puhtas λ-arvutuses.
Avaldisi λ-arvutuses kutsutakse termideks. Termide hulk Λ on defineeritud induktiivses vormis järgneva nelja reegliga.
Kirjanduses kasutatakse ka järgnevat (samaväärset) süntaktilist definitsiooni λ-termide jaoks.
|
λ-termidest mõelge kui programmikoodist. Varsti näeme, kuidas λ-arvutus arvutab termile t vastava väärtuse v — seda kirjutame kui t ↠ v. Hetkel võtke lihtsalt teatavaks, et väärtuse arvutamine käib samm-haaval ja väärtus ise on term, kus ühtegi sammu teha ei saa. Ehk siis λ-termid kodeerivad nii ülesande püstitust, vahepealseid seisundeid kui ka lõpptulemust.
Enamasti kasutame muutujateks ladina tähti näiteks a, b, c või x, y ja z. Kui muutuja on mõeldud tähistama funktsiooni siis kasutame aga näiteks f, g või h. Vajadusel kasutame ka pikemaid muutujanimesid, näiteks parem või vasak.
Näiteks on λ-termid muutujad x ja f. Sellisel juhul mõelge muutujatest x või f nagu globaalsetest muutujatest — s.t. nende muutujate tähendus peab tulema välisest kontekstist ja üldiselt ei saa me midagi muud nende kohta arvata. λ-arvutuses kutsutakse globaalseid muutujaid vabadeks muutujateks.
Abstraktsioon on funktsioon. Kui e on term, siis (λx. e) on (ilma nimeta) funktsiooni definitsioon, mille formaalne parameeter on x ja mille keha on term e. Abstraktsiooni (λx. e) keha e sees olevaid parameetri x esinemisi nimetatakse seotud muutujakas — selle väärtus ei tulene välisest kontekstist vaid hoopis funktsiooni argumendi väärtusest. Detaile vaatame hiljem aga üldjoontes, kui sellele funktsioonile (λx. e) anda argument, siis funktsiooni tulemus arvutatakse funktsiooni keha e järgi, võttes kehas vaba muutuja x asemel tegeliku argumendi.
Kõige lihtsam funktsioon λ-arvutuses on identsusfunktsioon ehk term (λx. x), kus funktsiooni kehaks on sama muutuja x mis on funktsiooni formaalseks parameetriks. Kui funktsiooni keha x eraldiseisvalt vaadata, siis on tegemist vaba muutujaga. Abstraktsioon seob aga keha sees olevad vabad muutujad enda parameetriga. Ehk termis (λx. e) on muutuja x seotud. Intuitiivselt näeme, et tegemist ongi identsusfunktsiooniga, kuna ta igal juhul tagastab oma argumendi muutmata kujul. Pane tähele, et ka (λy. y) on identsusfunktsioon.
Aplikatsioon on funktsioonirakendus. Kui term f väärtustub funktsiooniks siis iga termi t puhul term (f t) väärtustub selle funktsiooni tulemuseks, kui funktsiooni argumendiks võtta termi t väärtus.
Näiteks on λ-termid (f x) ja ((λx. x) y). Esimesel juhul on funktsiooniks vaba muutuja f ja argumendiks vaba muutuja x. Teisel juhul on funktsiooniks identsusfunktsioon (λx. x) ja argumendiks vaba muutuja y. Erinevalt y-st pole x termis ((λx. x) y) vaba muutuja ja arvutuse tulemus ei sõltu sellest, mis on globaalse muutuja x väärtus.
Üldiselt võime konstantideks võtta suvalise hulga väärtuseid ja operatsioone nendel väärtustel — tingimusel, et need konstandid on eristatavad abstraktsioonist, aplikatsioonist ja muutujatest.
Näiteks, kui võtame C := ℕ ∪ { add } siis on term (λx. ((add 10) x)) võiks näiteks esitada funktsiooni, mis liidab oma argumendile juurde kümme.
Enne võimalike konstantide valimist, vaatame kuidas vähendada sulgude arvu.
Termid moodustavad puustruktuuri ja puustruktuuri esitamiseks tekstis on tavaks kasutada sulge. Kui tahame struktuuri üles kirjutada nii selgelt kui võimalik, oleks mõistlik kasutada minimaalsel arvul sulge. Selleks kasutame kirjanduses tavaks saanud reegleid, mida tuleks lugeda nii, et kui me kirjutame nii nagu vasakul, siis me mõtleme sama termi nagu paremal. Ehk mõlema kirjapildi abil mõtleme sama asja.
|
Kirjanduses on tavaks, et aplikatsioon on vasakassotsiatiivne, ehk rohkem kui kahe järjestikuse aplikatsiooni puhul on sulud vaikimisi vasakul. Seega vaikimisi eeldame, et funktsioonile rakendatakse mitu argumenti, mitte et see sisaldab mitut funktsiooni.
Veel on tavaks, et abstraktsioon seob nii pikalt paremale kui võimalik. Sulgude puudumisel on kõik peale punkti seotud abstraktsiooniga.
Kolmas reegel lubab üksteise sees asuvaid abstraktsioone kirjutada ühe λ-sümboliga.
Näited λ-termidest:
Esiteks võtame konstantideks tõeväärtused true ∈ C, false ∈ C ning tingimusfunktsiooni cond ∈ C. Aga lisaks peame ka näitama, kuidas nendega arvutus toimub.
Konstantide arvutusreeglid antakse λ-arvutuses δ-reeglitega, mis on lihtsustusseos termide vahel. Kui kirjutada e1 →δ e2, siis see tähendab, et term e1 lihtsustub termiks e2 vastavalt konstantide reeglitele.
Kui tingimusavaldisele on rakendatud kolm argumenti millest esimene on tõeväärtus true , siis on tulemus teine argument. Aga kui tingimusavaldisele on rakendatud kolm argumenti millest esimene on tõeväärtus false , siis on tulemus kolmas argument.
Ehk kõigi termide e1 ka e2 jaoks kehtib
|
Näiteks on term cond true false true . See term redutseerub termiks false ühe δ-reduktsiooni sammuga. Term cond true (cond false false true) true redutseerub ühe sammuga termiks cond false false true ning järgmise sammuga termiks true .
Mitme sammuga redutseerumist kirjutatakse ka järgnevalt.
|
Joonisime alla redutseeritava termi e. reedeksi — kõik mis pole allajoonitud jääb samaks. Viimases näites redutseerisime tervet termi korraga.
On tavaks, et λ-arvutuses lubatakse reduktsiooni käib sügavamal termis — lihtsustus võib toimuda samahästi väljaspool kui ka seespool. Ehk, kui t1 → t2 siis iga u∈Λ ja x∈ V korral. See kehtib nii δ- kui ka muude reduktsioonide kohta.
|
See tähendab, et võib redutseerida ka teises järjekorras. Näiteks cond -i teine argument enne.
|
Enamasti tahame, et tulemus ei sõltuks lihtsustussammude järjekorrast. Peame olema reduktsiooni defineerimisel ettevaatlikud!
Edasi võtame konstantide hulka protsessori poolt toetatud (näiteks 64bit) täisarvud Int ⊂ C. Lisaks aritmeetika baastehted liitmine add ∈ C, lahutamine sub ∈ C, korrutamine mul ∈ C ja võrdlemine nulliga iszero ∈ C .
Reduktsioon vastab protsessori käitumisele, kui kõik vajalikud argumendid on antud. Vaata järgnevaid näiteid.
Seni oleme vaadanud baasandmetüüpe: tõeväärtused ja täisarvud. Kuidas aga teha abstraktseid andmetüüpe — näiteks paare?
Lisame konstandid pair ∈ C, fst ∈ C ja snd ∈ C paaride jaoks. Näiteks on termideks pair x y, fst x ja snd (pair x y).
Ehk kõigi termide e1 ka e2 jaoks kehtib
|
Vaata järgnevaid näiteid.
Nüüd lisame konstandid listide jaoks. Listid on rekursiivne abstraktne andmestruktuur. Lisame konstandid nil ∈ C, cons ∈ C ning null∈ C, hd∈ C ja tl∈ C. Näiteks on termideks nil, cons x nil, null nil ja hd (cons x nil).
Kõigi termide e1 ka e2 jaoks kehtib
|
Vaata järgnevaid näiteid.
Eelnevad näited käsitlesid positiivseid juhte, kus argumendid olid just parajad, et tuleks mõistlik tulemus. Mis juhtub aga muul juhul? Vastus: muul juhul lihtsustada ei saa ja term jääb selliseks nagu ta on. Vaata järgnevaid näiteid, mis on δ-normaalkujul ehk rohkem samme teha ei saa.
Võrreldes praktiliste programmeerimiskeeltega kaob λ-arvutuses ülevaatlikus, kuna termid tulevad tihti väga pikad. Pole mooduleid ega globaalseid definitsioone, kus saaks hoida valmis algoritme ja funktsioone.
Üks võimalus globaalsete definitsioonide kasutamiseks ilma konstruktsioonide lisamiseta λ termide definitsiooni on kasutada makrodefinistioone. See tähendab seda, et definitsioonid asendatakse termi enne redutseerimise sammudega alustamist.
Näiteks võime defineerida kuulsad S, K ja I kombinaatorid järgnevate makrodega
|
Kombinaator tähendab siin kinnist (ehk vabade muutujateta) termi mis on normaalkujul (ehk mida ei saa iseseisvalt lihtsustada). Nende kombinaatorite tähtsusest räägime natuke hiljem.
On tavaks, et makrodefinitsioonid on kombinaatorid. Sellisel juhul on termi asendatuna alati sama tähendusega ja ei lisa väärtustamisele lihtsustamissamme.
Vaadake, kuidas makrosid on kasutatud termide kirjutamisel.
|
Vaadates viimaseid näiteid näeme, et pikemad λ-termid näevad arusaamatud välja. Selliste termide puhul polegi enamasti mõtet hakata neid intuitsiooni kaudu analüüsima. Lahendus on hoopis püüda neid terme masinlikult lihtsamateks redutseerida. Ehk rakendada reduktsiooni reegleid ja loota, et tulemus on midagi arusaadavat.