2isqrt (example 3.6)

Percentage Accurate: 38.3% → 99.1%
Time: 7.6s
Alternatives: 4
Speedup: N/A×

Specification

?
\[x > 1 \land x < 10^{+308}\]
\[\begin{array}{l} \\ \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \end{array} \]
(FPCore (x) :precision binary64 (- (/ 1.0 (sqrt x)) (/ 1.0 (sqrt (+ x 1.0)))))
double code(double x) {
	return (1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0)));
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x)
use fmin_fmax_functions
    real(8), intent (in) :: x
    code = (1.0d0 / sqrt(x)) - (1.0d0 / sqrt((x + 1.0d0)))
end function
public static double code(double x) {
	return (1.0 / Math.sqrt(x)) - (1.0 / Math.sqrt((x + 1.0)));
}
def code(x):
	return (1.0 / math.sqrt(x)) - (1.0 / math.sqrt((x + 1.0)))
function code(x)
	return Float64(Float64(1.0 / sqrt(x)) - Float64(1.0 / sqrt(Float64(x + 1.0))))
end
function tmp = code(x)
	tmp = (1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0)));
end
code[x_] := N[(N[(1.0 / N[Sqrt[x], $MachinePrecision]), $MachinePrecision] - N[(1.0 / N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 4 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 38.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \end{array} \]
(FPCore (x) :precision binary64 (- (/ 1.0 (sqrt x)) (/ 1.0 (sqrt (+ x 1.0)))))
double code(double x) {
	return (1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0)));
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x)
use fmin_fmax_functions
    real(8), intent (in) :: x
    code = (1.0d0 / sqrt(x)) - (1.0d0 / sqrt((x + 1.0d0)))
end function
public static double code(double x) {
	return (1.0 / Math.sqrt(x)) - (1.0 / Math.sqrt((x + 1.0)));
}
def code(x):
	return (1.0 / math.sqrt(x)) - (1.0 / math.sqrt((x + 1.0)))
function code(x)
	return Float64(Float64(1.0 / sqrt(x)) - Float64(1.0 / sqrt(Float64(x + 1.0))))
end
function tmp = code(x)
	tmp = (1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0)));
