Является ли (x - x) всегда положительным ноль для удвоений или иногда отрицательным нолем?

Ответ 1

x - x может быть +0.0 или NaN. Никаких других значений, которые он может принимать в арифметике IEEE 754 в раунде до ближайшего (и в Java, режим округления всегда от ближайшего к ближайшему). Вычитание двух идентичных конечных значений определяется как создание +0.0 в этом режиме округления. Марк Дикинсон, в комментариях ниже, ссылается на стандарт IEEE 754, говорящий в разделе 6.3:

Когда сумма двух операндов с противоположными знаками (или разностью двух операндов с одинаковыми знаками) равна нулю, знак этой суммы (или разности) должен быть +0 во всех атрибутах округления, кроме roundTowardNegative [...].

Эта страница показывает, что в частности 0.0 - 0.0 и -0.0 - (-0.0) являются +0.0.

Инфиниты и NaN оба производят NaN при вычитании из них.

Ответ 2

Решение SMT Z3 поддерживает арифметику IEEE с плавающей запятой. Попросите Z3 найти случай, когда x - x != 0. Он сразу находит NaN, а также +-infinity. Исключая их, не существует x, удовлетворяющего этому уравнению.

(set-logic QF_FPA)    

(declare-const x (_ FP 11 53))
(declare-const r (_ FP 11 53))

(assert (and 
    (not (= x (as NaN (_ FP 11 53))))
    (not (= x (as plusInfinity (_ FP 11 53))))
    (not (= x (as minusInfinity (_ FP 11 53))))
    (= r (- roundTowardZero x x))
    (not (= r ((_ asFloat 11 53) roundTowardZero 0.0 0)))
))

(check-sat)
(get-model)

Z3 реализует арифметику с плавающей запятой IEEE, преобразовывая все операции в логические схемы и используя стандартный SAT-решатель для поиска модели. Запрет на любые ошибки в этом переводе или SAT-решатель является абсолютно точным.

Доказательство для...

• ... roundTowardZero: http://rise4fun.com/Z3/7H4
• ... roundNearestTiesToEven: http://rise4fun.com/Z3/Opl4W

Обратите внимание на контрпример для режима округления roundTowardNegative: http://rise4fun.com/Z3/T845. Для некоторого x результат x - x отрицательный ноль. Такой случай вряд ли может быть обнаружен людьми. Тем не менее, с решателем SMT легко найти. Мы можем изменить = на ==, чтобы Z3 вместо семантики сравнения IEEE использовала вместо точного равенства. После этого изменения снова нет встречного примера, поскольку -0 == +0 в соответствии с IEEE.

Я попытался сделать режим округления переменной. Это будет работать теоретически, но у Z3 есть ошибка. Сейчас нам нужно вручную указать режим округлого кодирования. Если бы мы могли сделать это переменной, мы могли бы попросить Z3 доказать это утверждение для всех режимов округления в одном запросе.