F29FA - Foundations 1

Course leader(s):

• Fairouz Dib Kamareddine (Edinburgh, September)
• Adrian Turcanu (Dubai, September)
• Mahmoud Mousa (Dubai, September)
• Thomas Anung Basuki (Malaysia, September)

Syllabus

1.1 An introduction to the crisis of the foundations of mathematics, Frege’s abstraction principle for generalised functions and to why the lambda calculus was conceived and how it influenced programming languages and proof checkers.

2.1 The syntax and semantics of the language of the computable the lambda calculus and its implementation. Grafting versus substitution, reduction, evaluation.

3.1 Reduction strategies, confluence, termination, normalisation, standardisation, and other properties

4.1 Different languages de Bruijn syntax, combinators, item notation, explicit syntax, etc. and translations between them as well as implementation

5.1 Defining the computable inside the lambda calculus, including number arithmetic, propositional logic, lists, fixed points and recursion.

6.1 Undecidability and showing the limit of computation. The undefinability of the non-computable. The undefinability of “termination”. The undefinability of the “halting problem”

Learning outcomes

By the end of the course, students should be able to do the following:

• use the syntactic rules of lambda calculus to represent functions and to interpret their meaning.
• differentiate bound and free variables to perform capture-free substitution.
• evaluate given terms using different strategies in the context of alpha, beta and eta reduction.
• analyse the normalisation behaviour of a term.
• distinguish different syntactic styles and use translation functions to navigate between notations (e.g., variable names/de Bruijn indices/combinatory logic/item notation).
• use fixed point theorems to find fixed points of expressions or to solve equations and to represent recursion.
• differentiate computable and non-computable functions in terms of lambda definability using Church’s thesis.
• use lambda calculus to represent a variety of computable expressions or use reasoning to show that something is not computable.

Further details

Curriculum explorer: Click here

SCQF Level: 9

Credits: 15