Back to Search Start Over

Error in ulps of the multiplication or division by a correctly-rounded function or constant in binary floating-point arithmetic

Authors :
Brisebarre, Nicolas
Muller, Jean-Michel
Picot, Joris
Arithmétiques des ordinateurs, méthodes formelles, génération de code (ARIC)
Laboratoire de l'Informatique du Parallélisme (LIP)
École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon
Institut National de Recherche en Informatique et en Automatique (Inria)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
Centre National de la Recherche Scientifique (CNRS)
École normale supérieure de Lyon (ENS de Lyon)
ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020)
Source :
IEEE Transactions on Emerging Topics in Computing, IEEE Transactions on Emerging Topics in Computing, In press, ⟨10.1109/TETC.2023.3294986⟩
Publication Year :
2023
Publisher :
HAL CCSD, 2023.

Abstract

International audience; Assume we use a binary floating-point arithmetic and that RN is the round-to-nearest function. Also assume that c is a constant or a real function of one or more variables, and that we have at our disposal a correctly rounded implementation of c, say ĉ = RN(c). For evaluating x • c (resp. x/c or c/x), the natural way is to replace it by RN(x • ĉ) (resp. RN(x/ĉ) or RN(ĉ/x)), that is, to call function ĉ and to perform a floatingpoint multiplication or division. This can be generalized to the approximation of n/d by RN(^n/ ^d) and the approximation of n • d by RN(^n • ^d), where ^n = RN(n) and ^d = RN(d), and n and d are functions for which we have at our disposal a correctly rounded implementation. We discuss tight error bounds in ulps of such approximations. From our results, one immediately obtains tight error bounds for calculations such as x * pi, ln(2)/x, x/(y + z), (x + y) * z, x/sqrt(y), sqrt(x)/y, (x + y)(z + t), (x + y)/(z + t), (x + y)/(zt), etc. in floating-point arithmetic.

Details

Language :
English
ISSN :
21686750
Database :
OpenAIRE
Journal :
IEEE Transactions on Emerging Topics in Computing, IEEE Transactions on Emerging Topics in Computing, In press, ⟨10.1109/TETC.2023.3294986⟩
Accession number :
edsair.dedup.wf.001..dccb4187bebed5e5aa2a48ed60b2bfb4