Гарантирует ли double z = x-y, что z + y == x для плавающей запятой IEEE 754?

Question

У меня есть проблема, которую можно свести к этой постановке задачи:

Учитывая серию пар, где каждый находится в диапазоне [0, 1e7], изменить последний элемент так, чтобы сумма чисел равнялась точно целевое число. Серия двойников уже суммируется с число цели в эпсилоне (1e-7), но они не ==.

---

Следующий код работает, но гарантированно ли он работает для всех входных данных, которые отвечают требованиям, описанным в первом предложении?

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. Из-за нестабильности чисел решатель иногда возвращает слегка отрицательные значения и значения, которые не суммируются точно X. Мы преодолели проблему отрицательных чисел - теперь просто пытаемся решить проблему суммы X. (Да, могут быть ограничения, которые мы не выполняем, изменяя результаты, но убедившись, что сумма этих чисел к X имеет более высокий приоритет, где другие ограничения не так важны.)}

Answer 1

z = x-y; не гарантирует z+y == x, и не всегда есть решение проблемы поиска z такого z+y == x. Доказательство следует.

Мы предполагаем двоичную арифметику IEEE-754 с плавающей точкой с округлением до ближайшего, связанного с четным. Используется базовый 64-битный формат, но результат сохраняется для других форматов. Обратите внимание, что в 64-битном формате используются 53-битные значения, то есть могут быть представлены только числа с 53 или менее значащими двоичными цифрами.

Рассмотрим цель x равную 1 + 2 ⁻⁵² . Пусть y будет 2 ⁻⁵³ . Затем, после z = x-y;, z+y == x оценивается как ложное. Арифметические детали показаны ниже, но:

• z = x-y; устанавливает z в 1, а затем z+y выдает 1, что меньше x.
• Если мы увеличим z до следующего представимого числа, 1 + 2 ^-52 , то z+y даст 1 + 2 ^-51 , что больше x.
• Так что нет значения z, которое делает z+y == x истинным.

подробности:

Математический результат x - y равен 1 + 2 ⁻⁵³ . Поскольку он имеет 54 значащих бита (от 2 ⁰ до 2 ^-53 ), он не может быть представлен, и вычисленный результат x-y должен быть округлен. Два ближайших числа: 1 и 1 + 2 ⁻⁵² . Правило привязки к четности создает первое число 1, поскольку младший бит его значения равен 0, а младший бит для 1 + 2 ⁻⁵² равен 1.

Таким образом z = x-y; устанавливает z в 1.

Тогда математический результат z + y равен 1 + 2 ⁻⁵³ . Как указано выше, это округляется до 1, поэтому вычисленный результат z+y равен 1. Таким образом, z+y == x сравнивает 1 с 1 + 2 ^-52 и выдает false.

Кроме того, никакое значение z не может сделать сравнение верным. Если мы увеличиваем z на наименьший доступный шаг от 1 до 1 + 2 ⁻⁵² , то математическая сумма z + y равна 1 + 2 ⁻⁵² + 2 * 1 079 * -53 . Это посередине между двумя представимыми числами 1 + 2 ^-52 и 1 + 2 ^-51 . Первый имеет младший бит 1, а второй младший бит 0, поэтому вычисленный результат этого z+y равен 1 + 2 ^-51 , что, конечно, не равно 1+ 2 ^-52 .

Сложение с плавающей точкой слабо монотонно, поэтому нет значений z, которые бы выдали 1 + 2 ⁻⁵² для z+y.

Answer 2

Нет, это не так.Вот конкретный контрпример.закодирован в Python, но вы можете легко повторить тот же эксперимент в C #:

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

Вот небольшой контрпример с x, y, z все положительными:

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

Answer 3

Арифметика с плавающей точкой не является точной по определению (если только вы не имеете дело только с целыми числами (отредактируйте для корректности: до 2 ⁵³ , то есть 9007199254740992); у вас будет всегда расхождения при округлении. Если вы хотите, чтобы округление соответствовало ожиданиям людей : используйте decimal вместо double. Если вы сделаете то же самое с decimal, он будет работать правильно для любого набора чисел, которые не являются патологическими с точки зрения десятичных цифр.