Exact Real Arithmetic with Perturbation Analysis and Proof of Correctness
Sarmen Keshishzadeh, Jan Friso Groote

TL;DR
This paper introduces a simple real number representation and top-down approximation algorithms for algebraic and transcendental operations, with proofs of correctness and a perturbation analysis ensuring minimal recomputation.
Contribution
It presents a novel approach combining a simple real number model with rigorous proofs and perturbation analysis to guarantee correct and efficient arbitrary-precision computations.
Findings
Algorithms guarantee correct approximations of algebraic and transcendental operations.
Perturbation analysis shows recomputation is only done when necessary.
Full proofs establish the necessity of iterative calculations for precision.
Abstract
In this article, we consider a simple representation for real numbers and propose top-down procedures to approximate various algebraic and transcendental operations with arbitrary precision. Detailed algorithms and proofs are provided to guarantee the correctness of the approximations. Moreover, we develop and apply a perturbation analysis method to show that our approximation procedures only recompute expressions when unavoidable. In the last decade, various theories have been developed and implemented to realize real computations with arbitrary precision. Proof of correctness for existing approaches typically consider basic algebraic operations, whereas detailed arguments about transcendental operations are not available. Another important observation is that in each approach some expressions might require iterative computations to guarantee the desired precision. However, no formal…
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
TopicsNumerical Methods and Algorithms · Computability, Logic, AI Algorithms · Embedded Systems Design Techniques