end
code[x_] := N[(N[(1.0 / N[Sqrt[x], $MachinePrecision]), $MachinePrecision] - N[(1.0 / N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
\end{array}

Alternative 1: 99.1% accurate, N/A× speedup?

\[\begin{array}{l} \\ \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}{x \cdot \left(\left(1 - -0.5 \cdot {x}^{-1}\right) - \frac{0.125}{x \cdot x}\right)} \end{array} \]
(FPCore (x)
 :precision binary64
 (/
  (/
   (fma
    -0.125
    (pow (pow x -1.0) 0.5)
    (fma
     -0.0390625
     (pow (pow (pow x 5.0) -1.0) 0.5)
     (fma 0.0625 (pow (pow (pow x 3.0) -1.0) 0.5) (* 0.5 (pow x 0.5)))))
   x)
  (* x (- (- 1.0 (* -0.5 (pow x -1.0))) (/ 0.125 (* x x))))))
double code(double x) {
	return (fma(-0.125, pow(pow(x, -1.0), 0.5), fma(-0.0390625, pow(pow(pow(x, 5.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(x, 3.0), -1.0), 0.5), (0.5 * pow(x, 0.5))))) / x) / (x * ((1.0 - (-0.5 * pow(x, -1.0))) - (0.125 / (x * x))));
}
function code(x)
	return Float64(Float64(fma(-0.125, ((x ^ -1.0) ^ 0.5), fma(-0.0390625, (((x ^ 5.0) ^ -1.0) ^ 0.5), fma(0.0625, (((x ^ 3.0) ^ -1.0) ^ 0.5), Float64(0.5 * (x ^ 0.5))))) / x) / Float64(x * Float64(Float64(1.0 - Float64(-0.5 * (x ^ -1.0))) - Float64(0.125 / Float64(x * x)))))
end
code[x_] := N[(N[(N[(-0.125 * N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.0390625 * N[Power[N[Power[N[Power[x, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Power[x, 0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / x), $MachinePrecision] / N[(x * N[(N[(1.0 - N[(-0.5 * N[Power[x, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(0.125 / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}{x \cdot \left(\left(1 - -0.5 \cdot {x}^{-1}\right) - \frac{0.125}{x \cdot x}\right)}
\end{array}
Derivation
  1. Initial program 42.0%

    \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}} \]
    2. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{x}}} - \frac{1}{\sqrt{x + 1}} \]
    3. lift-sqrt.f64N/A

      \[\leadsto \frac{1}{\color{blue}{\sqrt{x}}} - \frac{1}{\sqrt{x + 1}} \]
    4. lift-/.f64N/A

      \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\frac{1}{\sqrt{x + 1}}} \]
    5. lift-+.f64N/A

      \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{\color{blue}{x + 1}}} \]
    6. lift-sqrt.f64N/A

      \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\color{blue}{\sqrt{x + 1}}} \]
    7. frac-subN/A

      \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}}} \]
    8. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}}} \]
    9. lower--.f64N/A

      \[\leadsto \frac{\color{blue}{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    10. lower-*.f64N/A

      \[\leadsto \frac{\color{blue}{1 \cdot \sqrt{x + 1}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    11. pow1/2N/A

      \[\leadsto \frac{1 \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    12. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    13. lift-+.f64N/A

      \[\leadsto \frac{1 \cdot {\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    14. lower-*.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - \color{blue}{\sqrt{x} \cdot 1}}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    15. pow1/2N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - \color{blue}{{x}^{\frac{1}{2}}} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    16. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - \color{blue}{{x}^{\frac{1}{2}}} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    17. lower-*.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{\color{blue}{\sqrt{x} \cdot \sqrt{x + 1}}} \]
    18. pow1/2N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{\color{blue}{{x}^{\frac{1}{2}}} \cdot \sqrt{x + 1}} \]
    19. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{\color{blue}{{x}^{\frac{1}{2}}} \cdot \sqrt{x + 1}} \]
    20. pow1/2N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{{x}^{\frac{1}{2}} \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}}} \]
    21. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{{x}^{\frac{1}{2}} \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}}} \]
    22. lift-+.f6442.0

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{0.5} - {x}^{0.5} \cdot 1}{{x}^{0.5} \cdot {\color{blue}{\left(x + 1\right)}}^{0.5}} \]
  4. Applied rewrites42.0%

    \[\leadsto \color{blue}{\frac{1 \cdot {\left(x + 1\right)}^{0.5} - {x}^{0.5} \cdot 1}{{x}^{0.5} \cdot {\left(x + 1\right)}^{0.5}}} \]
  5. Taylor expanded in x around inf

    \[\leadsto \frac{\color{blue}{\frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \left(\frac{-5}{128} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{x}^{3}}} + \frac{1}{2} \cdot \sqrt{x}\right)\right)}{x}}}{{x}^{\frac{1}{2}} \cdot {\left(x + 1\right)}^{\frac{1}{2}}} \]
  6. Step-by-step derivation
    1. lower-/.f64N/A

      \[\leadsto \frac{\frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \left(\frac{-5}{128} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{x}^{3}}} + \frac{1}{2} \cdot \sqrt{x}\right)\right)}{\color{blue}{x}}}{{x}^{\frac{1}{2}} \cdot {\left(x + 1\right)}^{\frac{1}{2}}} \]
  7. Applied rewrites99.2%

    \[\leadsto \frac{\color{blue}{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}}{{x}^{0.5} \cdot {\left(x + 1\right)}^{0.5}} \]
  8. Taylor expanded in x around inf

    \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{\color{blue}{x \cdot \left(\left(1 + \frac{1}{2} \cdot \frac{1}{x}\right) - \frac{\frac{1}{8}}{{x}^{2}}\right)}} \]
  9. Step-by-step derivation
    1. lower-*.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{x \cdot \color{blue}{\left(\left(1 + \frac{1}{2} \cdot \frac{1}{x}\right) - \frac{\frac{1}{8}}{{x}^{2}}\right)}} \]
    2. lower--.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{x \cdot \left(\left(1 + \frac{1}{2} \cdot \frac{1}{x}\right) - \color{blue}{\frac{\frac{1}{8}}{{x}^{2}}}\right)} \]
  10. Applied rewrites99.2%

    \[\leadsto \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}{\color{blue}{x \cdot \left(\left(1 - -0.5 \cdot {x}^{-1}\right) - \frac{0.125}{x \cdot x}\right)}} \]
  11. Add Preprocessing

Alternative 2: 99.1% accurate, N/A× speedup?

\[\begin{array}{l} \\ \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot e^{\log x \cdot 0.5}\right)\right)\right)}{x}}{{x}^{0.5} \cdot e^{\log \left(x + 1\right) \cdot 0.5}} \end{array} \]
(FPCore (x)
 :precision binary64
 (/
  (/
   (fma
    -0.125
    (pow (pow x -1.0) 0.5)
    (fma
     -0.0390625
     (pow (pow (pow x 5.0) -1.0) 0.5)
     (fma
      0.0625
      (pow (pow (pow x 3.0) -1.0) 0.5)
      (* 0.5 (exp (* (log x) 0.5))))))
   x)
  (* (pow x 0.5) (exp (* (log (+ x 1.0)) 0.5)))))
