21 - Lambda kalkul
17:28
Lambda kalkul (definice všech pojmů, operací...).
[link]
[link]
Pojmy
Lambda kalkul je 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. 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 a parciálně rekurzivním funkcím.
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. 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.
λ-kalkul má 3 typy výrazů 
proměnné - Obyčejné proměnné, tak jak je známe z jiných jazyků, většinou se značí 𝑥, 𝑦, 𝑧. 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ř. 𝜆 𝑥.𝑥+2). 
Funkce v λ-kalkulu může mít jenom jeden parametr, takže pokud jich má mít víc, např. máme funkci 𝑔(𝑥, 𝑦) = 𝑥 − 𝑦, tak se to zapíše 𝜆 𝑥. 𝜆 𝑦 . 𝑥 − 𝑦. Toto se zkracuje na 𝜆 𝑥 𝑦 . 𝑥 − 𝑦 a znamená to, že funkce má dva parametry a při zavolání vrací jejich rozdíl.
aplikace (volání funkce) - když si vezmu naši funkci 𝑓(𝑥) = 𝑥 + 2, tak ta se zavolá např. s argumentem 3 takto: 𝑓(3). Funkce v λ-kalkulu se volají podobně jako v LISPu (který alespoň trochu určitě znáte :)), kde se funkce volá takto: (𝑓 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é
Proměnná je v λ-výrazu vázaná, pokud se jedná o parametr nějaké funkce, takže např. ve výrazu (𝝀 𝒙 . 𝒚 𝒙) je 𝒙 vázaná proměnná. Ostatní proměnné (v minulém příkladu 𝑦) jsou volné. Nehledejte v tom nic složitého. Proměnná se vždycky váže na nejbližsí lambdu směrem doleva, takže ve výrazu (𝜆 𝑥 ((𝜆 𝑥 . 𝑥) 𝑤)) se proměnná 𝑥 uprostřed výrazu váže na lambdu co je hned vlevo od ní a ne na tu úplně vlevo! Proměnná 𝑤 je samozřejmě volná. 
Zjednodušování zápisu
Tady toho moc vysvětlit nejde, takže se když tak mrkněte na tuto část do opory, já jen ve stručnosti shrnu, co je možné zjednodušit na co: 
místo (𝐴 𝐵) lze napsat 𝐴 𝐵 
Další zjednodušení je možné provést pojmenováním nějakého výrazu pomocí LET. Např. 𝐿𝐸𝑇 𝐾 = 𝜆 𝑥 𝑦 . 𝑥 a poté můžu 𝐾 používat v jiných výrazech, např. to může být argument při volání funkce atd.
Redukce a konverze
A dostáváme se k zřejmě nejobtížnější části, nicméně věřím, že se mi to podaří popsat dostatečně pochopitelně :). Jenom poznámka – to, jestli se říká konverze nebo redukce je jedno, protože někde to je tak a jinde naopak. Pomocí nich je možné měnit λ-výrazy, takže jsou velmi důležité. V λ-kalkulu máme celkem tři druhy konverzí.
Substituce: E[E'/V] - volné výskyty V jsou nahrazeny E' v E
Platnost substituce: Žádná volná proměnná v E' se nesmí stát vázanou v E[E'/V]
α-konverze (alfa)
Idea: Vyjadřuje myšlenku, že názvy proměnných nejsou důležité. Jedná se o prachsprostou substituci. 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). 
Správně - λx.xy→𝛼  λz.zy 
Špatně - λx.xy→𝛼  λy.yy
Špatně - λx.xy→𝛼  [file]  
β-konverze (beta)
Idea: Vyjadřuje myšlenku volání (aplikace) funkce. Zde se substituuje proměnná za parametr volané funkce. Opět je třeba dát pozor na platnost substituce.
η-konverze (eta)
Idea: Tuto konverzi není třeba umět používat, uvádím ji zde jen pro úplnost (i v opoře je). Vyjadřuje myšlenku ekvivalence dvou funkcí. Respektive je to odstranění abstrakce.
Správně - λx.uvx→𝜂  (uv), můžeme to udělat, jelikož ve výrazu (uv) není 𝑥 volná.
Špatně - λx.xyx→𝜂  (xy), nelze, jelikož 𝑥 je ve výrazu (xy) volná.
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. 
Identita/Rovnost/Relace
Identita: E1≡𝐸2, stejné stringy
Rovnost: E1=E2, stejné výsledky
Relace: E1→E2, 𝐸1 lze zredukovat na 𝐸2
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
Operátor pevného bodu nám slouží k definování rekurze.
Aplikací E na Y dostaneme pevný bod k_e:  k_e = Y E
Z definice pevného bodu funkce (lambda výrazu) platí, že při jeho aplikaci na danou funkci dostaneme znovu pevný bod:  E k_e = k_e
Potom platí E k_e = k_e = Y E = E (Y E)
E (Y E) dostaneme z E k_e a dosazením Y E za e_k
Klíčová vlastnost operátoru pevného bodu je Y E = E (Y E)
Alternativní definice operátoru pevného bodu pomocí lambda kalkulu
Bottom 𝐿𝐸𝑇⊥=𝑌(𝜆𝑓𝑥.𝑓)
Bottom je výraz, který bude na výstup neustále produkovat sám sebe. V podstatě modeluje nekonečnou smyčku v programu.
Definice rekurze pomocí operátoru pevného bodu
Napište lambda výraz SUM, který bude mít jako argumenty posloupnost čísel ukončenou nulou. Výraz sečte svoje argumenty a vrátí výsledek. Je možné použít ternární operátor iszero c ? a : b (vrátí a pokud c == 0, jinak vrátí b) a funkci add a b, která sečte čísla a, b.
Definice:
LET SUM = Y G
Výpočet:
SUM 2 3 0 = (Y G)  2 3 0 = G (Y G) 2 3 0 = G SUM 2 3 0 
G SUM 2 3 0 = (𝜆 𝑓 𝑎 𝑏. 𝑖𝑠𝑧𝑒𝑟𝑜 𝑏 ?𝑎 :𝑓 𝑎𝑑𝑑 𝑎 𝑏) SUM 2 3 0
𝑖𝑠𝑧𝑒𝑟𝑜 3 ?2 :𝑆𝑈𝑀 𝑎𝑑𝑑 3 20
SUM 5 0 = (Y G) 5 0 = G (Y G) 5 0 = G SUM 5 0
G SUM 5 0 =  (𝜆 𝑓 𝑎 𝑏. 𝑖𝑠𝑧𝑒𝑟𝑜 𝑏 ?𝑎 :𝑓 𝑎𝑑𝑑 𝑎 𝑏) 5 0
𝑖𝑠𝑧𝑒𝑟𝑜 0 ?5 :𝑆𝑈𝑀 𝑎𝑑𝑑 5 0=𝟓
Notes
1. Otazka (předmět) (okruh): Lambda kalkul. (FLP)
Kdo me primarne zkousel: Kolář
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: V otázke som mal napísané nejaké podbody, ktoré som však nedokázal prečítať, jediné čo som rozoznal bola Lambda a kalkul. Na začiatku mi povedal, že mám začať sám a vravieť čo viem. Tak som napísal možné tvary Lambda výrazu, na čo povedal, že mi tam niečo chýba. Najprv som nevedel čo myslí, ale potom som zistil, že chcel okolo abstrakcie a aplikácie zátvorky. Potom som rozprával kedy je premenná voľná a prešiel som na konverzie, že čo ktorá je, kde ma niekedy prerušil a pýtal sa na veci ako čo sa substituuje v Alfa konverzii, kedy je platná Alfa/Beta konverzia, kedy sa môže vykonať Eta. Nakoniec sa ma ešte spýtal na identitu, rovnosť a reláciu implikácie. Povedal, že jemu to stačí, ale Češka mal ešte otázku s čím je výpočetne ekvivalentný Lambda Kalkul. Povedal som Primitívne rekurzívne funkcie, ale správne malo byť Parciálne rekurzívne funkcie. Nakoniec B.
From <[link]> 
1. Otazka (předmět) (okruh): 21. Lambda kalkul (FLP)
Kdo me primarne zkousel: Kolář
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Mal som zacat definiciou lambda kalkulu. Narazil som na to, ze som vedel ako sa v nom vsetko robi, ale nevedel som definiciu, tak ju zo mna vytiahol po chvilke. Ako funguje aplikacia, abstrakcia, viazana/volna premenna, redukcie, kedy je redukcia platna. Na vsetko priklady. Operator pevneho bodu tiez nechcel. To je vsetko. Trvalo to len chvilku. Obcas hundral ze sa nevyjadrujem uplne presne, ale nakoniec C 
From <[link]> 
2. Otazka (okruh): 27. Práce v lambda kalkulu
Kdo me primarne zkousel: Vojnar
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Klasika. Nadefinoval jsem pravdivostí hodnoty. Pak se zeptal na NOT a že mám ukázat jak se vyhodnotí s nějakou hodnotou. Já jsem si ale nebyl úplně jistý jestli si na to vzpomenu zprávně, tak jsem to raději odvodil a už u toho jsem říkal jak to funguje. Pak to stejné u AND.
B
From <[link]> 
1. Otazka (okruh):
Práce v Lambda kalkulu (pravdivostní hodnoty a funkce).
Kdo me primarne zkousel:
Vojnar
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Chtěl definice TRUE, FALSE a NOT. Potom praktickou ukázku vyhodnocení NOTu a jak se jmenuje operace dosazení (beta-redukce). Potom chtěl slovně popsat, jak by se dělal AND (jenom princip) + říct, že je to short evaluation. Rychlovka, žádné chytáky, toť vše.
From <[link]> 
1. Otazka (okruh): Lambda kalkul
Kdo me primarne zkousel: Krivka
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Rekl sem co to je, co je promenna, abstrakce, aplikace, pak alfa a beta redukce. Vice mene neformalne, delal sem tam naky chyby. Ale byl hodnej a neryl.
From <[link]> 
1. Otazka (okruh):
Lambda Kalkul
Kdo me primarne zkousel:
Kolář
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Krásna otázka. Začal som normálne všeobecne o lambda kalkule, potom to, že používa iba premennú/abstrakciu/aplikáciu. Začal som premennou a povedal, že to mám zapísať do gramatiky. Moc som nevedel, čo presne chce. Na tabuli som mal napísané akurát tak jedno "x" a nevedel som, čo viac k tomu. Potom som sa trochu zamyslel a dopísal tam "E -> x", čo bolo asi dobre, lebo už na to nič nepovedal. Potom som ďalej zapísal abstrakciu/aplikáciu. Začal som hovoriť a písať redukcie. Na to mi povedal, že najprv nám bude treba voľné a viazané premenné, tak som zapísal [file] a na tom to len jednou vetou vysvetlil. K redukciám chcel počuť, že sa dajú previesť len ak je substitúcia platná, na to sa spýtal, že čo to znamená. A k eta redukcií chcel počuť, že "V" nemôže byť voľné v "E".
Všetko som v podstate vedel a povedal .. občas mi niečo dlhšie trvalo, ale v zásade som sa ani moc nemýlil .. B
From <[link]> 
1. Otazka (okruh): Lambda kalkul
Kdo me primarne zkousel: Dusan Kolar
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Zacal jsem obecne, ze je tam promenna, aplikace a abstrakce. Pak jsem to napsal. Chtel vedet True a False. Rikal jsem, ze jsme si rikali dve verze, tak chtel tu jednodussi. Pak chtel AND. Dal rekl jak jsou definovany cisla (neptal se me na to, ale oznamil mi to. Tzn. nemusel jsem to rikat sam) a chtel vedet jak udelat odcitani. Ptal se taky na pevnej bod. Tam jsem rekl, ze umoznuje v LE vyrazech rekurzi. Snazil jsem toho ze me vytahnout vic. Treba pouziti, ale trochu jsem to motal, tak se na to vykaslal.
From <[link]> 
1. Otázka (okruh): Lambda kalkul
Kdo mě primárně zkoušel: Hruška Tomáš
Začal jsem tím, co je Lambda kalkul, pak pokračoval v definicích Lambda výrazu, proměnná, abstrakce, aplikace, substituce a její platnost. Psal jsem to na tabuli. Dál jsem vysvětlil a napsal alfa a beta konverzi. Prof. Hruška byl hodný, nijak netopil. Ještě jsem zodpověděl několik doplňujících otázek a to stačilo. Bylo to velmi rychlé - asi 5 min. Úplná pohoda.
From <[link]> 
kdo me primarne zkousel: krivka
Zacala jsem tim, co vse muze byt vyraz. Pak ze mame 3 redukce. Zacala jsem alfou. Zamotala jsem se do matematickeho vzorce (no proste do toho predpisu... prohodila jsem na prave strane substituci - dosazovala jsem jakoby naopak...). Tak jsem hned rekla, ze sem se do toho zamotala a ze jim ukazu prakticky priklad, kde to bude jasnejsi. Na tom jsem ukazala i neplatny priklad substituce. Krivka se me zeptal, jestli je to prave nebo leve asociativni, to jsem se omluvila, ze bych hadala, ze mu to z fleku nereknu. Pak beta redukce, no do toho predpisu jsem se zamotala strasne, to jsem nenapsala ani naznak:D Ale opet jsem to ukazala na priklade. Pak uz se jen Krivka zeptal na rozdil mezi rovnosti a identitou. U rovnosti mi dal jeste navodnou otazku, zda ten prevod je jen jednosmerny ci obousmerny - rekla jsem ze obousmerny a konec 
 Vysledna B, ja bych si za svou neschopnost zapsat ty redukce formalne dala C, ale ani za D bych se nezlobila.
