Limits of real numbers in the binary signed digit representation

We extract verified algorithms for exact real number computation fromconstructive proofs. To this end we use a coinductive representation of realsas streams of binary signed digits. The main objective of this paper is theformalisation of a constructive proof that real numbers are closed with respectto limits. All the proofs of the main theorem and the first application areimplemented in the Minlog proof system and the extracted terms are furthertranslated into Haskell. We compare two approaches. The first approach is adirect proof. In the second approach we make use of the representation of realsby a Cauchy-sequence of rationals. Utilizing translations between the tworepresenation and using the completeness of the Cauchy-reals, the proof is veryshort. In both cases we use Minlog's program extraction mechanism toautomatically extract a formally verified program that transforms a convergingsequence of reals, i.e.~a sequence of streams of binary signed digits togetherwith a modulus of convergence, into the binary signed digit representation ofits limit. The correctness of the extracted terms follows directly from thesoundness theorem of program extraction. As a first application we use theextracted algorithms together with Heron's method to construct an algorithmthat computes square roots with respect to the binary signed digitrepresentation. In a second application we use the convergence theorem to showthat the signed digit representation of real numbers is closed undermultiplication