double code(double x) {
	return (fma(-0.125, pow(pow(x, -1.0), 0.5), fma(-0.0390625, pow(pow(pow(x, 5.0), -1.0), 0.5), fma(0.0625, pow(pow(pow(x, 3.0), -1.0), 0.5), (0.5 * exp((log(x) * 0.5)))))) / x) / (pow(x, 0.5) * exp((log((x + 1.0)) * 0.5)));
}
function code(x)
	return Float64(Float64(fma(-0.125, ((x ^ -1.0) ^ 0.5), fma(-0.0390625, (((x ^ 5.0) ^ -1.0) ^ 0.5), fma(0.0625, (((x ^ 3.0) ^ -1.0) ^ 0.5), Float64(0.5 * exp(Float64(log(x) * 0.5)))))) / x) / Float64((x ^ 0.5) * exp(Float64(log(Float64(x + 1.0)) * 0.5))))
end
code[x_] := N[(N[(N[(-0.125 * N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(-0.0390625 * N[Power[N[Power[N[Power[x, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.0625 * N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] + N[(0.5 * N[Exp[N[(N[Log[x], $MachinePrecision] * 0.5), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / x), $MachinePrecision] / N[(N[Power[x, 0.5], $MachinePrecision] * N[Exp[N[(N[Log[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot e^{\log x \cdot 0.5}\right)\right)\right)}{x}}{{x}^{0.5} \cdot e^{\log \left(x + 1\right) \cdot 0.5}}
\end{array}
Derivation
  1. Initial program 42.0%

    \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}} \]
    2. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{x}}} - \frac{1}{\sqrt{x + 1}} \]
    3. lift-sqrt.f64N/A

      \[\leadsto \frac{1}{\color{blue}{\sqrt{x}}} - \frac{1}{\sqrt{x + 1}} \]
    4. lift-/.f64N/A

      \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\frac{1}{\sqrt{x + 1}}} \]
    5. lift-+.f64N/A

      \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{\color{blue}{x + 1}}} \]
    6. lift-sqrt.f64N/A

      \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\color{blue}{\sqrt{x + 1}}} \]
    7. frac-subN/A

      \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}}} \]
    8. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}}} \]
    9. lower--.f64N/A

      \[\leadsto \frac{\color{blue}{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    10. lower-*.f64N/A

      \[\leadsto \frac{\color{blue}{1 \cdot \sqrt{x + 1}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    11. pow1/2N/A

      \[\leadsto \frac{1 \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    12. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    13. lift-+.f64N/A

      \[\leadsto \frac{1 \cdot {\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    14. lower-*.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - \color{blue}{\sqrt{x} \cdot 1}}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    15. pow1/2N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - \color{blue}{{x}^{\frac{1}{2}}} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    16. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - \color{blue}{{x}^{\frac{1}{2}}} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}} \]
    17. lower-*.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{\color{blue}{\sqrt{x} \cdot \sqrt{x + 1}}} \]
    18. pow1/2N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{\color{blue}{{x}^{\frac{1}{2}}} \cdot \sqrt{x + 1}} \]
    19. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{\color{blue}{{x}^{\frac{1}{2}}} \cdot \sqrt{x + 1}} \]
    20. pow1/2N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{{x}^{\frac{1}{2}} \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}}} \]
    21. lower-pow.f64N/A

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{\frac{1}{2}} - {x}^{\frac{1}{2}} \cdot 1}{{x}^{\frac{1}{2}} \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}}} \]
    22. lift-+.f6442.0

      \[\leadsto \frac{1 \cdot {\left(x + 1\right)}^{0.5} - {x}^{0.5} \cdot 1}{{x}^{0.5} \cdot {\color{blue}{\left(x + 1\right)}}^{0.5}} \]
  4. Applied rewrites42.0%

    \[\leadsto \color{blue}{\frac{1 \cdot {\left(x + 1\right)}^{0.5} - {x}^{0.5} \cdot 1}{{x}^{0.5} \cdot {\left(x + 1\right)}^{0.5}}} \]
  5. Taylor expanded in x around inf

    \[\leadsto \frac{\color{blue}{\frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \left(\frac{-5}{128} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{x}^{3}}} + \frac{1}{2} \cdot \sqrt{x}\right)\right)}{x}}}{{x}^{\frac{1}{2}} \cdot {\left(x + 1\right)}^{\frac{1}{2}}} \]
  6. Step-by-step derivation
    1. lower-/.f64N/A

      \[\leadsto \frac{\frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \left(\frac{-5}{128} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{1}{16} \cdot \sqrt{\frac{1}{{x}^{3}}} + \frac{1}{2} \cdot \sqrt{x}\right)\right)}{\color{blue}{x}}}{{x}^{\frac{1}{2}} \cdot {\left(x + 1\right)}^{\frac{1}{2}}} \]
  7. Applied rewrites99.2%

    \[\leadsto \frac{\color{blue}{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}}{{x}^{0.5} \cdot {\left(x + 1\right)}^{0.5}} \]
  8. Step-by-step derivation
    1. lift-+.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot {\color{blue}{\left(x + 1\right)}}^{\frac{1}{2}}} \]
    2. lift-pow.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot \color{blue}{{\left(x + 1\right)}^{\frac{1}{2}}}} \]
    3. pow-to-expN/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot \color{blue}{e^{\log \left(x + 1\right) \cdot \frac{1}{2}}}} \]
    4. lower-exp.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot \color{blue}{e^{\log \left(x + 1\right) \cdot \frac{1}{2}}}} \]
    5. lower-*.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot e^{\color{blue}{\log \left(x + 1\right) \cdot \frac{1}{2}}}} \]
    6. lower-log.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot e^{\color{blue}{\log \left(x + 1\right)} \cdot \frac{1}{2}}} \]
    7. lift-+.f6495.3

      \[\leadsto \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}{{x}^{0.5} \cdot e^{\log \color{blue}{\left(x + 1\right)} \cdot 0.5}} \]
  9. Applied rewrites95.3%

    \[\leadsto \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot {x}^{0.5}\right)\right)\right)}{x}}{{x}^{0.5} \cdot \color{blue}{e^{\log \left(x + 1\right) \cdot 0.5}}} \]
  10. Step-by-step derivation
    1. lift-pow.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot {x}^{\frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot e^{\log \left(x + 1\right) \cdot \frac{1}{2}}} \]
    2. pow-to-expN/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot e^{\log x \cdot \frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot e^{\log \left(x + 1\right) \cdot \frac{1}{2}}} \]
    3. lower-exp.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot e^{\log x \cdot \frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot e^{\log \left(x + 1\right) \cdot \frac{1}{2}}} \]
    4. lower-*.f64N/A

      \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{-1}{8}, {\left({x}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{-5}{128}, {\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}}, \mathsf{fma}\left(\frac{1}{16}, {\left({\left({x}^{3}\right)}^{-1}\right)}^{\frac{1}{2}}, \frac{1}{2} \cdot e^{\log x \cdot \frac{1}{2}}\right)\right)\right)}{x}}{{x}^{\frac{1}{2}} \cdot e^{\log \left(x + 1\right) \cdot \frac{1}{2}}} \]
    5. lower-log.f6499.0

      \[\leadsto \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot e^{\log x \cdot 0.5}\right)\right)\right)}{x}}{{x}^{0.5} \cdot e^{\log \left(x + 1\right) \cdot 0.5}} \]
  11. Applied rewrites99.0%

    \[\leadsto \frac{\frac{\mathsf{fma}\left(-0.125, {\left({x}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.0390625, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(0.0625, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5}, 0.5 \cdot e^{\log x \cdot 0.5}\right)\right)\right)}{x}}{{x}^{0.5} \cdot e^{\log \left(x + 1\right) \cdot 0.5}} \]
  12. Add Preprocessing

