Exact Real Arithmetic with Perturbation Analysis and Proof of Correctness

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 reasoning is provided to prove that such iterative calculations are essential in the approximation procedures. In our approximations of real functions, we explicitly relate the precision of the inputs to the guaranteed precision of the output, provide full proofs and a precise analysis of the necessity of iterations.