Alex Simpson (University of Edinburgh, U.K.)

Real numbers in type theory

Abstract: The course will look at two different approaches to implementing real-number computation in type theory. One approach is to encode real numbers using any one of a range of standard encodings (Cauchy sequences, signed binary, etc.). An alternative, which will be the main focus of the course, is to add real numbers as an abstract datatype, thereby providing an implementation-independent interface for real-number computation. One substantial issue concerning the second approach is how to realise it at all: what is a suitable interface for real-number computation? A second concern is to relate the two approaches.

To keep matters simple, much of the course will look at implementing the closed interval [-1,1] of real numbers in the basic setting of simply-typed lamda-caclculus with natural numbers (Goedel's System T). But the course will end by extending to the full real line, on the one hand, and dependent type theory, on the other.

Lecture 1: Simply-typed lambda-calculus and System T. Encoding real-number computation in System T. Adding an abstract datatype for [-1,1]. Programming using the abstract datatype. Equational reasoning with the abstract datatype.

Lecture 2: Implementing the abstract datatype via compilation back to system T. Completeness of the abstract datatype relative to T-computability. Necessity of the double function.

Lecture 3: Implementing the full real line. Extending the type theory to dependent type theory. Directions for further research.

The course is based longstanding but still ongoing joint work with Martin Escardo (University of Birmingham).