Paper Info
Title
Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number
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/(a2+b2) 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.
Year
DOI
Venue
2015
10.1016/j.entcs.2015.10.004
Electronic Notes in Theoretical Computer Science
Keywords
DocType
Volume
Floating-point,formal proof,square,square root,radix,Coq
Journal
317
ISSN
Citations 
PageRank 
1571-0661
0
0.34
References 
Authors
0
1
Name
Order
Citations
PageRank
Sylvie Boldo129226.85