Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number

Sylvie Boldo 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Floating-point experts know that mathematical formulas may fail or give imprecise results when implemented in floating-point arithmetic. This article describes an example where, surprisingly, it is absolutely not the case. Indeed, using radix 2 and an unbounded exponent range, the computation of the square root of the square of a floating-point number a is exactly |a|. A consequence is the fact that the floating-point computation of a/ sqrt (a^2 + b^2) is always in the interval [−1, 1]. This removes the need for a test when calling an arccos or an arcsin on this value. For more guarantees, this property was formally checked using the Coq proof assistant and the Flocq library. The conclusion will give hints on what happens without assumptions and in other radices, where the behavior is very different.
Type de document :
Communication dans un congrès
Sergiy Bogomolov and Matthieu Martel. Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. Electronic Notes in Theoretical Computer Science, pp.50--55, 2015, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification. <http://nsv2015.informatik.uni-freiburg.de/>
Liste complète des métadonnées

https://hal.inria.fr/hal-01148409
Contributeur : Sylvie Boldo <>
Soumis le : mardi 5 mai 2015 - 15:49:03
Dernière modification le : vendredi 17 février 2017 - 16:10:47
Document(s) archivé(s) le : mercredi 19 avril 2017 - 14:55:51

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01148409, version 1

Citation

Sylvie Boldo. Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. Sergiy Bogomolov and Matthieu Martel. Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. Electronic Notes in Theoretical Computer Science, pp.50--55, 2015, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification. <http://nsv2015.informatik.uni-freiburg.de/>. <hal-01148409>

Partager

Métriques

Consultations de
la notice

498

Téléchargements du document

283