Lazy computation with exact real numbers

We provide a semantical framework for exact real arithmetic using linear fr actional transformations on the extended real line. We present an extension of PCF with a real type which introduces an eventually breadth-first strat egy for lazy evaluation of exact real numbers. In this language, we present the constant redundant if, rif, for defining functions by cases which, in contrast to parallel if (pif), overcomes the problem of undecidability of c omparison of real numbers in finite time. We use the upper space of the one -point compactification of the real line to develop a denotational semantic s for the lazy evaluation of real programs. Finally two adequacy results ar e proved, one for programs containing rif and one for those not containing it. Our adequacy results in particular provide the proof of correctness of algorithms for computation of single-valued elementary functions.