[conistonwater]

So the question is: if you feel like you don't get the math formula, but you get the windows-and-buckets explanation of it, is it still possible that your understanding doesn't match the true underlying concept? Because that is the pitfall with a lot of intuitive explanations, that unless you are sure that the explanations are equivalent to the true thing, you might end up understanding an idea that is close but slightly off.

So a puzzle: if two positive numbers in exactly the same window are subtracted, what is the worst-case rounding error you can get in the result?

[jessermeyer]

To confuse analogies with formal reasoning is a misuse of analogies. They are stepping stones, a kind of 'sniff test' or 'sizing up' of the mind to set the stage for more formal understanding. Is this your point?

Because, to re-use your argument, the pitfall with many formal definitions is that they are not easily understandable, whose payoff is often not much more than the analogy for the learner, but requires significantly more resources.

So, which would you prefer as an introduction? A "good enough" understanding, or no understanding because the bar of entry was too high?

[kllrnohj]

> you might end up understanding an idea that is close but slightly off

Just like most floating point numbers

ba dum tss

[sharpneli]

Error relative to the original numbers or to the result?

[ambicapter]

Is it 2(1/2^23)(window size)?

[conistonwater]

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.