2isqrt (example 3.6)

Average Error: 19.9 → 17.3

Time: 45.6s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le 83896.23902101439307443797588348388671875:\\ \;\;\;\;\mathsf{fma}\left(-\frac{1}{\sqrt[3]{\sqrt{1 + x}}}, \frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}}, \frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt[3]{\sqrt{1 + x}}}\right) + \mathsf{fma}\left(1, \frac{1}{\sqrt{x}}, \frac{1}{\sqrt[3]{\sqrt{1 + x}}} \cdot \frac{-1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{fma}\left(\frac{1}{x}, 0.25, \left(\left(1 + \frac{0.25}{x}\right) - 1\right) - \mathsf{fma}\left(0.15625, \frac{1}{x \cdot x}, \frac{0.09375}{x \cdot x}\right)\right)}{\sqrt{\sqrt{x}} \cdot \sqrt{\sqrt{1 + x}}} + \left(\left(-\frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}} \cdot \frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}}\right) + \frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}} \cdot \frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}}\right)\\ \end{array}\]

C

double f(double x) {
        double r5657055 = 1.0;
        double r5657056 = x;
        double r5657057 = sqrt(r5657056);
        double r5657058 = r5657055 / r5657057;
        double r5657059 = r5657056 + r5657055;
        double r5657060 = sqrt(r5657059);
        double r5657061 = r5657055 / r5657060;
        double r5657062 = r5657058 - r5657061;
        return r5657062;
}

↓

double f(double x) {
        double r5657063 = x;
        double r5657064 = 83896.2390210144;
        bool r5657065 = r5657063 <= r5657064;
        double r5657066 = 1.0;
        double r5657067 = r5657066 + r5657063;
        double r5657068 = sqrt(r5657067);
        double r5657069 = cbrt(r5657068);
        double r5657070 = r5657066 / r5657069;
        double r5657071 = -r5657070;
        double r5657072 = 1.0;
        double r5657073 = r5657069 * r5657069;
        double r5657074 = r5657072 / r5657073;
        double r5657075 = r5657074 * r5657070;
        double r5657076 = fma(r5657071, r5657074, r5657075);
        double r5657077 = sqrt(r5657063);
        double r5657078 = r5657072 / r5657077;
        double r5657079 = -1.0;
        double r5657080 = r5657079 / r5657073;
        double r5657081 = r5657070 * r5657080;
        double r5657082 = fma(r5657066, r5657078, r5657081);
        double r5657083 = r5657076 + r5657082;
        double r5657084 = r5657066 / r5657063;
        double r5657085 = 0.25;
        double r5657086 = r5657085 / r5657063;
        double r5657087 = r5657066 + r5657086;
        double r5657088 = r5657087 - r5657066;
        double r5657089 = 0.15625;
        double r5657090 = r5657063 * r5657063;
        double r5657091 = r5657066 / r5657090;
        double r5657092 = 0.09375;
        double r5657093 = r5657092 / r5657090;
        double r5657094 = fma(r5657089, r5657091, r5657093);
        double r5657095 = r5657088 - r5657094;
        double r5657096 = fma(r5657084, r5657085, r5657095);
        double r5657097 = sqrt(r5657077);
        double r5657098 = sqrt(r5657068);
        double r5657099 = r5657097 * r5657098;
        double r5657100 = r5657096 / r5657099;
        double r5657101 = sqrt(r5657066);
        double r5657102 = r5657101 / r5657098;
        double r5657103 = r5657102 * r5657102;
        double r5657104 = -r5657103;
        double r5657105 = r5657104 + r5657103;
        double r5657106 = r5657100 + r5657105;
        double r5657107 = r5657065 ? r5657083 : r5657106;
        return r5657107;
}

Error

Bits error versus x

Target

Original	19.9
Target	0.6
Herbie	17.3

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

Derivation

1. Split input into 2 regimes

2. if x < 83896.2390210144

   1. Initial program 0.4

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

   3. Applied add-cube-cbrt 0.4

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

   4. Applied *-un-lft-identity 0.4

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

   5. Applied times-frac 0.4

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

   6. Applied div-inv 0.4

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

   7. Applied prod-diff 0.4

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

   if 83896.2390210144 < x

   1. Initial program 39.8

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

   3. Applied add-sqr-sqrt 39.8

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

   4. Applied sqrt-prod 48.5

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

   5. Applied add-sqr-sqrt 48.5

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

   6. Applied times-frac 52.9

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

   7. Applied add-sqr-sqrt 52.9

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

   8. Applied sqrt-prod 50.9

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

   9. Applied *-un-lft-identity 50.9

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

   10. Applied times-frac 39.9

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

   11. Applied prod-diff 39.9

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

   12. Simplified 60.1

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

   13. Simplified 45.0

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

   15. Applied associate-*r/ 39.9

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

   16. Applied frac-sub 39.9

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

   17. Taylor expanded around inf 39.9

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

   18. Simplified 34.5

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

4. Final simplification 17.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 83896.23902101439307443797588348388671875:\\ \;\;\;\;\mathsf{fma}\left(-\frac{1}{\sqrt[3]{\sqrt{1 + x}}}, \frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}}, \frac{1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}} \cdot \frac{1}{\sqrt[3]{\sqrt{1 + x}}}\right) + \mathsf{fma}\left(1, \frac{1}{\sqrt{x}}, \frac{1}{\sqrt[3]{\sqrt{1 + x}}} \cdot \frac{-1}{\sqrt[3]{\sqrt{1 + x}} \cdot \sqrt[3]{\sqrt{1 + x}}}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{fma}\left(\frac{1}{x}, 0.25, \left(\left(1 + \frac{0.25}{x}\right) - 1\right) - \mathsf{fma}\left(0.15625, \frac{1}{x \cdot x}, \frac{0.09375}{x \cdot x}\right)\right)}{\sqrt{\sqrt{x}} \cdot \sqrt{\sqrt{1 + x}}} + \left(\left(-\frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}} \cdot \frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}}\right) + \frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}} \cdot \frac{\sqrt{1}}{\sqrt{\sqrt{1 + x}}}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019168 +o rules:numerics
(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)))))