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

• Anglický název: Lambda Calculus and Functional Programming 1
• Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2020
• Semestr: zimní
• E-Kredity: 4
• Rozsah, examinace: zimní s.:2/1, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština, angličtina
• Způsob výuky: prezenční
• Garant: doc. Mgr. Petr Gregor, Ph.D.; RNDr. Jan Hric
• Vyučující: RNDr. Jan Hric
• Třída: Informatika Mgr. - Teoretická informatika
• Kategorizace předmětu: Informatika > Programování, Teoretická informatika
• Je korekvizitou pro: NAIL079
• Je neslučitelnost pro: NAIX078
• Je záměnnost pro: NAIX078

Anotace

čeština

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

Poslední úprava: T_KTI (12.05.2004)

angličtina

Combinatorial calculi and lambda calculi, untyped calculi, representability of recursive functions, Church Rosser property and consistency of lambda calculus, typed lambda calculi, functional programming constructs

Poslední úprava: T_KTI (14.05.2015)

Cíl předmětu

čeština

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

Poslední úprava: Hric Jan, RNDr. (23.04.2015)

angličtina

To learn the theory of lambda-calculus, combinatory logic and explainn connections to functional programming.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Podmínky zakončení předmětu

čeština

Na ústní zkoušce s přípravou prokázat znalost přednesených témat. Zápočet za domácí úlohy a vybrané příklady.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

angličtina

Oral exam on topics from lecture. Homeworks and selected examples for credits.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Literatura

čeština

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

Poslední úprava: T_KTI (23.04.2015)

angličtina

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)

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

Poslední úprava: T_KTI (14.05.2015)

Sylabus

čeština

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

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

angličtina

Introduction. Schoenfinkel combinatorial calculus. Combinatorial objects as

representants of single-parameter functions. Representation of multiple-parameter

functions. Abstraction of variables and unknowns. Combinatorial completeness of

calculus. Calculus consistency. Church-Rosser property.

Lambda calculus, informal description. Variables, free and bound, abstraction

bounded and unbounded. Lambda objects in normal form. Church-Rosser property

and uniformity of lambda objects in normal form.

Lambda calculi. Syntactic description of lambda objects, free and bound variables,

alpha and beta reduction. Extensions of lambda calculus, extensionality, delta rule.

Conversion, application, abstraction. Lambda terms, combinators. Fixed-point theorems.

Representation of computable functions. Numerals, boolean constants, tuples.

Representability of (total) recursive functions by lambda terms.

Consistency of combinatorial calculi and lambda calculi. Church-Rosser property

and calculi consistency. Objects without normal form. Paradoxes. Combinatorial

logic and predicate logic: Curry paradox.

Functional programming and lambda calculus. Computational model of functional

language, reduction, normal forms and functional programming, controlling of

computation in functional programming. Strict functions.

Typed lambda calculus. Extension of lambda calculus language with object types.

Motivation for introduction of types: partial correctness of programs, effectivity of computations. Type

variables and value assignment to type variables. Curry and Church type systems.

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