java - tratamiento - prueba elisa y carga viral indetectable

¿(X-x) siempre es cero positivo para los dobles, o a veces cero negativo?

Question

Cuando x es un double , ¿se garantiza (x - x) que es +0.0 , o podría ser a veces -0.0 (dependiendo del signo de x )?

Answer 1

El solucionador SMT Z3 es compatible con la aritmética de punto flotante IEEE. Pidamos a Z3 que encuentre un caso donde x - x != 0 . Inmediatamente encuentra NaN así como +-infinity . Excluyendo esos, no hay x que satisfaga esa ecuación.

(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 implementa la aritmética de punto flotante IEEE al convertir todas las operaciones en circuitos booleanos y al usar el solucionador SAT estándar para encontrar un modelo. Salvo cualquier error en esa traducción o el solucionador de SAT, el resultado es perfectamente preciso.

Prueba para ...

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

Tenga en cuenta el contraejemplo para el modo de redondeo roundTowardNegative : http://rise4fun.com/Z3/T845 . Para una cierta x el resultado de x - x es cero negativo. Tal caso difícilmente lo pueden encontrar los humanos. Sin embargo, con un solucionador de SMT es fácil de encontrar. Podemos cambiar = a == para que Z3 use la semántica de comparación de igualdad IEEE en lugar de la igualdad exacta. Después de ese cambio, nuevamente no hay contra-ejemplo porque -0 == +0 según IEEE.

Traté de hacer del modo de redondeo una variable. Eso funcionaría en teoría, pero Z3 tiene un error aquí. Por ahora tenemos que especificar manualmente un modo de redondeo codificado. Si pudiéramos convertirlo en una variable, podríamos pedirle a Z3 que pruebe esta afirmación para todos los modos de redondeo en una consulta.

Answer 2

x - x puede ser +0.0 o NaN . No hay otros valores que pueda tomar en aritmética IEEE 754 en la ronda al más cercano (y en Java, el modo de redondeo siempre es de redondeado a más cercano ). La resta de dos valores finitos idénticos se define como producir +0.0 en este modo de redondeo. Mark Dickinson , en los comentarios a continuación, cita el estándar IEEE 754 diciendo, sección 6.3:

Cuando la suma de dos operandos con signos opuestos (o la diferencia de dos operandos con signos similares) es exactamente cero, el signo de esa suma (o diferencia) será +0 en todos los atributos de redondeo, excepto roundTowardNegative [...] .

Esta page muestra que, en particular, 0.0 - 0.0 y -0.0 - (-0.0) son ambos +0.0 .

Infinities y NaN producen NaN cuando se restan de ellos mismos.