The IEEE standard prescribes four rounding modes: “round to nearest” (near), “round toward 0” (trunc), “round toward +INFINITY”, and “round toward -INFINITY”. The last two are formalized here by the functions inf and minf.
PROOF: If , then
if , then
PROOF: If , then
if , then
In this section, we collect a set of general results that pertain to all of the IEEE rounding modes, most of which are essentially restatements of lemmas that are proved in earlier sections. Since these results also hold for two of the other modes that we have discussed, away and , we shall state them as generally as possible. For this purpose, we define a common rounding mode to be any of the six, i.e., trunc, away, near, , inf, or minf.
PROOF: This is an immediate consequence of Definitions 5.3.1, 5.3.2, 5.5.1, and 5.5.2.
Most of following results are consequences of Lemma 5.5.3 and the corresponding lemmas pertaining to trunc and away.
PROOF: See Lemmas 5.1.2 and 5.2.2.
Note that inf and minf do not share the oddness property held by the other modes. A generalization is given by the following lemma.
PROOF: Suppose, for example, that inf and . Then since ,
The other cases are handled similarly.
PROOF: See Lemmas 5.1.9 and 5.2.11.
PROOF: See Lemmas 5.1.11 and 5.2.13.
(a) If , then . |
(b) If , then . |
PROOF: See Lemmas 5.1.12 and 5.2.14.
PROOF: This is an immediate consequence of Lemmas 5.1.5 and 5.2.5:
PROOF: See Lemmas 5.1.8 and 5.2.7.
PROOF: See Lemmas 5.1.6 and 5.2.10.
PROOF: The modes trunc, away, near, and are covered by Lemmas 5.1.13, 5.2.15, 5.3.13, and 5.3.30. For the modes inf and minf, we may assume, using Lemma 5.5.4, that and are either both positive or both negative. It follows that either
or
PROOF: The modes trunc, away, near, and are covered by Lemmas 5.1.4, 5.2.4, 5.3.8, and 5.3.20. For the modes inf and minf, we may assume, using Lemma 5.5.5, that , in which case
and
PROOF: See Lemmas 5.1.16 and 5.2.19.
PROOF: The modes trunc and away are handled by Lemma 5.4.9; near and are covered by Lemma 5.4.10; inf and minf are reduced to trunc and away by Lemma 5.4.1.
For the sake of simplicity, our main result pertaining to constant injection is formulated in the context of bit vector rounding.
PROOF: For the modes away and inf, the identity follows from Lemma 5.2.22, with , and Lemma 4.2.7. For near and , it reduces to Lemma 5.3.34. For trunc and minf, the lemma is trivial.
Our final result provides an alternative to Lemma 5.5.16 as an implementation of rounding.
PROOF: Suppose first that is -exact. By Lemma 4.2.10, , and it follows from Lemma 2.3.12 that
Consequently, none of the conditions (1)-(3) holds, and by Lemma 5.5.7,
Therefore, we may assume that is not -exact. Note that by Lemma 5.2.16,
The cases , minf , , and inf now follow trivially.
We turn to the cases and . Let
and
Since , Lemma 1.2.7 implies
By Lemmas 2.2.11 and 2.2.19,
Therefore,
This leads to the following observations:
For the case , it is clear from Definition 5.3.1 and (i) and (ii) above that we need only show that is odd if and only if . But according to Lemmas 2.3.2 and 2.3.12,