Limits with Signed Digit Streams
Franziskus Wiesnet

TL;DR
This paper develops algorithms for signed digit representations of real numbers, including limits and square roots, using constructive proofs and program extraction techniques with proof assistants and functional programming languages.
Contribution
It introduces a novel algorithm for limits of signed digit streams and applies it to compute square roots, using proof extraction from constructive proofs.
Findings
Algorithm for limits of signed digit streams
Constructive proofs enable direct extraction of algorithms
Implementation in Haskell demonstrates practical applicability
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Computability, Logic, AI Algorithms
