Average Error: 19.9 → 1.4
Time: 15.8s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \le 7750.30240499724:\\ \;\;\;\;{x}^{\frac{-1}{2}} - {\left(1 + x\right)}^{\frac{-1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{5}{16}}{x \cdot x}, \frac{e^{\log x \cdot \frac{-1}{2}}}{x}, \mathsf{fma}\left(\frac{1}{2}, \frac{e^{\log x \cdot \frac{-1}{2}}}{x}, \frac{-3}{8} \cdot \frac{e^{\log x \cdot \frac{-1}{2}}}{x \cdot x}\right)\right)\\ \end{array}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\begin{array}{l}
\mathbf{if}\;x \le 7750.30240499724:\\
\;\;\;\;{x}^{\frac{-1}{2}} - {\left(1 + x\right)}^{\frac{-1}{2}}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\frac{5}{16}}{x \cdot x}, \frac{e^{\log x \cdot \frac{-1}{2}}}{x}, \mathsf{fma}\left(\frac{1}{2}, \frac{e^{\log x \cdot \frac{-1}{2}}}{x}, \frac{-3}{8} \cdot \frac{e^{\log x \cdot \frac{-1}{2}}}{x \cdot x}\right)\right)\\

\end{array}
double f(double x) {
        double r3121700 = 1.0;
        double r3121701 = x;
        double r3121702 = sqrt(r3121701);
        double r3121703 = r3121700 / r3121702;
        double r3121704 = r3121701 + r3121700;
        double r3121705 = sqrt(r3121704);
        double r3121706 = r3121700 / r3121705;
        double r3121707 = r3121703 - r3121706;
        return r3121707;
}
↓
double f(double x) {
        double r3121708 = x;
        double r3121709 = 7750.30240499724;
        bool r3121710 = r3121708 <= r3121709;
        double r3121711 = -0.5;
        double r3121712 = pow(r3121708, r3121711);
        double r3121713 = 1.0;
        double r3121714 = r3121713 + r3121708;
        double r3121715 = pow(r3121714, r3121711);
        double r3121716 = r3121712 - r3121715;
        double r3121717 = 0.3125;
        double r3121718 = r3121708 * r3121708;
        double r3121719 = r3121717 / r3121718;
        double r3121720 = log(r3121708);
        double r3121721 = r3121720 * r3121711;
        double r3121722 = exp(r3121721);
        double r3121723 = r3121722 / r3121708;
        double r3121724 = 0.5;
        double r3121725 = -0.375;
        double r3121726 = r3121722 / r3121718;
        double r3121727 = r3121725 * r3121726;
        double r3121728 = fma(r3121724, r3121723, r3121727);
        double r3121729 = fma(r3121719, r3121723, r3121728);
        double r3121730 = r3121710 ? r3121716 : r3121729;
        return r3121730;
}

Error

Bits error versus x

Target

Original19.9
Target0.7
Herbie1.4
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Split input into 2 regimes

  2. if x < 7750.30240499724

    1. Initial program 0.3

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

    3. Applied pow1/20.3

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

    4. Applied pow-flip0.1

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

    5. Simplified0.1

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

    7. Applied pow1/20.1

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

    8. Applied pow-flip0.1

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

    9. Simplified0.1

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

    if 7750.30240499724 < x

    1. Initial program 40.1

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

    3. Applied pow1/240.1

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

    4. Applied pow-flip44.9

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

    5. Simplified44.9

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

    7. Applied pow1/244.9

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

    8. Applied pow-flip40.1

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

    9. Simplified40.1

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

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

    11. Simplified2.9

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

  4. Final simplification1.4

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

Reproduce

herbie shell --seed 2019154 +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)))))