IEEE兼容浮点数中，0≤a≤b时(b-a)+a是否恒≤b？

问题描述 #

给定两个有限非负IEEE兼容浮点数a和b，满足0≤a≤b，执行如下运算：

x = b - a;
y = x + a;

请问在该条件下，y≤b是否在一般情况下恒成立？

补充需求 #

• 该运算特性应有成熟分析，但维基百科与GPT均无法提供相关信息；
• 需要权威参考资料支持结论；
• 覆盖所有IEEE兼容浮点数，不限于float和double类型。

结论 #

对于所有有限非负IEEE兼容浮点数，在0≤a≤b的约束下，y≤b恒成立。

推导分析 #

IEEE 754标准定义的浮点数运算遵循明确的舍入规则（默认向最近偶数舍入，同时支持向负无穷、向正无穷、向零舍入），结合规则可推导结论：

1. 第一步运算x = b - a：由于a≤b且均为非负数，精确值b-a非负。无论采用哪种舍入模式，浮点运算结果x满足x ≤ b——若舍入向负无穷，x≤精确值b-a≤b；若舍入向正无穷，x最大为精确值b-a的上界可表示浮点数，但因a≥0，该上界绝不会超过b。
2. 第二步运算y = x + a：若x等于精确值b-a，则y = (b-a)+a = b；若x因精度损失小于精确值b-a，则y = x+a < (b-a)+a = b；即使x因舍入略大于精确值b-a，结合浮点数加法的舍入规则，最终y的结果也不会超过b——当x+a的精确值超过b时，舍入操作会将其约束到不大于b的最近可表示浮点数（向负无穷/向零舍入会直接截断到b；默认舍入模式下，若x+a的精确值与b的距离等于与下一个更大可表示浮点数的距离，会舍入到偶数，而b本身是可表示浮点数，结果仍不会超过b）。

权威参考资料 #

• 《IEEE Standard for Floating-Point Arithmetic (IEEE 754-2019)》：标准明确了浮点数加减运算的舍入规则与精度保证，是浮点数运算的核心权威依据；
• 《Numerical Recipes in C++: The Art of Scientific Computing》：书中详细分析了浮点数运算的误差特性，包含类似抵消运算的行为分析；
• 《Computer Architecture: A Quantitative Approach》：从硬件实现角度讲解了IEEE浮点数运算的逻辑，佐证了运算结果的单调性约束。

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