Lambda kalkul je formálny systém v matematickej logike na vyjadrenie výpočtov založených na abstrakcii a aplikovanie funkcií pomocou väzieb a premenných substitúcií. Ide o univerzálny model, ktorý je možné aplikovať na dizajn akéhokoľvek Turingovho stroja. Lambda kalkul bol prvýkrát predstavený Churchom, slávnym matematikom, v 30. rokoch 20. storočia.
Systém pozostáva z budovania členov lambda a vykonávania operácií redukcie na nich.
Vysvetlenia a aplikácie
Grécke písmeno lambda (λ) sa používa vo výrazoch lambda a výrazoch lambda na označenie väzby premennej vo funkcii.
Lambda kalkul môže byť nezadaný alebo napísaný. V prvom variante možno funkcie použiť len vtedy, ak sú schopné prijímať dáta tohto typu. Typizované lambda calculi sú slabšie, môžu vyjadrovať menšiu hodnotu. Ale na druhej strane vám umožňujú dokázať viac vecí.
Jedným z dôvodov, prečo existuje toľko rôznych typov, je túžba vedcov urobiť viac bez toho, aby sa vzdali príležitosti dokázať silné vety o lambda počte.
Systém má aplikácie v mnohých rôznych oblastiach matematiky, filozofie, lingvistiky a informatiky. Po prvé, lambda kalkul je kalkul, ktorý zohral dôležitú úlohu vo vývoji teórie programovacích jazykov. Sú to štýly funkčnej tvorby, ktoré systémy implementujú. Sú tiež horúcou témou výskumu v teórii týchto kategórií.
Pre figuríny
Lambda kalkul zaviedol matematik Alonzo Church v 30. rokoch 20. storočia ako súčasť svojho výskumu základov vedy. Pôvodný systém sa ukázal ako logicky nekonzistentný v roku 1935, keď Stephen Kleen a J. B. Rosser vyvinuli Kleene-Rosserov paradox.
Neskôr, v roku 1936, Church vybral a zverejnil iba časť, ktorá je relevantná pre výpočty, čo sa dnes nazýva netypový lambda kalkul. V roku 1940 tiež predstavil slabšiu, ale logicky konzistentnú teóriu známu ako systém hlavného typu. Vo svojej práci vysvetľuje celú teóriu jednoduchými termínmi, takže sa dá povedať, že Church publikoval calculus lambda for dummies.
Až do 60. rokov 20. storočia, keď sa jeho vzťah k programovacím jazykom vyjasnil, bol λ len formalizmus. Vďaka aplikáciám Richarda Montagu a iných lingvistov v sémantike prirodzeného jazyka zaujala kalkulácia čestné miesto v lingvistike aj v informatike.
Pôvod symbolu
Lambda neznamená slovo ani skratku, pochádza z odkazu v Russell's Principal Mathematics, po ktorom nasledujú dve typografické zmeny. Príklad zápisu: pre funkciu f s f (y)=2y + 1 je 2ŷ + 1. A tu na označenie vstupnej premennej použijeme striešku („klobúk“) nad y.
Cirkev pôvodne zamýšľala používať podobné symboly, ale sadzači nedokázali umiestniť symbol „klobúka“nad písmená. Namiesto toho to pôvodne vytlačili ako "/\y.2y+1". V ďalšej epizóde úprav nahradili pisári „/ \“vizuálne podobným znakom.
Úvod do lambda kalkulu
Systém pozostáva z jazyka termínov, ktoré sú zvolené určitou formálnou syntaxou, a súboru transformačných pravidiel, ktoré umožňujú manipuláciu s nimi. Posledný bod možno považovať za rovnicovú teóriu alebo za operačnú definíciu.
Všetky funkcie v lambda kalkule sú anonymné, čo znamená, že nemajú mená. Berú iba jednu vstupnú premennú a na implementáciu grafov s viacerými premennými sa používa currying.
Lambda výrazy
Syntax výpočtu definuje niektoré výrazy ako platné a iné ako neplatné. Rovnako ako rôzne reťazce znakov sú platné programy C a niektoré nie sú. Skutočné vyjadrenie lambda kalkulu sa nazýva "lambda termín".
Nasledujúce tri pravidlá poskytujú induktívnu definíciu, ktorá môže byťpoužiť na konštrukciu všetkých syntakticky platných pojmov:
Premenná x samotná je platným výrazom lambda:
- ak T je LT a x je nekonštantné, potom (lambda xt) sa nazýva abstrakcia.
- ak T ako aj s sú pojmy, potom (TS) sa nazýva aplikácia.
Nič iné nie je výraz lambda. Koncept je teda platný vtedy a len vtedy, ak ho možno získať opakovaným uplatňovaním týchto troch pravidiel. Niektoré zátvorky však môžu byť vynechané podľa iných kritérií.
Definícia
Lambda výrazy pozostávajú z:
- premenné v 1, v 2, …, v n, …
- symboly abstrakcie 'λ' a bodka '.'
- zátvorky ().
Množinu Λ je možné definovať indukčne:
- Ak x je premenná, potom x ∈ Λ;
- x nie je konštantné a M ∈ Λ, potom (λx. M) ∈ Λ;
- M, N ∈ Λ, potom (MN) ∈ Λ.
Označenie
Na zachovanie prehľadnosti zápisu výrazov lambda sa bežne používajú tieto konvencie:
- Vonkajšie zátvorky sú vynechané: MN namiesto (MN).
- Predpokladá sa, že aplikácie zostanú asociatívne: namiesto ((MN) P je možné napísať MNP).
- Telo abstrakcie siaha ďalej doprava: λx. MN znamená λx. (MN), nie (λx. M) N.
- Postupnosť abstrakcií je zredukovaná: λx.λy.λz. N môže byť λxyz. N.
Voľné a viazané premenné
Operátor λ spája svoju nekonštantu kdekoľvek v tele abstrakcie. Premenné, ktoré spadajú do rozsahu, sa nazývajú viazané. Vo výraze λ x. M, časť λ x sa často označuje ako spojivo. Akoby naznačoval, že premenné sa stanú skupinou s pridaním X x k M. Všetky ostatné nestabilné sa nazývajú voľné.
Napríklad vo výraze λ y. x x y, y - viazané netrvalé a x - voľné. A tiež stojí za zmienku, že premenná je zoskupená podľa svojej „najbližšej“abstrakcie. V nasledujúcom príklade je riešenie lambda kalkulu reprezentované jediným výskytom x, ktorý súvisí s druhým výrazom:
λ x. y (λ x. z x)
Množina voľných premenných M sa označuje ako FV (M) a je definovaná rekurziou cez štruktúru pojmov takto:
- FV (x)={x}, kde x je premenná.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Vzorec, ktorý neobsahuje voľné premenné, sa nazýva uzavretý. Uzavreté výrazy lambda sú známe aj ako kombinátory a sú ekvivalentné výrazom v kombinatorickej logike.
Skratka
Význam výrazov lambda je určený tým, ako sa dajú skrátiť.
Existujú tri typy strihov:
- α-transformácia: zmena viazaných premenných (alfa).
- β-redukcia: použitie funkcií na ich argumenty (beta).
- η-transform: pokrýva pojem extenzionality.
Aj tu jehovoríme o výsledných ekvivalenciách: dva výrazy sú β-ekvivalentné, ak sa dajú β-transformovať na rovnakú zložku, a α / η-ekvivalencia je definovaná podobne.
Pojem redex, skratka pre redukovateľný obrat, sa vzťahuje na podtémy, ktoré možno znížiť jedným z pravidiel. Lambda počet pre figuríny, príklady:
(λ x. M) N je beta redex vo výraze na nahradenie N x v M. Zložka, na ktorú sa redex redukuje, sa nazýva jeho redukcia. Zníženie (λ x. M) N je M [x:=N].
Ak x nie je voľné v M, λ x. M x tiež em-REDEX s regulátorom M.
α-transformation
Alfa premenovania vám umožňujú zmeniť názvy viazaných premenných. Napríklad x. x môže dať λ y. r. Pojmy, ktoré sa líšia iba v alfa transformácii, sa považujú za α-ekvivalentné. Pri použití lambda kalkulu sa α-ekvivalenty často považujú za recipročné.
Presné pravidlá pre konverziu alfa nie sú úplne triviálne. Po prvé, pri tejto abstrakcii sa premenujú iba tie premenné, ktoré sú spojené s rovnakým systémom. Napríklad alfa transformácia λ x.λ x. x môže viesť k λ y.λ x. x, ale nemusí to viesť k λy.λx.y To posledné má iný význam ako originál. Je to analogické s konceptom programovania variabilného tieňovania.
Po druhé, alfa transformácia nie je možná, ak by bola zachytená inou nestálou abstrakciou. Ak napríklad nahradíte x za y v λ x.λ y. x, potom môžete získaťλy.λy. u, čo vôbec nie je to isté.
V programovacích jazykoch so statickým rozsahom možno na zjednodušenie rozlíšenia mien použiť konverziu alfa. Zároveň dbajte na to, aby pojem premennej nezakrýval označenie v oblasti, ktorá obsahuje.
V zápise indexu De Bruyne sú akékoľvek dva alfa-ekvivalentné výrazy syntakticky totožné.
Výmena
Zmeny zapísané E [V:=R] sú procesom nahradenia všetkých voľných výskytov premennej V vo výraze E obratom R. Substitúcia v zmysle λ je definovaná lambda rekurzie počet na štruktúre konceptu takto (poznámka: x a y - iba premenné a M a N - ľubovoľný λ-výraz).
x [x:=N] ≡ N
y [x:=N] ≡ y, ak x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]), ak x ≠ y, za predpokladu, že y ∉ FV (N).
Pre substitúciu do lambda abstrakcie je niekedy potrebné α-transformovať výraz. Napríklad nie je pravda, že (λ x. Y) [y:=x] vedie k (λ x. X), pretože substituované x by malo byť voľné, ale nakoniec bolo viazané. Správna náhrada je v tomto prípade (λ z. X) až do α-ekvivalencie. Všimnite si, že substitúcia je jednoznačne definovaná až do lambda.
β-reduction
Beta redukcia odráža myšlienku použitia funkcie. Beta-reduktívna je definovaná v termínochzámena: ((X V. E) E ') je E [V:=E'].
Ak napríklad predpokladáme nejaké kódovanie 2, 7, ×, existuje nasledujúca β-redukcia: ((λ n. N × 2) 7) → 7 × 2.
Beta redukciu možno vnímať rovnako ako koncept lokálnej redukovateľnosti pri prirodzenej dedukcii prostredníctvom Curryho-Howardovho izomorfizmu.
η-transform
Táto konverzia vyjadruje myšlienku extenzionality, ktorá v tomto kontexte znamená, že dve funkcie sú rovnaké, keď dávajú rovnaký výsledok pre všetky argumenty. Tento prevod sa vymieňa medzi λ x. (F x) a f vždy, keď sa x nezdá voľné v f.
Túto akciu možno považovať za rovnakú ako koncepciu lokálnej úplnosti v prirodzenej dedukcii prostredníctvom Curryho-Howardovho izomorfizmu.
Normálne formy a fúzia
Pre netypizovaný počet lambda nie je pravidlo β-redukcie vo všeobecnosti ani silné, ani slabé normalizujúce.
Napriek tomu sa dá ukázať, že β-redukcia sa zlučuje, keď prebieha pred α-transformáciou (t.j. dve normálne formy možno považovať za rovnocenné, ak je možná α-transformácia z jednej na druhú).
Výrazne normalizujúce výrazy aj výrazy slabo prispôsobujúce sa preto majú jedinú normálnu formu. Pre prvé termíny je zaručené, že akákoľvek redukčná stratégia povedie k typickej konfigurácii. Zatiaľ čo v prípade slabo normalizovaných podmienok to niektoré redukčné stratégie nemusia nájsť.
Ďalšie metódy programovania
Pre lambda kalkul existuje veľa tvorivých idiómov. Mnohé z nich boli pôvodne vyvinuté v kontexte používania systémov ako základu pre sémantiku programovacieho jazyka a efektívne ich aplikovali ako nízkoúrovňový konštrukt. Keďže niektoré štýly obsahujú lambda kalkul (alebo niečo veľmi podobné) ako úryvok, tieto techniky nachádzajú využitie aj v praktickej tvorbe, ale potom môžu byť vnímané ako nejasné alebo cudzie.
Pomenované konštanty
V lambda kalkule má knižnica formu množiny predtým definovaných funkcií, kde termíny sú len konkrétne konštanty. Čistý počet nemá koncept pomenovaných nemenných, pretože všetky atómové lambda termíny sú premenné. Možno ich však napodobniť aj tak, že sa premenné vezme ako názov konštanty, použije sa lambda abstrakcia na viazanie tohto prchavého v tele a abstrakcia sa aplikuje na zamýšľanú definíciu. Takže ak použijete f na vyjadrenie M v N, môžete povedať
(λ f. N) M.
Autori často zavádzajú syntaktický koncept, ako napríklad nechať veci písať intuitívnejším spôsobom.
f=M až N
Zreťazením takýchto definícií je možné napísať „program“lambda kalkulu ako nula alebo viac definícií funkcií nasledovaných jedným členom lambda, pričom sa použijú tie definície, ktoré tvoria väčšinu programu.
Významným obmedzením je, že názov f nie je definovaný v M,keďže M je mimo záväzného rozsahu lambda abstrakcie f. To znamená, že atribút rekurzívnej funkcie nemožno použiť ako M s let. Pokročilejšia syntax letrec, ktorá vám umožňuje písať definície rekurzívnych funkcií v tomto štýle, navyše namiesto toho používa kombinátory s pevnou bodkou.
Tlačené analógy
Tento typ je typizovaný formalizmus, ktorý používa symbol na vyjadrenie abstrakcie anonymnej funkcie. V tomto kontexte sú typy zvyčajne objekty syntaktickej povahy, ktoré sú priradené k lambda termínom. Presná povaha závisí od príslušného počtu. Typizovaný LI možno z určitého pohľadu považovať za spresnenie netypizovaného LI. Ale na druhej strane ich možno považovať aj za fundamentálnejšiu teóriu a netypový počet lambda je špeciálny prípad len s jedným typom.
Typované LI sú základom programovacích jazykov a chrbticou funkčných jazykov, ako sú ML a Haskell. A nepriamo aj imperatívne štýly tvorby. Typované lambda kalkuly hrajú dôležitú úlohu pri vývoji typových systémov pre programovacie jazyky. Tu typovateľnosť zvyčajne zachytáva požadované vlastnosti programu, napríklad nespôsobí narušenie prístupu do pamäte.
Typované lambda výpočty úzko súvisia s matematickou logikou a teóriou dôkazov prostredníctvom Curry-Howardovho izomorfizmu a možno si ich predstaviť ako vnútorný jazyk tried kategórií, napr.jednoducho je to štýl karteziánskeho uzáveru.