Alternative 3: 98.8% accurate, N/A× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}\\ \frac{\left(t\_0 \cdot -0.5\right) \cdot \mathsf{fma}\left(0.5, x, 1\right)}{x \cdot x} - \frac{\mathsf{fma}\left({\left({x}^{-1}\right)}^{0.5}, -0.5, \mathsf{fma}\left(t\_0, -0.5, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot 0.375\right)\right)}{x} \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (let* ((t_0 (pow (pow (pow x 5.0) -1.0) 0.5)))
   (-
    (/ (* (* t_0 -0.5) (fma 0.5 x 1.0)) (* x x))
    (/
     (fma
      (pow (pow x -1.0) 0.5)
      -0.5
      (fma t_0 -0.5 (* (pow (pow (pow x 3.0) -1.0) 0.5) 0.375)))
     x))))
double code(double x) {
	double t_0 = pow(pow(pow(x, 5.0), -1.0), 0.5);
	return (((t_0 * -0.5) * fma(0.5, x, 1.0)) / (x * x)) - (fma(pow(pow(x, -1.0), 0.5), -0.5, fma(t_0, -0.5, (pow(pow(pow(x, 3.0), -1.0), 0.5) * 0.375))) / x);
}
function code(x)
	t_0 = ((x ^ 5.0) ^ -1.0) ^ 0.5
	return Float64(Float64(Float64(Float64(t_0 * -0.5) * fma(0.5, x, 1.0)) / Float64(x * x)) - Float64(fma(((x ^ -1.0) ^ 0.5), -0.5, fma(t_0, -0.5, Float64((((x ^ 3.0) ^ -1.0) ^ 0.5) * 0.375))) / x))
