When double rounding is odd - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2004

When double rounding is odd

(1) , (1)
1

Résumé

Double rounding consists in a first rounding in an intermediate extended precision and then a second rounding in the working precision. The natural question is then of the precision and correctness of the final result. Unfortunately, the used double rounding algorithms do not obtain a correct rounding of the initial value. We prove an efficient algorithm for the double rounding to give the correct rounding to the nearest value assuming the first rounding is to odd. As this rounding is unusual and this property is surprising, we formally proved this property using the Coq automatic proof checker.
Le double arrondi consiste en un premier arrondi dans une précision étendue suivi d’un second arrondi dans la précision de travail. La question naturelle qui se pose est celle de la précision et de la correction du résultat final ainsi obtenu. Malheureusement, les algorithmes de double arrondi utilisés ne produisent pas un arrondi correct de la valeur initiale. Nous décrivons ici un algorithme efficace de double arrondi permettant de fournir l’arrondi correct au plus proche à condition que le premier arrondi soit impair. Comme cet arrondi est inhabituel et que cette propriété est surprenante, nous avons prouvé formellement ce résultat en utilisant l’assistant de preuves Coq.
Fichier principal
Vignette du fichier
RR2004-48.pdf (152.18 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101979 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101979 , version 1

Citer

Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. [Research Report] LIP RR-2004-48, Laboratoire de l'informatique du parallélisme. 2004, 2+7p. ⟨hal-02101979⟩
11 Consultations
12 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More