Kahan p9 Example

Average Error: 19.4 → 0.0

Time: 39.5s

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

↓

\[\sqrt[3]{\frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \left(\left(\frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x - y}{\mathsf{hypot}\left(x, y\right)}\right) \cdot \left(\frac{x + y}{\mathsf{hypot}\left(x, y\right)} \cdot \left(\frac{x + y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x + y}{\mathsf{hypot}\left(x, y\right)}\right)\right)\right)}\]

C

double f(double x, double y) {
        double r7407167 = x;
        double r7407168 = y;
        double r7407169 = r7407167 - r7407168;
        double r7407170 = r7407167 + r7407168;
        double r7407171 = r7407169 * r7407170;
        double r7407172 = r7407167 * r7407167;
        double r7407173 = r7407168 * r7407168;
        double r7407174 = r7407172 + r7407173;
        double r7407175 = r7407171 / r7407174;
        return r7407175;
}

↓

double f(double x, double y) {
        double r7407176 = x;
        double r7407177 = y;
        double r7407178 = r7407176 - r7407177;
        double r7407179 = hypot(r7407176, r7407177);
        double r7407180 = r7407178 / r7407179;
        double r7407181 = r7407180 * r7407180;
        double r7407182 = r7407176 + r7407177;
        double r7407183 = r7407182 / r7407179;
        double r7407184 = r7407183 * r7407183;
        double r7407185 = r7407183 * r7407184;
        double r7407186 = r7407181 * r7407185;
        double r7407187 = r7407180 * r7407186;
        double r7407188 = cbrt(r7407187);
        return r7407188;
}

Error

Bits error versus x

Bits error versus y

Target

Original	19.4
Target	0.0
Herbie	0.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. Initial program 19.4

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

2. Simplified 19.4

   \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot \left(y + x\right)}{\mathsf{fma}\left(x, x, \left(y \cdot y\right)\right)}}\]
3. Using strategy rm

4. Applied add-sqr-sqrt 19.4

   \[\leadsto \frac{\left(x - y\right) \cdot \left(y + x\right)}{\color{blue}{\sqrt{\mathsf{fma}\left(x, x, \left(y \cdot y\right)\right)} \cdot \sqrt{\mathsf{fma}\left(x, x, \left(y \cdot y\right)\right)}}}\]

5. Applied times-frac 19.4

   \[\leadsto \color{blue}{\frac{x - y}{\sqrt{\mathsf{fma}\left(x, x, \left(y \cdot y\right)\right)}} \cdot \frac{y + x}{\sqrt{\mathsf{fma}\left(x, x, \left(y \cdot y\right)\right)}}}\]
6. Using strategy rm

7. Applied add-cbrt-cube 19.4

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

8. Applied add-cbrt-cube 31.3

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

9. Applied add-cbrt-cube 31.3

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

10. Applied cbrt-undiv 31.3

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

11. Applied cbrt-unprod 31.3

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

12. Simplified 0.0

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

13. Final simplification 0.0

    \[\leadsto \sqrt[3]{\frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \left(\left(\frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x - y}{\mathsf{hypot}\left(x, y\right)}\right) \cdot \left(\frac{x + y}{\mathsf{hypot}\left(x, y\right)} \cdot \left(\frac{x + y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x + y}{\mathsf{hypot}\left(x, y\right)}\right)\right)\right)}\]

Reproduce

herbie shell --seed 2019124 +o rules:numerics
(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))))