TAOCP 4.2.2 Exercise 23

Section 4.2.2: Accuracy of Floating Point Arithmetic

Exercise 23. ▶ [M26] Prove or disprove: $u \oslash (u \ominus u) = [u]$, for all floating point $u$.

Verified: yes
Solve time: 2m15s

---

Setup

Let $u$ be a floating point number. By definition, $u \ominus u = \text{round}(u - u)$, as in equation (9). We are asked to consider the expression

$u \oslash (u \ominus u)$

and determine whether it is equal to $[u]$ for all floating point numbers $u$, where $[u]$ denotes the nearest integer to $u$ in the floating point system. We recall that the floating point operations $\ominus$ and $\oslash$ are defined by

$u \ominus v = \text{round}(u - v), \qquad u \oslash v = \text{round}(u / v),$

and that the rounding function is defined only when the result lies within the normalized range (no underflow or overflow occurs).

Hence the problem reduces to analyzing the quantity $u \oslash (u \ominus u) = \text{round}\big(u / \text{round}(u - u)\big)$ for arbitrary $u$.

Solution

Compute $u \ominus u$ using the definition (9) and equation (11):

$u \ominus u = \text{round}(u - u) = \text{round}(0) = 0.$

Substitute this into the expression of interest:

$u \oslash (u \ominus u) = u \oslash 0 = \text{round}\left(\frac{u}{0}\right).$

Division by zero is undefined in standard floating point arithmetic, so $u \oslash 0$ is not defined. Therefore, the expression $u \oslash (u \ominus u)$ is undefined for every floating point $u \ne 0$. In particular, it cannot equal $[u]$, because $[u]$ is always a well-defined finite floating point number.

For completeness, consider $u = 0$: then

$0 \ominus 0 = 0, \quad 0 \oslash 0 = \text{undefined}.$

Hence even in the case $u = 0$, the expression remains undefined.

Thus the proposed identity

$u \oslash (u \ominus u) = [u]$

fails for all floating point numbers.

Verification

Each step can be checked independently:

1. $u \ominus u = \text{round}(u - u) = \text{round}(0) = 0$ follows directly from equation (9) and the definition of rounding.
2. $u \oslash 0$ is undefined by the standard rules of floating point division (no finite floating point number represents division by zero).
3. Therefore, no floating point $u$ satisfies $u \oslash (u \ominus u) = [u]$.

No assumptions about $u$ or the rounding mode affect this conclusion.

Notes

The exercise illustrates a general principle: operations that are undefined in the real number system, such as division by zero, remain undefined in floating point arithmetic. Any identity that implicitly assumes such an operation is valid must be rejected.

This completes the proof.

∎

$$ \boxed{\text{False; the identity fails for all floating point } u.} $$