Kahan p9 Example

Average Error: 20.0 → 5.1

Time: 19.9s

Precision: 64

\[0.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 -5.923851932889086889175353994573230838978 \cdot 10^{146}:\\ \;\;\;\;\sqrt[3]{-1}\\ \mathbf{elif}\;y \le -2.162218354637777142050677566983459148019 \cdot 10^{-159} \lor \neg \left(y \le 5.591292396420954063948983086185825877861 \cdot 10^{-164}\right):\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(y + x\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array}\]

C

double f(double x, double y) {
        double r79565 = x;
        double r79566 = y;
        double r79567 = r79565 - r79566;
        double r79568 = r79565 + r79566;
        double r79569 = r79567 * r79568;
        double r79570 = r79565 * r79565;
        double r79571 = r79566 * r79566;
        double r79572 = r79570 + r79571;
        double r79573 = r79569 / r79572;
        return r79573;
}

↓

double f(double x, double y) {
        double r79574 = y;
        double r79575 = -5.923851932889087e+146;
        bool r79576 = r79574 <= r79575;
        double r79577 = -1.0;
        double r79578 = cbrt(r79577);
        double r79579 = -2.1622183546377771e-159;
        bool r79580 = r79574 <= r79579;
        double r79581 = 5.591292396420954e-164;
        bool r79582 = r79574 <= r79581;
        double r79583 = !r79582;
        bool r79584 = r79580 || r79583;
        double r79585 = x;
        double r79586 = r79585 - r79574;
        double r79587 = r79574 + r79585;
        double r79588 = r79586 * r79587;
        double r79589 = r79585 * r79585;
        double r79590 = r79574 * r79574;
        double r79591 = r79589 + r79590;
        double r79592 = r79588 / r79591;
        double r79593 = 1.0;
        double r79594 = r79584 ? r79592 : r79593;
        double r79595 = r79576 ? r79578 : r79594;
        return r79595;
}

Error

Bits error versus x

Bits error versus y

Target

Original	20.0
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 3 regimes

2. if y < -5.923851932889087e+146

   1. Initial program 61.3

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

   3. Applied add-cbrt-cube 63.9

      \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\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)}}}\]

   4. Applied add-cbrt-cube 64.0

      \[\leadsto \frac{\left(x - y\right) \cdot \color{blue}{\sqrt[3]{\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)}}}{\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)}}\]

   5. Applied add-cbrt-cube 64.0

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(x - y\right) \cdot \left(x - y\right)\right) \cdot \left(x - y\right)}} \cdot \sqrt[3]{\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)}}{\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)}}\]

   6. Applied cbrt-unprod 64.0

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(\left(x - y\right) \cdot \left(x - y\right)\right) \cdot \left(x - y\right)\right) \cdot \left(\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)\right)}}}{\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)}}\]

   7. Applied cbrt-undiv 64.0

      \[\leadsto \color{blue}{\sqrt[3]{\frac{\left(\left(\left(x - y\right) \cdot \left(x - y\right)\right) \cdot \left(x - y\right)\right) \cdot \left(\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)\right)}{\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)}}}\]

   8. Simplified 59.4

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

   9. Taylor expanded around inf 0

      \[\leadsto \sqrt[3]{{\color{blue}{-1}}^{3}}\]

   if -5.923851932889087e+146 < y < -2.1622183546377771e-159 or 5.591292396420954e-164 < y

   1. Initial program 0.1

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

   if -2.1622183546377771e-159 < y < 5.591292396420954e-164

   1. Initial program 30.2

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

   3. Applied add-cbrt-cube 53.0

      \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\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)}}}\]

   4. Applied add-cbrt-cube 53.0

      \[\leadsto \frac{\left(x - y\right) \cdot \color{blue}{\sqrt[3]{\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)}}}{\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)}}\]

   5. Applied add-cbrt-cube 53.1

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(x - y\right) \cdot \left(x - y\right)\right) \cdot \left(x - y\right)}} \cdot \sqrt[3]{\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)}}{\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)}}\]

   6. Applied cbrt-unprod 52.7

      \[\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(\left(x - y\right) \cdot \left(x - y\right)\right) \cdot \left(x - y\right)\right) \cdot \left(\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)\right)}}}{\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)}}\]

   7. Applied cbrt-undiv 52.7

      \[\leadsto \color{blue}{\sqrt[3]{\frac{\left(\left(\left(x - y\right) \cdot \left(x - y\right)\right) \cdot \left(x - y\right)\right) \cdot \left(\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(x + y\right)\right)}{\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)}}}\]

   8. Simplified 31.1

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

   9. Taylor expanded around 0 15.8

      \[\leadsto \sqrt[3]{\color{blue}{1}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 5.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -5.923851932889086889175353994573230838978 \cdot 10^{146}:\\ \;\;\;\;\sqrt[3]{-1}\\ \mathbf{elif}\;y \le -2.162218354637777142050677566983459148019 \cdot 10^{-159} \lor \neg \left(y \le 5.591292396420954063948983086185825877861 \cdot 10^{-164}\right):\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(y + x\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array}\]

Reproduce

herbie shell --seed 2019194 
(FPCore (x y)
  :name "Kahan p9 Example"
  :pre (and (< 0.0 x 1.0) (< y 1.0))

  :herbie-target
  (if (< 0.5 (fabs (/ x y)) 2.0) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1.0 (/ 2.0 (+ 1.0 (* (/ x y) (/ x y))))))

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