In floating-point arithmetic, the Sterbenz lemma or Sterbenz's lemma[1] is a theorem giving conditions under which floating-point differences are computed exactly.
It is named after Pat H. Sterbenz, who published a variant of it in 1974.
[2] Sterbenz lemma — In a floating-point number system with subnormal numbers, if
are floating-point numbers such that
is also a floating-point number.
Thus, a correctly rounded floating-point subtraction
{\displaystyle x\ominus y=\operatorname {fl} (x-y)=x-y}
is computed exactly.
The Sterbenz lemma applies to IEEE 754, the most widely used floating-point number system in computers.
be the radix of the floating-point system and
Consider several easy cases first: For the rest of the proof, assume
without loss of generality.
in terms of their positive integral significands
β
and minimal exponents
The subtraction gives:
{\displaystyle {\begin{aligned}x-y&=s_{x}\cdot \beta ^{e_{x}-p+1}-s_{y}\cdot \beta ^{e_{y}-p+1}\\&=s_{x}\beta ^{e_{x}-e_{y}}\cdot \beta ^{e_{y}-p+1}-s_{y}\cdot \beta ^{e_{y}-p+1}\\&=(s_{x}\beta ^{e_{x}-e_{y}}-s_{y})\cdot \beta ^{e_{y}-p+1}.\end{aligned}}}
is a floating-point number.
For example, the difference of the two smallest positive normal floating-point numbers
which is necessarily subnormal.
In floating-point number systems without subnormal numbers, such as CPUs in nonstandard flush-to-zero mode instead of the standard gradual underflow, the Sterbenz lemma does not apply.
The Sterbenz lemma may be contrasted with the phenomenon of catastrophic cancellation: In other words, the Sterbenz lemma shows that subtracting nearby floating-point numbers is exact, but if the numbers one has are approximations then even their exact difference may be far off from the difference of numbers one wanted to subtract.
The Sterbenz lemma is instrumental in proving theorems on error bounds in numerical analysis of floating-point algorithms.
For example, Heron's formula
{\displaystyle A={\sqrt {s(s-a)(s-b)(s-c)}}}
for the area of triangle with side lengths
is the semi-perimeter, may give poor accuracy for long narrow triangles if evaluated directly in floating-point arithmetic.
, the alternative formula
{\displaystyle A={\frac {1}{4}}{\sqrt {{\bigl (}a+(b+c){\bigr )}{\bigl (}c-(a-b){\bigr )}{\bigl (}c+(a-b){\bigr )}{\bigl (}a+(b-c){\bigr )}}}}
can be proven, with the help of the Sterbenz lemma, to have low forward error for all inputs.