end
code[x_] := Block[{t$95$0 = N[Power[N[Power[N[Power[x, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision]}, N[(N[(N[(N[(t$95$0 * -0.5), $MachinePrecision] * N[(0.5 * x + 1.0), $MachinePrecision]), $MachinePrecision] / N[(x * x), $MachinePrecision]), $MachinePrecision] - N[(N[(N[Power[N[Power[x, -1.0], $MachinePrecision], 0.5], $MachinePrecision] * -0.5 + N[(t$95$0 * -0.5 + N[(N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] * 0.375), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / x), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}\\
\frac{\left(t\_0 \cdot -0.5\right) \cdot \mathsf{fma}\left(0.5, x, 1\right)}{x \cdot x} - \frac{\mathsf{fma}\left({\left({x}^{-1}\right)}^{0.5}, -0.5, \mathsf{fma}\left(t\_0, -0.5, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot 0.375\right)\right)}{x}
\end{array}
\end{array}
Derivation
  1. Initial program 42.0%

    \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \]
  2. Add Preprocessing
  3. Taylor expanded in x around inf

    \[\leadsto \color{blue}{\frac{\frac{-1}{2} \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot \left(1 + \frac{1}{2} \cdot x\right)\right) - \left(\frac{-1}{2} \cdot \sqrt{x} + \left(\frac{-1}{2} \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot \left(1 + \frac{1}{4} \cdot x\right)\right) + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)}{{x}^{2}}} \]
  4. Applied rewrites81.5%

    \[\leadsto \color{blue}{\frac{\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5} \cdot -0.5\right) \cdot \mathsf{fma}\left(0.5, x, 1\right)}{x \cdot x} - \frac{\mathsf{fma}\left(-0.5, {x}^{0.5}, \mathsf{fma}\left({\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot -0.5, \mathsf{fma}\left(0.25, x, 1\right), 0.5 \cdot {\left({x}^{-1}\right)}^{0.5}\right)\right)}{x \cdot x}} \]
  5. Taylor expanded in x around inf

    \[\leadsto \frac{\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}} \cdot \frac{-1}{2}\right) \cdot \mathsf{fma}\left(\frac{1}{2}, x, 1\right)}{x \cdot x} - \frac{\frac{-1}{2} \cdot \sqrt{\frac{1}{x}} + \left(\frac{-1}{2} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{{x}^{3}}} + \frac{1}{2} \cdot \sqrt{\frac{1}{{x}^{3}}}\right)\right)}{\color{blue}{x}} \]
  6. Step-by-step derivation
    1. lower-/.f64N/A

      \[\leadsto \frac{\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{\frac{1}{2}} \cdot \frac{-1}{2}\right) \cdot \mathsf{fma}\left(\frac{1}{2}, x, 1\right)}{x \cdot x} - \frac{\frac{-1}{2} \cdot \sqrt{\frac{1}{x}} + \left(\frac{-1}{2} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{{x}^{3}}} + \frac{1}{2} \cdot \sqrt{\frac{1}{{x}^{3}}}\right)\right)}{x} \]
  7. Applied rewrites99.0%

    \[\leadsto \frac{\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5} \cdot -0.5\right) \cdot \mathsf{fma}\left(0.5, x, 1\right)}{x \cdot x} - \frac{\mathsf{fma}\left({\left({x}^{-1}\right)}^{0.5}, -0.5, \mathsf{fma}\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, -0.5, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot 0.375\right)\right)}{\color{blue}{x}} \]
  8. Add Preprocessing

