Charles Explorer logo
🇨🇿

Lambda-kalkulus a funkcionální programování 1

Předmět na Matematicko-fyzikální fakulta |
NAIL078

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

Anotace

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í.