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”.
Learning Outcomes: Subject Mastery
Understanding, Knowledge and Cognitive Skills Scholarship, Enquiry and Research (Research-Informed Learning)
- Understanding the challenges of definability, calculability and reasoning inside a language.
- Understanding of different variable techniques (de Bruijn indices, combinator variables).
- Understanding of variable binding and capture-free substitution.
- Navigate between different computation paths and understand the implication of different evaluation strategies.
- Navigate between different syntactic styles and languages.
- Knowledge of how to represent computations in the λ-calculus.
- Connecting syntax to meaning and distinguishing what is inside a language and what is external.
- Gain an understanding of the syntax of the computable and the connection to fixed points and recursion.
- Gain an understanding of how to syntactically show that something is not computable.
Learning Outcomes: Personal Abilities
Industrial, Commercial & Professional Practice Autonomy, Accountability & Working with Others Communication, Numeracy & ICT
- To be able to think about the meaning of programs and computations mathematically.
- To understand the limit of computation and language and be aware of contradictions and the need to be thorough and careful.
SCQF Level: 9.
Credits: 15.