Average Error: 20.1 → 0.3
Time: 4.2s
Precision: binary64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \]
↓
\[\begin{array}{l} t_0 := {\left(1 + x\right)}^{-0.5}\\ t_1 := {\left({\left(1 + x\right)}^{0.25}\right)}^{-1}\\ \mathbf{if}\;\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \leq 2.2486610555365327 \cdot 10^{-13}:\\ \;\;\;\;\frac{\frac{\frac{0.5}{x} \cdot x - \frac{0.375}{x}}{x}}{\sqrt{x}}\\ \mathbf{else}:\\ \;\;\;\;\left({x}^{-0.5} - t_0\right) + \mathsf{fma}\left(-t_1, t_1, t_0\right)\\ \end{array} \]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\begin{array}{l}
t_0 := {\left(1 + x\right)}^{-0.5}\\
t_1 := {\left({\left(1 + x\right)}^{0.25}\right)}^{-1}\\
\mathbf{if}\;\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \leq 2.2486610555365327 \cdot 10^{-13}:\\
\;\;\;\;\frac{\frac{\frac{0.5}{x} \cdot x - \frac{0.375}{x}}{x}}{\sqrt{x}}\\

\mathbf{else}:\\
\;\;\;\;\left({x}^{-0.5} - t_0\right) + \mathsf{fma}\left(-t_1, t_1, t_0\right)\\


\end{array}

(FPCore (x) :precision binary64 (- (/ 1.0 (sqrt x)) (/ 1.0 (sqrt (+ x 1.0)))))
↓
(FPCore (x)
 :precision binary64
 (let* ((t_0 (pow (+ 1.0 x) -0.5)) (t_1 (pow (pow (+ 1.0 x) 0.25) -1.0)))
   (if (<=
        (- (/ 1.0 (sqrt x)) (/ 1.0 (sqrt (+ x 1.0))))
        2.2486610555365327e-13)
     (/ (/ (- (* (/ 0.5 x) x) (/ 0.375 x)) x) (sqrt x))
     (+ (- (pow x -0.5) t_0) (fma (- t_1) t_1 t_0)))))
double code(double x) {
	return (1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0)));
}
↓
double code(double x) {
	double t_0 = pow((1.0 + x), -0.5);
	double t_1 = pow(pow((1.0 + x), 0.25), -1.0);
	double tmp;
	if (((1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0)))) <= 2.2486610555365327e-13) {
		tmp = ((((0.5 / x) * x) - (0.375 / x)) / x) / sqrt(x);
	} else {
		tmp = (pow(x, -0.5) - t_0) + fma(-t_1, t_1, t_0);
	}
	return tmp;
}

Error

Bits error versus x

Target

Original20.1
Target0.7
Herbie0.3
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}} \]

Derivation

  1. Split input into 2 regimes

  2. if (-.f64 (/.f64 1 (sqrt.f64 x)) (/.f64 1 (sqrt.f64 (+.f64 x 1)))) < 2.24866106e-13

    1. Initial program 40.6

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

    2. Applied egg-rr45.7

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

    3. Taylor expanded in x around inf 0.2

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

    4. Simplified0.2

      \[\leadsto \frac{\color{blue}{\frac{0.5}{x} - \frac{0.375}{x \cdot x}}}{\sqrt{x}} \]

    5. Applied egg-rr0.2

      \[\leadsto \frac{\color{blue}{\frac{\frac{0.5}{x} \cdot x - \frac{0.375}{x}}{x}}}{\sqrt{x}} \]

    if 2.24866106e-13 < (-.f64 (/.f64 1 (sqrt.f64 x)) (/.f64 1 (sqrt.f64 (+.f64 x 1))))

    1. Initial program 0.6

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

    2. Applied egg-rr0.4

      \[\leadsto \color{blue}{\left({x}^{-0.5} - {\left(1 + x\right)}^{-0.5}\right) + \mathsf{fma}\left(-{\left({\left(1 + x\right)}^{0.25}\right)}^{-1}, {\left({\left(1 + x\right)}^{0.25}\right)}^{-1}, {\left(1 + x\right)}^{-0.5}\right)} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification0.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \leq 2.2486610555365327 \cdot 10^{-13}:\\ \;\;\;\;\frac{\frac{\frac{0.5}{x} \cdot x - \frac{0.375}{x}}{x}}{\sqrt{x}}\\ \mathbf{else}:\\ \;\;\;\;\left({x}^{-0.5} - {\left(1 + x\right)}^{-0.5}\right) + \mathsf{fma}\left(-{\left({\left(1 + x\right)}^{0.25}\right)}^{-1}, {\left({\left(1 + x\right)}^{0.25}\right)}^{-1}, {\left(1 + x\right)}^{-0.5}\right)\\ \end{array} \]

Reproduce

herbie shell --seed 2022129 
(FPCore (x)
  :name "2isqrt (example 3.6)"
  :precision binary64

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

  (- (/ 1.0 (sqrt x)) (/ 1.0 (sqrt (+ x 1.0)))))