IA081 Lambda calculus

Faculty of Informatics
Spring 2024
Extent and Intensity
2/0/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Teacher(s)
prof. RNDr. Jiří Zlatuška, CSc. (lecturer)
Guaranteed by
prof. RNDr. Jiří Zlatuška, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Jiří Zlatuška, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Tue 10:00–11:50 B411
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
fields of study / plans the course is directly associated with
Course objectives
The goal is to introduce lambda-calculus to students and to demonstrate expressive power of lambda-caluclus on a couple of general computation concepts.
Learning outcomes
At the end of this cource, students shall learnd and understand basic techniques and results of the theory of sequential functions as described by the lambda-calculus and combinatoru logic; will understand the basics of the typed and untyped version of the formalism; shall learn basic elements of model construction for of lambda-calulus; shall be able to employ recursive constructs used in programming as well in the corresponding semantics constructs; will be abble to use it as a reference formalism useful for variaous applications.
Syllabus
  • Pure lambda-calculus: lambda-terms, structure of terms, equational theories.
  • Reductions: one-way transformations, general reductions, beta-reduction.
  • Lambda-calculus and computations: coding, recursive definitions, lambda-computability, fixed-point combinators, undecidable properties.
  • Modification of the theory: combinatory logic, extensionality, eta-reduction.
  • Typed lambda-calculus: types and terms, normal forms, set models, strong normalization, types as formulae.
  • Domain models: complete partial orders, domains, least fixed points, partiality.
  • Domain construction: compound domains, recursive domain construction, limit domains.
Literature
  • ZLATUŠKA, Jiří. Lambda-kalkul. 1. vyd. Brno: Masarykova univerzita, 1993, 264 s. ISBN 8021008261. info
  • BARENDREGT, H. P. Lambda calculus : its syntax and semantics. Rev. ed. Amsterdam: Elsevier, 1998, xv, 621 s. ISBN 0-444-86748-1. info
  • HINDLEY, J. Roger and J. P. SELDIN. An Introduction to Combinators and the (lambda)-calculus. Cambridge: Cambridge University Press, 1986, 360 s. ISBN 0521318394. info
  • AMADIO, Roberto M. and Pierre-Louis CURIEN. Domains and Lambda calculi. Cambridge: Cambridge University Press, 1998, xvi, 484. ISBN 0521622778. info
Teaching methods
lectures
Assessment methods
individual written essay
Language of instruction
English
Further comments (probably available only in Czech)
Study Materials
The course is taught once in two years.
The course is also listed under the following terms Spring 2004, Spring 2005, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2015, Spring 2017, Spring 2019, Spring 2020, Spring 2022.
  • Enrolment Statistics (recent)
  • Permalink: https://is.muni.cz/course/fi/spring2024/IA081