Lambda kalkul

Lambda počet ( λ-počet ) je formální systém vyvinutý americkým matematikem Alonzem Churchem k formalizaci a analýze konceptu vyčíslitelnosti .

Čistý λ-kalkul

Čistý λ-počet , jehož termíny , také nazývané objekty ("oba") nebo λ -termíny, jsou sestaveny výhradně z proměnných pomocí aplikace a abstrakce. Zpočátku se neočekává přítomnost žádných konstant.

Aplikace a abstrakce

λ-počet je založen na dvou základních operacích:

Aplikace ( lat. applicatio - příloha, příloha) znamená aplikaci nebo volání funkce ve vztahu k dané hodnotě. Obvykle se označuje , kde je funkce a je argument. To odpovídá notaci obecně přijímané v matematice , která se také někdy používá, ale pro λ-počet je důležité, že je interpretován jako algoritmus , který vypočítává výsledek z dané vstupní hodnoty. V tomto smyslu může být žádost posuzována dvěma způsoby: jako výsledek žádosti o , nebo jako proces výpočtu . Poslední výklad aplikace souvisí s pojmem β-redukce . $f\a$ $F$ $A$ $f(a)$ $F$ $F$ $A$ $F$ $A$ $f\a$

Abstrakce neboli λ-abstrakce ( lat. abstractio - rozptýlení, separace) zase staví funkce podle daných výrazů. Totiž, jestliže je výraz, který volně obsahuje , pak zápis znamená: λ je funkcí argumentu , který má tvar , označuje funkci . S pomocí abstrakce tedy můžete konstruovat nové funkce. Požadavek, do kterého volně vstupuje , není příliš důležitý – stačí předpokládat, že pokud tomu tak není. $t\ekviv t[x]$ $X$ $\ \lambda xt[x]$ $X$ $t[x]$ $x\mapsto t[x]$ $X$ $t$ $\lambda xt\equiv t$

α-ekvivalence

Základní formou ekvivalence definovanou v pojmech lambda je ekvivalence alfa. Například a : jsou alfa ekvivalentní termíny lambda a oba představují stejnou funkci (funkci identity). Termíny a nejsou ekvivalentem alfa, protože nejsou v lambda abstrakci. $\lambda xx$ $\lambda yy$ $X$ $y$

β-redukce

Vzhledem k tomu, že výraz označuje funkci, která každému přiřadí hodnotu , pak k vyhodnocení výrazu $\lambda x.2\cdot x+1$ $X$ $2\cdot x+1$

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

který zahrnuje aplikaci i abstrakci , je nutné místo proměnné provést substituci čísla 3 v termínu . Výsledkem je . Tato myšlenka může být zapsána v obecné formě jako $2\cdot x+1$ $X$ $2\cdot 3+1=7$

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

a nazývá se β-redukce . Vyjádření tvaru , tedy aplikace abstrakce na určitý termín, se nazývá redex . Ačkoli je β-redukce v podstatě jediným „podstatným“ axiomem λ-kalkulu, vede k velmi bohaté a složité teorii. Spolu s tím má λ-počet vlastnost Turingovy úplnosti , a proto je nejjednodušším programovacím jazykem . $(\lambda xt)\ a$

η-transformovat

$\eta$ -konverze vyjadřuje myšlenku, že dvě funkce jsou totožné právě tehdy, když při aplikaci na jakýkoli argument dávají stejné výsledky. -transformation překládá vzorce a do sebe navzájem (pouze pokud nemá žádné volné výskyty v : jinak se volná proměnná po transformaci stane vázanou externí abstrakcí nebo naopak). $\eta$ $\lambda xf\ x$ $F$ $X$ $F$ $X$

Currying (currying)

Funkce dvou proměnných a lze ji považovat za funkci jedné proměnné , vracející funkci jedné proměnné , tedy jako výraz . Tato technika funguje úplně stejně pro funkce jakékoli arity . To ukazuje, že funkce mnoha proměnných mohou být vyjádřeny v λ-kalkulu a jsou „ syntaktickým cukrem “. Popsaný proces přeměny funkcí mnoha proměnných na funkci jedné proměnné se nazývá currying (také: currying ), podle amerického matematika Haskella Curryho , ačkoli jej jako první navrhl Moses Sheinfinkel ( 1924 ). $X$ $y$ $f(x,y)=x+y$ $X$ $y$ $\ \lambda x.\lambda y.x+y$

Sémantika netypového λ-kalkulu

Skutečnost, že členy λ-kalkulu působí jako funkce aplikované na členy λ-kalkulu (tedy možná na sebe), vede k potížím při konstrukci adekvátní sémantiky λ-kalkulu. Aby měl λ-počet nějaký význam, je nutné získat množinu, do které by byl zasazen jeho prostor funkcí . V obecném případě toto neexistuje z důvodů omezení mohutností těchto dvou množin a funkcí od do : druhá má větší mohutnost než první. $D$ $D\to D$ $D$ $D$ $D$ $D$

