Floating point bitwise comparator. If f1 and f2 are floating point numbers with the following properties can we always say f1 > f2?

Question

Recall floating-point representation:

Suppose $f$ is a floating-point number then we can express f as, If $f$ is normal: $$(-1)^{s}\cdot2^{e-127}(1 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k})$$ If $f$ is denormal/subnormal: $(e = 0)$ $$(-1)^{s}\cdot2^{-126}(0 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k})$$

where

• $s$ is the sign of $f$.
• $e$ is the stored exponent of $f$. This means $e-127$ is the effective exponent of $f$.
• $b_k$ is the $k$-th bit of $f$ where $b_0$ is the LSB and $b_{22}$ is the MSB.

Let $f_1$ be a floating-point number with constants $s_1, e_1,$ and $b_{1k}$.

Let $f_2$ be a floating-point number with constants $s_2, e_2,$ and $b_{2k}$.

I'm trying to find out if the following statement is true: $e_1 > e_2 > 0$ and $s_1 = s_1$ then $f_1 > f_2$.

My initial strategy was to subtract $f_2$ from $f_1$ and show that it must be strictly greater than $0$.

What I have so far.

$ \begin{align*} f_1-f_2 &= 2^{e_1-127}(1 + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{-k}) - 2^{e_2-127}(1 + \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{-k})\\ &= 2^{-127}(2^{e_1}(1 + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{-k}) - 2^{e_2}(1 + \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{-k})) \\ &= 2^{-127}(2^{e_1} + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{e_1-k} - 2^{e_2} - \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{e_2-k})\\ &=2^{-127}(2^{e_1} - 2^{e_2} + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{e_1-k} - \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{e_2-k})\\ &=2^{-127}(2^{e_1} - 2^{e_2} + \sum\limits_{k=1}^{23}(b_{1,23-k}\cdot 2^{e_1-k}-b_{2,23-k}\cdot 2^{e_2-k})) \end{align*} $

Now since $e_1 > e_2 \iff e_1-e_2 > 0 \iff 2^{e_1}-2^{e_2} > 1$ we have that:

$ \begin{align*} f_1-f_2 & > 2^{-127}(1 + \sum\limits_{k=1}^{23}(b_{1,23-k}\cdot 2^{e_1-k}-b_{2,23-k}\cdot 2^{e_2-k})) \end{align*} $

In order for the above to always be greater than zero I require that $\sum\limits_{k=1}^{23}(b_{1,23-k}\cdot 2^{e_1-k}-b_{2,23-k}\cdot 2^{e_2-k}) > -1$.

However, I don't know how to formally show this. Any help/hints are much appreciated as inequalities are not my strong suit.

Answer 1

If we study the expression for a floating point number, $$(-1)^{s}\cdot2^{e-127}(1 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k}),$$

and pay attention to the sum $\sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k}$, we note that

$$0 \leq \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k} \leq \sum\limits_{k=1}^{23} 2^{-k} < \sum\limits_{k=1}^\infty 2^{-k} = 1,$$

where the last equality is formed by evaluating the geometric series. Thus we find that

$$2^{e-127} \leq2^{e-127}(1 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k}) < 2^{e-127}\cdot 2$$

Thus if $s = 0$ and $e_1 > e_2$ we find that $f_2 < 2^{e_2 - 127} \cdot 2 \leq 2^{e_1 - 127} \leq f_1$.

Note that if $s = 1$ and $e_1 > e_2$, the signs are reversed and we actually have $f_2 > f_1$. But always $|f_1| > |f_2|$.

---

The extended result of the above is that if we ignore the effects of denormal numbers, NaNs, infinities and say that $-0 < 0$, we have

$$f_1 < f_2 \iff n_1 < n_2,$$

where $n_1, n_2$ are the bit patterns of $f_1, f_2$ interpreted as $w$-bit two's complement integers.

Answer 2

The relevant bit:

I'm trying to find out if the following statement is true: $e_1 > e_2 > 0$ and $s_1 = s_1$ then $f_1 > f_2$.

If course it is not true. If both numbers are negative then $e_1 > e_2 > 0$ implies that $f_1 < f_2 ≤ 0$.

Apart from that:

1. If the signs are different then the positive number is greater than the negative one, with the exception that +0 and -0 are equal, and if one is +NaN and the other is -NaN then they are unordered.

2. If the signs are both positive, then the number with the greater exponent is greater, and if the exponents are the same then the number with the greater mantissa is greater, with the exception that +NaN compares unordered to anything.

3. If the signs are both positive, and the exponent and mantissa are the same, then the numbers are equal except +NaN compares unordered to anything.

4. If the signs are both negative, then use the same tests as for positive signs, except that you replace "greater" with "less".