# 6.1  Truncation

The most basic rounding mode, which the IEEE standard calls “round toward 0”, may be described as a three-step operation on the significand of its first argument. Thus, has the same sign and exponent as , while its significand is computed from as follows:

1. Shift the binary point of by bits to the right.

2. Extract the floor of the result.

3. Shift the binary point by bits to the left.

In other words, is the result of replacing by . This is the content of the following definition.

Definition 6.1.1   (rtz) For all and ,

Example: Let and . Then , , ,

and

Note that this value is the largest 5-exact number that does not exceed .

Although the second argument of any rounding mode is normally positive, the following lemma is occasionally useful.

PROOF: By Lemma 4.1.8,

which implies

Like all rounding modes, RTZ preserves sign.

Lemma 6.1.2   (sgn-rtz) Let and . If , then

This particular mode also has the property of oddness, which, we shall see, is not common to all IEEE modes.

Lemma 6.1.3   (rtz-minus) For all and ,

All of the modes that we shall consider commute with the shift operation.

PROOF: By Lemma 4.1.14,

The inequality stated in the next lemma is the defining characteristic of as a rounding mode.

PROOF: By Definition 1.1.1 and Lemma 4.1.1,

As we have noted, RTZ also preserves exponent.

PROOF: Since , by Lemma 4.1.5. But by Lemmas 4.1.8 and 1.1.3,

and hence, by Lemma 4.1.3,

The following inequality complements Lemma 6.1.5, confining to an interval.

PROOF: By Definitions 6.1.1 and 1.1.1 and Lemma 4.1.1,

The second inequality follows from Definition 4.1.1..

PROOF: By Lemmas 6.1.2 and 6.1.5,

The corollary now follows from Lemma 6.1.7

PROOF: Since , it suffices to observe that

(rtz-exactp-b) Let and . If and x is -exact, then

PROOF: By Definition 4.2.1 and Lemma 1.1.1,

and hence by Definition 6.1.1 and Lemma 4.1.1,

(rtz-exactp-c) Let , , and . If is -exact and , then .

PROOF: If , then by Lemma 6.1.5. Therefore, we may assume that . Suppose . Then by Lemma 4.2.16,

(rtz-squeeze) Let , and . Assume that is -exact, where and . Then .

PROOF: By Lemmas 6.1.5 and 6.1.11, . The claim follows from Lemma 4.2.16 and 6.1.9

PROOF: First suppose . By Lemma 6.1.5, . Since is -exact by Lemma 6.1.9, Lemma 6.1.11 implies

Now suppose . By Lemma 6.1.2, we may assume that . Thus, since , we have and by Lemma 6.1.3,

Note that with lemmas 6.1.9, 6.1.10, and 6.1.13, we have established as a true rounding mode, as defined by the axioms listed at the beginning of this chapter.

If is -exact but not -exact, then is equidistant from two successive -exact numbers. In this case, we have an explicit formula for .

(rtz-midpoint) Let and . If is -exact but not -exact, then

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

Thus, we may assume , and by Lemma 6.1.3, we may also assume .

Let and . Since , by Lemma 4.2.16, and hence and . It follows that .

By hypothesis, but , and therefore, is odd. Let . Then

Thus, is -exact, and by Lemma 4.2.15, so is . Now by Lemma 6.1.11, , but if , then since is -exact, Lemma 4.2.16 would imply , contradicting . Therefore,

The following lemma states an intuitively obvious property of truncation, which may be derived directly from Definition 6.1.1.

PROOF: We assume ; the case follows easily from Lemma 6.1.3. Applying Lemma 1.1.5, we have

Figure 6.1 is provided as a visual aid in understanding the following lemma, which formulates the precise conditions under which a truncated sum may be computed by truncating one of the summands in advance of the addition.

(plus-rtz) Let , , and . If , , and is -exact, then

PROOF: Let . Since is -exact,

Let . Then by Lemma 1.1.4,

Lemma 6.1.16 holds for subtraction as well, but only if the summands are properly ordered.

(minus-rtz) Let , , and . If , , and is -exact, then

PROOF: Let . Since is -exact,

Let . Then by Lemma 1.1.4,

Truncation of a bit vector may be described as a shifted bit slice.

(bits-rtz) Let and , and let . If , then

PROOF: By Lemmas 2.2.5 and 2.2.16,

PROOF: Let . By Lemmas 6.1.18, 2.2.18, and 2.2.23,

(rtz-split) Let , , and , and let . If and , then

PROOF: By Lemmas 6.1.18 and2.2.22,

(rtz-logand) Let , , and , and let . If , then

PROOF: By Lemmas 6.1.18 and 3.1.11,

and by Lemmas 3.1.2 2.2.5, and 3.1.13,

But since

David Russinoff 2017-08-01