Is (x - x) always positive zero for doubles, or sometimes negative zero?

Solution 1:

x - x can be +0.0 or NaN. There are no other values it can take in IEEE 754 arithmetics in round-to-nearest (and in Java, the rounding mode is always round-to-nearest). The subtraction of two identical finite values is defined as producing +0.0 in this rounding mode. Mark Dickinson, in comments below, cites the IEEE 754 standard as saying, section 6.3:

When the sum of two operands with opposite signs (or the difference of two operands with like signs) is exactly zero, the sign of that sum (or difference) shall be +0 in all rounding-direction attributes except roundTowardNegative [...].

This page shows that in particular 0.0 - 0.0 and -0.0 - (-0.0) are both +0.0.

Infinities and NaN both produce NaN when subtracted from themselves.

Solution 2:

The SMT solver Z3 supports IEEE floating point arithmetic. Let's ask Z3 to find a case where x - x != 0. It immediately finds NaN as well as +-infinity. Excluding those, there is no x that satisfies that equation.

(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 implements IEEE floating point arithmetic by converting all operations to boolean circuits and using the standard SAT solver to find a model. Barring any bugs in that translation or the SAT solver the result is perfectly precise.

Proof for...

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

Note the counterexample for the rounding mode roundTowardNegative: http://rise4fun.com/Z3/T845. For a certain x the result of x - x is negative zero. Such a case can hardly be found by humans. Yet, with an SMT solver it is easy to find. We can change = to == so that Z3 uses IEEE equality comparison semantics instead of exact equality. After that change, there is again no counter-example because -0 == +0 according to IEEE.

I tried making the rounding mode a variable. That would work in theory but Z3 has a bug here. For now we have to manually specify a hard-coded rounding mode. If we could make it a variable we could ask Z3 to prove this statement for all rounding modes in one query.