2isqrt (example 3.6)

Average Error: 19.8 → 10.7

Time: 18.5s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le 8754.1150934849247:\\ \;\;\;\;\frac{\left(\sqrt{\frac{1}{\sqrt{x}}} + \sqrt{\frac{1}{\sqrt{x + 1}}}\right) \cdot \left(\sqrt{\frac{1}{\sqrt{x}}} \cdot \frac{1}{\sqrt{x}} - {\left(\sqrt{\frac{1}{\sqrt{x + 1}}}\right)}^{3}\right)}{\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}} + \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}} + \sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)}\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(0.3125 \cdot \sqrt{\frac{1}{{x}^{7}}} + 0.5 \cdot \sqrt{\frac{1}{{x}^{3}}}\right) - 1 \cdot \left(0.375 \cdot \sqrt{\frac{1}{{x}^{5}}}\right)\\ \end{array}\]

C

double f(double x) {
        double r120889 = 1.0;
        double r120890 = x;
        double r120891 = sqrt(r120890);
        double r120892 = r120889 / r120891;
        double r120893 = r120890 + r120889;
        double r120894 = sqrt(r120893);
        double r120895 = r120889 / r120894;
        double r120896 = r120892 - r120895;
        return r120896;
}

↓

double f(double x) {
        double r120897 = x;
        double r120898 = 8754.115093484925;
        bool r120899 = r120897 <= r120898;
        double r120900 = 1.0;
        double r120901 = sqrt(r120897);
        double r120902 = r120900 / r120901;
        double r120903 = sqrt(r120902);
        double r120904 = r120897 + r120900;
        double r120905 = sqrt(r120904);
        double r120906 = r120900 / r120905;
        double r120907 = sqrt(r120906);
        double r120908 = r120903 + r120907;
        double r120909 = r120903 * r120902;
        double r120910 = 3.0;
        double r120911 = pow(r120907, r120910);
        double r120912 = r120909 - r120911;
        double r120913 = r120908 * r120912;
        double r120914 = r120903 * r120903;
        double r120915 = r120907 * r120907;
        double r120916 = r120903 * r120907;
        double r120917 = r120915 + r120916;
        double r120918 = r120914 + r120917;
        double r120919 = r120913 / r120918;
        double r120920 = 0.3125;
        double r120921 = 1.0;
        double r120922 = 7.0;
        double r120923 = pow(r120897, r120922);
        double r120924 = r120921 / r120923;
        double r120925 = sqrt(r120924);
        double r120926 = r120920 * r120925;
        double r120927 = 0.5;
        double r120928 = pow(r120897, r120910);
        double r120929 = r120921 / r120928;
        double r120930 = sqrt(r120929);
        double r120931 = r120927 * r120930;
        double r120932 = r120926 + r120931;
        double r120933 = r120900 * r120932;
        double r120934 = 0.375;
        double r120935 = 5.0;
        double r120936 = pow(r120897, r120935);
        double r120937 = r120921 / r120936;
        double r120938 = sqrt(r120937);
        double r120939 = r120934 * r120938;
        double r120940 = r120900 * r120939;
        double r120941 = r120933 - r120940;
        double r120942 = r120899 ? r120919 : r120941;
        return r120942;
}

Error

Bits error versus x

Target

Original	19.8
Target	0.8
Herbie	10.7

\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

1. Split input into 2 regimes

2. if x < 8754.115093484925

   1. Initial program 0.4

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

   3. Applied add-exp-log 4.8

      \[\leadsto \color{blue}{e^{\log \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)}}\]
   4. Using strategy rm

   5. Applied add-sqr-sqrt 4.8

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

   6. Applied add-sqr-sqrt 4.8

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

   7. Applied difference-of-squares 4.8

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

   8. Applied log-prod 4.8

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

   9. Applied exp-sum 4.7

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

   10. Simplified 3.9

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

   11. Simplified 0.7

       \[\leadsto \left(\sqrt{\frac{1}{\sqrt{x}}} + \sqrt{\frac{1}{\sqrt{x + 1}}}\right) \cdot \color{blue}{\left(\sqrt{\frac{1}{\sqrt{x}}} - \sqrt{\frac{1}{\sqrt{x + 1}}}\right)}\]
   12. Using strategy rm

   13. Applied flip3-- 0.7

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

   14. Applied associate-*r/ 0.7

       \[\leadsto \color{blue}{\frac{\left(\sqrt{\frac{1}{\sqrt{x}}} + \sqrt{\frac{1}{\sqrt{x + 1}}}\right) \cdot \left({\left(\sqrt{\frac{1}{\sqrt{x}}}\right)}^{3} - {\left(\sqrt{\frac{1}{\sqrt{x + 1}}}\right)}^{3}\right)}{\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}} + \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}} + \sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)}}\]
   15. Using strategy rm

   16. Applied cube-mult 0.7

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

   17. Simplified 0.6

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

   if 8754.115093484925 < x

   1. Initial program 39.4

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

   3. Applied add-exp-log 39.4

      \[\leadsto \color{blue}{e^{\log \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)}}\]
   4. Using strategy rm

   5. Applied add-sqr-sqrt 49.6

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

   6. Applied add-sqr-sqrt 39.4

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

   7. Applied difference-of-squares 39.4

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

   8. Applied log-prod 39.4

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

   9. Applied exp-sum 39.4

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

   10. Simplified 39.4

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

   11. Simplified 39.4

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

   12. Taylor expanded around inf 20.9

       \[\leadsto \color{blue}{\left(0.3125 \cdot \left(\sqrt{\frac{1}{{x}^{7}}} \cdot {\left(\sqrt{1}\right)}^{2}\right) + 0.5 \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)\right) - 0.375 \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)}\]

   13. Simplified 20.9

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

4. Final simplification 10.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 8754.1150934849247:\\ \;\;\;\;\frac{\left(\sqrt{\frac{1}{\sqrt{x}}} + \sqrt{\frac{1}{\sqrt{x + 1}}}\right) \cdot \left(\sqrt{\frac{1}{\sqrt{x}}} \cdot \frac{1}{\sqrt{x}} - {\left(\sqrt{\frac{1}{\sqrt{x + 1}}}\right)}^{3}\right)}{\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}} + \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}} + \sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)}\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(0.3125 \cdot \sqrt{\frac{1}{{x}^{7}}} + 0.5 \cdot \sqrt{\frac{1}{{x}^{3}}}\right) - 1 \cdot \left(0.375 \cdot \sqrt{\frac{1}{{x}^{5}}}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019199 
(FPCore (x)
  :name "2isqrt (example 3.6)"

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

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