Alternative 4: 98.7% accurate, N/A× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := {\left({x}^{0.5}\right)}^{-1}\\ t_1 := t\_0 \cdot 0.375\\ t_2 := 0.25 + \left(-1 \cdot -0.5\right) \cdot \left(t\_0 \cdot t\_1\right)\\ t_3 := t\_2 \cdot t\_2\\ t_4 := {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}\\ t_5 := {t\_1}^{1}\\ t_6 := \mathsf{fma}\left(t\_5, t\_5, -0.25 \cdot {x}^{-1}\right)\\ \frac{\mathsf{fma}\left(-0.25, t\_4, \mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot \frac{t\_6}{t\_3}, 0.125 \cdot \mathsf{fma}\left(t\_4, \frac{t\_6 \cdot t\_6}{t\_3 \cdot t\_2}, \frac{t\_1}{{x}^{3} \cdot t\_3}\right)\right)\right) - \mathsf{fma}\left(-0.125, t\_0 \cdot {t\_2}^{-1}, \frac{{t\_1}^{3}}{\left(x \cdot x\right) \cdot t\_2}\right)}{x} \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (let* ((t_0 (pow (pow x 0.5) -1.0))
        (t_1 (* t_0 0.375))
        (t_2 (+ 0.25 (* (* -1.0 -0.5) (* t_0 t_1))))
        (t_3 (* t_2 t_2))
        (t_4 (pow (pow (pow x 5.0) -1.0) 0.5))
        (t_5 (pow t_1 1.0))
        (t_6 (fma t_5 t_5 (* -0.25 (pow x -1.0)))))
   (/
    (-
     (fma
      -0.25
      t_4
      (fma
       -0.125
       (* (pow (pow (pow x 3.0) -1.0) 0.5) (/ t_6 t_3))
       (*
        0.125
        (fma t_4 (/ (* t_6 t_6) (* t_3 t_2)) (/ t_1 (* (pow x 3.0) t_3))))))
     (fma -0.125 (* t_0 (pow t_2 -1.0)) (/ (pow t_1 3.0) (* (* x x) t_2))))
    x)))
double code(double x) {
	double t_0 = pow(pow(x, 0.5), -1.0);
	double t_1 = t_0 * 0.375;
	double t_2 = 0.25 + ((-1.0 * -0.5) * (t_0 * t_1));
	double t_3 = t_2 * t_2;
	double t_4 = pow(pow(pow(x, 5.0), -1.0), 0.5);
	double t_5 = pow(t_1, 1.0);
	double t_6 = fma(t_5, t_5, (-0.25 * pow(x, -1.0)));
	return (fma(-0.25, t_4, fma(-0.125, (pow(pow(pow(x, 3.0), -1.0), 0.5) * (t_6 / t_3)), (0.125 * fma(t_4, ((t_6 * t_6) / (t_3 * t_2)), (t_1 / (pow(x, 3.0) * t_3)))))) - fma(-0.125, (t_0 * pow(t_2, -1.0)), (pow(t_1, 3.0) / ((x * x) * t_2)))) / x;
}
function code(x)
	t_0 = (x ^ 0.5) ^ -1.0
	t_1 = Float64(t_0 * 0.375)
	t_2 = Float64(0.25 + Float64(Float64(-1.0 * -0.5) * Float64(t_0 * t_1)))
	t_3 = Float64(t_2 * t_2)
	t_4 = ((x ^ 5.0) ^ -1.0) ^ 0.5
	t_5 = t_1 ^ 1.0
	t_6 = fma(t_5, t_5, Float64(-0.25 * (x ^ -1.0)))
	return Float64(Float64(fma(-0.25, t_4, fma(-0.125, Float64((((x ^ 3.0) ^ -1.0) ^ 0.5) * Float64(t_6 / t_3)), Float64(0.125 * fma(t_4, Float64(Float64(t_6 * t_6) / Float64(t_3 * t_2)), Float64(t_1 / Float64((x ^ 3.0) * t_3)))))) - fma(-0.125, Float64(t_0 * (t_2 ^ -1.0)), Float64((t_1 ^ 3.0) / Float64(Float64(x * x) * t_2)))) / x)
