Kahan p9 Example

Average Error: 20.5 → 5.0

Time: 16.0s

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.375278492253273374474910915175481103343 \cdot 10^{150}:\\ \;\;\;\;\sqrt[3]{-1}\\ \mathbf{elif}\;y \le -8.743307936790758972176410083672769129911 \cdot 10^{-162}:\\ \;\;\;\;\sqrt[3]{{\left(\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\right)}^{3}}\\ \mathbf{elif}\;y \le 3.818900502976060184978387855020150274323 \cdot 10^{-177}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(x - y\right) \cdot x + \left(x - y\right) \cdot y}{x \cdot x + y \cdot y}\\ \end{array}\]

C

double f(double x, double y) {
        double r114803 = x;
        double r114804 = y;
        double r114805 = r114803 - r114804;
        double r114806 = r114803 + r114804;
        double r114807 = r114805 * r114806;
        double r114808 = r114803 * r114803;
        double r114809 = r114804 * r114804;
        double r114810 = r114808 + r114809;
        double r114811 = r114807 / r114810;
        return r114811;
}

↓

double f(double x, double y) {
        double r114812 = y;
        double r114813 = -5.3752784922532734e+150;
        bool r114814 = r114812 <= r114813;
        double r114815 = -1.0;
        double r114816 = cbrt(r114815);
        double r114817 = -8.743307936790759e-162;
        bool r114818 = r114812 <= r114817;
        double r114819 = x;
        double r114820 = r114819 - r114812;
        double r114821 = r114819 + r114812;
        double r114822 = r114820 * r114821;
        double r114823 = r114819 * r114819;
        double r114824 = r114812 * r114812;
        double r114825 = r114823 + r114824;
        double r114826 = r114822 / r114825;
        double r114827 = 3.0;
        double r114828 = pow(r114826, r114827);
        double r114829 = cbrt(r114828);
        double r114830 = 3.81890050297606e-177;
        bool r114831 = r114812 <= r114830;
        double r114832 = 1.0;
        double r114833 = r114820 * r114819;
        double r114834 = r114820 * r114812;
        double r114835 = r114833 + r114834;
        double r114836 = r114835 / r114825;
        double r114837 = r114831 ? r114832 : r114836;
        double r114838 = r114818 ? r114829 : r114837;
        double r114839 = r114814 ? r114816 : r114838;
        return r114839;
}

Error

Bits error versus x

Bits error versus y

Target

Original	20.5
Target	0.0
Herbie	5.0

\[\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 < -5.3752784922532734e+150

   1. Initial program 62.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 64.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 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 62.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. Taylor expanded around 0 0

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

   if -5.3752784922532734e+150 < y < -8.743307936790759e-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 add-cbrt-cube 37.7

      \[\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 38.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 38.2

      \[\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 38.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 38.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 0.1

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

   if -8.743307936790759e-162 < y < 3.81890050297606e-177

   1. Initial program 30.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 53.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 53.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 53.2

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

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

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

      \[\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 *-un-lft-identity 30.1

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

   11. Applied times-frac 30.9

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

   12. Simplified 30.9

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

   13. Taylor expanded around inf 14.8

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

   if 3.81890050297606e-177 < y

   1. Initial program 3.0

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

   3. Applied distribute-lft-in 3.0

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

4. Final simplification 5.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -5.375278492253273374474910915175481103343 \cdot 10^{150}:\\ \;\;\;\;\sqrt[3]{-1}\\ \mathbf{elif}\;y \le -8.743307936790758972176410083672769129911 \cdot 10^{-162}:\\ \;\;\;\;\sqrt[3]{{\left(\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\right)}^{3}}\\ \mathbf{elif}\;y \le 3.818900502976060184978387855020150274323 \cdot 10^{-177}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(x - y\right) \cdot x + \left(x - y\right) \cdot y}{x \cdot x + y \cdot y}\\ \end{array}\]

Reproduce

herbie shell --seed 2019304 
(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))))