Betareduktiolla

Betareduktiolla tarkoitetaan lambda-kalkyylin ilmaisujen soveltamista funktiolle antamalla argumentti. Perusmuotoinen beta-reduktio on ilmaisun muutos (λx. M) N → M[x := N], eli x:n esiintymät M:ssä korvataan N:llä. Tällainen ilmaisua kutsutaan redexiksi (beta-redex). Kun ilmaisulla ei ole enää beetareduktiota mahdollisuutta, puhutaan beta-normaalimuodosta.

Redeksiä käytetään kuvauksessa evaluoinnista: beta-reduktio kuvaa suoraa soveltamisen mekanismia lambda-kalkyylissä. Eri evaluointistrategioissa ratkaiseva kysymys on, missä järjestyksessä redexit otetaan käsittelyyn. Beta-normaalimuoto on tila, jossa ei ole enää minkäänlaista beta-reduktiota mahdollisesti.

Substituutio ja muuttujien nimeäminen ovat olennaisia: M[x := N] tarkoittaa x:n korvaamista N:llä M:ssä. Tapahtuu riskia muuttujien vangitsemisesta, jolloin vapaiden ja sidottujen muuttujien erottaminen on tärkeää. Alpha-konversion avulla sidottuja muuttujia voidaan nimetä uudelleen ennen substituutiota, jotta vangitseminen vältetään.

Esimerkkejä:

- (λx. x) a voidaan muuttaa muotoon a.

- ((λx. λy. x y) a) b etenee askeleittain: (λx. λy. x y) a → β (λy. a y); sitten (λy. a y) b → β a b.

Merkitys: Betareduktio on keskeinen käsite teoreettisessa laskennassa ja toimivan ohjelmoinnin perusta useissa funktionaalisissa kielissä (kuten Haskell, Scheme, OCaml). Se mahdollistaa funktioiden soveltamisen ja evaluoinnin, ja sen käsitteet liittyvät myös konfluenceen (Church-Rosserin ominaisuus) sekä normalisointiin.