Recent Advances in -definability over Continuous Data Types
Margarita Korovina June 2003 |
Abstract:
The purpose of this paper is to survey our recent research in
computability and definability over continuous data types such as the real
numbers, real-valued functions and functionals. We investigate the expressive
power and algorithmic properties of the language of -formulas
intended to represent computability over the real numbers. In order to
adequately represent computability we extend the reals by the structure of
hereditarily finite sets. In this setting it is crucial to consider the real
numbers without equality since the equality test is undecidable over the
reals. We prove Engeler's Lemma for -definability over the reals
without the equality test which relates -definability with
definability in the constructive infinitary language
.
Thus, a relation over the real numbers is -definable if and only if
it is definable by a disjunction of a recursively enumerable set of
quantifier free formulas. This result reveals computational aspects of
-definability and also gives topological characterisation of -definable relations over the reals without the equality test. We also
illustrate how computability over the real numbers can be expressed in the
language of -formulas
Available as PostScript, PDF, DVI. |