Cesko.wiki Lambda kalkul
Author
Albert FloresLambda kalkul je formální systém a výpočetní model používaný v teoretické informatice a matematice pro studium funkcí a rekurze. Jeho autory jsou Alonzo Church a Stephen Cole Kleene. Lambda kalkul je teoretickým základem funkcionálního programování a příslušných programovacích jazyků, obzvláště Lispu.
Lambda kalkul analyzuje funkce nikoli z hlediska původního matematického smyslu zobrazení z množiny do množiny, ale jako metodu výpočtu. Dá se chápat jako jednoduchý univerzální programovací jazyk. +more Je univerzální, neboť libovolnou rekurzivně spočetnou funkci lze vyjádřit a vyčíslit pomocí tohoto formalismu, lambda kalkul je tedy výpočetní silou ekvivalentní Turingovu stroji.
Tento článek se bude zaobírat netypovým lambda kalkulem. Existuje totiž rozšíření zvané typový lambda kalkul.
Základní přehled
V lambda kalkulu každý výraz popisuje funkci jednoho argumentu, který je sám funkcí jednoho argumentu, a jejímž výsledkem je opět funkce jednoho argumentu. Funkce lze definovat bez pojmenování, uvedením lambda výrazu, který popisuje, jak se z hodnoty argumentu vypočte hodnota funkce. +more Příkladem může být funkce „přičti dvojku“, f(x) = x + 2. V lambda kalkulu se taková funkce zapíše jako λ x. x + 2 (nebo, beze změny významu λ y. y + 2, jméno argumentu není podstatné). Aplikace takové funkce na číslo 3 se zapíše jako (λ x. x + 2) 3. Aplikace je asociativní zleva: f x y = (f x) y.
Formální popis
Mějme dány nejvýše spočetné množiny C resp. V (konstant resp. +more proměnných). Množinou všech lambda výrazů rozumíme množinu Λ (velká lambda) řetězů obsahujících symboly z C ∪ V ∪ {, λ} takových, že:.
# c ∈ C => c ∈ Λ # v ∈ V => v ∈ Λ # M,N ∈ Λ → (M N) ∈ Λ # x ∈ V, M ∈ Λ → (λ x . M) ∈ Λ
V dalším budeme označovat konstanty písmeny c, d, e, …, proměnné odzadu tj. z, y, x, … a obecné λ-výrazy velkými písmeny latinky. +more Budeme také vynechávat závorky, tj. místo (λ x. x) budeme psát λ x. x (nebo jen λ xx). Podobně výraz λx (x y z) budeme značit jako λx . x y z. (Tečka odděluje "argumenty" λ od těla λ-výrazu a umožňuje zkrácený zápis λ xy. y ve významu λ x (λ y (y)). Jinými slovy, tečka nahrazuje levou závorku, ke které je pravá závorka co nejvíce vpravo - tj. u další pravé závorky).
Faktu, že na pojmenování (označení) vázaných proměnných nezáleží, využijeme. Tomuto se formálně říká Alfa konverze.
Příklad: Výraz λx . xy je stejný jako λw . wy.
Nechť M je libovolný λ-výraz. Množinu všech volných proměnných M značíme FV(M) a definujeme ji následovně:
* FV(x) = {x} * FV(NL) = FV(N) ∪ FV(L) * FV(λx . N) = FV(N) - {x}
Lambda výraz M, pro který je množina FV prázdná, nazýváme uzavřeným λ-výrazem nebo také kombinátorem.
Příklad: y (λxy . λyz) obsahuje volné proměnné z, y a vázané x, y. Výraz λxy . λxy je kombinátorem.
Mnemotechnická pomůcka pro označení množin: C … constant, V … variable, FV … free variable.
Nechť M, N ∈ Λ. Výraz tvaru M=N, kde = je speciální symbol, nazýváme rovnost. Někdy se používá označení ==.
Lambda kalkul definujeme jako teorii rovností mezi λ-výrazy založenou na následujících axiomech:
# (λx . M) N = M[x := N] (tzv. +more Beta konverze) # M = M # M = N → N = M (asociativita) # M = N ∧ N = L → M = L (tranzitivita) # M = M` → ZM = ZM` # M = M` → MZ = M`Z # M = M` → λx . M = λx . M`.
V některých učebnicích se předpokládá, že M neobsahuje y. Axiom je tedy tvaru
* λx . M = λy . ( M[x := y] )
Pokud je v λ-kalkulu dokazatelná rovnost M=N, píšeme λ~M=N a říkáme, že λ-výrazy M, N jsou navzájem (Beta) konvertibilní. (Poznámka: použil jsem označení pomocí ~, ale v literatuře se častěji setkáte se znakem ⊥ otočeným o 90 stupňů vpravo. +more (\lambda\vdash M=N)).
Zápisem M≡N rozumíme tu skutečnost, že dva λ-výrazy jsou buď totožné, nebo je lze ztotožnit přejmenováním vázaných proměnných.
Příklad: λx . xy ≡ λx . xy, λz . xz ≡ λy . xy (alfa konverze), ale λx . xz ≠ λx . xy.
Mezi standardní kombinátory řadíme:
* I: λx . x (identita) * K: λxy . x (ev. K*: λxy . y) * S: λxyz . xz (yz)
Tyto kombinátory dávají základ SKI kalkulu. Je vhodné si ověřit, že: * IM = M * KMN = M * SMNL = ML(NL)
Například druhý případ: KMN, což můžeme přepsat jako (λxy . x)MN = (λy. x[x := M])N, což je (λy . M)N = M[y := n] a to je M. Dokázali jsme, že KMN = M.
Věta o pevném bodě
# Ke každému λ-výrazu F (F ∈ Λ) existuje X ∈ Λ tak, že FX = X. # Definujeme-li (tzv. +more kombinátor pevného bodu) Y = λf (λx . f(xx))(λx . f(xx)), pak pro libovolná F ∈ Λ platí: YF=F(YF).
Důsledkem je tvrzení: ke každému kontextu C[f, x] (tj. λ-výrazu, který případně obsahuje proměnné f, x) existuje λ-výraz F ∈ Λ tak, že pro všechny X ∈ Λ:
:FX = C[f, x][f := F][x := X]
Podtrženo a sečteno: každý λ-výraz obsahuje pevný bod a máme i kombinátor pevného bodu, pomocí kterého tento pevný bod najdeme. Je nutno si uvědomit, že v lambda kalkulu pracujeme s funkcemi (vyššího řádu), pevným bodem tedy je opět funkce.
Reprezentace objektů λ-kalkulu
Pravdivostní hodnoty kódujeme pomocí λ-výrazů T (pravda) a F (nepravda) definovaných následovně: * T ≡ K (λxy . x) * F ≡ K* (λxy . y)
Logický výraz pokud D pak P jinak Q, taky známý jako if-then-else, kde D (logická proměnná) nabývá hodnot T nebo F, může být zakódován jako DPQ. Pro D = T (resp. +more D = F) dostáváme.
:TPQ ≡ (λxy . x) PQ = P (resp. FPQ = Q)
Teoretické využití
Pomocí lambda kalkulu lze dobře definovat vyčíslitelnost.
Libovolná funkce F: N → N je vyčíslitelná právě tehdy, když existuje lambda výraz f, u kterého pro libovolná přirozená čísla x a y platí F(x) = y právě tehdy, když f x
y, kde x a y jsou Churchova čísla odpovídající x a y. Tak vypadá jeden ze způsobů definice vyčíslitelnosti, který je základem Churchovy-Turingovy teze. Problém určit, zda dva výrazy v lambda kalkulu jsou ekvivalentní, nemůže žádný univerzální algoritmus vyřešit a tento problém byl první, u kterého se nerozhodnutelnost podařilo dokázat. V důkazu tohoto faktu Alonzo Church nejprve problém zredukoval na určení, zda daný lambda výraz má nějakou normální formu, přičemž takovou formou se míní ekvivalentní výraz, který nelze dále zjednodušit. Poté v rámci důkazu sporem předpokládá, že takový predikát je vyčíslitelný a lze ho tedy vyjádřit pomocí lambda kalkulu. S využitím předchozích Kleeneho výsledků dokázal lambda výrazům přiřadit Gödelovo číslo a poté obdobnou technikou jako v důkazu první Gödelovy věty o neúplnosti vytvořil lambda výraz e. Konečně, pokud je e aplikováno samo na sebe (na své Gödelovo číslo), výsledkem je spor. Pomocí něho lze také definovat operace v objektových databázích. Na principech lambda kalkulu je založená dotazovací část jazyka smalltalk. Tento jazyk používá například rozsáhlá objektová databáze GemStone.
Související články