(x - x)对于双精度是否总是正零,或者有时负零？

Question

如果x是double,则(x - x)保证是+0.0,也可能有时-0.0(取决于标志x)？

Answer 1

x - x可以是+0.0或NaN.IEEE 754算术中没有其他值可以采用舍入到最接近的值(在Java中,舍入模式始终是舍入到最接近的).减去两个相同的有限值被定义为+0.0在该舍入模式中产生.Mark Dickinson在下面的评论中引用了IEEE 754标准,第6.3节:

当具有相反符号的两个操作数之和(或具有相同符号的两个操作数的差异)恰好为零时,除了roundTowardNegative [...]之外,所有舍入方向属性中该和(或差)的符号应为+0. .

此页面显示特别是0.0 - 0.0并且-0.0 - (-0.0)都是+0.0.

当从自身中减去时,无穷大和NaN都产生NaN.

Answer 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通过将所有操作转换为布尔电路并使用标准SAT求解器来查找模型来实现IEEE浮点算法.除非该翻译或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 在一个查询中为所有舍入模式证明这个语句.