Formally Verified Argument Reduction with a Fused-Multiply-Add

Details Formally Verified Argument Reduction with a Fused-Multiply-Add Formally Verified Argument Reduction with a Fused-Multiply-Add

2007-08-28

arxiv.org/abs/0708.3722v1

Computer Science

Mathematical Software

Scientific paper

Cody & Waite argument reduction technique works perfectly for reasonably large arguments but as the input grows there are no bit left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed with a fused-multiply-add provides a fully accurate result for many possible values of the input with a constant almost accurate to the full working precision. We also present an algorithm for a fully accurate second reduction step to reach double full accuracy (all the significand bits of two numbers are significant) even in the worst cases of argument reduction. Our work recalls the common algorithms and presents proofs of correctness. All the proofs are formally verified using the Coq automatic proof checker.

Affiliated with

Also associated with

No associations

Rating

Formally Verified Argument Reduction with a Fused-Multiply-Add does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Formally Verified Argument Reduction with a Fused-Multiply-Add, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formally Verified Argument Reduction with a Fused-Multiply-Add will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-362882