We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. The main objective of this paper is an algorithm which takes a sequence of signed digit representations of reals and returns the signed digit representation of their limit, if the sequence converges. As a first application we use this algorithm together with Heron's method to build up an algorithm which converts the signed digit representation of a non-negative real number into the signed digit representation of its square root. Instead of writing the algorithms first and proving their correctness afterwards, we work the other way round, in the tradition of program extraction from proofs. In fact we first give constructive proofs, and from these proofs we then compute the extracted terms, which is the desired algorithm. The correctness of the extracted term follows directly by the Soundness Theorem of program extraction. In order to get the extracted term from some proofs which are 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 notation of the extracted term, which can be easily rewritten as a definition in Haskell.

翻译：本文研究抽象实数的带符号数字表示法，该方法本质上是二进制表示法的扩展，增加了额外数字-1。本文的主要目标是提出一种算法，该算法接收实数带符号数字表示序列，并在序列收敛时返回其极限的带符号数字表示。作为首个应用，我们将该算法与海伦法结合，构建出将非负实数的带符号数字表示转换为其平方根的带符号数字表示的算法。与传统先编写算法后验证正确性的方式不同，我们采用证明程序提取的传统方法逆向操作。实际上，我们首先给出构造性证明，然后从这些证明中计算提取项，即所需算法。提取项的正确性直接遵循程序提取的可靠性定理。为从某些通常较长的证明中获取提取项，我们使用证明辅助工具Minlog。然而，要应用提取项，编程语言Haskell更为实用。因此在每个证明后，我们会展示提取项的表示形式，该形式可轻松重写为Haskell中的定义。