**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**