2isqrt (example 3.6)

Average Error: 20.1 → 1.5

Time: 22.9s

Precision: 64

Math

\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le 5626.584148737379:\\ \;\;\;\;\mathsf{fma}\left(\left(\frac{-1}{\sqrt[3]{\sqrt{1 + x}}}\right), \left(\frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}}\right), \left(\frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt[3]{\sqrt{1 + x}}}\right)\right) + \mathsf{fma}\left(1, \left({x}^{\frac{-1}{2}}\right), \left(\frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}} \cdot \frac{-1}{\sqrt[3]{\sqrt{1 + x}}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\left(\frac{\frac{5}{16}}{x \cdot x}\right), \left(\frac{e^{\log x \cdot \frac{-1}{2}}}{x}\right), \left(\left(\frac{1}{2} - \frac{\frac{3}{8}}{x}\right) \cdot \frac{e^{\log x \cdot \frac{-1}{2}}}{x}\right)\right)\\ \end{array}\]

C

double f(double x) {
        double r3381624 = 1.0;
        double r3381625 = x;
        double r3381626 = sqrt(r3381625);
        double r3381627 = r3381624 / r3381626;
        double r3381628 = r3381625 + r3381624;
        double r3381629 = sqrt(r3381628);
        double r3381630 = r3381624 / r3381629;
        double r3381631 = r3381627 - r3381630;
        return r3381631;
}

↓

double f(double x) {
        double r3381632 = x;
        double r3381633 = 5626.584148737379;
        bool r3381634 = r3381632 <= r3381633;
        double r3381635 = -1.0;
        double r3381636 = 1.0;
        double r3381637 = r3381636 + r3381632;
        double r3381638 = sqrt(r3381637);
        double r3381639 = cbrt(r3381638);
        double r3381640 = r3381635 / r3381639;
        double r3381641 = r3381639 * r3381639;
        double r3381642 = r3381636 / r3381641;
        double r3381643 = r3381636 / r3381639;
        double r3381644 = r3381642 * r3381643;
        double r3381645 = fma(r3381640, r3381642, r3381644);
        double r3381646 = -0.5;
        double r3381647 = pow(r3381632, r3381646);
        double r3381648 = r3381642 * r3381640;
        double r3381649 = fma(r3381636, r3381647, r3381648);
        double r3381650 = r3381645 + r3381649;
        double r3381651 = 0.3125;
        double r3381652 = r3381632 * r3381632;
        double r3381653 = r3381651 / r3381652;
        double r3381654 = log(r3381632);
        double r3381655 = r3381654 * r3381646;
        double r3381656 = exp(r3381655);
        double r3381657 = r3381656 / r3381632;
        double r3381658 = 0.5;
        double r3381659 = 0.375;
        double r3381660 = r3381659 / r3381632;
        double r3381661 = r3381658 - r3381660;
        double r3381662 = r3381661 * r3381657;
        double r3381663 = fma(r3381653, r3381657, r3381662);
        double r3381664 = r3381634 ? r3381650 : r3381663;
        return r3381664;
}

Error

Bits error versus x

Target

Original	20.1
Target	0.7
Herbie	1.5

\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

1. Split input into 2 regimes

