IEEE 754 浮点数编码排序与步长性质证明

在某机器中，浮点数采用 IEEE 754 标准表示，每个浮点数都对应着一个二进制编码，去掉负数（即符号位为 1 的那些编码）、去掉特殊值（即阶码位全 1 的那些编码），剩下的编码按照这个二进制编码对应的整数值排序并从 0 开始编号，第 k 个其对应的浮点数值记为 f(k)，例如全 0 编码 0000……000 的序号是 0，f(0) = 0, 并记最大的编号为 f(max)。显然，越排在后面的编码，对应的浮点数值越大；同时将相邻两个编码的浮点数差值定义为步长，即 step(i) = f(i+1)-f(i), 显然，步长值是单调非减的。

(1) 请证明第一个显然，即如果有 0≤ m< n ≤ max, 则有 f(m) < f(n) (2) 请证明第二个显然，即如果有 0≤ m< n< max, 则有 step(m)≤ step(n)

(1) 假设存在 m<n 且 f(m)≥f(n)，则 f(n)-f(m)≤0，即步长为负数，与步长单调非减矛盾，故假设不成立，即 f(m) < f(n)。

(2) 假设存在 m<n 且 step(m)>step(n)，则 f(n)-f(m) > f(m+1)-f(m)，即 f(n)-f(m+1) > f(m+1)-f(m)，即步长在 m+1 处变小，与步长单调非减矛盾，故假设不成立，即 step(m)≤ step(n)。