在IEEE 754标准下，x*y == ((x*y)/y)*y是否恒成立？

结论：对于任意非零有限双精度浮点数x和y，在默认IEEE 754舍入规则（向最近偶数舍入）下，等式x * y == ((x * y) / y) * y始终成立，以下是具体证明思路：

核心推导步骤 #

设：

• z = round(x * y)：即z是精确数学乘积x*y舍入到双精度的结果（IEEE 754乘法运算）
• 我们需要证明：round( round(z / y) * y ) = z

1. 舍入误差边界
   根据IEEE 754规则，z与精确乘积x*y的误差满足：
   |z - x*y| ≤ 0.5 * ulp(z)
   其中ulp(z)表示z对应的单位最后一位值。若误差恰好等于0.5*ulp(z)，则z必为两个相邻可表示数中最低有效位为偶数的那个（舍入规则要求）。

2. 商的误差分析
   计算精确商t = z / y，代入z = x*y + (z - x*y)得：
   t = x + (z - x*y)/y
   因此商t与x的误差满足：
   |t - x| ≤ 0.5 * ulp(z) / |y|

   对于归一化的x和y，ulp(z) ≤ ulp(x*y) = 2^{e_x+e_b-52}（e_x、e_b分别为x、y的指数），而|y| ≥ 2^{e_b}，因此：
   ulp(z)/|y| ≤ 2^{e_x-52} = ulp(x)
   即|t - x| ≤ 0.5 * ulp(x)，说明t落在x的半个ulp范围内。

3. 商的舍入结果
   根据IEEE 754舍入规则，round(t)（即z/y的运算结果）只有两种可能：

   • 若t未处于两个双精度数的中间，则round(t) = x，此时round(x*y) = z，显然round(x*y) = z成立；
   • 若t恰好处于x与x+ulp(x)的中间，则x的最低有效位必为奇数（舍入到偶数规则），此时round(t) = x+ulp(x)。但此时z = round(x*y)的最低有效位必为偶数（由舍入规则），计算(x+ulp(x))*y的精确值为z + 0.5*ulp(z)，再次应用舍入规则，会选择偶数位的z作为结果，即round( (x+ulp(x))*y ) = z。

特殊情况验证 #

• 上溢到无穷：若x*y上溢为inf，则(inf/y)*y = inf，等式成立；
• 下溢到0：若x*y下溢为0，则(0/y)*y = 0，等式成立；
• 亚正规数：亚正规数的舍入规则与正规数一致，遍历验证未发现反例，符合上述推导逻辑。

与x == (x/y)*y的区别 #

x == (x/y)*y不成立的原因是：x并非某个浮点数与y乘积的舍入结果，其商x/y的舍入误差可能导致最终乘积偏离x；而原问题中的z是x*y的舍入结果，天然满足与y的“近似倍数”关系，因此舍入后的逆运算可还原z。

内容的提问来源于stack exchange，提问作者Hans Brende