Average Error: 19.5 → 5.6
Time: 15.3s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \le 8017.181738326081:\\ \;\;\;\;\mathsf{fma}\left(\frac{-1}{\sqrt{\sqrt{1 + x}}}, \frac{1}{\sqrt{\sqrt{1 + x}}}, \frac{1}{\sqrt{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt{\sqrt{1 + x}}}\right) + \mathsf{fma}\left(1, {x}^{\frac{-1}{2}}, -\frac{1}{\sqrt{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt{\sqrt{1 + x}}}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\frac{1}{x \cdot x} + \frac{1}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right) - \frac{1}{x \cdot \left(x \cdot x\right)}}{{x}^{\frac{-1}{2}} + \frac{1}{\sqrt{1 + x}}}\\ \end{array}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\begin{array}{l}
\mathbf{if}\;x \le 8017.181738326081:\\
\;\;\;\;\mathsf{fma}\left(\frac{-1}{\sqrt{\sqrt{1 + x}}}, \frac{1}{\sqrt{\sqrt{1 + x}}}, \frac{1}{\sqrt{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt{\sqrt{1 + x}}}\right) + \mathsf{fma}\left(1, {x}^{\frac{-1}{2}}, -\frac{1}{\sqrt{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt{\sqrt{1 + x}}}\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{\left(\frac{1}{x \cdot x} + \frac{1}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right) - \frac{1}{x \cdot \left(x \cdot x\right)}}{{x}^{\frac{-1}{2}} + \frac{1}{\sqrt{1 + x}}}\\

\end{array}
double f(double x) {
        double r2185644 = 1.0;
        double r2185645 = x;
        double r2185646 = sqrt(r2185645);
        double r2185647 = r2185644 / r2185646;
        double r2185648 = r2185645 + r2185644;
        double r2185649 = sqrt(r2185648);
        double r2185650 = r2185644 / r2185649;
        double r2185651 = r2185647 - r2185650;
        return r2185651;
}
↓
double f(double x) {
        double r2185652 = x;
        double r2185653 = 8017.181738326081;
        bool r2185654 = r2185652 <= r2185653;
        double r2185655 = -1.0;
        double r2185656 = 1.0;
        double r2185657 = r2185656 + r2185652;
        double r2185658 = sqrt(r2185657);
        double r2185659 = sqrt(r2185658);
        double r2185660 = r2185655 / r2185659;
        double r2185661 = r2185656 / r2185659;
        double r2185662 = r2185661 * r2185661;
        double r2185663 = fma(r2185660, r2185661, r2185662);
        double r2185664 = -0.5;
        double r2185665 = pow(r2185652, r2185664);
        double r2185666 = -r2185662;
        double r2185667 = fma(r2185656, r2185665, r2185666);
        double r2185668 = r2185663 + r2185667;
        double r2185669 = r2185652 * r2185652;
        double r2185670 = r2185656 / r2185669;
        double r2185671 = r2185669 * r2185669;
        double r2185672 = r2185656 / r2185671;
        double r2185673 = r2185670 + r2185672;
        double r2185674 = r2185652 * r2185669;
        double r2185675 = r2185656 / r2185674;
        double r2185676 = r2185673 - r2185675;
        double r2185677 = r2185656 / r2185658;
        double r2185678 = r2185665 + r2185677;
        double r2185679 = r2185676 / r2185678;
        double r2185680 = r2185654 ? r2185668 : r2185679;
        return r2185680;
}

Error

Bits error versus x

Target

Original19.5
Target0.6
Herbie5.6
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Split input into 2 regimes

  2. if x < 8017.181738326081

    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 add-sqr-sqrt0.1

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

    8. Applied sqrt-prod0.1

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

    9. Applied *-un-lft-identity0.1

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

    10. Applied times-frac0.1

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

    11. Applied *-un-lft-identity0.1

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

    12. Applied prod-diff0.1

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

    if 8017.181738326081 < x

    1. Initial program 39.5

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

    3. Applied pow1/239.5

      \[\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 flip--44.9

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

    8. Taylor expanded around inf 11.3

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

    9. Simplified11.3

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

  4. Final simplification5.6

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

Reproduce

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