6.2 Rounding Away from Zero

The dual of truncation is defined similarly, using the ceiling instead of the floor.

Example: Let and . Then , , ,

and

Note that this value is the smallest 5-exact number not exceeded by .

The next three lemmas list simple properties of *RAZ* that it shares with
.

PROOF: By Lemma 4.1.14,

The negative-precision case is less than intuitive.

PROOF: By Lemma 4.1.8,

We have the following bounds on .

PROOF: By Lemmas 1.1.9 and 4.1.1,

PROOF: By Definitions 6.2.1 and 1.1.1 and Lemma 4.1.1,

PROOF: By Lemmas 6.2.1 and 6.2.5,

Unlike
, *RAZ* is not guaranteed to preserve the
exponent of its argument, but the only exception is the case in which
a number is rounded up to a power of 2.

PROOF: By Lemma 4.1.8,

PROOF: The first inequality follows from Lemmas 6.2.5 and 4.1.5, and the second from Lemmas 6.2.8 and 4.1.3.

The standard rounding mode properties may now be derived.

PROOF: By Corollary 6.2.10 and Lemma 4.2.6, we may assume that

PROOF: According to Lemma 6.2.11, the hypothesis implies that , and hence Lemma 4.1.3 applies.

PROOF: By Definition 4.2.1 and Lemma 1.1.10,

PROOF: If , then

PROOF: By Lemmas 6.2.5, 6.2.11, and 4.2.16, . By Lemmas 6.2.14 and 4.2.16, .

PROOF: We may assume that . Suppose . By Lemmas 6.2.13 and 4.2.19, , and by Lemmas 6.2.15 and 4.2.20, .

PROOF: First suppose . By Lemma 6.2.5, . Since is -exact by Lemma 6.2.11, Lemma 6.2.14 implies

Now suppose . By Lemma 6.2.1, we may assume that . Thus, since , we have and by Lemma 6.2.2,

If is not -exact, then and are successive -exact numbers.

PROOF: Let . By Lemma 6.1.6, . Since , . Since and are both -exact and , Lemmas 4.2.15 and 4.2.16 imply that is -exact and . But by Lemma 6.1.7, , and therefore, by Lemma 6.2.14, .

The next four results correspond to Lemmas 6.1.14, 6.1.15 6.1.16, and 6.1.17 of the preceding section.

PROOF: For the case , we have
by Definition 4.2.1, and by
Lemmas 4.1.1 and 6.2.4,

Thus, we may assume , and by Lemma 6.2.2, we may also assume . Let and . As noted in the proof of Lemma 6.1.14, and are both -exact and . Now by Lemma 6.2.14, , but if , then since is -exact, Lemma 4.2.16 would imply , contradicting . Therefore, .

PROOF: We may assume . Consider first the case

Thus, we may assume . By Corollary 6.2.10,

PROOF: Let . Since is -exact,

PROOF: Let . Since is -exact,

The following result combines Lemmas 6.1.17 and 6.2.22.

PROOF: By Lemmas 6.1.3 and 6.2.2, we may assume that . The case is handled by Lemma 6.1.16. For the case , Lemmas 6.1.17 and 6.2.22 cover the subcases and , respectively.

We turn now to the problem of bit-level implementation of rounding.
Truncation, according to Lemma 6.1.18, is equivalent to a
bit slice operation, which may be implemented as a logical operation
using Corollary 6.1.21. Other rounding modes may be reduced to the
case of truncation by a method known as *constant injection*. Let
be -exact with
, say

As suggested by the diagram, the addition generates a carry into the position of unless , i.e., unless is -exact, and is rounded up accordingly. This observation is formalized by the following lemma.

PROOF: Let . Since and are both -exact and

If is -exact, then , and hence . Thus, we may assume is not -exact. But then since and is -exact,

David Russinoff 2017-08-01