(This was originally on my old website, I have resurrected it here.)
These are some notes, adding background, after watching Exact Real Arithmetic in Haskell.
We want to represent computable reals, intuitively those that can be computed to any precision by an algorithm. A very interesting fact is that since we can represent algorithms by finite strings, there are countably infinite computable reals, however there are uncountably many reals, so almost all reals are uncomputable!
We also want to exactly compute transcendental functions, e.g. \( \sin \), \( \log \), etc. A transcendental function is an analytic function (locally given by a convergent power series), that doesn't satisfy a polynomial equation.
This is different to traditional arbitrary precision arithmetic because arbitrary precision arithmetic doesn't help with transcendental functions.
We write a sequence \( x_0, x_1, \ldots \) as \( (x_k) \).
A sequence \( (x_k) \) is a Cauchy sequence if for all \( \epsilon > 0 \), there exists \( N > 0 \), such that for all \( m, n > N \), we have \( |x_m - x_n| < \epsilon \).
This just means that for any closeness value we choose, \( \epsilon \), if we go sufficiently far out (\( m,n > N \)) into the sequence, the values are within \( \epsilon \) of each other.
We can construct the reals from Cauchy sequences over rationals. The reals become equivalence classes of Cauchy sequences, i.e. we lump sequences together if their difference converges to 0. In technical speak the reals can be realised as the field of equivalence classes of Cauchy sequences where \( (x_k) \sim (y_k) \) iff \( x_k - y_k \to 0 \). We can embed \( \mathbb{Q} \) in \( \mathbb{R} \) as \( x \mapsto [(x, x, \ldots)] \), where \( [\cdot] \) denotes equivalence class. Addition and multiplication are pointwise, as is negation. We need to be a little more careful for reciprocals, for sequences corresponding to a non-zero real, eventually the sequence will be non-zero, so a reciprocal sequence can be built by concatenating junk values, and the pointwise reciprocal of the non-zero tail.
A computable real can be represented as a fast binary Cauchy sequence if there is a computable sequence \( {n_0, n_1, \ldots} \), such that \( |x - 2^{-k}n_k| < 2^{-k} \).
These enforce a rate of convergence, the factor of \( 2^{-k} \) is to make it an integer sequence.
Check out Correctness of an Implementation of Exact Arithmetic for proofs.
Original link is dead, here is a Wayback Machine link.
This is how Data.Number.CReal works.