形式陈述
设 是给定浮点系统公理库浮点数系统与 IEEE 754Floating-point system · IEEE 754以有限尾数和指数表示机器数,并说明 IEEE 754 的特殊值、格式与运算语义。的有限可表示数集合。舍入映射 按选定方向把精确实数送到可表示数。IEEE 754 的默认方向是 round to nearest, ties to even:选择最近的浮点数;若精确值恰在两数中点,则选择最低有效位为偶数的那个。标准还定义 ties-to-away,以及向 、向 和向零三种定向舍入;后面统一的半 ulp 上界专指最近舍入。
对可表示数 , 描述其末位单位,即所在 binade 中相邻浮点数的间距;在二进制正规区间 中它等于 。幂次边界的上下间距不同,因此跨边界谈“一个 ulp”必须声明采用哪一侧或哪套标准定义。设精度为 、基数为 ,在 round-to-nearest 下通常定义 unit roundoff
在 binary64 中 。machine epsilon 在不同文献和语言库中可能指 ,即 与下一个浮点数的间距,也可能被当作 ;使用时必须声明约定。
当 、舍入结果处于正规范围且没有溢出时,最近舍入满足
这是带条件的相对误差公理库误差度量:绝对、相对与分量误差Error measures · Absolute and relative error用绝对、相对、范数型与逐分量尺度准确说明近似量偏离真值的程度。陈述。若 是最小正次正规数,则对落入次正规舍入区的精确数,最近舍入满足
这里应使用绝对界,不能除以趋近于零的 后继续声称相对误差受 控制。定向舍入最多偏向相邻格点而不是半格,常数也随之改变。溢出结果由舍入方向决定,可能是无穷也可能是同号最大有限数。
直觉
ulp 是浮点尺在 附近的一格,unit roundoff 是正规范围内“最多偏半格”换算成相对尺度后的统一上界。数值越大,绝对格距越大,因此一个固定增量可能在 附近可见,在更大的累计值旁边却落不到新的格点;次正规区则反过来保持固定绝对格距,逐步失去相对有效位。
ties-to-even 让连续出现的精确中点不总朝同一方向舍入,可减少某些系统性偏差;它不保证一组实际数据的舍入误差均值为零,也不允许把误差当独立随机噪声。
例子与边界
在 binary64 中, 的下一可表示数是 。若 ,最近舍入下 ;当 恰处中点时,ties-to-even 仍选择 。实数加法已经形成精确和,只是它落在 的舍入区间,写回 binary64 后增量不再可见。前缀累加中部分和逐渐变大时,同一个增量也可能从可见变成不可见。
对正数 接近最小正规数时,次正规结果仍可能非常接近精确值,但 不再受统一的 控制。将正常范围的相对模型无条件延伸到零附近,会把格式边界藏进错误的定理里。
正确舍入也不等于“真实结果没有误差”。它只保证返回目标格式中按指定方向最合适的数;若精确结果不可表示,误差仍然存在,只是这一步没有更好的同格式答案。把一个值先舍入到扩展精度、再舍入到目标精度还可能出现 double rounding;证明若假定每步直接正确舍入到 binary64,就必须核对实际中间格式。
推论与应用
unit roundoff 是标准浮点算术模型公理库浮点算术标准误差模型Standard floating-point arithmetic model以每次基本运算的小相对扰动和 gamma 记号组织多步浮点误差分析。的基本参数,多步误差界中的 由它构造。浮点求和公理库浮点求和:顺序、成对与补偿Floating-point summation · Compensated summation比较顺序、成对和补偿求和的误差传播,并区分准确性、可复现性与并行代价。进一步说明相同局部舍入规则怎样随顺序和算法积累成不同总体误差。
使用舍入误差公式时应同时记录格式、舍入方向、正规/次正规范围和是否允许溢出。若实现采用融合乘加或扩展精度,中间舍入次数改变,分析路径也应相应调整,而不是事后把所有差异塞进一个模糊的“机器误差”。
参考资料
- IEEE, IEEE Standard for Floating-Point Arithmetic, IEEE Std 754-2019.
- David Goldberg, “What Every Computer Scientist Should Know About Floating-Point Arithmetic,” ACM Computing Surveys 23(1), 1991.
- Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002, Ch. 2.