6
$\begingroup$

I want to know whether the equation : a-b+b = a is always true for a, b belongs to double precision floating-point number and |a|>=|b|.

If the equation is true, how can I proof it?

If not, what precondition can make the equation right?

A counterexample shows the equation is not true, so I now want to know, the inequality |((a-b)+b)-a|<=ulp(a) is true or not, how can I proof the inequality?

I have tested the python code below for half hours, the inequality |a-b+b-a|<=ulp(a) seems hold.

def getulp(x):
x = float(x)
k = frexp(x)[1]-1
if x == 0.0:
    return pow(2, -1074)
if (k<1023)&(k>-1022):
    return pow(2,k-52)
else:
    return pow(2,-1074)



while 1> 0:
k = np.random.randint(-100, 100)
ub = np.float_power(2,k-1)
db = np.float_power(2,k)
j = np.random.randint(-100, 100)
ub2 = np.float_power(2, j - 1)
db2 = np.float_power(2, j)
x = np.random.uniform(ub,db,1)
y = np.random.uniform(ub2,db2,1)
if x>y:
    temp = x-y+y
    if np.fabs(temp-x)>getulp(x):
        print x
        print y
        print "The inequality false"
else:
    temp = y-x+x
    if np.fabs(temp-y)>getulp(y):
        print x
        print y
        print "The inequality false"

Thanks for the counterexample by @Kirill, I will explain why I need to proof the equation. I want to proof, image the a, b are two end points of a line, then if I know the value b and a-b, I want to proof that I can get the value of a without error larger than one ULP(a) error. So I can give the condition |a|>=|b| or |a|<=|b|, but I can not limit their actual value.

$\endgroup$
  • $\begingroup$ The equation reduces to a=a, which is rather fundamental. $\endgroup$ – Nuclear Wang Jun 26 '18 at 16:05
  • 8
    $\begingroup$ a-b+b is not always equal to a, if a, b is floating-point number, for example, if a= 1, and b = 1e100, the results a-b+b = 0 while a = 1. Rounding error lead to the difference. $\endgroup$ – Star Jun 26 '18 at 16:09
  • 1
    $\begingroup$ @Star I think the previous commenter was pointing you towards a subtle distinction; The equation is always trivially true. An implementation may or may not fail due to carry forward of round-off errors from subcalculations. $\endgroup$ – origimbo Jun 26 '18 at 17:43
  • 5
    $\begingroup$ a=3.9999999981380427, b=1.0000000000000016, (a-b)+b=3.999999998138043≠a is a counterexample. I also want to point out that the question of what precondition would make it hold is really broad. For example, $2>a>b>1$ is sufficient (I checked with an SMT solver), but is that even helpful? It might help if you said why it is important to you that $(a-b)+b=a$ should hold, that would really narrow down the question. $\endgroup$ – Kirill Jun 26 '18 at 17:51
  • $\begingroup$ Thanks for the counterexample by @Kirill. The counterexample shows the equation is not true, so I now want to know, the inequality a-b+b-a<=ulp(a) is true or not, how can I proof the inequality? $\endgroup$ – Star Jun 26 '18 at 23:26
9
$\begingroup$

You can sometimes prove such results (or get counterexamples) using an SMT solver such as Z3 that supports floating point arithmetic. Here is a proof of a version of your theorem that says $|((x+y)-y)-x| \leq 2^{-23}|x|$ when $x>y>1$ and $x+y\neq\infty_{32}$ in 32-bit floating point arithmetic:

λ> import Data.SBV
λ> :set -XScopedTypeVariables
λ> prove $ \(x::SFloat) (y::SFloat) -> fpIsNormal (x+y) &&& x .> y &&& y .> 1 ==> fpAbs (((x+y)-y)-x) .< fpAbs x * 1.1920928955078125e-7
Q.E.D.

Here I used the sbv package in Haskell. If it holds for 32-bit floats, it should hold for 64-bit floats also.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.