PředmětyPředměty(verze: 837)
Předmět, akademický rok 2018/2019
   Přihlásit přes CAS
Lambda-kalkulus a funkcionální programování I - NAIL078
Anglický název: Lambda Calculus and Functional Programming I
Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2015
Semestr: zimní
E-Kredity: 5
Rozsah, examinace: zimní s.:2/1 Z+Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: čeština, angličtina
Způsob výuky: prezenční
Garant: RNDr. Jan Hric
Třída: Informatika Mgr. - Teoretická informatika
Kategorizace předmětu: Informatika > Programování, Teoretická informatika
Je korekvizitou pro: NAIL079
Anotace -
Poslední úprava: T_KTI (12.05.2004)
Kombinatorické kalkuly a lambda kalkuly, netypované kalkuly, representovatelnost rekursivních funkcí. Churchova a Rosserova vlastnost a konsistence lambda kalkulu. Typovaný lambda kalkulus a jeho vztah k funkcionálnímu programovaní.
Cíl předmětu
Poslední úprava: RNDr. Jan Hric (23.04.2015)

Naučit teorii lambda-kalkulu, kombinatorické logiky a ukázat souvislosti s funkcionálním programováním.

Literatura -
Poslední úprava: T_KTI (23.04.2015)

Henk Barendregt, Erik Barensen: Introduction to Lambda Calculus, 1998, rev. 2000, 53 s. http://www.cs.ru.nl/E.Barendsen/onderwijs/T3/materiaal/lambda.pdf

Hendrik Pieter Barendregt: The Lambda Calculus: Its Syntax and Semantics. Elsevier, Amstredam, 1984. Rev. ed. 1998, 621 s. 0-444-86748-1

Henk Barendregt, Wil Dekkers, Richard Statman: Lambda Calculus with Types. Cambridge University Press, Cambridge, 2010. 682 s. (rev. 2013, 978-0-521-76614-2)

J. Roger Hindley, Jonathan P. Seldin: Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, Cambridge, 2. vyd., 2008, 360 s. 978-0-521-89885-0 (1986. 359 s. 0-521-31839-4)

Jiří Zlatuška: Lambda-kalkul. Masarykova univerzita, Brno, 1993. 264 s. 80-210-0826-1

Katalin Bimbó: Combinatory Logic, The Stanford Encyclopedia of Philosophy (Spring 2013 Edition), Edward N. Zalta (ed.), http://plato.stanford.edu/archives/spr2013/entries/logic-combinatory/#4

Sylabus -
Poslední úprava: RNDr. Jan Hric (28.04.2018)

Úvod. Motivace a vztah k funkcionálnímu programování. Lambda kalkulus, neformální popis. Objekty jako representanti funkcí jedné proměnné. Representace funkcí více proměnných. Abstrakce vzhledem k proměnným a neurčitým. Syntaktický popis lambda objektů, volné a vázané proměnné, abstrakce. Redukce, pravidla alfa a beta redukce, rovnostní teorie.

Lambda termy, kombinátory. Věty o pevném bodě. Numerály, booleovské konstanty, uspořádané dvojice. Representace vyčíslitelných funkcí. Nerozhodnutelné problémy. Kódování lambda-termů. Representovatelnost (totálních) rekursivních funkcí pomocí lambda termů. Sémantika lambda kalkulu.

Kombinatorické kalkuly, varianty. Bezespornost kombinatorických kalkulů a lambda kalkulů. Kombinatorická úplnost kalkulu. Objekty, které nemají normální tvar. Paradoxy. Kombinatorická logika a predikátová logika: Curryho paradox.

Lambda objekty v normálním tvaru. Church-Rosserova vlastnost a jednoznačnost lambda-objektů v normálním tvaru. Další rozšíření lambda kalkulu, extensionalita, delta pravidla.

Funkcionální programování a lambda kalkulus. Výpočetní model funkcionálního jazyka, redukce, normální tvary a funkcionální programování. Řízení výpočtu ve funkcionálním programování, strategie výpočtu. Striktní funkce.

Typový lambda kalkul. Rozšíření jazyka lambda kalkulu o typy objektů. Motivace zavedení typů: částečná správnost programů, efektivnost výpočtů. Curryho a Churchův systém typování, jejich vztah.

 
Univerzita Karlova | Informační systém UK