Boldo, Sylvie
- Daumas, Marc
Rapport de recherche de l'INRIA -
Rhone-Alpes ,
Equipe :
ARENAIRE 38 pages - Janvier 2003 - Document en anglais
Titre français : Un test simple caractérisant la précision de la règle de Horner pour un
polynôme
Abstract : Polynomials are used in many applications and hidden in libraries such as libm. Whereas the accuracy of the functions used by linear algebra have long been studied, little is available to decide on one scheme to evaluate a polynomial. Common knowledge solely emphasizes that Horner's rule is a good scheme unless the indeterminate is close to one of the polynomial's roots. We propose here a criterion for one step of Horner's scheme to be faithful. A result is defined to be faithful when it was correctly rounded whereas the rounding mode (up, down or to the nearest) cannot be known by the user. Our criterion is checked against the IEEE standard for floating point arithmetic using the Coq automatic proof checker. We then present three programs in Maple, Java and C that check the criterion for a whole polynomial associated with a domain for the indeterminate and a possible truncation error. An example of use is given with the approximation of elementary functions.
Résumé : Les polynômes sont utilisés dans de nombreuses applications et enfouis dans des librairies telles que libm. Alors que la précision des fonctions utilisées en algèbre linéaire est étudiée depuis longtemps, on trouve peu d'aide pour décider d'un schéma d'évaluation polynomial. La culture commune reconnaît seulement que l'évaluation de Horner se comporte bien à moins que l'indéterminée ne soit proche d'une des racines du polynôme. Nous proposons ici un critère de fidélité pour une étape du schéma de Horner. Un résultat est défini comme fidèle s'il a été obtenu par un arrondi correct bien que l'utilisateur ne puisse pas savoir quel arrondi a été utilisé (vers le haut, le bas ou au plus proche). Notre critère a été validé vis à vis de la norme IEEE sur l'arithmétique à virgule flottante avec l'outil automatiq- ue Coq. Nous présentons ensuite trois programmes en Maple, Java et C qui vérifient notre critère sur un polynôme entier associé à un domaine pour l'indéterminée et une éventuelle erreur de troncature. Un exemple d'utilisatio- n est donné avec l'approximation des fonctions élémentaires.
Key-Words : FLOATING POINT / IEEE 754 STANDARD / HORNER'S RULE / FORMAL PROOF / COQ
Mots-clés : VIRGULE FLOTTANTE / NORME IEEE 754 / RÈGLE DE HORNER / PREUVE FORMELLE / COQ
