Lambda-kalkulus
A lambda-kalkulus (vagy λ-kalkulus) egy formális rendszer, amit eredetileg matematikai függvények tulajdonságainak (definiálhatóság, rekurzió, egyenlőség) vizsgálatára vezettek be. Az elmélet kidolgozói Alonzo Church és Stephen Cole Kleene voltak az 1930-as években. Church, 1936-ban, a λ-kalkulus segítségével bizonyította, hogy nem létezik algoritmus a híres Entscheidungsproblem (döntési probléma) megoldására. A λ-kalkulus (akárcsak a Turing-gép) lehetővé teszi, hogy pontosan (formálisan) definiáljuk, mit is értünk kiszámítható függvény alatt.
A λ-kalkulust nyugodtan nevezhetjük a legegyszerűbb általános célú programozási nyelvnek. Csak egyfajta értéket ismer: a függvényt (absztrakciót), és csak egyfajta művelet van benne: a függvény alkalmazás (változó-behelyettesítés). Ezen látszólagos egyszerűsége ellenére minden algoritmus, ami Turing-gépen megvalósítható, az megvalósítható tisztán a λ-kalkulusban is. Ez az azonosság a λ-kalkulus és a Turing-gép kifejező ereje (expressive power) között adja egyébként a Church–Turing-tézis alapját.
Míg korábban a λ-kalkulus elsősorban a kiszámíthatóságelmélet (Theory of Computation) miatt volt érdekes, napjainkban ez már kevésbé hangsúlyos, és sokkal inkább a funkcionális programozási nyelvek elméleti és gyakorlati megalapozásában játszott jelentős, mondhatni központi szerepe került előtérbe.
A szócikk tárgya a λ-kalkulus, eredeti, típus nélküli változata. A λ-kalkulus bevezetése óta számos típusos lambda-kalkulus került kifejlesztésre, és valójában ezek a típusos változatok adják a mai funkcionális programozási nyelvek alapját.
Történelem
[szerkesztés]Eredetileg Church célja egy olyan ambiciózus formális rendszer kidolgozása volt, amely segítségével a teljes matematikát tisztán formális alapokra lehetett volna helyezni. Ezt korábban már többen megpróbálták (többek között Gottlob Frege és Bertrand Russell), de nem jártak sikerrel. Amikor Church új rendszeréről is kiderült, hogy (hasonlóan Frege rendszeréhez) megfogalmazható benne a Russell-paradoxon, akkor döntött úgy, hogy a λ-kalkulus (amely a rendszere részét képezte) önmagában is hasznos lehet kiszámíthatósági problémák vizsgálatára, és így önálló elméletként fejlesztette azt tovább.
Mit jelent a lambda?
[szerkesztés]A görög lambda betű (λ) csak jelölési konvenció a kötött változó megjelölésére az utána következő kifejezésben.
A λ használata általánosan elterjedt, bár egyes francia tudományos szövegekben mai napig használják a [x] jelölést a szokványosabb λx helyett ha jelezni akarják, hogy az x változó kötött.
Jelenlegi formáját egy „evolúciós” folyamatnak köszönheti:
- Russell és Whitehead a Principia Mathematica-ban a kalap jelölést használta:
t[â]. - Church módosította a jelölést:
â.t[a], de ezt csak∧a.t[a]formában tudták az akkori nyomdászok megjeleníteni. - Végül egy újabb nyomdász kezében, valószínűleg tévedésből kialakult a végleges forma:
λa.t[a].
Informális bevezetés
[szerkesztés]A λ-kalkulus vizsgálatának tárgyai a λ-kifejezések. A λ-kifejezéseknek pontosan két fajtája létezik: λ-absztrakció és alkalmazás.
λ-absztrakció
[szerkesztés]A λ-kalkulusban a kétfajta kifejezés közül az egyik az absztrakció, vagy függvény. Vegyük például a következő
egyszerű algebrai kifejezést: 3x 5. Ha behelyettesítünk egy adott természetes számot az x változó összes előfordulási helyére, majd elvégezzük az algebrai műveleteket, akkor végeredményül egy természetes számot kapunk. x = 2 esetén például a kifejezés értéke 3*2 5 = 11 lesz. A kifejezés értéke tehát az x változó függvénye.
Annak jelölésére, hogy ez így van, az x változót kiemeljük a kifejezés elé (absztraháljuk) és λ-val jelöljük meg: λx.(3x 5). Az ilyen λ-kifejezést λ-absztrakciónak nevezzük és az x változót kötöttnek tekintjük. Mivel minden λ-absztrakció tekinthető egy egyváltozós függvénynek is (jelen esetben az x változó függvényének) ezért a λ-absztrakciót gyakran egyszerűen függvénynek nevezik. (Szigorúan véve ez a szóhasználat helytelen, hiszen nem minden függvény fejezhető ki λ-absztrakcióval és nem minden λ-absztrakció feleltethető meg függvénynek.[forrás?] Szerencsére a gyakorlati esetekben ez a megfeleltetés többnyire helytálló.) A λ-absztrakcióval definiált függvények névtelen függvények lesznek, pontosabban a teljes λ-kifejezés lesz a nevük.
Azon változókat, amelyeket egyetlen λ sem köt, szabad változóknak nevezzük. Például a λx.y kifejezésben az y szabad változó. A λx.y kifejezést bármire alkalmazva mindig y-t kapunk eredményül.
Maga az „absztrakció” elnevezés valószínűleg abból a szokásból ered, hogy a matematikusok gyakran helyettesítenek bonyolultabb kifejezéseket egyszerűbbekkel, mondjuk egy új függvény bevezetésével, ily módon emelve az „absztrakciós szintet.”
Alkalmazás
[szerkesztés]Az egyetlen művelet, amit egy λ-absztrakcióval végezhetünk, az az alkalmazás (applikáció). Az alkalmazás jelölésére egyszerűen egymás mellé írjuk a λ-absztrakciót és azt a λ-kifejezést, amire alkalmazni akarjuk. Az így kapott λ-kifejezést alkalmazásnak hívjuk. A fenti példánál maradva, λx.(3x 5) 12 azt jelenti, hogy alkalmazzuk a λx.(3x 5) függvényt 12-re. Fontos megérteni, hogy az alkalmazás a λ-kalkulusban egyszerűen változó-behelyettesítést jelent: a λx.(3x 5) (z – 4) kifejezés eredménye az alkalmazás kiértékelése után 3(z – 4) 5 lesz, amit úgy kapunk, hogy (z – 4)-et helyettesítünk az x változó összes előfordulási helyére a λ-absztrakcióban. Az alkalmazás, akárcsak a hagyományos függvény alkalmazás, balra köt: f x y = (f x) y. Tehát az f függvényt először x-re alkalmazzuk, majd az alkalmazás eredményét (ami maga is egy függvény) alkalmazzuk y-ra.
Többváltozós függvények
[szerkesztés]Többváltozós függvényeket egyváltozós függvények egymás utáni alkalmazásával definiálhatunk a λ-kalkulusban (lásd még: currying.) Vegyük például a kétváltozós f(x,y) = x y függvényt. Az ennek megfelelő λ-kifejezés a következő: λx.(λy.(x y)). Ha alkalmazni akarjuk ezt a kétváltozós függvényt a x = 4, y = 7 párra, azt a következő kifejezéssel tehetjük meg: λx.(λy.(x y)) 4 7. Nézzük meg, hogyan néz ki ennek a kifejezésnek a kiértékelése, egymás utáni változó-behelyettesítéssel:
λx.(λy.(x y)) 4 7 ⇒ λy.(4 y)) 7 ⇒ 4 7 ⇒ 11
Magasabbrendű függvények
[szerkesztés]Egy λ-absztrakciót alkalmazhatunk másik λ-absztrakcióra is (tehát a függvények alkalmazhatóak más függvényekre is).
Vegyük például a λf.(λz.(f (f z))) kifejezést, ami egy függvényre alkalmazva egy olyan kifejezést eredményez ami az f függvényt kétszer alkalmazza egymás után.
Ha ezt a függvényt alkalmazzuk a korábbi
λx.(3x 5)
kifejezésre, akkor a következő kifejezést kapjuk:
λf.(λz.(f (f z))) λx.(3x 5).
Ha elvégezzük az f változó behelyettesítését, akkor az így kapott kifejezés
λz.(λx.(3x 5) (λx.(3x 5) z))
lesz. Nézzük meg mi történik, ha ezt az új kifejezést alkalmazzuk 2-re és egymás után elvégezzük a szükséges változó-behelyettesítéseket:
λz.(λx.(3x 5) (λx.(3x 5) z)) 2 ⇒ λx.(3x 5) (λx.(3x 5) 2) ⇒ λx.(3x 5) (3*2 5) ⇒ λx.(3x 5) (6 5) ⇒ λx.(3x 5) 11 ⇒ 3*11 5 ⇒ 33 5 ⇒ 38
Az eredmény 38 amit akkor kapunk, ha az f(x) = 3x 5 függvényt kétszer egymás után alkalmazzuk 2-re: f(f(2)) = 38. Tehát a λf.(λz.(f (f z))) kifejezés valóban két egymás utáni függvényalkalmazást definiál.
Kiértékelhetőség
[szerkesztés]Az eddigi példákban a λ-kifejezések mindegyikét ki lehetett értékelni, azaz olyan formára lehetett hozni, ahol nem maradt már „tennivaló” (elvégzendő művelet.) Ez nem minden λ-kifejezésre igaz. Vegyük például a (λx.x x) (λx.x x) kifejezést. Ebben egy λ-absztrakciót önmagára alkalmazunk. Ha megpróbáljuk kiértékelni, akkor azt tapasztaljuk, hogy a változó-behelyettesítés elvégzése után ugyanazt a kifejezést kaptuk vissza. Ennek a λ-kifejezésnek (és még sok másiknak) nincs határozott értéke amihez véges kiértékelési (redukálási) lépésekkel eljuthatnánk.
„Tiszta” λ-kalkulus
[szerkesztés]A Church által definiált, „tiszta” λ-kalkulusban nincs összeadás és kivonás, sem természetes számok (pontosabban, nincsenek előre definiálva), de bevezethetők mint egyes λ-kifejezések rövidítései, ahogy azt később látni fogjuk.
Formális definíciók
[szerkesztés]Legyen V változók megszámlálhatóan végtelen halmaza: V = {a, b, c, …, x, y, z, a1, b1, c1, …} és <változó> ∈ V. Ebben az esetben a λ-kifejezések szintaxisát az alábbi környezetfüggetlen nyelvtan definiálja:
<lambda-kifejezés> → <változó> |
<lambda-absztrakció> |
<alkalmazás>
<lambda-absztrakció> → (λ<változó>.<lambda-kifejezés>)
<alkalmazás> → '(<lambda-kifejezés> <lambda-kifejezés>)
A jelölés könnyítése érdekében általában két konvenciót vezetnek be: (1) az alkalmazás balra köt és (2) a λ-absztrakciót a lehető leghosszabban kiterjesztjük jobbra. Ezek a konvenciók lehetővé teszik, hogy
sok esetben spóroljunk a zárójelekkel. Például a nyelvtan által generált ((λx.(x x)) (λy.y)) kifejezés helyett használhatjuk az egyszerűbb (λx.x x) λy.y kifejezést a félreértés veszélye nélkül.
Szabad és kötött változók
[szerkesztés]Vizsgáljuk meg az f(x) = x 5 egyváltozós függvényt. Ezt a függvényt tetszőleges számra alkalmazhatjuk és a függvény értéke minden esetben pontosan meghatározott: f(2) = 7, f(3) = 8. Vegyük azonban a g(x) = x y 5 függvényt. Ezt a függvényt alkalmazva egy számra csak egy újabb kifejezést kapunk, amiben marad egy ismeretlen változó: g(2) = y 7, g(3) = y 8. Ennek az az oka, hogy az y változó nem kötött a függvény definíciójában tehát a g függvény értéke nem csak az x váltózótól függ. A nem kötött változókat szabadnak nevezzük. Csak azt a λ-absztrakciót tekintjük függvénynek, amely nem tartalmaz szabad változókat. Azt a λ-kifejezést amelyik nem tartalmaz szabad változókat zártnak nevezzük. Annak eldöntésére, hogy egy λ-kifejezés zárt-e vagy sem, definiálni kell mikor tekintünk egy változót kötöttnek. Informálisan, egy változó akkor kötött egy λ-kifejezésben, ha tőle balra található egy λ amelyik „kiterjed rá.” Például a λx.x kifejezésben nincs szabad változó, míg a λx.y kifejezésben az y szabad változó.
Formálisan, legyen FV(E) az E kifejezésben előforduló szabad változók
(Free Variables) halmaza, amelyet a λ-kifejezéseken az alábbi szerkezeti indukcióval definiálunk:
FV(x) = {x} (változó)
FV(λx.E) = FV(E) – {x} (λ-absztrakció)
FV(E1 E2) = FV(E1) ∪ FV(E2) (alkalmazás)
Intuitíven, az E = λx.x λx.y kifejezésben egyetlen szabad változó van, y. Ugyanehhez az eredményhez eljuthatunk formálisan is, ha kiértékeljük az FV(E) kifejezést:
FV(E) =
FV(λx.x λx.y) =
FV(λx.x) ∪ FV(λx.y) =
(FV(x) – {x}) ∪ (FV(y) – {x}) =
({x} – {x}) ∪ ({y} – {x}) =
∅ ∪ {y} =
{y}
Egy λ-kifejezés E zárt, ha FV(E) = ∅.
Változó-behelyettesítés
[szerkesztés]Legyenek E és F tetszőleges λ-kifejezések és v egy tetszőleges változó. Jelölje E[v ← F] azt a λ-kifejezést, amit úgy kapunk E-ből, hogy v minden szabad előfordulását F-re cseréljük. Tehát (x 4)[x ← 8] = (8 4) és (x 4)[x ← (y - 3)] = ((y - 3) 4).
A változó-behelyettesítés mechanikus végrehajtása kézenfekvőnek tűnik de néhány esetben egy kis körültekintésre van szükség különben nem helyes eredményt kapunk. Vegyük például a (λx.y 5) kifejezést amelyben y az egyetlen szabad változó. Intuitíve
az egyes változók konkrét neve nem lényeges, ezért megtehetjük, hogy y-t átnevezzük mondjuk z-nek: (λx.y 5)[y ← z] = (λx.z 5). A kifejezés jelentése ettől az átnevezéstől még nem változott. Végezzük el azonban a következő behelyettesítést:
(λx.z 5)[z ← x] = (λx.x 5). Az új kifejezésben már nincs egyetlen szabad változó sem, tehát a kifejezés jelentése megváltozott. Könnyű észrevenni, a gondot az okozta, hogy z egy olyan környezetben fordult elő amelyikben az x változó kötöttnek számít. Amikor z helyére x került, ez az új változó-előfordulás szabadból kötötté vált. Ezt a jelenséget nevezzük változó-elfogásnak (variable capture). Mivel a változó-elfogás megváltoztatja a λ-kifejezés jelentését, ezért szeretnénk úgy definiálni a változó-behelyettesítést, hogy ezt a lehetőséget kiküszöböljük.
A változó-behelyettesítés formális definíciójához szerkezeti indukciót használunk:
x[v ← F] = F (x = v)
x[v ← F] = x (x ≠ v)
(E1 E2)[v ← F] = E1[v ← F] E2[v ← F]
(λx.E)[v ← F] = (λx.E) (x = v)
(λx.E)[v ← F] = (λx.E[v ← F]) (x ≠ v és x ∉ FV(F))
(λx.E)[v ← F] = (λz.E[x ← z][v ← F]) (x ≠ v és x ∈ FV(F) és z ∉ (FV(E) ∪ FV(F)))
A fenti szabályokból kiderül, hogy a változó-elfogást a kötött változó átnevezésével kerüljük el. A korábbi (λx.z 5)[z ← x] példa esetében például változó-elfogás fenyeget, ezért a kötött változót (jelen esetben x-et) le kell cserélnünk egy új változóra, amelyik nem okoz ütközést, mondjuk w-re. A behelyettesítés eredménye a formális szabályok szerint tehát (λw.x 5) lesz, azaz az x változó nem válik kötötté, mint a korábbi, naiv behelyettesítés esetén történt.
Szintaktikai egyezőség
[szerkesztés]Két λ-kifejezés szintaktikailag egyező (≡) ha pontosan ugyanazzal a karaktersorozattal írhatók le. Ezek alapján λx.x ≡ λx.x de λx.x ≢ λy.y. A szintaktikai egyezőség önmagában nem túl hasznos, de segít definiálni bonyolultabb konverziókat. Általában amikor azt mondjuk, hogy egy konverzió egy λ-kifejezést egy másikba visz át, ezalatt azt értjük, hogy a konverzió végrehajtása után a két λ-kifejezés szintaktikailag egyező.
α-konverzió
[szerkesztés]Az intuíciónk azt súgja, hogy egy függvény (λ-absztrakció) jelentése nem változik meg attól ha átnevezzük benne a kötött változókat. A λx.(x x) ugyanazt a függvényt definiálja, mint a λy.(y y) vagy a λz.(z z).
Ez a felismerés motiválja az α-konverzió (alfa-konverzió) definícióját:
(λx.E) →α (λw.E[x ← w]) (w ∉ FV(E)) (E F) →α (E' F) (E →α E') (E F) →α (E F') (F →α F')
Jelölje továbbá →α* α-konverziók véges (akár nulla) hosszúságú sorozatát.
Két λ-kifejezés E és F α-ekvivalens (≡α), ha létezik α-konverziók olyan véges sorozata, amelyik az egyiket a másikba viszi át:
E ≡α F ↔ E →α* E' ≡ F.
Ezentúl, ha azt mondjuk, hogy két λ-kifejezés egyező, ezalatt mindig azt értjük, hogy α-ekvivalensek. Ennek az az oka, hogy az α-ekvivalencia egyszerűen a kötött változók átnevezgetését jelenti, ami érdemben nem befolyásolja a λ-kifejezés jelentését. Tehát
a (λx.x) (λy.y y) és (λz.z) (λv.v v) kifejezéseket egyezőnek tekintjük:
(λx.x) (λy.y y) →α (λz.z) (λy.y y) →α (λz.z) (λv.v v) ≡ (λz.z) (λv.v v)
β-konverzió és β-redukció
[szerkesztés]A β-konverzió (béta-konverzió) a függvény-alkalmazás elnevezése a λ-kalkulusban. Amikor egy λ-absztrakciót alkalmazunk egy λ-kifejezésre, akkor a λ-kifejezést behelyettesítjük a λ-val kötött változó szabad előfordulásainak helyeire. Formálisan:
((λv.E) F) →β E[v ← F]
A β-konverzió, akárcsak az α-konverzió, egy ekvivalencia-relációt definiál a λ-kifejezéseken. A β-konverzió, a látszat ellenére, szimmetrikus reláció. Vegyük például a (3 5) kifejezést. Ez β-ekvivalens a (λx.(x 5)) 3 kifejezéssel, ami pedig β-ekvivalens a (λy.(λx.(x y))) 3 5 kifejezéssel.
A β-konverzió aszimmetrikus változata a β-redukció. A β-redukció legfontosabb szerepe a λ-kifejezések szisztematikus kiértékelésében van. A β-redukció esetén mindig a „nyíl irányában” haladunk, azaz végrehajtjuk a kijelölt függvény-alkalmazásokat, ilymódon redukálva a λ-kifejezést.
Egy λ-kifejezésben egyszerre több alkalmazás is várhat kiértékelésre. Ezeket az alkalmazásokat redukálható részkifejezéseknek, röviden „redex”-nek (Reducible Expression) nevezzük. A β-redukció definíciójában nincs megkötés arra, hogy ezeket milyen sorrendben kell elvégezni, de a választott sorrendnek jelentősége van. A választott kiértékelési sorrendet kiértékelési stratégiának nevezzük. Az alábbi λ-kifejezés például két redexet is tartalmaz:
(λx.(x 5)) ((λy.y) 2))
Az egyik redex maga a teljes kifejezés, míg a másik a (λy.y) 2 részkifejezés.
A β-redukcióval tehát két „irányba” is továbbléphetünk. Példaképpen hasonlítsuk össze a két lehetséges β-redukció eredményét:
((λy.y) 2) 5 ←β (λx.(x 5)) ((λy.y) 2)) →β (λx.(x 5)) 2
Az eredményül kapott kifejezések jelentősen eltérnek, de mindkettőben lehetőség van még további β-redukció elvégzésére:
2 5 ←β ((λy.y) 2) 5 ←β … →β (λx.(x 5)) 2 →β 2 5
Végeredményül mindkét esetben ugyanazt a kifejezést kaptuk, bár más lépések során jutottunk el hozzájuk. Az, hogy ez így történt, korántsem véletlen, hanem a λ-kifejezések kiértékelésének alapvető tulajdonsága, amely a normál formákkal függ szorosan össze.
η-konverzió
[szerkesztés]Legyen E egy λ-kifejezés és x egy változó amelyik nem szabad E-ben. Ekkor az η-konverziót (eta-konverziót) az alábbi módon definiálhatjuk:
λx.E x →η E ( x ∉ FV(E) )
Intuitítven, az η-konverzió azt fejezi ki, hogy egy λ-absztrakció jelentése nem változik meg attól, hogy „beburkoljuk” egy újabb λ-absztrakcióba. Ennek az oka az, hogy egy tetszőleges F kifejezésre alkalmazva a „beburkolt” absztrakciót, egyetlen β-redukciós lépéssel eljuthatunk az E F „eredeti” alkalmazáshoz amit akkor kapnánk, ha közvetlenül E-t alkalmaznánk F-re:
(λx.E x) F →β E F
Más szóval, mindegy, hogy E-t, vagy λx.E x-t alkalmazzuk F-re, hiszen a β-redukció elvégzése után ugyanazt az eredményt kapjuk.
Fontos, hogy az η-konverzióval „eldobott” változó ne legyen szabad E-ben, különben a kifejezés jelentése megváltozik. Például a λx.x x kifejezésre nem alkalmazható az η-konverzió mert E = x tehát x szabad E-ben.
Normál forma
[szerkesztés]Az a λ-kifejezés amelyben nincs egyetlen redukálható részkifejezés sem, normál formában van. A λ-kifejezések kiértékelésének célja tehát a normál forma elérése, egymás utáni β-redukciókkal. Példák normál formában lévő λ-kifejezésekre:
λy.y 42 λx.(λy.x y – 18)
λ-kifejezések, amelyek még nincsenek normál formában:
(λy.y) 7 (λx.(λy.x y – 18)) 2 9 (λx.(x 5)) ((λy.y) 2))
Nem minden λ-kifejezés hozható normál formára. Vannak olyan esetek, amikor mindig marad redukálható részkifejezés így a β-redukció a végtelenségig folytatható:
(λx.x x x) (λx.x x x) →β (λx.x x x) (λx.x x x) (λx.x x x) →β (λx.x x x) (λx.x x x) (λx.x x x) (λx.x x x) →β …
Ezen λ-kifejezésekre azt mondjuk, divergálnak és a jelölésükre egy speciális szimbólumot vezetünk be: ⊥. Ha azt szeretnénk kijelenteni egy λ-kifejezésről, hogy divergál, akkor azt a következőképpen tehetjük meg:
(λx.x x x) (λx.x x x) = ⊥
Vannak olyan λ-kifejezések, amelyek a kiértékelési stratégiától függően divergálnak vagy sem. Vegyük például a következő λ-kifejezést és használjuk azt a kiértékelési stratégiát, amelyik mindig a legjobboldalibb redexet redukálja:
(λy.8) ((λx.x x x) (λx.x x x)) →β (λy.8) ((λx.x x x) (λx.x x x) (λx.x x x)) →β (λy.8) ((λx.x x x) (λx.x x x) (λx.x x x) (λx.x x x)) →β …
Ezzel szemben ha olyan kiértékelési stratégiát választunk amely mindig a legbaloldalibb redexet redukálja, gyorsan eljutunk a kifejezés normál formájához:
(λy.8) ((λx.x x x) (λx.x x x)) →β 8
A Church-Rosser tétel azt mondja ki (többek között), hogy ha egy λ-kifejezésnek van normál formája, akkor ahhoz véges redukciós lépések sorozatával eljuthatunk, ha mindig a legbaloldalibb redukálható részkifejezést redukáljuk. (Ez az eredmény egyben egy kiértékelési algoritmust is ad a kezünkbe.) Ugyanezen okokból egyébként a lusta funkcionális programozási nyelvek is ezt a kiértékelési stratégiát használják.
További következménye a Church-Rosser tételnek, hogy ha egy λ-kifejezés semmilyen kiértékelési stratégia mellett nem divergál, akkor bármilyen kiértékelési stratégiát választva ugyanahhoz a normál formához jutunk el.
A normál forma fogalmát felhasználva definiálhatjuk az azonosság fogalmát λ-kifejezéseken: két λ-kifejezés azonos, ha α-ekvivalens normál formára hozhatóak véges számú β-redukciós lépéssel.
Természetes számok és alapműveleteik
[szerkesztés]A λ-kalkulus formális definíciójában nem szerepelnek sem a természetes számok, sem a rajtuk végzett alapműveletek (összeadás, szorzás stb.) Ezeket utólag, összetettebb λ-kifejezések rövidítéseiként vezethetjük be. Fontos megjegyezni, hogy az alább következő definíciók jelentősége inkább elméleti, mintsem gyakorlati: a λ-kalkulus kifejező erejét hivatottak bizonyítani. Azon programozási nyelvek amelyek a λ-kalkulusra épülnek (funkcionális programozási nyelvek) a természetes számokat a nyelv részének tekintik és belső megvalósításukra alacsony szintű és hatékony primitíveket használnak.
A természetes számok bevezetésére a legelterjedtebb a Church egészek használata:
0 := λf.λx.x 1 := λf.λx.f x 2 := λf.λx.f (f x) 3 := λf.λx.f (f (f x)) …
Egy Church egész n tehát egy magasabbrendű függvényt definiál a λ-kalkulusban amelyet egy egyváltozós függvényre f alkalmazva visszaadja annak n-edik hatványát. Például: 3 f →β f3
A Church egészek definícióját felhasználva definiálhatjuk a rákövetkező (SUCCessor) függvényt amely n-re alkalmazva n 1-et ad:
SUCC := λn.λf.λx.f (n f x)
Példa:
SUCC 1 := (λn.λf.λx.f (n f x)) 1 →β λf.λx.f (1 f x) := λf.λx.f ((λf.λx.f x) f x) →β λf.λx.f ((λx.f x) x) →β λf.λx.f (f x) := 2
Az összeadást (PLUS) az alább módon definiálhatjuk:
PLUS := λm.λn.λf.λx.m f (n f x) ( m n )
Példaképpen érdemes ellenőrizni, hogy a PLUS 2 1 kifejezés valóban 3-at ad eredményül:
PLUS 2 1 := λm.λn.λf.λx.m f (n f x) 2 1 →β λn.λf.λx.2 f (n f x) 1 →β λf.λx.2 f (1 f x) := λf.λx.2 f ((λf.λx.f x) f x) →β λf.λx.2 f ((λx.f x) x) →β λf.λx.2 f (f x) := λf.λx.(λf.λx.f (f x)) f (f x) →β λf.λx.(λx.f (f x)) (f x) →β λf.λx.f (f (f x)) := 3
A szorzást (MULTiplication) az összeadást felhasználva definiáljuk:
MULT := λm.λn.m (PLUS n) 0 ( m * n )
Informálisan, az n*m szorzat felfogható úgy is, mintha n-et m-szer hozzáadnánk 0-hoz.
Az alapműveletek bevezetését a fenti stílusban lehet folytatni, de a további definíciók némelyike már elég sok leleményességet igényel. Vegyük például a megelőző (PREDecessor) függvényt amely n-re alkalmazva n–1-et ad vissza:
PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u) ( n – 1 )
Példaképpen érdekes ellenőrizni, hogy a fenti definíció valóban helyesen működik:
PRED 1 := (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)) 1 →β λf.λx.1 (λg.λh.h (g f)) (λu.x) (λu.u) := λf.λx.(λk.λy.k y) (λg.λh.h (g f)) (λu.x) (λu.u) →β λf.λx.(λy.(λg.λh.h (g f)) y) (λu.x) (λu.u) →β λf.λx.(λg.λh.h (g f)) (λu.x) (λu.u) →β λf.λx.(λh.h ((λu.x) f)) (λu.u) →β λf.λx.(λu.u) ((λu.x) f) →β λf.λx.(λu.x) f →β λf.λx.x := 0
A PRED fenti definíciójában a kulcs a (λu.x) függvény, amely „eldob” egy függvényalkalmazást, így az eredeti n-edik hatvány helyett az n – 1-edik hatványt kapjuk, ami a Church egészek definíciója szerint pontosan a megelőző természetes szám lesz. További fontos tulajdonsága a PRED függvénynek, hogy nullára alkalmazva nullát ad eredményül, tehát a PRED függvény nem vezet ki a természetes számok halmazából.
A PRED függvény segítségével definiálhatjuk a kivonás (MINUS) műveletét:
MINUS := λm.λn.n PRED m ( m – n )
Az m – n művelet felfogható úgy is, hogy m-re n-szer alkalmazzuk a megelőző (PRED) függvényt. A PRED függvény tulajdonságaiból következően ha egy nagyobb számot kivonunk egy kisebből, akkor nullát kapunk eredményül, tehát a MINUS függvény sem vezet ki a természetes számok halmazából.
Természetesen az osztás művelete is definiálható a λ-kalkulusban, de ehhez előbb szükség lesz a rekurzív függvények bevezetésére.
Boole-algebra és predikátumok
[szerkesztés]A logikai igazságértékeket (TRUE = igaz, FALSE = hamis) az alábbi módon szokás definiálni:
TRUE := λu.λv.u FALSE := λu.λv.v
Mint minden kifejezés, így a logikai igazságértékek is csak függvények a λ-kalkulusban: a TRUE függvény egyszerűen „eldobja” a második paraméterét, míg a FALSE függvény az első paraméterével teszi ugyanezt. Ez az ábrázolásmód eredetileg Churchtől származik, ezért a fenti függvényeket Church boolean-oknak is nevezik.
A Church booleanok segítségével definiálhatjuk a logikai műveleteket (AND = logikai és, OR = logikai vagy, NOT = tagadás):
AND := λu.λv.u v FALSE OR := λu.λv.u TRUE v NOT := λb.λu.λv.b v u
Ellenőrzésképpen elvégezhetjük egy egyszerű logikai kifejezés kiértékelését:
AND TRUE FALSE := (λu.λv.u v FALSE) TRUE FALSE := (λu.λv.u v FALSE) (λx.λy.x) FALSE →β (λv.(λx.λy.x) v FALSE) FALSE →β (λx.λy.x) FALSE FALSE →β λy.FALSE FALSE →β FALSE
Ahhoz, hogy a későbbiekben programokat tudjunk írni a λ-kalkulusban, szükségünk lesz egy függvényre, amellyel választani tudunk két különböző alternatíva között:
IFTHENELSE := λb.λu.λv.b u v
A magyar szakirodalomban ezt a függvényt az előkelő vezérlési szerkezet néven nevezik, mert ez teszi lehetővé feltételes kifejezések írását. Ha az IFTHENELSE függvény első paramétere egy b Church boolean, akkor a kifejezés jelentése: HA b AKKOR u EGYÉBKÉNT v. Érdemes megemlíteni, hogy λ-kalkulusban nincsenek utasítások, ezért a feltételes „utasítás” is csak egy függvény. A C programozási nyelvben járatosak számára hasznos analógia lehet a háromoperandusú feltételes kifejezésre gondolni: boolean-kifejezés ? kifejezés1 : kifejezés2.
Mielőtt nekivágnánk „valódi” programokat írni a λ-kalkulusban, szükségünk lesz függvényekre, amelyek logikai teszteket végeznek el. Ezen függvényeket predikátumoknak nevezzük. A későbbiek szempontjából hasznos lesz egy olyan predikátumot definiálni, amelyikkel megvizsgálhatjuk, hogy egy adott természetes szám egyenlő-e nullával (n egy Church-egész):
ISZERO := λn.n (λx.FALSE) TRUE
Aki járatos valamennyire az Assembly programozási nyelvben, azt talán nem éri meglepetésként, hogy ennek az egyetlen predikátumnak a segítségével definiálhatóak a szokásos algebrai relációs műveletek a természetes számokon:
GT := λx.λy.NOT (ISZERO (MINUS x y)) ( x > y ) EQ := λx.λy.NOT (OR (GT x y) (GT y x)) ( x = y ) GE := λx.λy.OR (GT x y) (EQ x y) ( x ≥ y ) LT := λx.λy.GT y x ( x < y ) LE := λx.λy.GE y x ( x ≤ y )
Irodalom
[szerkesztés]Csörnyei Zoltán: Lambda-kalkulus. Typotex Kiadó, 2007. ISBN 978-963-9664-46-3
Kapcsolódó szócikkek
[szerkesztés]Ha a λ-kalkulusból „kivesszük” λ-absztrakciót és csak az alkalmazást engedjük meg, akkor az így kapott rendszer kombinátor logika lesz.
