(x-x)는 복식의 경우 항상 양의 0입니까, 때로는 음의 0입니까?

(x-x)는 복식의 경우 항상 양의 0입니까, 때로는 음의 0입니까?

---

때 xA를한다 double,한다 (x - x)보장 +0.0, 또는 때때로 수 있습니다 -0.0(의 기호에 따라 x)?

---

x - x+0.0또는 일 수 있습니다 NaN. IEEE 754 산술에서 가장 가까운 값으로 반올림 할 수있는 다른 값은 없습니다 (그리고 Java에서는 반올림 모드가 항상 가장 가까운 값으로 반올림 됨 ). 두 개의 동일한 유한 값의 빼기는 이 반올림 모드에서 생성하는 것으로 정의+0.0 됩니다. Mark Dickinson 은 아래 주석에서 IEEE 754 표준을 6.3 절로 인용합니다.

반대 부호를 가진 두 피연산자의 합 (또는 유사한 부호를 가진 두 피연산자의 차이)이 정확히 0 인 경우 해당 합계 (또는 차이)의 부호는 roundTowardNegative를 제외한 모든 반올림 방향 속성에서 +0이됩니다. [...] .

이 페이지 는 특히 0.0 - 0.0및 -0.0 - (-0.0)둘 다 보여줍니다 +0.0.

Infinities와 NaN은 둘 다 자신에서 빼면 NaN을 생성합니다.

---

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는 음의 0입니다. 그러한 경우는 인간에게 거의 발견되지 않습니다. 그러나 SMT 솔버를 사용하면 쉽게 찾을 수 있습니다. 우리는 변경할 수 =에 ==Z3는 IEEE 동등 비교의 L 대신 정확한 평등을 사용하도록. 그 변경 후에는 -0 == +0IEEE에 따라 반대 사례가 다시 없습니다 .

반올림 모드를 변수로 만들려고했습니다. 이론적으로는 작동하지만 Z3에는 여기에 버그가 있습니다. 지금은 하드 코딩 된 반올림 모드를 수동으로 지정해야합니다. 변수로 만들 수 있다면 Z3에게 한 쿼리에서 모든 반올림 모드에 대해이 진술을 증명하도록 요청할 수 있습니다.

참고 URL : https://stackoverflow.com/questions/24950928/is-xx-always-positive-zero-for-doubles-or-sometimes-negative-zero