In floating-point arithmetic, the Sterbenz lemma or Sterbenz's lemma is a theorem giving conditions under which floating-point differences are computed exactly. It is named after Pat Holmes Sterbenz, who published a variant of it in 1974.
The Sterbenz lemma applies to IEEE 754, the most widely used floating-point number system in computers.
Proof Let β {\displaystyle \beta } be the radix of the floating-point system and p {\displaystyle p} the precision. Consider several easy cases first:
If x {\displaystyle x} is zero then x − y = − y {\displaystyle x-y=-y} , and if y {\displaystyle y} is zero then x − y = x {\displaystyle x-y=x} , so the result is trivial because floating-point negation is always exact. If x = y {\displaystyle x=y} the result is zero and thus exact. If x < 0 {\displaystyle x<0} then we must also have y / 2 ≤ x < 0 {\displaystyle y/2\leq x<0} so y < 0 {\displaystyle y<0} . In this case, x − y = − ( − x − − y ) {\displaystyle x-y=-(-x--y)} , so the result follows from the theorem restricted to x , y ≥ 0 {\displaystyle x,y\geq 0} . If x ≤ y {\displaystyle x\leq y} , we can write x − y = − ( y − x ) {\displaystyle x-y=-(y-x)} with x / 2 ≤ y ≤ 2 x {\displaystyle x/2\leq y\leq 2x} , so the result follows from the theorem restricted to x ≥ y {\displaystyle x\geq y} . For the rest of the proof, assume 0 < y < x ≤ 2 y {\displaystyle 0<y<x\leq 2y} without loss of generality. Write x , y > 0 {\displaystyle x,y>0} in terms of their positive integral significands s x , s y ≤ β p − 1 {\displaystyle s_{x},s_{y}\leq \beta ^{p}-1} and minimal exponents e x , e y {\displaystyle e_{x},e_{y}} :
x = s x ⋅ β e x − p + 1 y = s y ⋅ β e y − p + 1 {\displaystyle {\begin{aligned}x&=s_{x}\cdot \beta ^{e_{x}-p+1}\\y&=s_{y}\cdot \beta ^{e_{y}-p+1}\end{aligned}}}
Note that x {\displaystyle x} and y {\displaystyle y} may be subnormal—we do not assume s x , s y ≥ β p − 1 {\displaystyle s_{x},s_{y}\geq \beta ^{p-1}} . The subtraction gives:
… excerpt ends here. Continue reading the full article.
