A certified infinite norm for the implementation of elementary functions

Abstract : The high-quality floating-point implementation of useful functions f : R → R,such as exp, sin, erf requires bounding the error ε = p−f f of an approximation p with regard to the function f. This involves bounding the infinite norm kεk∞ of the error function. Its value must not be underestimated when implementations must be safe.Previous approaches for computing infinite norm are shown to be either unsafe,not sufficiently tight or too tedious in manual work.We present a safe and self-validating algorithm for automatically upper- andlower-bounding infinite norms of error functions. The algorithm is based onenhanced interval arithmetic. It can overcome high cancellation and high conditionnumber around points where the error function is defined only by continuousextension.The given algorithm is implemented in a software tool. It can generate a proofof correctness for each instance on which it is run.
Document type :
Reports
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102507
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 1:54:46 PM
Last modification on : Friday, April 19, 2019 - 1:38:15 AM

File

RR2007-26.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102507, version 1

Collections

Citation

Sylvain Chevillard, Christoph Quirin Lauter. A certified infinite norm for the implementation of elementary functions. [Research Report] Laboratoire de l'informatique du parallélisme. 2007, 2+11p. ⟨hal-02102507⟩

Share

Metrics

Record views

12

Files downloads

31