University of Cambridge

Logic
&
Semantics

Exact Real Arithmetic using Mobius Transformations

By Peter Potts (13th November 1998)

In this talk, I will develop a domain theoretic and computationally feasible framework for exact real arithmetic. I will 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 Mobius transformations. In this talk, I will develop the work of Vuillemin, Nielsen and Kornerup, and show that incrementality and efficiency can be simultaneously achieved in exact real arithmetic. I will 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 Mobius transformations, leading to the notion of expression trees. 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. Finally, I will describe a denotational semantics for the redundant if statement.

LS Home page or Talks in 1998/99