Martín Escardó

LFCS, Informatics, University of Edinburgh

Introduction to exact real number computation

Abstract

Instead of approximating a number by a fixed-length finite numeral, one can realize a number by a ``generator''. A real number generator is a procedure that successively generates as many digits as one is willing to wait for (and, of course, as the resources of the computer allow). Thus, operations on numbers are realized by operations on number generators. For instance, addition is realized by a process that, given generators for numbers x and y, produces a generator for the number x+y. In this case, computations are usually performed by demand; if one wants 5 correct digits of y=g(f(x)), one may need 20 digits of the intermediate computation f(x), and 7 digits of the input x. In this way, round-off errors are completely avoided.

Exact computation is not limited to the basic operations, of course. For example, it is possible to compute transcendental functions, limits of Cauchy sequences, definite integrals of functions, roots of (certain) functions, etc.

In this talk I'll introduce the theory of real number computation. Challenging problems arise from the fact that equality of real numbers is undecidable. More generally, all computable functions are continuous (at their domain of definition). Primitive recursive functions are not enough; even the division operation (a partial function) is not primitive recursive, because it takes unbounded time to tell a number apart from zero and start making progress.

Are these limitations due to the discrete character of computers (and of logic, for that matter)? Do deterministic physical processes implement computable functions? There are differential equations, e.g. the wave equation, whose solution is non-computable even when its initial value is computable.

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections.
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh