Kahan p9 Example

Average Error: 20.0 → 5.1

Time: 11.6s

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)}{y \cdot y + x \cdot x}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{{\left(\frac{y + x}{y + x}\right)}^{3}}\\ \end{array}\]

C

double f(double x, double y) {
        double r58286 = x;
        double r58287 = y;
        double r58288 = r58286 - r58287;
        double r58289 = r58286 + r58287;
        double r58290 = r58288 * r58289;
        double r58291 = r58286 * r58286;
        double r58292 = r58287 * r58287;
        double r58293 = r58291 + r58292;
        double r58294 = r58290 / r58293;
        return r58294;
}

↓

double f(double x, double y) {
        double r58295 = y;
        double r58296 = -5.923851932889087e+146;
        bool r58297 = r58295 <= r58296;
        double r58298 = -1.0;
        double r58299 = cbrt(r58298);
        double r58300 = -2.1622183546377771e-159;
        bool r58301 = r58295 <= r58300;
        double r58302 = 5.591292396420954e-164;
        bool r58303 = r58295 <= r58302;
        double r58304 = !r58303;
        bool r58305 = r58301 || r58304;
        double r58306 = x;
        double r58307 = r58306 - r58295;
        double r58308 = r58295 + r58306;
        double r58309 = r58307 * r58308;
        double r58310 = r58295 * r58295;
        double r58311 = r58306 * r58306;
        double r58312 = r58310 + r58311;
        double r58313 = r58309 / r58312;
        double r58314 = r58308 / r58308;
        double r58315 = 3.0;
        double r58316 = pow(r58314, r58315);
        double r58317 = cbrt(r58316);
        double r58318 = r58305 ? r58313 : r58317;
        double r58319 = r58297 ? r58299 : r58318;
        return r58319;
}

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}}\]

   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 inf 15.8

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