Overview

(2) Before introducing exact numerical computation, we discuss the usual problems that arise in computation with floating-point numbers, considering a particular example. (3) We then arrive at exact numerical computation in a series of attempts, considering the same example as a guide. (4) At this point the notions of operational and denotational semantics are introduced. In the above development, only operational aspects have been discussed. (5) To make the connection with the denotational aspects, we make the set of decimal expansions into a topological space, so that notions of limit and continuity are available. (6) Using this, we prove the fact, first discovered by Brouwer, that infinite decimal expansions are inadequate as a notation system for an operational semantics of real number computation. We then prove the fact, also discovered by Brouwer, that computable functions are continuous. (7) We then briefly discuss several alternative notation systems for real number computation that mathematicians, logicians and computer scientists have proposed over the years. They are all equivalent, in the sense that one can effectively translate between them, and a Church-Turing Thesis for real number computation has been formulated. Moreover, they are characterized, among all possible notation systems, by a topological maximality property. Among these systems, we choose signed-digit binary notation as a paradigmatic example. (8) Each number is denoted by (infinitely) many syntactical representations. We show that it is not possible to effectively pick a canonical one. (9) We then discuss how the numerical order can be read off from the signed-digit binary notation of two numbers. We show that there is an effective normalization procedure for pairs of signed-digit infinite numerals, such that, for normal pairs, the numerical and lexicographical orders coincide. In particular, a normal pair of numerals denote the same number if and only if they are equal. (10) After this preliminary discussion on the effective character of the order relation, we discuss the main difficulty in real number computation, namely that the (in)equality predicates are undecidable. We show that this is not as bad as it may seem at first sight, by exhibiting a general computable definition-by-cases scheme based on inequality tests. (11) We finish by briefly discussing functional approaches for real number computation, putting the above ideas together.