Pro mou snažší orientaci prosím předmět zprávy uveďte „FP: “. Děkuji.
Jména řešitelů, kteří odevzdali úlohu do týdne, jsou označena ^*, těch co odevzdali do 2 týdnů ⁺.
Zde najdete hodnocení úloh.

1. Najděte termy M a N t.ž. N nemá normální formu a MN má normální formu.
2. Najděte termy M a N t.ž. M nemá normální formu a MN má normální formu.

Nápověda: Použijte termy K = λxy.x a Ω = (λx.xx)(λx.xx).

Vyřešili: Tomáš Křen^*, Martin Jiřička, David Nohejl.

Reprezentujte lambda termy datovou strukturou a implementujte

• substituci (s případným přejmenováním proměnných),
• β-redukci.

Vyřešili: Tomáš Křen^*, Martin Jiřička⁺.

Implementujte normalizující strategii, ať už pro klasický λ-kalkulus nebo pro de Bruijnovu notaci.

Vyřešili: Tomáš Křen^*, Martin Jiřička^*.

Implementujte aplikativní strategii vyhodnocování. [Pokud implementujete obě strategie, zkuste najít term(y), na kterých se výrazně liší doba vyhodnocení.]

Vyřešili: Tomáš Křen^*, Martin Jiřička^*.

Implementujte línou call-by-need strategii. Při substituci termu budou jeho jednotlivé kopie sdíleny, a budou tak sdílet i (částečné nebo úplné) vyhodnocení.

1. Ověřte, že výsledné vyhodnocování je líné pomocí nějakého termu, který má NF a zároveň má nějakou nekonečnou posloupnost redukcí.
2. Najděte term, na kterém je strategie call-by-name neefektivní a ověřte, že vaše implementace call-by-need je efektivní.

Můžete také použít líný programovací jazyk (např. Haskell) a využít jeho líného vyhodnocování.

Vyřešili: Tomáš Křen^*, Martin Jiřička.

Zapiště nějaký kombinátor pevného bodu (např. Y nebo Θ) a pomocí něj zapište funkci pro výpočet Fibonacciho posloupnosti, která sama o sobě nebude rekurzivní. Poznámky:

• Použijete-li netypovaný jazyk umožňující zapisovat anonymní funkce (Python - lambda x: …, JavaScript - function(x) { … }, apod.), zapište kombinátor přímo v podobě odpovídající λ-termu.
• Bude-li to jazyk s aplikativním vyhodnocováním, nahraďte v kombinátoru pod-termy typu x x termy λy.x x y, (tzv. jejich η-expanzi) abyste předešli zacyklení.
• Použijete-li silně typovaný jazyk s líným vyhodnocováním (Haskell), bude zápis x x problematický. Proto kombinátor pevného bodu zapište přímo jeho rekurzivní definicí.
• Použijete-li silně typovaný jazyk s aplikativním vyhodnocováním (Scala, OCaml, …), zapište kombinátor pevného bodu přímo jeho rekurzivní definici, kterou zabalíte pomocí η-expanze, tedy místo y = λf.(…) bude y = λf.λx.(…)x. Tím předejdete zacyklení.
• Můžete použít také vlastní interpret λ-kalkulu z minulých cvičení.

Vyřešili: Tomáš Křen^*, Martin Jiřička, David Nohejl.

Napište překladač z lambda termů do zvoleného jazyka. Vhodné jsou netypované jazyky umožňující vytvářet anonymní funkce, např. Python nebo JavaScript. Výsledné zpracování lambda termů tak bude aplikativní.

Vyřešili: Tomáš Křen^*, Martin Jiřička⁺.

Do interpretu/překladače λ-kalkulu přidejte konstantu # a pro každé n konstanty a pravidla:

• δ n →_δ c_n
• δ (# n) →_δ n+1

Konverzi z c_n zpět na číslo pak provedeme c_n (λn.δ(#n)) 0

Poznámka: Stručný popis originální Churchovy δ-redukce zde.

Vyřešili: Tomáš Křen^*, Martin Jiřička⁺ (s odřenýma ušima).

Implementujte operace AND, OR, a NOT na Churchových booleovských hodnotách (true = λxy.x, false = λxy.y).

Vyřešili: Martin Jiřička⁺, Tomáš Křen, David Nohejl.

Každý z následujících bodů je samostatné cvičení, které můžete zpracovat nezávisle na ostatních:

1. Pomocí Y kombinátoru implementujte funkci počítající n-tý člen Fibonacciho posloupnosti v Churchových numerálech. Vyřešili: Tomáš Křen^*, Martin Jiřička.
2. Implementujte tetraci jako λ-term na Churchových numerálech. Vyřešili: Tomáš Křen^*.
3. Implementujte ternární funkci hyper-operace jako λ-term na Churchových numerálech. Pro jednoduchost začněte od násobení, tedy H(0,x,y)=x*y, H(1,x,y)=x^y, H(2,x,y) je tetrace… Vyřešili: Tomáš Křen^*.

Výsledky ověřte, například na překladači/interpretu, z předchozích úloh.

Nové úlohy jsou na fóru!