Nägime, kuidas δ-reduktsioon lihtsustas termi, milles olid konstantidele rakendatud konstandid ja muud termid. Kuidas aga lihtsustata termi, kus abstraktsioonile (λ x. e1) on rakendatud argument e2. Sellist juhtu nimetataksegi β-reduktsiooniks.
Intuitiivselt on termi (λ x. e1) e2 reduktsioon üsnagi lihtne — selle väärtus on funktsiooni keha väärtus, kui funktsiooni kehas võtta vaba muutuja x asemel termi e2. Näiteks
Siin võib juhtuda aga üks probleem, mida nimetatakse vaba muutuja vangistamiseks. Vaatame termi (λ x y. (λ x y. sub x y) y x) 3 6 kahte erinevat reduktsioonijada. Esiteks redutseerime termi võimalikult väljast.
|
Nüüd aga redutseerime kõigepealt seestpoolt.
|
Tulemus on ühel juhul 3 ja teisel juhul 0. Mis läks valesti? Vastus: vigane on esimene reduktsioon, kus abstraktsiooni kehas λ y. sub x y pidime asendama vabad x-d termiga y. Intuitiivne vastus λ y. sub y y on aga vale, sest kui enne said vähendatav ja lahutaja olla erinevad, siis peale vigast lihtsustust peavad need olema võrdsed — ehk vahe on alati null. Teistpidi vaadates, y, mis oli funktsioonirakenduse reedeksis vaba muutuja, on peale asendamist nüüd seotud sisemise abstraktsiooniga.
Peame ettevaatlikult ja põhjalikult defineerima vangistamisest hoiduva asendamise. Selleks peame esmalt formaalselt defineerima, mis on termi vabad muutujad.
Termi t vabade muutujate hulga arvutab järgnev funktsioon FV ∈ Λ → 2V, mis on defineeritud süntaktiliselt iga termi liigi jaoks.
|
Ehk, kui term on muutuja x∈ V, siis see muutuja ongi vaba. Konstant c∈C ei sisalda vabu muutujaid. Abstraktsiooni λ x. e vabad muutujad on keha e vabad muutujad, kuid peame eemaldama funktsiooni parameetri x, kuna see on seotud just selle lambdaga. Lõpetuseks, aplikatsiooni t u vabad muutujad on lihtsalt t ja u vabade muutujate ühend.
Näited:
|
Vabade muutujate leidmiseks saab kasutada funktsiooni FV, aga paberil/tahvlil arvutades on see liiga tülikas. Enamasti piisab, kui käia üle termi ja iga muutuja juures leida, kus või kas ta on seotud. Vaata järgnevat näidet.
Esimesed kaks muutujat x ja y pole vabad, kuna saime leida abstraktsiooni parameetri, kus nad on seotud. Viimase y juures aga sellist lambdat ei leidu — seega see on muutuja y vaba esinemine.
Nüüd saame defineerida vangistamisest hoiduva substitutsiooni operatsiooni. Kirjutame t[x→ u], mis asendab termis t vabad muutujad x∈ V termidega u selliselt, et u vabad muutujad ei saa vangistatud. Substitutsioon on defineeritud süntaktiliselt iga termi t liigi jaoks.
|
Kui term on muutuja y, siis substitutsioon y[x→ u] tagastab u, kui x on sama muutuja mis y. Kui x≠ y, siis jätame termi muutmata ehk tagastame y. Substitutsioon jätab konstandid samaks ja aplikatsiooni puhul teostatakse substitutsioon nii funktsiooni kui ka argumendi peal. Kõige keerulisem juht on abstraktsioon substitutsioon (λ y. t)[x→ u]. Kui x=y, siis lambda termis vabu x-e ei leidu ja saame tagastada termi muutmata kujul. Kui asendatavas termis u pole y vaba, siis saame otse teha substitutsiooni abstraktsiooni kehas t. Muul juhul peame tegema substitutsiooni, et vältida u-s vaba muutuja y vangistamist. Selleks leiame n.n. värske muutuja z — muutuja, mis ei esine termides u ega t. Seejärel teisendame termi (λ y. t) termiks (λ z. t[y→z]).
Seega on β-reduktsiooni reegel iga t,u∈Λ jaoks järgmine. Aga tuleb meeles pidada, et saame redutseerida ka termis seespool.
| (λ x. t) u →βt[x→u] |
Nüüd redutseerime meie motiveerivat näidet uuesti seestpoolt.
|
Sama tulemus mis kõigepealt väljast redutseerides. Veendusime, et vähemalt sellel juhul ei sõltu tulemus lihtsustussammude järjekorrast.
Hiljem näeme, et teoorias pole konstante ega δ-reduktsiooni vaja — konstandid saab defineerida makrodena nii, et mitmesammuline β-reduktsioon täidab ka δ-reduktsiooni ülesannet. See on nii, kuna arvutusteooria standardid programmi töö efektiivsusele on madalad — efektiivselt arvutatavus ei tähenda kiirust vaid ainult seda et lahenduseni on võimalik konstruktiivselt jõuda.
Programmeerimiskeeltes oleme harjunud kasutama sisukaid muutujanimesid kuigi teame, et nime valik ei mõjuta tegelikult programmi tööd. Heade nimede panemine väldib arusaamatusi programmeerimise protsessi käigus — see aitab ühel programmeerijal kiiremini mõista teise programmeerija programme. Aga meie ei tegele siin praktilise programmeerimisega vaid uurime arvutusmudelit.
Arusaama, et nime valik ei mõjuta tegelikult programmi tööd, nimetatakse α-ekvivalentsuseks (või α-kongruentsuseks). Intuitiivselt, kaks termi, mis võivad erineda ainult seotud muutujate nimede poolest, peaks arvutusprotsessis käituma identselt. Kirjanduses kasutatakse ka sõnastust, et α-ekvivalentsed termid on identsed seotud muutujate ümbernimetamise täpsuseni.
Näited α-ekvivalentsetest termidest.
Formaalselt on termid t, u∈Λ α-ekvivalentsed, ehk t =αu, siis ja ainult siis kui α([], [], t, u) = true. Abifunktsioon α∈ list V → list V → Λ → Λ → B, kus B on tõeväärtuste hulk, on defineeritud järgnevalt.
Näiteks soovime veenduda, et (λ x y. x) =α(λ y x. y). Arvutame järgnevalt.
Enamasti pole nii detailne arvutuskäik vajalik, et tuvastada, kas termid on α-ekvivalentsed. Paberil/tahvlil arutledes piirdume intuitiivse käsitlusega.
Formaalsels lähenemises on aga tarvis tähele panna, et vaba muutuja asendamine teise muutujaga ei tee termi suuremaks (lemma 1). Seda tähelepanekut kasutame hiljem väidete induktsiooniga tõestamisel, kui substitutsioon teostab vangistamise vältimiseks α-teisenduse.
Tõestus. Tõestus induktsiooniga üle termi t struktuuri. Induktsiooni hüpoteesiks, et t-st struktuurselt väiksemate termide puhul lemma kehtib.
Termi väärtustamiseks piisab δ- ja β-reduktsiooni reeglitest. λ-arvutusel on aga ka kasutusjuht, kus tahame teada termide võrdsust. Sel juhul ei redutseeri me üht termi vaid kahte termi ja vaatame siis, kas mõlema normaalkujud on α-ekvivalentsed. Näiteks on termide võrdsust vaja teada sõltuvate tüüpidega keeltes, kus ka tüübid kodeeritakse sisuliselt λ-termidega. Siin aga tekib probleem.
Vaatame näiteks terme add ja (λ x y. add x y). Mõlemad on βδ-normaalkujul — ühtegi reduktsiooni teha ei saa. Samas, pole need termid α-ekvivalentsed. Kas need polegi võrdsed?
Loogikas on mõiste ekstensionaalsus, mis tähendab seda, et objektid on võrdsed kui need on väliselt eristamatud. Termid add ja (λ x y. add x y) on väliselt eristamatud, kuna argumente lisades on väärtused samad.
Ekstensionaalsuse vaste λ-arvutuses on η-reduktsioon, mis iga t∈Λ puhul, kus x∉FV(t), lihtsustab abstraktsiooni järgnevalt. Jällegi, pidage meeles, et see võib toimuda ka sügavamal termi sees.
|
Ehk, siis kui term on kujul (λ x. t x), kus alamterm t ei sisalda x-i vabalt, saame ümbritseva lambda ja aplikatsiooni ära jätta.
Termide add ja (λ x y. add x y) normaalkuju kasutades βηδ-reduktsioone on mõlemal juhul add . Seega on termid võrdsed — või täpsemalt öeldud βηδ-võrdsed.
|
Teoreetilises λ-arvutuses on kaks põhimõttelist erinevat strateegiat: väljast-enne ja seest-enne. Kuna tehniliselt võib nii välimisi kui sisemisi olla mitu, siis on tavaks võtta alati vasakpoolseim. Nii saame kaks standardset reduktsioonijärjekorda.
Näiteks vaatame termi (λ x y. add y y) (mul 2 3) (sub 5 2). Leiame kõik reeksid.
| ( |
| ) |
Tulemusest on näha meie võimalused. Esmalt redutseerime normaaljärjekorras ehk väljast sisse.
|
Nüüd redutseerime aga sama termi aplikatiivjärjekorras ehk seest välja.
|
Mõlemal juhul läks normaalkuju leidmiseks viis sammu ja tulemuseks on arv kuus. Vaatame erinevusi.
Normaaljärjekorras ei pidanud me arvutama mul 2 3, kuna abstraktsiooni kehas polnud parameetrit x kasutatud. See-eest pidime sub 5 2 kaks korda arvutama, kuna abstraktsiooni kehas on y kasutatud kaks korda.
Aplikatiivjärjekorras arvutasime nii mul 2 3 kui ka sub 5 2 välja olenemata sellest, mida funktsioon teeb. Samas ei pea me midagi topelt arvutama.
Kõigil termidel ei olegi normaalkuju. Vaatame näiteks kirjandusest tuntud makrodefinitsiooni ω = λ x. x x ning termi ω ω. Termil ω ω = (λ x. x x) (λ x. x x) on üks reedeks — kogu term (λ x. x x) (λ x. x x). Nii pole vahet, mis järjekorda reduktsiooniks eelistada — tulemus on ikka sama term.
|
Aga on ka terme, kus normaaljärjekord viib normaalkujuni aga aplikatiivjärjekord ei vii. Üks näide sellisest termist on (λ x. 1) (ω ω), mis normaaljärjekorras saavutab normaalkuju ühe sammuga (λ x. 1) (ω ω) →β 1. Aplikatiivjärjekorras tuleb aga enne funktsiooni asendamist leida argumendi normaalkuju — seda aga ei leidu.
|
Järgnevalt vaatame reduktsiooni tähtsamaid omadusi, alustades Church-Rosseri teoreemist.
Kui termi t jaoks leidub u ja v, nii et t↠βη u ja t↠βη v, siis leidub ka term k nii, et u↠βη k ja v↠βη k.
Church-Rosseri teoreemi põhiline mõte on selles, et reduktsioon ei saa halval juhul minna tupikusse nii, et algselt võimalik olnud lahendus jääb kättesaamatuks. Ebasoodne järjekorra valik võib teha redutseerimisel tööd juurde aga mitte lõpmatult palju tööd.
Kasutades Church-Rosseri teoreemi, saame näidata normaalkujude unikaalsust.
Kui termi t βη-normaalkuju eksisteerib, on see unikaalne.
Oletame, et termil t leidub βη-normaalkuju u ja βη-normaalkuju v. See tähendab, et t↠βη u ja t↠βη v. Church-Rosseri teoreemi järgi teame, et leidub k, nii et , et u↠βη k ja v↠βη k. Teame, et u ja v on βη-normaalkujul, ehk rohkem βη-reduktsioone teha ei saa. Seega u↠βη k saab olla vaid null-sammuline reduktsioon, ehk u=k. Ning ka v=k on ainuke võimalus, et v↠βη k. Seega on mõlemad normaalkujud võrdsed.
Pole selge, kuidas leida termile vastavat normaalkuju kõige paremini või kiiremini. Kõige kiirema järjekorra leidmiseks on vaja keerukat algoritmi – kui selline üldse leidub. Aga tuleb välja, et kui termil normaalkuju leidub, siis normaaljärjekord leiab selle väärtuse lõpliku arvu sammude järel.