1: \begin{abstract}

2: We work with the signed digit representation of abstract real numbers, which 

3: roughly is the binary representation enriched by the additional digit -1. 

4: The main objective of this paper is an algorithm which takes a sequence of signed 

5: digit representations of reals and returns the signed digit representation of their limit, if the sequence converges. 

6: As a first application we use this algorithm together with Heron's method to build up an algorithm which 

7: converts the signed digit representation of a non-negative real number into the signed digit 

8: representation of its square root. 

9: 

10: Instead of writing the algorithms first and proving their correctness afterwards, 

11: we work the other way round, in the tradition of program extraction from proofs. 

12: In fact we first give constructive proofs, and from these proofs we then compute the extracted terms, which is the desired algorithm. 

13: The correctness of the extracted term follows directly by the Soundness Theorem 

14: of program extraction. In order to get the extracted term from some proofs which are

15: often quite long, we use the proof assistant Minlog. However, to apply the extracted terms, the programming language Haskell is useful. Therefore after each proof we show a 

16: notation of the extracted term, which can be easily rewritten as a definition in Haskell.

17: 

18: Keywords: signed digit code, real number computation, coinductive definitions, corecursion, program extraction, realizability, convergence of reals, square root, Heron's method

19: \end{abstract}

20: