对于双精度，（x - x）是否始终为正零，或者有时为负零？

floating-point java

2022-08-31 14:25:22

什么时候是，何时保证是，或者有时可能是（取决于）的符号？xdouble(x - x)+0.0-0.0x

答案 1

x - x可以是或。在IEEE 754算术中，它没有其他值可以舍入到最接近（在Java中，舍入模式始终是舍入到最近）。两个相同的有限值的减法被定义为在此舍入模式下产生。马克·迪金森（Mark Dickinson）在下面的评论中引用了IEEE 754标准，第6.3节：+0.0NaN+0.0

当具有相反符号的两个操作数之和（或两个具有类似符号的操作数的差值）正好为零时，该和（或差值）的符号在所有舍入方向属性中应为 +0，除了 roundTowardNegative [...]。

此页面显示，特别是和两者兼而有之。0.0 - 0.0-0.0 - (-0.0)+0.0

无穷大和 NaN 在从自身中减去时都会产生 NaN。

答案 2

SMT 求解器 Z3 支持 IEEE 浮点运算。让我们让 Z3 找到一个案例，其中 .它立即找到以及.排除这些，没有满足该等式的东西。x - x != 0NaN+-infinityx

(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 通过将所有运算转换为布尔电路并使用标准 SAT 求解器查找模型来实现 IEEE 浮点运算。除非该翻译或SAT求解器中的任何错误，否则结果非常精确。

证明...

...： http://rise4fun.com/Z3/7H4roundTowardZero
...： http://rise4fun.com/Z3/Opl4WroundNearestTiesToEven

请注意舍入模式的反例：http://rise4fun.com/Z3/T845。对于某个，结果为负零。人类很难找到这样的案例。然而，使用SMT求解器很容易找到。我们可以更改为 Z3 使用 IEEE 相等比较语义，而不是精确相等。在那次改变之后，再次没有反例，因为根据IEEE。roundTowardNegativexx - x===-0 == +0

我尝试将舍入模式设置为变量。这在理论上是可行的，但Z3在这里有一个错误。现在，我们必须手动指定硬编码的舍入模式。如果我们能使它成为一个变量，我们可以要求 Z3 在一个查询中证明所有舍入模式的此语句。