Efficient and accurate computation of upper bounds of approximation errors

Sylvain Chevillard, John Harrison, Miorara Joldes and Christoph Lauter Theoretical Computer Science vol. 412, pp. 1523-1543, 2011.

Abstract:

For purposes of actual evaluation, mathematical functions f are commonly replaced by approximation polynomials p. Examples include floating-point implementations of elementary functions, quadrature or more theoretical proof work involving transcendental functions. Replacing ff by pp induces a relative error e = p/f - 1. In order to ensure the validity of the use of pp instead of ff, the maximum error, i.e. the supremum norm, must be safely bounded above over an interval I, whose width is typically of order 1. Numerical algorithms for supremum norms are efficient, but they cannot offer the required safety. Previous validated approaches often require tedious manual intervention. If they are automated, they have several drawbacks, such as the lack of quality guarantees. In this article, a novel, automated supremum norm algorithm on univariate approximation errors is proposed, achieving an a priori quality on the result. It focuses on the validation step and paves the way for formally certified supremum norms. Key elements are the use of intermediate approximation polynomials with bounded approximation error and a non-negativity test based on a sum-of-squares expression of polynomials. The new algorithm was implemented in the Sollya tool. The article includes experimental results on real-life examples.

PDF

Bibtex entry:

@ARTICLE{chevillard-approx,
        author          = "Sylvain Chevillard and John Harrison and
                           Miorara Joldes and Christoph Lauter",
        title           = "Efficient and accurate computation of upper bounds
                           of approximation errors",
        journal         = "Theoretical Computer Science",
        year            = 2011,
        volume          = 412,
        pages           = "1523--1543"}