IA081 Lambda calculus

Fakulta informatiky
jaro 2017
Rozsah
2/0. 3 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jiří Zlatuška, CSc. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jiří Zlatuška, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 10:00–11:50 B411
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu buse student seznámen se základnimi pojmy, technikami a výsledky teorie sekvenčních funkcí v podobě lambda-kalkulu a kombinatorické logiky; seznámí se se základy typová i netypové varianty těchto formalismů; bude umět je použít pro formalizaci vyčíslitelnosti; seznámí se s principy konstrukce modelů lambda-kalkulu; zvládne užívání formalizace rekurzivních konstrukcí v programování i příslušných modelech; bude schopný použit ho jako referenčním formalismus vhodný pro řadu aplikací.
Osnova
  • Čistý lambda-kalkul: lambda-termy, struktura termů, rovnostní teorie.
  • Redukce: jednosměrné transformace, obecné redukce, beta-redukce.
  • Lambda-kalkul a výpočty: kódování, rekurzívní definice, lambda-vyčíslitelnost, kombinátory pevného bodu, nerozhodnutelné vlastnosti.
  • Modifikace teorie: kombinatorická logika, extenzionalita, éta-redukce.
  • Typovaný lambda-kalkul: typy a termy, normální formy, množinové modely, silná normalizovatelnost, typy jako formule.
  • Doménové modely: úplná částečná uspořádání, domény, nejmenší pevné body, parcialita.
  • Konstrukce domén: složené domény, rekurzívní konstrukce domén, limitní domény.
Literatura
  • ZLATUŠKA, Jiří. Lambda-kalkul. 1. vyd. Brno: Masarykova univerzita, 1993, 264 s. ISBN 8021008261. info
  • BARENDREGT, H. P. Lambda calculus : its syntax and semantics. Rev. ed. Amsterdam: Elsevier, 1998, xv, 621 s. ISBN 0-444-86748-1. info
  • HINDLEY, J. Roger a J. P. SELDIN. An Introduction to Combinators and the (lambda)-calculus. Cambridge: Cambridge University Press, 1986, 360 s. ISBN 0521318394. info
  • AMADIO, Roberto M. a Pierre-Louis CURIEN. Domains and Lambda calculi. Cambridge: Cambridge University Press, 1998, xvi, 484. ISBN 0521622778. info
Výukové metody
přednášky
Metody hodnocení
samostatná písemná esej
Vyučovací jazyk
Angličtina
Informace učitele
Předmět je primárně určen pro vážné zájemce z řad doktorských a pokročilých magisterských studentů.
Další komentáře
Studijní materiály
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích jaro 2004, jaro 2005, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2015, jaro 2019, jaro 2020, jaro 2022, jaro 2024.