Hacker News new | ask | show | jobs
by ambicapter 3191 days ago
Is it 2(1/2^23)(window size)?
1 comments
conistonwater 3191 days ago
It should be zero, exactly zero, i.e., no rounding error. Because if you do long subtraction on the significands, the number of digits you need to store the result is at most the number of digits you had, because the numbers were within a factor of two from each other (so no shifting left or right).

Just to check, with sbv in haskell, using the Z3 SMT solver:

    λ> f (x::SFloat) (y::SFloat) = fpIsNormal x &&& fpIsNormal y &&& y/2 .<= x &&& x .<= 2*y ==> fromSFloat sRNE (x - y) .== (fromSFloat sRNE x :: SDouble) - (fromSFloat sRNE y :: SDouble)
    f :: SFloat -> SFloat -> SBool
    λ> prove (forAll_ f)
    Q.E.D.
Or without rounding through double, using the formula for exact rounding error of a sum:

    λ> g (x::SFloat) (y::SFloat) = fpIsNormal x &&& fpIsNormal y &&& 0 .<= x &&& y .<= x &&& x .<= 2*y ==> (x - ((x-y) + y)) .== 0
    g :: SFloat -> SFloat -> SBool
    λ> prove (forAll_ g)
    Q.E.D.
link