Abstract

In this talk, we develop a domain theoretic and computationally feasible framework for exact real arithmetic. We present a formal account of incremental digit representations born out of domain theory, which includes the redundant binary representation and continued fraction representation. The generalization of both these fundamental representations for the real numbers leads to the notion of a general normal product constructed using Möbius transformations. In this talk, we develop the work of Vuillemin, Nielsen and Kornerup, and show that incrementality and efficiency can be simultaneously achieved in exact real arithmetic. We examine a specialization of general normal products called exact floating point with elegant mathematical properties on the one-point compactification of the real line. Real functions are captured by the composition of 2-dimensional Möbius transformations, leading to the notion of expression trees. Various reduction rules and a lazy form of information flow analysis is used to allow expression trees to be converted efficiently into the exact floating point representation. Algorithms for the basic arithmetic operations and the transcendental functions are presented using the redundant if statement for range reduction and various expression trees derived from the theory of continued fractions.