Předmět Lambda-kalkulus a funkcionální programování I (NAIL078)

Na serveru studentino.cz naleznete nejrůznější studijní materiály: zápisky z přednášek nebo cvičení, vzorové testy, seminární práce, domácí úkoly a další z předmětu NAIL078 - Lambda-kalkulus a funkcionální programování I, Matematicko-fyzikální fakulta, Univerzita Karlova v Praze (UK).

Materiál	Typ	Datum	Počet stažení

Cíl

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

Sylabus

Ú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: částečná správnost programů, efektivnost výpočtů. Curryho a Churchův systém typování, jejich vztah.

Literatura

Henk Barendregt, Erik Barensen: Introduction to Lambda Calculus, 1998, rev. 2000, 53 s. http://www.cs.ru.nl/E.Barendsen/onderwijs/T3/materiaal/lambda.pdfHendrik Pieter Barendregt: The Lambda Calculus: Its Syntax and Semantics. Elsevier, Amstredam, 1984. Rev. ed. 1998, 621 s. 0-444-86748-1Henk 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-1Katalin 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

Garant

RNDr. Jan Hric