# 13.1  Quotient Refinement

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

The accuracy of may be derived from that of :

(init-approx) Let , , and . Assume that , and let . Then

PROOF: Since

and

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 as follows:

In the final step, the input rounding mode is used instead of RNE:

Our main lemma, due to Markstein [MAR90], ensures that the final quotient is correctly rounded under certain assumptions pertaining to the accuracy of the reciprocal and quotient approximations from which it is derived.

(r-exactp, markstein) Let , , , and be -exact, where , , and . Assume that the following inequalities hold:

(i) , where

(ii) .

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,

implies and . It follows from the bounds on and that . We shall show that as well.

If , then

and

which implies . On the other hand,

and hence, .

Similarly, if , then

and

which implies . On the other hand,

and .

To establish -exactness of , since

either or , and it suffices to show that

Since is -exact, , and , ; since and are -exact, , and ,

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

 (13.1)

or

Since (ii) implies

If , then since and are both -exact and , we have

and it will suffice to show that

but this reduces to , and we have assumed that .

On the other hand, if , then

and we need only show that

which is trivial.

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

 (13.2)

and

 (13.3)

The proof of (13.2) is the same as that of (13.1), and we may similarly show that (13.3) is a consequence of

But this is equivalent to , which follows from the assumptions that is -exact and

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.

(quotient-refinement-1, quotient-refinement-2) Let , , and . Assume that and . Let and . Then

If , then

where

PROOF: Let , , , and . Then

and

where

Thus,

and

For the proof of the first claim, we have

For the proof of the second claim, since , we have

and

If , then the claim follows trivially. Thus, we may assume that . But then

implies . It follows that and

David Russinoff 2017-08-01