A simple test qualifying the accuracy of Horner's rule for polynomials

Sylvie Boldo (1) , Marc Daumas (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

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.

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 automatique 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’utilisation est donné avec l’approximation des fonctions élémentaires.

Mots clés: Floating Point; Formal Proof; Horner's Rule; IEEE 754 Standard

Mots clés: Coq; Virgule flottante; Norme IEEE 754; Règle de Horner; Preuve formelle

Domaines: Informatique [cs]

Sylvie Boldo, Marc Daumas. A simple test qualifying the accuracy of Horner's rule for polynomials. [Research Report] LIP RR-2003-01, Laboratoire de l'informatique du parallélisme. 2003, 2+39p. ⟨hal-02102015⟩