IA081 Lambda kalkul

Fakulta informatiky
jaro 2004
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.
Rozvrh
Po 9:00–10:50 B411
Předpoklady
! I081 Lambda kalkul
Omezení zápisu do předmětu
Předmět je určen pouze studentům mateřských oborů.
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Tento předmět seznamuje se základnimi pojmy, technikami a výsledky teorie sekvenčních funkcí v podobě lambda-kalkulu a kombinatorické logiky. Tématem kursu je typová i netypová varianta těchto formalismů, jejich použití pro formalizaci vyčíslitelnosti a uvedeny jsou i základní výsledky týkající se modelů lambda-kalkulu. Lambda-kalkul má význam pro pochopení rekurzivních konstrukcí v programování i příslušných modelech a je referenčním formalismem užívaným v řadě 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
Metody hodnocení
přednášky a samostané studium dle literatury zadané přednášejícím
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 stududentů
Další komentáře
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích jaro 2005, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2015, jaro 2017, jaro 2019, jaro 2020, jaro 2022, jaro 2024.