Lambda-kalkulus
A lambda-kalkulus (vagy
A
Míg korábban a
A szócikk tárgya a
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
Mit jelent a lambda?
[szerkesztés]A görög lambda betű ([x] jelölést a szokványosabb
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
λ -absztrakció
[szerkesztés]A 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
Azon változókat, amelyeket egyetlen 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 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 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 f(x,y) = x + y függvényt. Az ennek megfelelő x = 4, y = 7 párra, azt a következő kifejezéssel tehetjük meg:
λ x.(λ y.(x + y)) 4 7 ⇒λ y.(4 + y)) 7 ⇒ 4 + 7 ⇒ 11
Magasabbrendű függvények
[szerkesztés]Egy
Vegyük például a
λ 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
Kiértékelhetőség
[szerkesztés]Az eddigi példákban a ( kifejezést. Ebben egy
„Tiszta” λ -kalkulus
[szerkesztés]A Church által definiált, „tiszta”
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
<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 (( kifejezés helyett használhatjuk az egyszerűbb ( 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
Formálisan, legyen FV(E) az E kifejezésben előforduló szabad változók
(Free Variables) halmaza, amelyet a
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 = 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 FV(E) = ∅.
Változó-behelyettesítés
[szerkesztés]Legyenek E és F tetszőleges E[v ← F] azt a (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 ( 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: (. 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:
(. 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
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 ( 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 ( 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
α -konverzió
[szerkesztés]Az intuíciónk azt súgja, hogy egy függvény (
(λ 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á →
E ≡α F ↔ E →α * E' ≡ F.
Ezentúl, ha azt mondjuk, hogy két ( és ( 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
((λ v.E) F) →β E[v ← F]
A (3 + 5) kifejezést. Ez ( kifejezéssel, ami pedig ( kifejezéssel.
A
Egy
(λ x.(x + 5)) ((λ y.y) 2))
Az egyik redex maga a teljes kifejezés, míg a másik a ( részkifejezés.
A
((λ 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
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
η -konverzió
[szerkesztés]Legyen E egy
λ x.E x →η E ( x ∉ FV(E) )
Intuitítven, 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
Fontos, hogy az
Normál forma
[szerkesztés]Az a
λ y.y 42λ x.(λ y.x + y – 18)
(λ y.y) 7 (λ x.(λ y.x + y – 18)) 2 9 (λ x.(x + 5)) ((λ y.y) 2))
Nem minden
(λ 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
(λ x.x x x) (λ x.x x x) = ⊥
Vannak olyan
(λ 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
További következménye a Church-Rosser tételnek, hogy ha egy
A normál forma fogalmát felhasználva definiálhatjuk az azonosság fogalmát
Természetes számok és alapműveleteik
[szerkesztés]A
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 3 f →
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ícójában a kulcs a (
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
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 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
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
Mielőtt nekivágnánk „valódi” programokat írni a
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
