Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
14th November, 1997: Martin Escardo
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 14th November, 1997: Martin Escardo

Speaker: Martin Escardo
Title: Real Number Computation, Domain Theory, and PCF
Time: 14th November, 1997, 14:00
Abstract:

Dana Scott proposed in the early seventies to use a certain interval domain as a model of computation with real numbers via their finitary approximations. If we endow the domain with the Scott topology and take the subspace of total elements, we get the real numbers with their usual topology. This relates domain theory to classical real analysis in a simple and useful way. (More connections will be discussed in the talk.)

An effective presentation of the interval domain induces a notion of computable (total or partial) real number and function. Different choices of bases and enumerations induce different sets of computable numbers and functions. However, we show that any two effective presentations for which very basic functions are computable give rise to the same computable numbers and functions. We also discuss connections to classical approaches to real number computability.

The basic operations discussed above are used as the primitive constants of an extension of PCF with a ground type for real numbers. This "Real PCF" enjoys a computational adequacy property (operational and denotational semantics coincide). If certain parallel features are included, all computable elements and functions are definable in the language. (More about parallelism in the talk.)

If we put the primitive "constructors" and "destructors" together, we obtain an algebra and a coalgebra of a functor. They from an "almost" free algebra a la Freyd, in a precise sense of "almost". This gives rise to (co)induction principles. These principles are used to prove the above results about invariance of computability and full definability.