In Chapter 4 we developed algorithms for the basic arithmetic operations. This chapter uses these operations as building blocks to implement higher level transcendental functions.

In order to compute the transcendental functions, we first define a function which converts a real represented as a sequence of nested intervals (as described in section 3.5) into a single signed binary numeral. This allows us to compute the limits of Cauchy sequences very simply, and hence many transcendental functions which can be defined as the limits of such sequences.

This general approach used to compute limits was originally proposed by Martín Escardó (personal communication). We develop this idea and give an algorithm and a proof of correctness and convergence here.