A certified infinite norm for the implementation of elementary functions
Résumé
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.
Pour garantir la qualité de l’implémentation en arithmétique flottante de fonctionsusuelles f : R → R telles que exp, sin, erf, il faut borner l’erreur ε = p−ffcommise entre f et une approximation p. Cela implique de borner la normeinfinie kεk∞de la fonction d’erreur. Si on veut que l’implémentation soit sure,on ne doit en aucun cas renvoyer une borne inférieure à la valeur exacte.Nous montrons que les approches précéedentes visant à calculer la norme infiniene sont pas satisfaisantes : soit elles ne sont pas sures, soit pas assez précises,soit elles nécessitent un travail manuel trop fastidieux.Nous présentons un algorithme sûr, qui fournit une preuve de sa propre correction,et qui minore et majore automatiquement la norme infinie de fonctionsd’erreur. Cet algorithme est fondé sur une version améliorée d’arithmétiqued’intervalle. Il peut contourner les difficultées dues à une grande cancellationet un mauvais conditionnement autour de points où la fonction d’erreur n’estdéfinie que par continuité.L’algorithme proposé a été implémenté dans un outil logiciel. Il peut générerune preuve de correction pour toute instance sur laquelle il est exécuté.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...