J.V. Tucker and J.I. Zucker (2005):
Computable total functions,
algebraic specifications and dynamical systems
Journal of Logic and Algebraic Programming, 62, 71-108.
[
preprint.pdf]
Abstract.
Data such as real and complex numbers, discrete and continuous time
data streams, waveforms, scalar and vector fields, and many other functions,
are fundamental for many kinds of computation. In the theory of data,
such data types are modelled using topological,
or metric,
many-sorted
algebras and continuous homomorphisms. A theory of such topological data
types is needed to answer the general questions:
1. What are the computable functions on topological algebras?
2. What methods exist to axiomatically specify functions on topological
algebras?
3. Can all computable functions be specified?
Such a theory seems to be in its infancy: there are many approaches to
computability theory on general and specific spaces, and few approaches
to specification theory. In some earlier papers, we have studied the
questions 1 and 2 with the needs of data type theory in mind, and built
a bridge between computations and specifications to try to answer 3. In
this paper, we extend and combine several of our results, to prove new
theorems that
(i) show the equivalence of some six deterministic or nondeterministic
models of computation on various metric algebras and, in particular, on
spaces R of real numbers;
(ii) provide finite universal algebraic specifications for all the
functions that can be computably approximated on metric algebras and, in
particular, on Euclidean n-space;
(iii) show the existence of finite universal algebraic specifications of
computably approximable finite dimensional deterministic dynamical
systems.
A technical issue is the localisation of uniform continuity using
exhaustions of open sets. We use specifications composed of conditional
equations, inequalities and, for convenience, new exhaustion primitives,
that define functions uniquely up to isomorphism.