Formally Verified Argument Reduction with a Fused-Multiply-Add - Computer Science > Mathematical SoftwareReportar como inadecuado




Formally Verified Argument Reduction with a Fused-Multiply-Add - Computer Science > Mathematical Software - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Abstract: Cody and Waite argument reduction technique works perfectly for reasonablylarge arguments but as the input grows there are no bit left to approximate theconstant with enough accuracy. Under mild assumptions, we show that the resultcomputed with a fused-multiply-add provides a fully accurate result for manypossible values of the input with a constant almost accurate to the fullworking precision. We also present an algorithm for a fully accurate secondreduction step to reach double full accuracy all the significand bits of twonumbers are significant even in the worst cases of argument reduction. Ourwork recalls the common algorithms and presents proofs of correctness. All theproofs are formally verified using the Coq automatic proof checker.



Autor: Sylvie Boldo INRIA Futurs, Marc Daumas LIRMM, Eliaus, Ren Cang Li

Fuente: https://arxiv.org/







Documentos relacionados