IEEE Std 754 Floating-Point: let t := a - b, does the standard guarantee that a == b + t?

c, c++, floating-point, ieee-754

Solution

Absolutely not. One obvious case is `a=DBL_MAX`, `b=-DBL_MAX`. Then `t=INFINITY`, so `b+t` is also `INFINITY`.

What may be more surprising is that there are cases where this happens without any overflow. Basically, they're all of the form where `a-b` is inexact. For example, if `a` is `DBL_EPSILON/4` and `b` is `-1`, `a-b` is 1 (assuming default rounding mode), and `a-b+b` is then 0.

The reason I mention this second example is that this is the canonical way of forcing rounding to a particular precision in IEEE arithmetic. For instance, if you have a number in the range [0,1) and want to force rounding it to 4 bits of precision, you would add and then subtract `0x1p49`.

Problem

Assume that `t`,`a`,`b` are all double (IEEE Std 754) variables, and both values of `a`, `b` are NOT `NaN` (but may be `Inf`). After `t = a - b`, do I necessarily have `a == b + t`?

Original source