Předmět se zabývá metodami funkcionálního programování, vztahem k lambda kalkulu a souvisejícími výpočetními modely. Obsah je zaměřen na teoretické aspekty funkcionálního programování a výrazně rozšiřuje úvodní představení základních konceptů v bakalářském a magisterském studiu. Funkcionální programování a lambda kalkul: Syntax lambda výrazů a jejich vyhodnocování. Aplikace funkcí a currying, Lambda abstrakce. Operační sémantika lambda kalkulu: vázané a volné proměnné, beta-konverze, alfa-konverze; vzájemná zastupitelnost. Přepisovací systémy, terminace, konfluence, Churchova-Rosserova vlastnost, normální formy. Vazba na čistý lambda kalkul. Reprezentace booleovských formulí, přirozených čísel, $n$-tic. Vyčíslitelné funkce: lambda-vyčíslitelné, totální rekurzivní, částečné rekurzivní. Věty o pevném bodu, nerozhodnutelné vlastnosti. Rekurzivní funkce, Y kombinátor jako lambda abstrakce. Denotační sémantika lambda kalkulu. Překlad vyššího programovacího jazyka do lambda kalkulu: let-výrazy, letrec-výrazy, strukturované typy a porovnávání se vzory. Funkcionální programování a uspořádané algebry: Specifikace abstraktních datových typů: vícedruhové algebry, jejich podalgebry, morfismy a součiny; princip konečné algebraické rekurze; ekvacionální teorie, vícedruhová ekvacionální logika; ekvacionální specifikace; počáteční sémantika a operační sémantika. Uspořádané algebry, jejich morfismy a součiny. Uspořádané variety a jejich charakterizace pomocí volných uspořádaných algeber. Logika nerovností (inekvacionální logika). Striktní uspořádané algebry, omega-uspořádané algebry. Rekurzivní schémata funkcionálních programů a jejich sémantika, vypočtené hodnoty, symbolická řešení, sémantické ekvivalence. Zásobníkový model vyhodnocování symbolických výrazů: Funkcionální programy jako posloupnosti symbolických výrazů. Zásobníkový vyhodnocovací proces. Elementy jazyka: primitivní a definované procedury (funkce), speciální formy, makra, prostředí, páry. Rozšiřování vyhodnocovacího procesu: lexikální a dynamické vazby, líné vyhodnocování, vyhodnocování s vyrovnávací pamětí, imperativní rysy, únikové funkce, aktuální pokračování, nedeterminismus a paralelismus. Metody implementace interpretů a překladačů funkcionálních programovacích jazyků.
|
-
Barendregt H. P. (1997). The Lambda Calculus: its Syntax and Semantics. 2nd reprint. Elsevier, Amsterdam.
-
Bird R., Wadler P. (1988). Introduction to Functional Programming. Prentice Hall, Englewood Cliffs, New Jersey.
-
H. Abelson, G. J. Sussman. (1985). Structure and Interpretation of Computer Programs (SICP). MIT Press.
-
Church A. (1941). The Calculi of Lambda Conversion. Princeton University Press, Princeton, NJ.
-
Leeuwen, J. van (ed.). (1994). Handbook Of Theoretical Computer Science: Formal Models and Semantics. Volume B, Elsevier.
-
Manis V. S., Little J. J. (1995). The Schematics of Computation. Prentice Hall, Englewood Cliffs, New Jersey.
-
Peyton Jones S. L. (1987). The Implementation of Functional Programming Languages. Prentice Hall.
-
Wechler W. (1992). Universal Algebra for Computer Scientists. Springer-Verlag Berlin Heidelberg.
-
Zlatuška J. (1993). Lambda-kalkul. Vydavatelství MU, Brno.
|