# Sterbenz lemma

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 H. Sterbenz, who published a variant of it in 1974.
Sterbenz lemma — In a floating-point number system with subnormal numbers, if $x$ and $y$ are floating-point numbers such that
${\frac {y}{2}}\leq x\leq 2y,$
then $x-y$ is also a floating-point number. Thus, a correctly rounded floating-point subtraction
$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.

## Proof

Let $\beta$ be the radix of the floating-point system and $p$ the precision.
Consider several easy cases first:
* If $x$ is zero then $x-y=-y$, and if $y$ is zero then $x-y=x$, so the result is trivial because floating-point negation is always exact.
* If $x=y$ the result is zero and thus exact.
* If $x<0$ then we must also have $y/2\leq x<0$ so $y<0$. In this case, $x-y=-(-x--y)$, so the result follows from the theorem restricted to $x,y\geq 0$.
* If $x\leq y$, we can write $x-y=-(y-x)$ with $x/2\leq y\leq 2x$, so the result follows from the theorem restricted to $x\geq y$.
For the rest of the proof, assume $0<y<x\leq 2y$ without loss of generality.
Write $x,y>0$ in terms of their positive integral significands $s_{x},s_{y}\leq \beta ^{p}-1$ and minimal exponents $e_{x},e_{y}$:
${\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$ and $y$ may be subnormal—we do not assume $s_{x},s_{y}\geq \beta ^{p-1}$.
The subtraction gives:
${\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}}$
Let $s'=s_{x}\beta ^{e_{x}-e_{y}}-s_{y}$. Since $0<y<x$ we have:
* $e_{y}\leq e_{x}$, so $e_{x}-e_{y}\geq 0$, from which we can conclude $\beta ^{e_{x}-e_{y}}$ is an integer and therefore so is $s'=s_{x}\beta ^{e_{x}-e_{y}}-s_{y}$; and
* $x-y>0$, so $s'>0$.
Further, since $x\leq 2y$, we have $x-y\leq y$, so that
$s'\cdot \beta ^{e_{y}-p+1}=x-y\leq y=s_{y}\cdot \beta ^{e_{y}-p+1}$
which implies that
$0<s'\leq s_{y}\leq \beta ^{p}-1.$
Hence
$x-y=s'\cdot \beta ^{e_{y}-p+1},\quad {\text{for}}\quad 0<s'\leq \beta ^{p}-1,$
so $x-y$ is a floating-point number. ◻
Note: Even if $x$ and $y$ are normal, i.e., $s_{x},s_{y}\geq \beta ^{p-1}$, we cannot prove that $s'\geq \beta ^{p-1}$ and therefore cannot prove that $x-y$ is also normal. For example, the difference of the two smallest positive normal floating-point numbers $x=(\beta ^{p-1}+1)\cdot \beta ^{e_{\mathrm {min} }-p+1}$ and $y=\beta ^{p-1}\cdot \beta ^{e_{\mathrm {min} }-p+1}$ is $x-y=1\cdot \beta ^{e_{\mathrm {min} }-p+1}$ 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.

## Relation to catastrophic cancellation

The Sterbenz lemma may be contrasted with the phenomenon of catastrophic cancellation:
* The Sterbenz lemma asserts that if $x$ and $y$ are sufficiently close floating-point numbers then their difference $x-y$ is computed exactly by floating-point arithmetic $x\ominus y=\operatorname {fl} (x-y)$, with no rounding needed.
* The phenomenon of catastrophic cancellation is that if ${\tilde {x}}$ and ${\tilde {y}}$ are approximations to true numbers $x$ and $y$—whether the approximations arise from prior rounding error or from series truncation or from physical uncertainty or anything else—the error of the difference ${\tilde {x}}-{\tilde {y}}$ from the desired difference $x-y$ is inversely proportional to $x-y$. Thus, the closer $x$ and $y$ are, the worse ${\tilde {x}}-{\tilde {y}}$ may be as an approximation to $x-y$, even if the subtraction itself is computed exactly.
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.

## Use in numerical analysis

The Sterbenz lemma is instrumental in proving theorems on error bounds in numerical analysis of floating-point algorithms. For example, Heron's formula $A={\sqrt {s(s-a)(s-b)(s-c)}}$ for the area of triangle with side lengths $a$, $b$, and $c$, where $s=(a+b+c)/2$ is the semi-perimeter, may give poor accuracy for long narrow triangles if evaluated directly in floating-point arithmetic. However, for $a\geq b\geq c$, the alternative formula $A={\frac {1}{4}}{\sqrt {{\bigla+(b+c){\bigr )}{\biglc-(a-b){\bigr )}{\biglc+(a-b){\bigr )}{\bigla+(b-c){\bigr )}}}$ can be proven, with the help of the Sterbenz lemma, to have low forward error for all inputs.