2. if x < 5626.584148737379

   1. Initial program 0.4

      \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
   2. Using strategy rm

   3. Applied pow1 0.4

      \[\leadsto \frac{1}{\sqrt{\color{blue}{{x}^{1}}}} - \frac{1}{\sqrt{x + 1}}\]

   4. Applied sqrt-pow1 0.4

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

   5. Applied pow-flip 0.1

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

   6. Simplified 0.1

      \[\leadsto {x}^{\color{blue}{\frac{-1}{2}}} - \frac{1}{\sqrt{x + 1}}\]
   7. Using strategy rm

   8. Applied add-cube-cbrt 0.1

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

   9. Applied add-sqr-sqrt 0.1

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

   10. Applied times-frac 0.1

       \[\leadsto {x}^{\frac{-1}{2}} - \color{blue}{\frac{\sqrt{1}}{\sqrt[3]{\sqrt{x + 1}} \cdot \sqrt[3]{\sqrt{x + 1}}} \cdot \frac{\sqrt{1}}{\sqrt[3]{\sqrt{x + 1}}}}\]

   11. Applied *-un-lft-identity 0.1

       \[\leadsto \color{blue}{1 \cdot {x}^{\frac{-1}{2}}} - \frac{\sqrt{1}}{\sqrt[3]{\sqrt{x + 1}} \cdot \sqrt[3]{\sqrt{x + 1}}} \cdot \frac{\sqrt{1}}{\sqrt[3]{\sqrt{x + 1}}}\]

   12. Applied prod-diff 0.1

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

   if 5626.584148737379 < x

   1. Initial program 39.7

      \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
   2. Using strategy rm

   3. Applied pow1 39.7

      \[\leadsto \frac{1}{\sqrt{\color{blue}{{x}^{1}}}} - \frac{1}{\sqrt{x + 1}}\]

   4. Applied sqrt-pow1 39.7

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

   5. Applied pow-flip 45.1

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

   6. Simplified 45.1

      \[\leadsto {x}^{\color{blue}{\frac{-1}{2}}} - \frac{1}{\sqrt{x + 1}}\]
   7. Using strategy rm

   8. Applied pow1/2 45.1

      \[\leadsto {x}^{\frac{-1}{2}} - \frac{1}{\color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}}}\]

   9. Applied pow-flip 39.7

      \[\leadsto {x}^{\frac{-1}{2}} - \color{blue}{{\left(x + 1\right)}^{\left(-\frac{1}{2}\right)}}\]

   10. Simplified 39.7

       \[\leadsto {x}^{\frac{-1}{2}} - {\left(x + 1\right)}^{\color{blue}{\frac{-1}{2}}}\]

   11. Taylor expanded around -inf 62.7

       \[\leadsto \color{blue}{\left(\frac{1}{2} \cdot \frac{e^{\frac{-1}{2} \cdot \left(\log -1 - \log \left(\frac{-1}{x}\right)\right)}}{x} + \frac{5}{16} \cdot \frac{e^{\frac{-1}{2} \cdot \left(\log -1 - \log \left(\frac{-1}{x}\right)\right)}}{{x}^{3}}\right) - \frac{3}{8} \cdot \frac{e^{\frac{-1}{2} \cdot \left(\log -1 - \log \left(\frac{-1}{x}\right)\right)}}{{x}^{2}}}\]

   12. Simplified 2.9

       \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\frac{\frac{5}{16}}{x \cdot x}\right), \left(\frac{e^{0 + \frac{-1}{2} \cdot \log x}}{x}\right), \left(\frac{e^{0 + \frac{-1}{2} \cdot \log x}}{x} \cdot \left(\frac{1}{2} - \frac{\frac{3}{8}}{x}\right)\right)\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 1.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 5626.584148737379:\\ \;\;\;\;\mathsf{fma}\left(\left(\frac{-1}{\sqrt[3]{\sqrt{1 + x}}}\right), \left(\frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}}\right), \left(\frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt[3]{\sqrt{1 + x}}}\right)\right) + \mathsf{fma}\left(1, \left({x}^{\frac{-1}{2}}\right), \left(\frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}} \cdot \frac{-1}{\sqrt[3]{\sqrt{1 + x}}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\left(\frac{\frac{5}{16}}{x \cdot x}\right), \left(\frac{e^{\log x \cdot \frac{-1}{2}}}{x}\right), \left(\left(\frac{1}{2} - \frac{\frac{3}{8}}{x}\right) \cdot \frac{e^{\log x \cdot \frac{-1}{2}}}{x}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019129 +o rules:numerics
(FPCore (x)
  :name "2isqrt (example 3.6)"

  :herbie-target
  (/ 1 (+ (* (+ x 1) (sqrt x)) (* x (sqrt (+ x 1)))))

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))