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ás elméleti és gyakorlati megalapozásában játszott jelentős, mondhatni központi szerepe került előtérbe. (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.)
A szócikk tárgya a λ-kalkulus, eredeti, típus nélküli változata.
Történelem
Church célja eredetileg 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?
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
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ó
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. 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
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
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
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
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
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
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
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
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]