Történeti áttekintés

A λ-kalkulus (λC) első definícióját Church adta meg 1932-33-ban. A cél az volt, hogy a teljes matematika formális leírására létrehozzon egy rendszert. Később kiderült, hogy ellentmondások is leírhatók a rendszerrel, így erre a célra nem volt megfelelő.

A függvények vizsgálatára viszont tökéletes volt, ez volt az első eszköz, mellyel a függvények kiszámíthatósága megvalósíthatóvá vált. A λ-kalkulus egyszerű, konzisztens matematikai rendszer, nincsenek benne paradoxonok, ellentmondások (noha képesek vagyunk ellentmondásokat is leírni benne!). Ebben a rendszerben a rekurzió is leírható rekurzió nélkül.

Érdekességképpen érdemes megjegyezni, hogy a λC ekvivalens a kombinátorlogikával, illetve, hogy minden funkcionális program egy λ-kifejezésnek tekinthető.

Egyszerű típusnélküli λ-kifejezések:

Tfh. adott egy nem feltétlenül véges, egymástól páronként különböző változókat, a λ jelet, a pontot, a nyitó és csukózárójelet tartalmazó halmaz. Ezen a halmazon, mint ábécén értelmezett λ kifejezések ekkor:
<λ-kifejezés> ::= <változó> | <λ-absztrakció> | <applikáció>
<λ-absztrakció> ::= (λ<változó>.<λ-kifejezés>)
<applikáció> ::= (<λ-kifejezés><λ-kifejezés>)

λ-absztrakció:

Ha E egy λ-kifejezés és x egy változó, akkor a λx.E λ-kifejezést λ-absztrakciónak, az x változót a λ-absztrakció változójának vagy formális paraméterének, az E λ-kifejezést a λ-absztrakció törzsének nevezzük.
Az E kifejezés a λ-absztrakció x változójának hatásköre, és azt mondjuk, hogy a hatáskörébe tartozó x változót a λ-absztrakció x változója köti (x kötött változó).
Megjegyzések:

1. A λ-absztrakció jobbaszociatív.
2. Amelyik változó nem kötött az szabad.
   

A 2 λ-absztrakció amivel minden leírható:

I = λx.x, K = λxy.x, S = λxyz.xz(yz).
Szemfülesek észrevehetik, hogy ez 3 függvény, I (identitás) csak kényelmi okokból van, de I előáll, mint: SKK.
No, akkor a webbencsel itt meg is lennénk, I, K és S függvényekből előáll, akármi is a webbencs. Egy gondunk lehet, ha a webbencs aljas módon rekurzívan definiálja magát. Ezen könnyen segíthetünk, elég lesz megmutatni, hogy rekurzió valójában nincs is:)

Applikáció:

Ha E és F λ-kifejezések, akkor az EF λ-kifejezést applikációnak nevezzük. Ha E egy λ-absztrakció, akkor az EF neve függvényapplikáció, ahol az F az E λ-kifejezés aktuális paramétere.

A rekurzió csak látszat."

Igen, ezt is megértünk, a rekurzió csak egy applikáció semmi több. Ja, és típus sincs, de most számoljunk le a rekurzióval:
Vegyük példának mondjuk a faktoriálist:

1. fac(n) = n*fac(n-1) ha n>1
2. fac = λn.* n fac (- n 1) (itt még megvan a rekurzió)
3. fac = (λf.λn.* n f (- n 1))fac , nevezzük (λf.λn.* n f (- n 1))-t H-nak, tehát:
4. fac = H fac , ahol H-nak kellene megkeresni a fixpontját.

Mindenki emlékszik, mi is a függvény fixpontja ugye? Aki nem, annak pár példa:

1. (λx.6)-nak egy fixpontja van, a 6
2. (λx.- 12 x)-nek egy fixpontja van, a 6
3. (λx.* x x)-nek két fixpontja van, a 0 és 1
4. (λx.* 1 x)-nek végtelen sok fixpontja van
5. (λx.+ 1 x)-nek nincs fixpontja

No, akkor keressünk egy Y-t, ami meghatározza H fixpontját, vagyis: fac = Y H
Legyen Y = λx.(λy.x(yy))(λy.x(yy)) (ezt Chuch találta), ekkor Y H = H (Y H). Y-t nevezik paradoxonkombinátornak is.
És no lám, az Y H = H (Y H)-ban egy kicsi rekurzió sincs. A paradoxonkombinátorokból Dunát lehetne rekeszteni, manapság mindenki csinál magának egyet.
Úgyhogy ha a webbencs rekurzívan van definiálva, akkor sincs baj, hiszen a rekurzió csak látszat.

2008. Szeptember 22. 3:21