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.
Supplier department: Department of Computer Science – Faculty of Informatics

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 (eng.) (programme FI, N-IN)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics (programme FI, N-AP)
• Information Systems (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)
• Embedded Systems (programme FI, N-IN)
• Service Science, Management and Engineering (eng.) (programme FI, N-AP)
• Service Science, Management and Engineering (programme FI, N-AP)
• Social Informatics (programme FI, B-AP)
• Theoretical Informatics (programme FI, N-IN)
• 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

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.

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