26 - Lambda kalkul (definice všech pojmů, operací...) Flashcards
co je to Lambda kalkul
- formální systém a výpočetní model používaný v teoretické informatice a matematice pro studium funkcí a rekurze
- Lambda kalkul je teoretickým základem funkcionálního programování a příslušných programovacích jazyků, obzvláště Lispu
- Dá se chápat jako jednoduchý univerzální programovací jazyk - lze pomocí tohoto formalismu vyjádřit libovolnou rekurzivně spočetnou funkci
- lambda kalkul je tedy výpočetní silou ekvivalentní Turingovu stroji a parciálně rekurzivním funkcím
Základní přehled lambda kalkul
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
- „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
3 typy výrazů λ-kalkul
proměnné - Obyčejné proměnné, tak jak je známe z jiných jazyků, většinou se značí x, y, z. Definují vazbu s okolím
abstrakce (definice funkce) - reprezentuje funkci s JEDNOU vázanou proměnnou (hlavička) a tělem, které je tvořené λ − výrazem (např. λ x.x+2)
- pokud jich má mít víc, např. máme funkci g(x, y) = x − y, tak se to zapíše λ x. λ y . x − y. Toto se zkracuje (vnoření abstrakcí) na λ x y . x − y
aplikace (volání funkce) - f(x) = x + 2 se místo f(3) volá jako (f 3) tzn. nejdříve je uvedena funkce a poté její argumenty.
- Funkce f se v λ-kalkulu tedy zavolá takto: (λ x . x + 2) 3
Každý z těchto tří prvků se označuje jako λ-výraz – ty budu značit velkými písmeny
např. E a znamená to, že pod E se může skrývat buď proměnná, abstrakce (definice funkce) nebo aplikace (volání funkce).
Volné a vázané proměnné
vázaná = jedná se o parametr funkce volná = pokud není vázaná
Proměnná se vždycky váže na nejbližsí lambdu směrem doleva!
takže ve výrazu (λ x ((λ x . x) w)) se proměnná x uprostřed výrazu váže na lambdu co je hned vlevo od ní a ne na tu úplně vlevo!
Proměnná w je samozřejmě volná
Zjednodušování zápisu lambda kalkul
- místo (A B) lze napsat A B
- místo (λ V .(A B C)) lze napsat λ V . A B C
- místo (λ F(λ G(λ H . x))) lze napsat jen λ F G H . x
pomocí LET. Např. LET K = λ x y . x a poté můžu K používat v jiných výrazech, např. to může být argument při volání funkce atd.
Redukce (konverze)
Výraz, který je možné podle nějaké redukce změnit se nazývá redex podle zkratky z reducible expression. Jedná-li se o redex podle příslušné konverze, tak se nazývá α-, β-, či η-redexem.
α-konverze (alfa) - substituce (názvy proměnných nejsou důležité)
- Ovšem pozor, daná substituce musí být platná, což znamená, že se žádná volná proměnná nesmí stát vázanou (to by ve výsledku znamenalo změnu významu daného výrazu) - Zapisujeme jako λ W . E [W/V ] (W za V) * Správně - λx.xy→_(α ) λz.zy * Špatně - λx.xy→_(α ) λy.yy
β-konverze (beta) - volání funkce (substituce proměnné za parametr volané funkce :D)
- pozor, substituce musí být stále platná (nemůže se změnit význam funkce) - (λ V . W) M - lze konvertovat na W [M/V ] * Správně - (λ xy.xy)(xy) →_α (λ xz.xz)(xy) →_β (λ z.(xy)z) =λ z.xyz * Špatně - (λ xy.xy)(xy) →_β λ y.(xy)y
η-konverze (eta) - ekvivalence (odstranění abstrakce) - vlastně konvertujeme výraz s parametrem, který není vázaný
• Správně - λx.(uv)x→(η ) (uv), můžeme to udělat, jelikož ve výrazu (uv) není x volná.
• Špatně - λx.(xy)x→(η ) (xy), nelze, jelikož x je ve výrazu (xy) volná.
Identita/Rovnost/Relace a normální forma
- Identita: E_1≡E_2, stejné stringy
- Rovnost: E_1=E_2, stejné výsledky
- Relace: E_1→E_2, E_1 lze zredukovat na E_2
Normální forma (= vypočítání (maximální redukce))
• Výraz je v normální formě, pokud neobsahuje žádné β- ani η- redexy (výrazy, ktoré je možné změnit podle β- alebo η- konverze). Takže jediná konverze, kterou je možné vykonat je α-konverze.
• Výraz se převede do normální formy opakovanou redukcí (konverzí) nejlevějšího β- alebo η- redexu, případně α-konverzí abychom zabránili neplatné substituci.
Operátor pevného bodu
slouží k definování rekurze. (a platí pro něj: Y E = E(Y E))
• Definice: LET Y=λf.(λx.f(xx))(λx.f(xx))
• Bottom LET⊥=Y(λfx.f)
Bottom je výraz, který bude na výstup neustále produkovat sám sebe. V podstatě modeluje nekonečnou smyčku v programu.
Reprezentace pravdivostních hodnot a operací nad nimi
- LET True=λxy.x
- LET False=λxy.y
- LET Not=λt.t False True (Not True=(λt.t False True)True→_β True False True→(λxy.x) False True→_β (λy.False)True→_β False)
- AND = λuv.uv False (pokud je první hodnota True, tak vrať výsledek další hodnoty, jinak vrať False)
- OR = λuv.u True v (pokud je první hodnota True, tak vracím rovnou True, jinak vracíme druhou hodnotu)
• AND True False→(λuv.uv False)True False→True False False→(λxy.x) False False→False
• OR False True→(λuv.u True v) False True→(λv.False True v)True→False True True→(λxy.y)True True→(λy.y)True→True
Reprezentace čísel a operací nad nimi
Pro reprezentaci čísel v lambda kalkulu se používají Peanova (Pínova) čísla:
○ LET 0 = λfn.n = λfn.f^0 n
○ LET 1 = λfn.fn = λfn.f^1 n
○ LET 2 = λfn.f(fn) = λfn.f^2 n
LET succ = λxgm.xg(gm), následník musí přidat k číslu jedno f navíc.
LET iszero=λm.m(λv.False) True
