Lambda kalkulus

A lambdaszámítás ( λ-calculus ) egy formális rendszer , amelyet Alonzo Church amerikai matematikus fejlesztett ki a kiszámíthatóság fogalmának formalizálására és elemzésére .

Tiszta λ-számítás

A tiszta λ-kalkulus , amelynek kifejezései , amelyeket objektumoknak ("mindkettő") vagy λ -termeknek is neveznek, kizárólag változókból épülnek fel alkalmazás és absztrakció segítségével. Kezdetben nem feltételezzük semmilyen állandó jelenlétét.

Alkalmazás és absztrakció

A λ-számítás két alapvető műveleten alapul:

Az alkalmazás ( lat. applicatio - csatolás, csatolás) egy függvény alkalmazását vagy meghívását jelenti egy adott értékhez képest. Általában jelöli , ahol egy függvény és egy argumentum. Ez megfelel a matematikában általánosan elfogadott jelölésnek , amelyet néha szintén használnak, de ami a λ-számításhoz fontos, az az, hogy algoritmusként értelmezi, amely egy adott bemeneti értékből számítja ki az eredményt. Ebben az értelemben a -ra való alkalmazást kétféleképpen tekinthetjük: -re való alkalmazás eredményeként , vagy számítási folyamatként . Az alkalmazás utolsó értelmezése a β-redukció fogalmához kapcsolódik . $f\a$ $f$ $a$ $f(a)$ $f$ $f$ $a$ $f$ $a$ $f\a$

Az absztrakció vagy λ-absztrakció ( lat. abstractio - zavarás, elválasztás) viszont függvényeket épít fel a megadott kifejezések szerint. Ugyanis, ha egy kifejezés, amely szabadon tartalmaz -t , akkor a jelölés azt jelenti: λ az argumentum függvénye , amelynek alakja , függvényt jelöl . Így az absztrakció segítségével új függvényeket hozhat létre. Az a követelmény, hogy szabadon belépjen , nem túl fontos – elég azt feltételezni, hogy ha nem. $t\equiv t[x]$ $x$ $\ \lambda xt[x]$ $x$ $t[x]$ $x\mapsto t[x]$ $x$ $t$ $\lambda xt\equiv t$

α-ekvivalencia

A lambda kifejezésekkel definiált ekvivalencia alapvető formája az alfa ekvivalencia. Például a és : alfa-egyenértékű lambda kifejezések, és mindkettő ugyanazt a funkciót (identitásfüggvény) képviseli. A és kifejezések nem alfa-egyenértékűek, mivel nem lambda-absztrakcióban szerepelnek. $\lambda xx$ $\lambda yy$ $x$ $y$

β-redukció

Mivel a kifejezés egy függvényt jelöl, amely mindegyikhez értéket rendel , akkor a kifejezés kiértékeléséhez $\lambda x.2\cdot x+1$ $x$ $2\cdot x+1$

(\lambda x.2\cdot x+1)\ 3,

amely magában foglalja az alkalmazást és az absztrakciót is, akkor a változó helyett a 3-as szám helyettesítését kell végrehajtani a kifejezésben . Az eredmény . Ezt a gondolatot általános formában így írhatjuk le $2\cdot x+1$ $x$ $2\cdot 3+1=7$

(\lambda xt)\ a=t[x:=a]

és β-redukciónak nevezik . A forma kifejezését , vagyis egy absztrakciónak egy bizonyos kifejezésre való alkalmazását redexnek nevezzük . Bár a β-redukció lényegében a λ-számítás egyetlen „lényeges” axiómája , egy nagyon gazdag és összetett elmélethez vezet. Ezzel együtt a λ-számításnak a Turing-teljesség tulajdonsága van , ezért a legegyszerűbb programozási nyelv . $(\lambda xt)\ a$

η-transzformáció

$\eta$ A -conversion azt az elképzelést fejezi ki, hogy két függvény akkor és csak akkor azonos, ha bármely argumentumra alkalmazva ugyanazt az eredményt adják. -transzformáció fordítja le a képleteket és egymásba (csak ha nincs szabad előfordulása a :-ben : ellenkező esetben a transzformáció utáni szabad változó kötött külső absztrakcióvá válik, vagy fordítva). $\eta$ $\lambda xf\ x$ $f$ $x$ $f$ $x$

Currying (currying)

Két változó függvénye, és egy változó függvényének tekinthető, egy változó függvényét adja vissza , azaz kifejezésként . Ez a technika pontosan ugyanúgy működik bármely aritás függvényében . Ez azt mutatja, hogy sok változó függvénye kifejezhető λ-számítással, és „ szintaktikai cukor ”. Haskell Curry amerikai matematikus után a sok változó függvényének egy változó függvényévé alakításának leírt folyamatát curryingnek ( és: curryingnek is ) nevezik , bár először Moses Sheinfinkel ( 1924 ) javasolta. $x$ $y$ $f(x,y)=x+y$ $x$ $y$ $\ \lambda x.\lambda y.x+y$

A típusolatlan λ-számítás szemantikája

Az a tény, hogy a λ-kalkulus tagjai a λ-kalkulus tagjaira (vagyis talán önmagukra) alkalmazott függvényekként működnek, nehézségeket okoz a λ-kalkulus megfelelő szemantikájának megalkotásában. Ahhoz, hogy a λ-számításnak bármiféle jelentést adjunk, szükség van egy halmazra , amelybe a függvénytere beágyazódik . Általános esetben ez nem létezik e két halmaz kardinalitásaira vonatkozó korlátozások miatt, és a függvények től -ig : a másodiknak nagyobb a kardinalitása, mint az elsőnek. $D$ $D\to D$ $D$ $D$ $D$ $D$

