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