2isqrt (example 3.6)

Average Error: 19.9 → 1.5

Time: 22.2s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le 11789.29797293433:\\ \;\;\;\;{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}\]

C

double f(double x) {
        double r2221106 = 1.0;
        double r2221107 = x;
        double r2221108 = sqrt(r2221107);
        double r2221109 = r2221106 / r2221108;
        double r2221110 = r2221107 + r2221106;
        double r2221111 = sqrt(r2221110);
        double r2221112 = r2221106 / r2221111;
        double r2221113 = r2221109 - r2221112;
        return r2221113;
}

↓

double f(double x) {
        double r2221114 = x;
        double r2221115 = 11789.29797293433;
        bool r2221116 = r2221114 <= r2221115;
        double r2221117 = -0.5;
        double r2221118 = pow(r2221114, r2221117);
        double r2221119 = 1.0;
        double r2221120 = r2221119 + r2221114;
        double r2221121 = pow(r2221120, r2221117);
        double r2221122 = r2221118 - r2221121;
        double r2221123 = 0.3125;
        double r2221124 = r2221114 * r2221114;
        double r2221125 = r2221123 / r2221124;
        double r2221126 = log(r2221114);
        double r2221127 = r2221126 * r2221117;
        double r2221128 = exp(r2221127);
        double r2221129 = r2221128 / r2221114;
        double r2221130 = 0.5;
        double r2221131 = -0.375;
        double r2221132 = r2221128 / r2221124;
        double r2221133 = r2221131 * r2221132;
        double r2221134 = fma(r2221130, r2221129, r2221133);
        double r2221135 = fma(r2221125, r2221129, r2221134);
        double r2221136 = r2221116 ? r2221122 : r2221135;
        return r2221136;
}

Error

Bits error versus x

Target

Original	19.9
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 < 11789.29797293433

   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 pow1 0.1

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

   9. Applied sqrt-pow1 0.1

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

   10. Applied pow-flip 0.1

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

   11. Simplified 0.1

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

   if 11789.29797293433 < x

   1. Initial program 39.6

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

   3. Applied pow1 39.6

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

   4. Applied sqrt-pow1 39.6

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

   5. Applied pow-flip 44.6

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

   6. Simplified 44.6

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

   8. Applied pow1 44.6

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

   9. Applied sqrt-pow1 44.6

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

   10. Applied pow-flip 39.6

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

   11. Simplified 39.6

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

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

   13. Simplified 2.8

       \[\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 simplification 1.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 11789.29797293433:\\ \;\;\;\;{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 2019152 +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)))))