Course co-ordinator(s): Prof Fairouz Kamareddine (Edinburgh), Adrian Turcanu (Dubai), Dr Thomas Basuki (Malaysia).
Aims:
- To give an introduction to and an appreciation of the syntax and meaning of the computable/decidable, and to the principles of reduction and evaluation of programs/functions as well as the pros and cons of different strategies such as termination and efficiency.
- To give an understanding of translating and moving between different syntax and formalisms while preserving the important properties.
- To give an understanding of what constitutes the object versus meta language of the syntax and to be able to distinguish between what is definable in a language and what is not.
- To gain practice into how a syntax can be passed to a machine and an initial understanding into bridging theory and implementation.
Detailed Information
Course Description: Link to Official Course Descriptor.
Pre-requisites: none.
Location: Dubai, Edinburgh, Malaysia.
Semester: 1.
Syllabus:
- 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.
- The syntax and semantics of the language of the computable (the lambda calculus) and its implementation. Grafting versus substitution, reduction, evaluation.
- Reduction strategies, confluence, termination, normalisation, standardisation, and other properties.
- Different languages (de Bruijn syntax, combinators, item notation, explicit syntax, etc.) and translations between them as well as implementation.
- Defining the computable inside the lambda calculus, including number arithmetic, propositional logic, lists, fixed points and recursion.
- Undecidability and showing the limit of computation. The undefinability of the non-computable. The undefinability of “termination”. The undefinability of the “halting problem”.
SCQF Level: 9.
Credits: 15.