



Next: Mathematical Methods for Computer Up: Lent Term 2008: Part Previous: Digital Communication I Contents
Foundations of Functional Programming
Lecturer: Dr M.J. Parkinson
No. of lectures: 12
This course is a prerequisite for Types (Part II).
Aims
This course aims (a) to show how lambda-calculus and related theories can provide a foundation for a large part of practical programming, (b) to present students with one particular type analysis algorithm so that they will be better able to appreciate the Part II Types course, and (c) to provide a bridge between the Part IA Foundations of Computer Science course and the theory options in Part II.
Lectures
- Introduction.
Combinators. Constants and Free Variables. Reduction.
Equality. The Church-Rosser theorem. Normal forms.
- The Lambda calculus.
Lambda-terms, alpha and beta conversions.
Free and bound variables. Abbreviations in the notation.
Pure and applied lambda calculi. Relationship
between combinators, lambda calculus and typical programming languages.
Eager and Lazy evaluation.
- Encoding of data: booleans, tuples, lists and trees, numbers.
The treatment of recursion: the Y combinator and its use.
- Modelling imperative programming styles: handling state information
and the continuation-passing style. Return address seen as an additional
continuation parameter.
- Relationship between this and Turing computability, the halting
problem etc.
- Combinator reduction as tree-rewrites.
Conversion from lambda-calculus to
combinators. The treatment of lambda-bindings
in an interpreter: the environment. Closures. ML implementation of
lambda-calculus. SECD machine. Brief survey of performance issues.
- Let-polymorphism reviewed following the Part IA coverage
of ML. Unification. A type-reconstruction algorithm. Decidability and
potential costs.
Objectives
At the end of the course students should
- understand the rules for the construction and processing
of combinatory terms and terms in the lambda calculus
- know how to model all major aspects of general-purpose
computation in terms of these primitives
- know how lambda terms may be efficiently interpreted by machine
- be able to derive ML-style type judgements
for languages based upon the lambda-calculus
Recommended reading
Hindley, J.R. & Seldin, J.P. (1986). Introduction to combinators and lambda-calculus. Cambridge University Press (now out of print but try a
library).
Revesz, G.E. (1988). Lambda calculus, combinators and functional programming. Cambridge University Press (now out of print but try a library).




Next: Mathematical Methods for Computer Up: Lent Term 2008: Part Previous: Digital Communication I Contents