*Abstract:*

We develop a theory of higher-order exact real number computation based on Scott domain theory. Our main object of investigation is a higher-order functional programming language, Real PCF, which is an extension of PCF with a data type for real numbers and constants for primitive real functions. Real PCF has both operational and denotational semantics, related by a computational adequacy property.

In the standard interpretation of Real PCF, types are
interpreted as continuous Scott domains. We refer to the domains in
the universe of discourse of Real PCF induced by the standard
interpretation of types as the *real numbers type
hierarchy*. Sequences are functions defined on natural numbers,
and predicates are truth-valued functions. Thus, in the real
numbers types hierarchy we have real numbers, functions between
real numbers, predicates defined on real numbers, sequences of real
numbers, sequences of sequences of real numbers, sequences of
functions, functionals mapping sequences to numbers (such as
limiting operators), functionals mapping functions to numbers (such
as integration and supremum operators), functionals mapping
predicates to truth-values (such as existential and universal
quantification operators), and so on.

As it is well-known, the notion of computability on a domain
depends on the choice of an effective presentation. We say that an
effective presentation of the real numbers type hierarchy is
*sound* if all Real PCF definable elements and functions are
computable with respect to it. The idea is that Real PCF has an
effective operational semantics, and therefore the definable
elements and functions should be regarded as concretely computable.
We then show that there is a unique sound effective presentation of
the real numbers type hierarchy, up to equivalence with respect to
the induced notion of computability. We can thus say that there is
an *absolute notion of computability* for the real numbers
type hierarchy.

All computable elements and all computable first-order functions
in the real numbers type hierarchy are Real PCF definable. However,
as it is the case for PCF, some higher-order computable functions,
including an existential quantifier, fail to be definable. If a
constant for the existential quantifier (or, equivalently, a
computable supremum operator) is added, the computational adequacy
property remains true, and Real PCF becomes a *computationally
complete programming language*, in the sense that all
computable functions of all orders become definable.

We introduce induction principles and recursion schemes for the real numbers domain, which are formally similar to the so-called Peano axioms for natural numbers. These principles and schemes abstractly characterize the real numbers domain up to isomorphism, in the same way as the so-called Peano axioms for natural numbers characterize the natural numbers. On the practical side, they allow us to derive recursive definitions of real functions, which immediately give rise to correct Real PCF programs (by an application of computational adequacy). Also, these principles form the core of the proof of absoluteness of the standard effective presentation of the real numbers type hierarchy, and of the proof of computational completeness of Real PCF.

Finally, results on integration in Real PCF consisting of joint work with Abbas Edalat are included.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file