Est-ce que (x - x) est toujours un zéro positif pour les doubles, ou parfois un zéro négatif ?

Question

Lorsque x est un double c'est (x - x) garanti pour être +0.0 ou est-ce qu'il pourrait parfois être -0.0 (selon le signe de x ) ?

Answer 1

x - x peut être +0.0 ou NaN . Il n'y a pas d'autres valeurs qu'il puisse prendre dans l'arithmétique IEEE 754 en round-to-nearest (et en Java, le mode d'arrondi est toujours le plus proche ). La soustraction de deux valeurs finies identiques est défini en tant que producteur +0.0 dans ce mode d'arrondi. Mark Dickinson dans les commentaires ci-dessous, cite la norme IEEE 754 en disant, section 6.3 :

Lorsque la somme de deux opérandes de signes opposés (ou la différence de deux opérandes de même signe) est exactement égale à zéro, le signe de cette somme (ou de cette différence) est égal à +0 dans tous les attributs d'arrondi, sauf roundTowardNegative [...].

Ce site page montre qu'en particulier 0.0 - 0.0 et -0.0 - (-0.0) sont tous deux +0.0 .

Les infinis et les NaN produisent tous deux NaN lorsqu'ils sont soustraits d'eux-mêmes.

Answer 2

Le solveur SMT Z3 supporte l'arithmétique à virgule flottante IEEE. Demandons à Z3 de trouver un cas où x - x != 0 . Il trouve immédiatement NaN ainsi que +-infinity . Si l'on exclut ces derniers, il n'y a pas x qui satisfait à cette équation.

(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 implémente l'arithmétique à virgule flottante IEEE en convertissant toutes les opérations en circuits booléens et en utilisant le solveur SAT standard pour trouver un modèle. En l'absence de tout bogue dans cette traduction ou dans le solveur SAT, le résultat est parfaitement précis.

Preuve de...

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

Notez le contre-exemple pour le mode d'arrondi roundTowardNegative : http://rise4fun.com/Z3/T845 . Pour un certain x le résultat de x - x est un zéro négatif. Un tel cas peut difficilement être trouvé par des humains. Pourtant, avec un solveur SMT, il est facile à trouver. Nous pouvons changer = à == de sorte que Z3 utilise la sémantique de comparaison de l'égalité IEEE au lieu de l'égalité exacte. Après ce changement, il n'y a à nouveau aucun contre-exemple car -0 == +0 selon l'IEEE.

J'ai essayé de faire du mode d'arrondi une variable. Cela devrait fonctionner en théorie, mais Z3 a un bug à ce niveau. Pour l'instant, nous devons spécifier manuellement un mode d'arrondi codé en dur. Si nous pouvions en faire une variable, nous pourrions demander à Z3 de prouver cette affirmation pour tous modes d'arrondi dans une seule requête.