The first step of each algorithm is the computation of an initial approximation of as an application of the function rcp24. An initial approximation of the quotient is then computed as
Each of the initial values and undergoes a series of refinements, culminating in the final rounded quotient .
Each refinement of the quotient is computed from the preceding approximation and the current reciprocal approximation
(i) , where
Let . Then is -exact, and for any IEEE rounding mode ,
PROOF: We may assume , for otherwise and the claim holds trivially. We may also assume , for otherwise,
If , then
Similarly, if , then
To establish -exactness of , since
For the proof of the second claim, we shall focus on the case ; the case is similar. Let . The quotient lies in the interval , and its rounded value is either or . For the directed rounding modes (RUP, RDN, and ), we need only show that also belongs to this interval, i.e., . Since , this condition may be expressed as
On the other hand, if , then
For the remaining case, , the proof may be completed by showing that and lie on the same side of the midpoint of the interval . Note that is impossible, for if this were true, then since is -exact, Lemma 4.2.10 would imply that is also -exact, but this is not the case. Thus, we must show that
IEEE-compliance of the algorithms of interest will be proved as applications of Lemma 13.1.2 by establishing the two hypotheses (i) and (ii) for appropriate values of and .
The next lemma consists of two results. The first specifies the accuracy of an intermediate quotient approximation;13.1 the second addresses the final approximation, supplying the first inequality (i) required by Lemma 13.1.2.
PROOF: Let , , , and . Then
David Russinoff 2017-08-01