end
code[x_] := Block[{t$95$0 = N[Power[N[Power[x, 0.5], $MachinePrecision], -1.0], $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 * 0.375), $MachinePrecision]}, Block[{t$95$2 = N[(0.25 + N[(N[(-1.0 * -0.5), $MachinePrecision] * N[(t$95$0 * t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(t$95$2 * t$95$2), $MachinePrecision]}, Block[{t$95$4 = N[Power[N[Power[N[Power[x, 5.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision]}, Block[{t$95$5 = N[Power[t$95$1, 1.0], $MachinePrecision]}, Block[{t$95$6 = N[(t$95$5 * t$95$5 + N[(-0.25 * N[Power[x, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(-0.25 * t$95$4 + N[(-0.125 * N[(N[Power[N[Power[N[Power[x, 3.0], $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision] * N[(t$95$6 / t$95$3), $MachinePrecision]), $MachinePrecision] + N[(0.125 * N[(t$95$4 * N[(N[(t$95$6 * t$95$6), $MachinePrecision] / N[(t$95$3 * t$95$2), $MachinePrecision]), $MachinePrecision] + N[(t$95$1 / N[(N[Power[x, 3.0], $MachinePrecision] * t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(-0.125 * N[(t$95$0 * N[Power[t$95$2, -1.0], $MachinePrecision]), $MachinePrecision] + N[(N[Power[t$95$1, 3.0], $MachinePrecision] / N[(N[(x * x), $MachinePrecision] * t$95$2), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / x), $MachinePrecision]]]]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := {\left({x}^{0.5}\right)}^{-1}\\
t_1 := t\_0 \cdot 0.375\\
t_2 := 0.25 + \left(-1 \cdot -0.5\right) \cdot \left(t\_0 \cdot t\_1\right)\\
t_3 := t\_2 \cdot t\_2\\
t_4 := {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}\\
t_5 := {t\_1}^{1}\\
t_6 := \mathsf{fma}\left(t\_5, t\_5, -0.25 \cdot {x}^{-1}\right)\\
\frac{\mathsf{fma}\left(-0.25, t\_4, \mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot \frac{t\_6}{t\_3}, 0.125 \cdot \mathsf{fma}\left(t\_4, \frac{t\_6 \cdot t\_6}{t\_3 \cdot t\_2}, \frac{t\_1}{{x}^{3} \cdot t\_3}\right)\right)\right) - \mathsf{fma}\left(-0.125, t\_0 \cdot {t\_2}^{-1}, \frac{{t\_1}^{3}}{\left(x \cdot x\right) \cdot t\_2}\right)}{x}
\end{array}
\end{array}
Derivation
  1. Initial program 42.0%

    \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \]
  2. Add Preprocessing
  3. Taylor expanded in x around inf

    \[\leadsto \color{blue}{\frac{\frac{-1}{2} \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot \left(1 + \frac{1}{2} \cdot x\right)\right) - \left(\frac{-1}{2} \cdot \sqrt{x} + \left(\frac{-1}{2} \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot \left(1 + \frac{1}{4} \cdot x\right)\right) + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)}{{x}^{2}}} \]
  4. Applied rewrites81.5%

    \[\leadsto \color{blue}{\frac{\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5} \cdot -0.5\right) \cdot \mathsf{fma}\left(0.5, x, 1\right)}{x \cdot x} - \frac{\mathsf{fma}\left(-0.5, {x}^{0.5}, \mathsf{fma}\left({\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot -0.5, \mathsf{fma}\left(0.25, x, 1\right), 0.5 \cdot {\left({x}^{-1}\right)}^{0.5}\right)\right)}{x \cdot x}} \]
  5. Applied rewrites46.5%

    \[\leadsto \frac{\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5} \cdot -0.5\right) \cdot \mathsf{fma}\left(0.5, x, 1\right)}{x \cdot x} - \frac{\frac{{\left(-0.5 \cdot {x}^{0.5}\right)}^{3} + {\left(\mathsf{fma}\left({\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot -0.5, \mathsf{fma}\left(0.25, x, 1\right), {\left({x}^{-1}\right)}^{0.5} \cdot 0.5\right)\right)}^{3}}{\left(-0.5 \cdot {x}^{0.5}\right) \cdot \left(-0.5 \cdot {x}^{0.5}\right) + \left(\mathsf{fma}\left({\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot -0.5, \mathsf{fma}\left(0.25, x, 1\right), {\left({x}^{-1}\right)}^{0.5} \cdot 0.5\right) \cdot \mathsf{fma}\left({\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot -0.5, \mathsf{fma}\left(0.25, x, 1\right), {\left({x}^{-1}\right)}^{0.5} \cdot 0.5\right) - \left(-0.5 \cdot {x}^{0.5}\right) \cdot \mathsf{fma}\left({\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot -0.5, \mathsf{fma}\left(0.25, x, 1\right), {\left({x}^{-1}\right)}^{0.5} \cdot 0.5\right)\right)}}{\color{blue}{x} \cdot x} \]
  6. Taylor expanded in x around inf

    \[\leadsto \frac{\left(\frac{-1}{4} \cdot \sqrt{\frac{1}{{x}^{5}}} + \left(\frac{-1}{8} \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot \frac{{\left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)}^{2} - \frac{1}{4} \cdot \frac{1}{x}}{{\left(\frac{1}{4} - \frac{-1}{2} \cdot \left(\sqrt{\frac{1}{x}} \cdot \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)\right)}^{2}}\right) + \left(\frac{1}{8} \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot \frac{{\left({\left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)}^{2} - \frac{1}{4} \cdot \frac{1}{x}\right)}^{2}}{{\left(\frac{1}{4} - \frac{-1}{2} \cdot \left(\sqrt{\frac{1}{x}} \cdot \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)\right)}^{3}}\right) + \frac{1}{8} \cdot \frac{\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}}{{x}^{3} \cdot {\left(\frac{1}{4} - \frac{-1}{2} \cdot \left(\sqrt{\frac{1}{x}} \cdot \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)\right)}^{2}}\right)\right)\right) - \left(\frac{-1}{8} \cdot \left(\sqrt{\frac{1}{x}} \cdot \frac{1}{\frac{1}{4} - \frac{-1}{2} \cdot \left(\sqrt{\frac{1}{x}} \cdot \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)}\right) + \frac{{\left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)}^{3}}{{x}^{2} \cdot \left(\frac{1}{4} - \frac{-1}{2} \cdot \left(\sqrt{\frac{1}{x}} \cdot \left(\frac{-1}{8} \cdot \sqrt{\frac{1}{x}} + \frac{1}{2} \cdot \sqrt{\frac{1}{x}}\right)\right)\right)}\right)}{\color{blue}{x}} \]
  7. Applied rewrites98.9%

    \[\leadsto \frac{\mathsf{fma}\left(-0.25, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot \frac{\mathsf{fma}\left({\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, {\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, -0.25 \cdot {x}^{-1}\right)}{\left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right) \cdot \left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}, 0.125 \cdot \mathsf{fma}\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \frac{\mathsf{fma}\left({\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, {\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, -0.25 \cdot {x}^{-1}\right) \cdot \mathsf{fma}\left({\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, {\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, -0.25 \cdot {x}^{-1}\right)}{\left(\left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right) \cdot \left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)\right) \cdot \left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}, \frac{{\left({x}^{0.5}\right)}^{-1} \cdot 0.375}{{x}^{3} \cdot \left(\left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right) \cdot \left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)\right)}\right)\right)\right) - \mathsf{fma}\left(-0.125, {\left({x}^{0.5}\right)}^{-1} \cdot {\left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}^{-1}, \frac{{\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{3}}{\left(x \cdot x\right) \cdot \left(0.25 - -0.5 \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}\right)}{\color{blue}{x}} \]
  8. Final simplification98.9%

    \[\leadsto \frac{\mathsf{fma}\left(-0.25, {\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \mathsf{fma}\left(-0.125, {\left({\left({x}^{3}\right)}^{-1}\right)}^{0.5} \cdot \frac{\mathsf{fma}\left({\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, {\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, -0.25 \cdot {x}^{-1}\right)}{\left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right) \cdot \left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}, 0.125 \cdot \mathsf{fma}\left({\left({\left({x}^{5}\right)}^{-1}\right)}^{0.5}, \frac{\mathsf{fma}\left({\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, {\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, -0.25 \cdot {x}^{-1}\right) \cdot \mathsf{fma}\left({\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, {\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{1}, -0.25 \cdot {x}^{-1}\right)}{\left(\left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right) \cdot \left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)\right) \cdot \left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}, \frac{{\left({x}^{0.5}\right)}^{-1} \cdot 0.375}{{x}^{3} \cdot \left(\left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right) \cdot \left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)\right)}\right)\right)\right) - \mathsf{fma}\left(-0.125, {\left({x}^{0.5}\right)}^{-1} \cdot {\left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}^{-1}, \frac{{\left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)}^{3}}{\left(x \cdot x\right) \cdot \left(0.25 + \left(-1 \cdot -0.5\right) \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot \left({\left({x}^{0.5}\right)}^{-1} \cdot 0.375\right)\right)\right)}\right)}{x} \]
  9. Add Preprocessing

Reproduce

?
herbie shell --seed 2025065 
(FPCore (x)
  :name "2isqrt (example 3.6)"
  :precision binary64
  :pre (and (> x 1.0) (< x 1e+308))

  :alt
  (! :herbie-platform c (- (pow x -1/2) (pow (+ x 1) -1/2)))

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