From <[link]> 
Lambda kalkul
Kdo me primarne zkousel: Rysavy
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Rikal jsem si easy win, behem minuty na rozmyslenou jsem si vybavil veskere operace AND, OR, peanova cisla apod. No a pak me hodne rychle vyvedl z omylu zkousejici, ktery se chtel zamerit jen na uplne zaklady (ktere jsem vedel jak funguji, co je tvori, ale formalni definice jsem si neopakoval). Pry je to moc lehke, tak zapsat alfa a beta redukci formalne, pak substituci, at nepouzivam promenne ve vyrazech, ale TERMY (velke X misto maleho apod.) a vyjadrim to formalne a obecne. Pekne jsem se v tom zamotal, nebyl jsem moc schopny ze stresu premyslet. Moc mi nedal prostor se pohnout kdekoliv dale (jak rad bych tam zadefinoval nejake operace, i tu rekurzi bych asi dal). Chvili me drzel po budiku, fakt jsem se citil jak kokot, ze neumim vymyslet tak jednoduchou vec, holt trema, navic otazky mi neprisly uplne sikovne, moc jsem v tom formalnim zapisu nevedel co po me chce. Po chvili cumeni do tabule prisel konec. Vubec, ale vubec jsem si nebyl jisty, jestli mi to da. Hrala me vsak myslenka dobre obhajoby diplomky a tak jsem relativne vklidu presel na druhou otazku. Pointa: Rysavy chce zaklady, nechce nijak potapet, zkousi uplne v pohode a pomaha, ale chce to podrobneji a formalne. Moc nepocitejte s tim, ze utecete k jine casti otazky. Nakonec za D, urcite se priklonili k DP a k tomu, ze jsem vypadal, ze vim jak to pouzivat, jen definice jsem nebyl schopen promyslet a napsat formalne.
From <[link]> 
Rysavy
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Rikal jsem si easy win, behem minuty na rozmyslenou jsem si vybavil veskere operace AND, OR, peanova cisla apod. No a pak me hodne rychle vyvedl z omylu zkousejici, ktery se chtel zamerit jen na uplne zaklady (ktere jsem vedel jak funguji, co je tvori, ale formalni definice jsem si neopakoval). Pry je to moc lehke, tak zapsat alfa a beta redukci formalne, pak substituci, at nepouzivam promenne ve vyrazech, ale TERMY (velke X misto maleho apod.) a vyjadrim to formalne a obecne. Pekne jsem se v tom zamotal, nebyl jsem moc schopny ze stresu premyslet. Moc mi nedal prostor se pohnout kdekoliv dale (jak rad bych tam zadefinoval nejake operace, i tu rekurzi bych asi dal). Chvili me drzel po budiku, fakt jsem se citil jak kokot, ze neumim vymyslet tak jednoduchou vec, holt trema, navic otazky mi neprisly uplne sikovne, moc jsem v tom formalnim zapisu nevedel co po me chce. Po chvili cumeni do tabule prisel konec. Vubec, ale vubec jsem si nebyl jisty, jestli mi to da. Hrala me vsak myslenka dobre obhajoby diplomky a tak jsem relativne vklidu presel na druhou otazku. Pointa: Rysavy chce zaklady, nechce nijak potapet, zkousi uplne v pohode a pomaha, ale chce to podrobneji a formalne. Moc nepocitejte s tim, ze utecete k jine casti otazky. Nakonec za D, urcite se priklonili k DP a k tomu, ze jsem vypadal, ze vim jak to pouzivat, jen definice jsem nebyl schopen promyslet a napsat formalne.
From <[link]> 
Lambda kalkul (pojmy, operace)
Kdo me primarne zkousel: Hruška
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: 
Nejdřív chtěl popsat z čeho se lambda kalkul skládá. (chtěl slyšet abstrakce, aplikace funkcí)
Než jsme se k tomu dostali, zeptal se taky proč se v lambda výrazech píše právě písmeno lambda - když jsem nevěděl, tak do toho vstoupil Kolář: "No to neví nikdo" - takže to se dál neřešilo.
Dál jsem měl popsat operace - alfa redukci (stačilo říct že je to přejmenování vázané proměnné v hlavičce a všech výskytů v tělu (průběžně ukazováno na (\V.E), beta redukci (musel jsem i rozepsat: (\V.E) E' -> E[E'/V]). Na eta-redukci nakonec vůbec nedošlo.
From <[link]> 
Kdo me primarne zkousel: prof. Hruška
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Mluvil jsem prakticky celou dobu sám a říkal jsem všechno neformálně, maximálně mě prof. Hruška občas nasměroval když chtěl slyšet něco formálně.
From <[link]> 
Lambda kalkul (definice všech pojmů, operací...) (FLP)
Kdo me primarne zkousel: Ryšavý
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Začal jsem obecně, kdo lambda kalkul definoval, kdo dokázal ekvivalenci s TS. Potom jsem začal již více mluvit o tom jazyku, tak mi řekl ať spíš napíšu zrovna ty syntaktické pravidla. Ty byly v pořádku, tak se mě zeptal na nějaké odvozovací pravidla. Tak jsem řekl, že máme alfa beta ný konverzi (na konci se mě vojnar zeptal jestli je to opravdu ný, tak jsem řekl, že si nejsem jistý, ale můžu ten symbol napsat a když jsem ho viděl napsaný tak jsem si samozřejmě vzpomněl že je to éta). Chtěl napsat Beta konverzi, to bylo taky ok. Pak se mě zeptal na konfluenci, k tomu jsem si vzpomněl jen z některého jiného předmětu, že je to soutok, ale víc nic. Snažili se mě navést, že je to něco s pořadím konverzí. Ale nakonec řekl, že to stejně asi v tom okruhu nebylo. Chtěl slyšet, že nezávisí na pořadí aplikace pravidel. Ještě proběhla debata nad symbolem éta a já jsem mohl jít s vědomím že to mám v kapse.
From <[link]> 