Dana Scott tento problém překonala na počátku 70. let 20. století tím, že zkonstruovala koncept regionu (zpočátku na úplných svazech [1] , později jej zobecnila na kompletní částečně uspořádanou množinu se speciální topologií ) a omezila jej na funkce spojité v této topologii [ 2] . Na základě těchto konstrukcí byla vytvořena denotační sémantika programovacích jazyků , a to zejména proto, že s jejich pomocí je možné dát přesný význam dvěma důležitým konstruktům programovacích jazyků, např. jako rekurze a datové typy . $D$ $D\to D$

Vztah k rekurzivním funkcím

Rekurze definuje funkci jako takovou; na první pohled to lambda kalkul neumožňuje, ale tento dojem je klamný. Uvažujme například rekurzivní funkci, která vypočítá faktoriál :

f(n) = 1, pokud n = 0; jinak n × f(n - 1).

V lambda počtu nemůže funkce přímo odkazovat sama na sebe. Funkci však lze předat parametr, který je s ní spojen. Tento argument je zpravidla na prvním místě. Když ji přiřadíme k funkci, získáme novou, již rekurzivní funkci. K tomu musí být do těla funkce předán argument odkazující na sebe sama (zde označený jako ). $r$

g := λr. λn.(1, pokud n = 0; jinak n × (rr (n-1))) f := gg

To řeší konkrétní problém výpočtu faktoriálu, ale je také možné obecné řešení. Daný termín lambda představující tělo rekurzivní funkce nebo smyčky, který se předá jako první argument, vrátí kombinátor s pevnou řádovou čárkou požadovanou rekurzivní funkci nebo smyčku. Funkce se nemusí pokaždé explicitně předávat.

Existuje několik definic kombinátorů s pevným bodem. Nejjednodušší z nich:

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

V počtu lambda je pevný bod ; pojďme si to ukázat: $\operatorname {Y\ g}$ $\operatorname {g}$

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

Nyní, abychom definovali faktoriál jako rekurzivní funkci, můžeme jednoduše napsat , kde je číslo, pro které se faktoriál počítá. Nechte , dostaneme: $\operatorname {g\ (Y\ g)} n$ $n$ $n=4$

g (Y g) 4 (λfn.(1, pokud n = 0; a n (f(n-1)), pokud n>0)) (Y g) 4 (λn.(1, pokud n = 0; a n ((Y g) (n-1)), pokud n>0)) 4 1, pokud 4 = 0; a 4 (g(Yg) (4-1)), pokud 4>0 4 (g(Y g) 3) 4 (λn.(1, pokud n = 0; a n ((Y g) (n-1)), pokud n>0) 3) 4 (1, pokud 3 = 0; a 3 (g(Y g) (3-1)), pokud 3 > 0) 4 (3 (g(Y g) 2)) 4 (3 (λn.(1, pokud n = 0; a n ((Y g) (n-1)), pokud n>0) 2)) 4 (3 (1, pokud 2 = 0; a 2 (g(Y g) (2-1)), pokud 2 > 0)) 4 (3 (2 (g(Y g) 1))) 4 (3 (2 (λn.(1, pokud n = 0; an ((Y g) (n-1)), pokud n>0) 1))) 4 (3 (2 (1, pokud 1 = 0; a 1 ((Y g) (1-1)), pokud 1 > 0))) 4 (3 (2 (1) ((Y g) 0)))) 4 (3 (2 (1) ((λn.(1, pokud n = 0; a n ((Y g) (n-1)), pokud n>0) 0)))) 4 (3 (2 (1 (1), pokud 0 = 0; a 0 ((Y g) (0-1)), pokud 0 > 0)))) 4 (3 (2 (1 (1)))) 24

Každá definice rekurzivní funkce může být reprezentována jako pevný bod odpovídající funkce, takže pomocí , lze každou rekurzivní definici vyjádřit jako výraz lambda. Zejména můžeme rekurzivně definovat odčítání, násobení, porovnávání přirozených čísel. $\operatorname {Y}$

V programovacích jazycích

V programovacích jazycích je "λ-kalkul" často chápán jako mechanismus " anonymních funkcí " - zpětných volání , které lze definovat přímo v místě, kde se používají, a které mají přístup k lokálním proměnným aktuální funkce ( closure ).

Viz také

Poznámky

↑ 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 Lattice-teoretické modely pro různé beztypové výpočty. — In: Proc. 4th Int. Kongres pro logiku, metodologii a filozofii vědy, Bukurešť, 1972.

Literatura

Barendregt X. Lambda kalkul. Jeho syntaxe a sémantika: Per. z angličtiny. — M.: Mir, 1985. — 606 s.