FI:IA081 Lambda calculus - Course Information

IA081 Lambda calculus

Extent and Intensity

2/0. 3 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. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Jiří Zlatuška, CSc.

Timetable

Mon 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

• Applied Informatics (programme FI, N-AP)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics (programme FI, N-AP)
• Information Systems (programme FI, N-IN)
• Informatics (programme FI, D-IN)
• Informatics (programme FI, M-IN)
• Informatics (programme FI, N-IN)
• Parallel and Distributed Systems (programme FI, N-IN)
• Computer Graphics (programme FI, N-IN)
• Computer Networks and Communication (programme FI, N-IN)
• Computer Systems (programme FI, N-IN)
• Embedded Systems (eng.) (programme FI, N-IN)
• Theoretical Informatics (programme FI, N-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-SS)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-TV)
• Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
• Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
• Image Processing (programme FI, N-AP)

Course objectives

This course contains basic techniques and results of the theory of sequential functions as described by the lambda-calculus and combibatoru logic. The course contains the typed and untyped version of the formalism, as well as basic results concerning models of lambda-calulus. Lambda-calculus is important for understanding recursive constructs used in programming as well in the corresponding semantics constructs, and it provides 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

Assessment methods (in Czech)

přednášky a samostané studium dle literatury zadané přednášejícím

Language of instruction

English

Further comments (probably available only in Czech)

The course is taught once in two years.

• Enrolment Statistics (Spring 2008, recent)
  
• Permalink: https://is.muni.cz/course/fi/spring2008/IA081