Kahan p9 Example

Average Error: 19.9 → 4.9

Time: 10.6s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

\[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 -1.26217265671792371 \cdot 10^{64}:\\ \;\;\;\;\sqrt[3]{{-1}^{3}}\\ \mathbf{elif}\;y \le -3.30902003427186255 \cdot 10^{-163} \lor \neg \left(y \le 1.0639458246816258 \cdot 10^{-162}\right):\\ \;\;\;\;\sqrt[3]{{\left(\frac{1}{\frac{\frac{x \cdot x + y \cdot y}{x - y}}{\left(x + y\right) \cdot \left(x + y\right)} \cdot \left(x + y\right)}\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{{1}^{3}}\\ \end{array}\]

C

double f(double x, double y) {
        double r76989 = x;
        double r76990 = y;
        double r76991 = r76989 - r76990;
        double r76992 = r76989 + r76990;
        double r76993 = r76991 * r76992;
        double r76994 = r76989 * r76989;
        double r76995 = r76990 * r76990;
        double r76996 = r76994 + r76995;
        double r76997 = r76993 / r76996;
        return r76997;
}

↓

double f(double x, double y) {
        double r76998 = y;
        double r76999 = -1.2621726567179237e+64;
        bool r77000 = r76998 <= r76999;
        double r77001 = -1.0;
        double r77002 = 3.0;
        double r77003 = pow(r77001, r77002);
        double r77004 = cbrt(r77003);
        double r77005 = -3.3090200342718626e-163;
        bool r77006 = r76998 <= r77005;
        double r77007 = 1.0639458246816258e-162;
        bool r77008 = r76998 <= r77007;
        double r77009 = !r77008;
        bool r77010 = r77006 || r77009;
        double r77011 = 1.0;
        double r77012 = x;
        double r77013 = r77012 * r77012;
        double r77014 = r76998 * r76998;
        double r77015 = r77013 + r77014;
        double r77016 = r77012 - r76998;
        double r77017 = r77015 / r77016;
        double r77018 = r77012 + r76998;
        double r77019 = r77018 * r77018;
        double r77020 = r77017 / r77019;
        double r77021 = r77020 * r77018;
        double r77022 = r77011 / r77021;
        double r77023 = pow(r77022, r77002);
        double r77024 = cbrt(r77023);
        double r77025 = pow(r77011, r77002);
        double r77026 = cbrt(r77025);
        double r77027 = r77010 ? r77024 : r77026;
        double r77028 = r77000 ? r77004 : r77027;
        return r77028;
}

Error

Bits error versus x

Bits error versus y

Target

Original	19.9
Target	0.0
Herbie	4.9

\[\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 < -1.2621726567179237e+64

   1. Initial program 40.5

      \[\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.3

      \[\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 63.7

      \[\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 63.7

      \[\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 40.5

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

   9. Taylor expanded around 0 0

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

   if -1.2621726567179237e+64 < y < -3.3090200342718626e-163 or 1.0639458246816258e-162 < 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 add-cbrt-cube 32.1

      \[\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 32.1

      \[\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 32.3

      \[\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 31.6

      \[\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 31.5

      \[\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 0.2

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

   10. Applied clear-num 0.2

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

   12. Applied flip-- 0.2

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

   13. Applied associate-*l/ 11.7

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

   14. Applied associate-/r/ 11.7

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

   15. Simplified 0.2

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

   if -3.3090200342718626e-163 < y < 1.0639458246816258e-162

   1. Initial program 29.7

      \[\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 52.3

      \[\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 52.3

      \[\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 52.4

      \[\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.1

      \[\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.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 29.7

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

   10. Applied clear-num 29.7

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

   12. Applied flip-- 29.7

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

   13. Applied associate-*l/ 40.9

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

   14. Applied associate-/r/ 40.9

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

   15. Simplified 29.7

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

   16. Taylor expanded around inf 15.1

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

4. Final simplification 4.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.26217265671792371 \cdot 10^{64}:\\ \;\;\;\;\sqrt[3]{{-1}^{3}}\\ \mathbf{elif}\;y \le -3.30902003427186255 \cdot 10^{-163} \lor \neg \left(y \le 1.0639458246816258 \cdot 10^{-162}\right):\\ \;\;\;\;\sqrt[3]{{\left(\frac{1}{\frac{\frac{x \cdot x + y \cdot y}{x - y}}{\left(x + y\right) \cdot \left(x + y\right)} \cdot \left(x + y\right)}\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{{1}^{3}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020045 
(FPCore (x y)
  :name "Kahan p9 Example"
  :precision binary64
  :pre (and (< 0.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))))