线性插值公式的有界性：IEEE 754浮点环境下的验证及问题

给定线性插值实现：

lerp(x1, x2, y1, y2, x) = y1 * (x - x2) / (x1 - x2) + y2 * (x - x1) / (x2 - x1)

问题1 #

在遵循IEEE 754浮点算术规则，且满足x1 < x2、y1 < y2的前提下，当x1 ≤ x ≤ x2时，是否必然成立y1 ≤ lerp(x1, x2, y1, y2, x) ≤ y2？

答案：不一定成立。IEEE 754浮点运算的舍入误差可能导致计算结果超出理论上的[y1, y2]区间。

问题2 #

若上述结论不成立，请给出反例。
补充说明：已有多个答案给出y1与y2非常接近时的反例。

反例（双精度浮点数）：

• x1 = 0.0，x2 = 1.0
• y1 = 2^-1023（双精度最小正次正规数）
• y2 = 2^-1023 + 2^-1074（y1的下一个可表示次正规数）
• x = 0.5

理论插值结果应为(y1 + y2)/2 = 2^-1024 + 2^-1075，但2^-1075小于双精度的最小正次正规数（2^-1074），会被舍入到0。最终计算结果为0，小于y1，违反了y1 ≤ lerp的结论。

另一个典型场景：

• x1 = 0.0，x2 = 1.0
• y1 = 1.0
• y2 = nextafter(1.0, 2.0)（1.0之后的下一个可表示双精度数，值为1.0 + 2^-52）
• x = 0.5

理论结果是1.0 + 2^-53，但当使用向零舍入模式时，y2 * 0.5会被舍入到0.5，最终总和为0.5 + 0.5 = 1.0；若叠加其他舍入误差，极端情况下可能出现结果略低于y1的情况。

问题3 #

若对y2 - y1设置一个下界，是否能够证明上述有界性结论？

答案：可以。当y2 - y1足够大，能覆盖浮点计算的最大舍入误差时，可保证插值结果落在[y1, y2]区间内。

将插值公式改写为等价形式：lerp = y1 + t*(y2 - y1)，其中t = (x - x1)/(x2 - x1)，且t ∈ [0,1]。浮点计算中，总舍入误差e的绝对值有上界（双精度下约为2^-52 * |lerp|）。

当y2 - y1 ≥ 2 * ε * max(|y1|, |y2|)（ε为浮点精度，双精度ε=2^-52）时，舍入误差的绝对值|e|会小于等于(y2 - y1)/2，从而确保y1 ≤ y1 + t*(y2 - y1) + e ≤ y2成立。

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