double z=x-y 是否保证 IEEE 754 浮点数的 z+y==x?

Does double z=x-y guarantee that z+y==x for IEEE 754 floating point?

我有一个问题可以简化为这个问题陈述:

Given a series of doubles where each is in the range [0, 1e7], modify the last element such that the sum of the numbers equals exactly a target number. The series of doubles already sums to the target number within an epsilon (1e-7), but they are not ==.


以下代码有效,但是否保证对满足第一句中所述要求的所有输入都有效?

public static double[] FixIt(double[] input, double targetDouble)
{
    var result = new double[input.Length];
    if (input.Length == 0) return result;

    double sum = 0;
    for (int i = 0; i < input.Length - 1; i++)
    {
        sum += input[i];
        result[i] = input[i];
    }

    double remainder = targetDouble - sum;
    result[result.Length - 1] = remainder;
    return result;
}

var arr1 = Enumerable.Repeat(Math.PI / 13, 13).ToArray();
var arr2 = FixIt(arr1, Math.PI);

Debug.Print(Math.PI.ToString("R")); //3.1415926535897931
Debug.Print(arr1.Sum().ToString("R")); //3.1415926535897922
Debug.Print(arr2.Sum().ToString("R")); //3.1415926535897931

这个问题的前一个版本问的是修改第一个元素,但是修改最后一个元素将问题简化为一个已知的总和和一个已知的目标,只剩下 last = target-sum 是否意味着sum+last == target.

(当然没有 NaN,并且对范围的限制意味着对 last 的一些限制也可能有所帮助。)

关于真正的问题:我们已经以各种方式多次遇到这个问题,但我们目前正在尝试做的是减少裁剪的浮点错误由于线性规划求解器 (Coin-OR CBC) 中的数值不稳定性。例如,有 6 个变量都必须在 [0,X] 范围内,并且变量的总和也必须是 X。由于数值不稳定,求解器偶尔会 returns 略微负值和值总和不等于 X。我们已经克服了负数问题 - 现在只是试图解决总和为 X 的问题。 (是的,我们改变结果可能会违反约束,但确保这些数字总和为 X 具有更高的优先级,而其他约束则不那么重要。)

根据定义,浮点运算并不精确(除非您只处理整数(正确性编辑:最多 253,即 9007199254740992));您将总是 有舍入差异。如果您希望四舍五入符合 humans 的预期:使用 decimal 而不是 double。如果您对 decimal 执行相同的操作,它将适用于任何在小数位方面不是病态的数字集。

z = x-y;不保证z+y == x,找到一个z这样的z+y == x的问题也不是总有办法解决的。证明如下。

我们假设 IEEE-754 二进制浮点算法四舍五入到最接近的值,与偶数相关。使用基本的 64 位格式,但结果适用于其他格式。请注意,64 位格式使用 53 位有效数字,这意味着只能表示具有 53 个或更少有效二进制数字的数字。

考虑一个目标 x 等于 1+2−52。设 y 为 2−53。然后,在 z = x-y; 之后,z+y == x 的计算结果为 false。算术细节如下所示,但是:

  • z = x-y;设置z为1,然后z+y产生1,小于x.
  • 如果我们将z增加到下一个可表示的数字,1+2−52,那么z+y产生1+2 −51,大于x.
  • 因此 z 没有使 z+y == x 为真的值。

详情:

xy的数学结果为1+2−53。由于它有 54 个有效位(从 20 到 2−53),它是不可表示的,[=29= 的计算结果] 必须四舍五入。最接近的两个数字是 1 和 1+2−52。偶数规则产生前一个数字 1,因为其有效数的低位为 0,而 1+2−52 的低位为 1.

因此 z = x-y;z 设置为 1。

z+y的数学结果为1+2−53。如上舍入为1,所以z+y的计算结果为1。所以z+y == x比较1和1+2−52,结果为false。

此外,z 的任何值都不能使比较为真。如果我们以最小可用步长递增 z,从 1 到 1+2−52,则 z+y 的数学和为1+2−52+2−53。这是两个可表示数字 1+2−52 和 1+2−51 之间的中间位置。前者低位为1,后者低位为0,所以这个z+y的计算结果为1+2−51,即当然不等于1+2−52.

浮点加法是弱单调的,因此没有 z 的值会为 z+y 产生 1+2−52

不,不是。这是一个具体的反例;在 Python 中编码,但您可以轻松地在 C# 中重复相同的实验:

>>> x = 0.24999916553497312
>>> y =  1.0000153779983518
>>> z = -0.7500162124633787
>>> z == x - y
True
>>> z + y == x
False

这是一个小的反例,其中 xyz 都是正数:

>>> x = 0.4500000000000001
>>> y = 0.20000000000000004
>>> z = 0.2500000000000001
>>> z == x - y
True
>>> z + y == x
False