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

, когда x Это double, is (x - x) гарантированно +0.0, или иногда это может быть -0.0 (в зависимости от знака x)?

2 68
javascript floating-point

2 ответа:

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

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

этой страница показывает, что, в частности 0.0 - 0.0 и -0.0 - (-0.0) как +0.0.

Бесконечности и NaN оба производят NaN при вычитании из себя.

60

решатель 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 результат отлично точный.

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

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

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

9