Higher-order exact real number computation with Real PCF

Martin Escardo

(University of Birmingham)

Real PCF is an extension of PCF with a ground type for (total and partial) real numbers. Thus, its types include R (real numbers), [R->R] (real valued functions of a real variable), [N->R] (sequences of real numbers), [[N->R]->R] (functionals taking sequences to numbers, such as limit operators), [[R->R]->R] (functionals taking functions to numbers, such as integration and global maxima operators), and so on.

The operational semantics of Real PCF is computationally adequate with respect to its standard model. Roughly, this means that every finite piece of information about the value of a program of ground type is computed in finitely many steps. Moreover, Real PCF extended with a certain search operator is universal with respect to its standard model, in the sense that every computable element and every computable function (of any order) of the model is denotable by at least one Real PCF term.

In this talk I'll present these and other results on Real PCF, and I'll formulate some open problems and conjectures.
Tuesday 28th November 2000, 14:00
Robert Recorde Room
Department of Computer Science