Kahan p9 Example

Average Error: 20.4 → 5.1

Time: 3.1m

Precision: 64

\[0 \lt x \lt 1 \land y \lt 1\]

Math

\[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

↓

\[\begin{array}{l} \mathbf{if}\;y \le -1.3308054258701725 \cdot 10^{+154}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -3.1512930280169555 \cdot 10^{-162}:\\ \;\;\;\;\sqrt[3]{\frac{\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)} \cdot \frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)}}}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)}}}\\ \mathbf{elif}\;y \le 8.250332507489211 \cdot 10^{-160}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)}}\\ \end{array}\]

C

double f(double x, double y) {
        double r34729430 = x;
        double r34729431 = y;
        double r34729432 = r34729430 - r34729431;
        double r34729433 = r34729430 + r34729431;
        double r34729434 = r34729432 * r34729433;
        double r34729435 = r34729430 * r34729430;
        double r34729436 = r34729431 * r34729431;
        double r34729437 = r34729435 + r34729436;
        double r34729438 = r34729434 / r34729437;
        return r34729438;
}

↓

double f(double x, double y) {
        double r34729439 = y;
        double r34729440 = -1.3308054258701725e+154;
        bool r34729441 = r34729439 <= r34729440;
        double r34729442 = -1.0;
        double r34729443 = -3.1512930280169555e-162;
        bool r34729444 = r34729439 <= r34729443;
        double r34729445 = 1.0;
        double r34729446 = x;
        double r34729447 = r34729446 * r34729446;
        double r34729448 = r34729439 * r34729439;
        double r34729449 = r34729447 + r34729448;
        double r34729450 = r34729446 - r34729439;
        double r34729451 = r34729439 + r34729446;
        double r34729452 = r34729450 * r34729451;
        double r34729453 = r34729449 / r34729452;
        double r34729454 = r34729453 * r34729453;
        double r34729455 = r34729445 / r34729454;
        double r34729456 = r34729455 / r34729453;
        double r34729457 = cbrt(r34729456);
        double r34729458 = 8.250332507489211e-160;
        bool r34729459 = r34729439 <= r34729458;
        double r34729460 = r34729445 / r34729453;
        double r34729461 = r34729459 ? r34729445 : r34729460;
        double r34729462 = r34729444 ? r34729457 : r34729461;
        double r34729463 = r34729441 ? r34729442 : r34729462;
        return r34729463;
}

Error

Bits error versus x

Bits error versus y

Target

Original	20.4
Target	0.1
Herbie	5.1

\[\begin{array}{l} \mathbf{if}\;0.5 \lt \left|\frac{x}{y}\right| \lt 2:\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{2}{1 + \frac{x}{y} \cdot \frac{x}{y}}\\ \end{array}\]

Derivation

1. Split input into 4 regimes

2. if y < -1.3308054258701725e+154

   1. Initial program 63.6

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
   2. Using strategy rm

   3. Applied clear-num 63.6

      \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(x + y\right)}}}\]
   4. Using strategy rm

   5. Applied add-cbrt-cube 63.6

      \[\leadsto \frac{1}{\frac{x \cdot x + y \cdot y}{\color{blue}{\sqrt[3]{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}}\]

   6. Applied add-cbrt-cube 63.6

      \[\leadsto \frac{1}{\frac{\color{blue}{\sqrt[3]{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}}}{\sqrt[3]{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}\]

   7. Applied cbrt-undiv 63.6

      \[\leadsto \frac{1}{\color{blue}{\sqrt[3]{\frac{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}}\]

   8. Applied add-cbrt-cube 63.6

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(1 \cdot 1\right) \cdot 1}}}{\sqrt[3]{\frac{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}\]

   9. Applied cbrt-undiv 63.6

      \[\leadsto \color{blue}{\sqrt[3]{\frac{\left(1 \cdot 1\right) \cdot 1}{\frac{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}}\]

   10. Simplified 63.6

       \[\leadsto \sqrt[3]{\color{blue}{\frac{\frac{1}{\frac{y \cdot y + x \cdot x}{\left(x - y\right) \cdot \left(x + y\right)} \cdot \frac{y \cdot y + x \cdot x}{\left(x - y\right) \cdot \left(x + y\right)}}}{\frac{y \cdot y + x \cdot x}{\left(x - y\right) \cdot \left(x + y\right)}}}}\]

   11. Taylor expanded around inf 0

       \[\leadsto \color{blue}{-1}\]

   if -1.3308054258701725e+154 < y < -3.1512930280169555e-162

   1. Initial program 0.0

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
   2. Using strategy rm

   3. Applied clear-num 0.0

      \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(x + y\right)}}}\]
   4. Using strategy rm

   5. Applied add-cbrt-cube 37.7

      \[\leadsto \frac{1}{\frac{x \cdot x + y \cdot y}{\color{blue}{\sqrt[3]{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}}\]

   6. Applied add-cbrt-cube 38.1

      \[\leadsto \frac{1}{\frac{\color{blue}{\sqrt[3]{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}}}{\sqrt[3]{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}\]

   7. Applied cbrt-undiv 38.1

      \[\leadsto \frac{1}{\color{blue}{\sqrt[3]{\frac{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}}\]

   8. Applied add-cbrt-cube 38.1

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(1 \cdot 1\right) \cdot 1}}}{\sqrt[3]{\frac{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}\]

   9. Applied cbrt-undiv 38.1

      \[\leadsto \color{blue}{\sqrt[3]{\frac{\left(1 \cdot 1\right) \cdot 1}{\frac{\left(\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x + y \cdot y\right)\right) \cdot \left(x \cdot x + y \cdot y\right)}{\left(\left(\left(x - y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)\right) \cdot \left(\left(x - y\right) \cdot \left(x + y\right)\right)}}}}\]

   10. Simplified 0.0

       \[\leadsto \sqrt[3]{\color{blue}{\frac{\frac{1}{\frac{y \cdot y + x \cdot x}{\left(x - y\right) \cdot \left(x + y\right)} \cdot \frac{y \cdot y + x \cdot x}{\left(x - y\right) \cdot \left(x + y\right)}}}{\frac{y \cdot y + x \cdot x}{\left(x - y\right) \cdot \left(x + y\right)}}}}\]

   if -3.1512930280169555e-162 < y < 8.250332507489211e-160

   1. Initial program 29.9

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

   2. Taylor expanded around inf 15.9

      \[\leadsto \color{blue}{1}\]

   if 8.250332507489211e-160 < y

   1. Initial program 0.1

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
   2. Using strategy rm

   3. Applied clear-num 0.1

      \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(x + y\right)}}}\]
3. Recombined 4 regimes into one program.

4. Final simplification 5.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.3308054258701725 \cdot 10^{+154}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -3.1512930280169555 \cdot 10^{-162}:\\ \;\;\;\;\sqrt[3]{\frac{\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)} \cdot \frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)}}}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)}}}\\ \mathbf{elif}\;y \le 8.250332507489211 \cdot 10^{-160}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{x \cdot x + y \cdot y}{\left(x - y\right) \cdot \left(y + x\right)}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019128 
(FPCore (x y)
  :name "Kahan p9 Example"
  :pre (and (< 0 x 1) (< y 1))

  :herbie-target
  (if (< 0.5 (fabs (/ x y)) 2) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1 (/ 2 (+ 1 (* (/ x y) (/ x y))))))

  (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))