Dana Scott az 1970-es évek elején legyőzte ezt a nehézséget azzal, hogy megkonstruálta a régió fogalmát (kezdetben teljes rácsokon [1] , majd később egy speciális topológiájú teljes, részben rendezett halmazra általánosította ), és ebben a topológiában folytonos funkciókra csökkentette . 2] . Ezen konstrukciók alapján jött létre a programozási nyelvek denotációs szemantikája különösen amiatt, hogy ezek segítségével pontos jelentést lehet adni két fontos programnyelvi konstrukciónak, mint pl. mint rekurzió és adattípusok . $D$ $D\to D$

Rekurzív függvényekhez való viszony

A rekurzió egy függvény meghatározása önmagában; első pillantásra a lambda kalkulus ezt nem teszi lehetővé, de ez a benyomás megtévesztő. Vegyünk például egy rekurzív függvényt, amely kiszámítja a faktoriálist :

f(n)=1, ha n=0; különben n × f(n - 1).

A lambda-számításban egy függvény nem hivatkozhat közvetlenül önmagára. Egy függvényhez azonban át lehet adni egy hozzá tartozó paramétert. Általában ez az érv az első. Egy függvényhez társítva egy új, már rekurzív függvényt kapunk. Ehhez egy önmagára hivatkozó argumentumot (itt jelöléssel ) kell átadni a függvénytörzsnek. $r$

g := λr. λn.(1, ha n = 0; különben n × (rr (n-1))) f := gg

Ez megoldja a faktoriális kiszámításának sajátos problémáját, de általános megoldás is lehetséges. Adott egy lambda kifejezés, amely egy rekurzív függvény vagy ciklus törzsét reprezentálja, és önmagát adja át első argumentumként, a fixpontos kombinátor visszaadja a szükséges rekurzív függvényt vagy hurkot. A függvényeknek nem kell minden alkalommal kifejezetten átadniuk magukat.

A fixpont-kombinátoroknak számos definíciója létezik. A legegyszerűbb közülük:

Y = λg.(λx.g (xx)) (λx.g (xx))

A lambda-számításban egy fix pont ; mutassuk meg: $\operátornév {Y\ g}$ ${\megjelenítési stílus \operátornév {g} }$

Y g (λh.(λx.h (xx)) (λx.h (xx))) g (λx.g (xx)) (λx.g (xx)) g((λx.g(xx))(λx.g(xx))) g (Yg)

Most, hogy a faktoriálist rekurzív függvényként definiáljuk, egyszerűen felírhatjuk , ahol az a szám, amelyre a faktoriális számít. Hadd , kapjuk: $\operatorname {g\ (Y\ g)} n$ $n$ $n=4$

g (Y g) 4 (λfn.(1, ha n = 0; és n (f(n-1)), ha n>0)) (Y g) 4 (λn.(1, ha n = 0; és n ((Y g) (n-1)), ha n>0)) 4 1, ha 4 = 0; és 4 (g(Y g) (4-1)), ha 4>0 4 (g(Y g) 3) 4 (λn.(1, ha n = 0; és n ((Y g) (n-1)), ha n>0) 3) 4 (1, ha 3 = 0; és 3 (g(Y g) (3-1)), ha 3>0) 4 (3 (g(Y g) 2)) 4 (3 (λn.(1, ha n = 0; és n ((Y g) (n-1)), ha n>0) 2)) 4 (3 (1, ha 2 = 0; és 2 (g(Y g) (2-1)), ha 2>0)) 4 (3 (2 (g(Y g) 1))) 4 (3 (2 (λn.(1, ha n = 0; és n ((Y g) (n-1)), ha n>0) 1)) 4 (3 (2 (1, ha 1 = 0; és 1 ((Y g) (1-1)), ha 1>0)) 4 (3 (2 (1)) ((Y g) 0))) 4 (3 (2 (1)) ((λn.(1, ha n = 0; és n ((Y g) (n-1)), ha n>0) 0)))) 4 (3 (2 (1 (1), ha 0 = 0; és 0 ((Y g) (0-1)), ha 0>0))) 4 (3 (2 (1 (1))) 24

Minden rekurzív függvénydefiníció a megfelelő függvény fix pontjaként ábrázolható, így a használatával minden rekurzív definíció lambda kifejezésként fejezhető ki. Különösen a természetes számok kivonását, szorzását, összehasonlítását tudjuk rekurzívan meghatározni. ${\megjelenítési stílus \operátornév {Y} }$

Programozási nyelveken

A programozási nyelvekben a "λ-kalkulust" gyakran az " anonim függvények " mechanizmusaként értelmezik - olyan visszahívási függvények, amelyek közvetlenül a felhasználásuk helyén definiálhatók, és amelyek hozzáférhetnek az aktuális függvény helyi változóihoz ( zárás ).

Lásd még

Jegyzetek

↑ Scott DS The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311-372.
↑ Scott DS Rácselméleti modellek különféle típusmentes kalkulusokhoz. — In: Proc. 4. Int. Logikai, Módszertani és Tudományfilozófiai Kongresszus, Bukarest, 1972.

Irodalom

Barendregt X. Lambda kalkulus. Szintaxisa és szemantikája: Per. angolról. — M.: Mir, 1985. — 606 p.