2sqrt (example 3.1)

Average Error: 29.6 → 0.2

Time: 4.6s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r127242 = x;
        double r127243 = 1.0;
        double r127244 = r127242 + r127243;
        double r127245 = sqrt(r127244);
        double r127246 = sqrt(r127242);
        double r127247 = r127245 - r127246;
        return r127247;
}

↓

double f(double x) {
        double r127248 = 1.0;
        double r127249 = x;
        double r127250 = r127249 + r127248;
        double r127251 = sqrt(r127250);
        double r127252 = sqrt(r127249);
        double r127253 = r127251 + r127252;
        double r127254 = -r127253;
        double r127255 = r127248 / r127254;
        double r127256 = -r127255;
        return r127256;
}

Error

Bits error versus x

Target

Original	29.6
Target	0.2
Herbie	0.2

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

Derivation

1. Initial program 29.6

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

3. Applied flip-- 29.4

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

4. Simplified 0.2

   \[\leadsto \frac{\color{blue}{1 + 0}}{\sqrt{x + 1} + \sqrt{x}}\]
5. Using strategy rm

6. Applied add-sqr-sqrt 0.2

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

7. Applied sqrt-prod 0.3

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

8. Applied fma-def 0.2

   \[\leadsto \frac{1 + 0}{\color{blue}{\mathsf{fma}\left(\sqrt{\sqrt{x + 1}}, \sqrt{\sqrt{x + 1}}, \sqrt{x}\right)}}\]
9. Using strategy rm

10. Applied add-sqr-sqrt 0.2

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

11. Applied sqrt-prod 0.2

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

12. Applied sqrt-prod 0.3

    \[\leadsto \frac{1 + 0}{\mathsf{fma}\left(\color{blue}{\sqrt{\sqrt{\sqrt{x + 1}}} \cdot \sqrt{\sqrt{\sqrt{x + 1}}}}, \sqrt{\sqrt{x + 1}}, \sqrt{x}\right)}\]
13. Using strategy rm

14. Applied frac-2neg 0.3

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

15. Simplified 0.3

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

16. Simplified 0.2

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

17. Final simplification 0.2

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

Reproduce

herbie shell --seed 2020059 +o rules:numerics
(FPCore (x)
  :name "2sqrt (example 3.1)"
  :precision binary64

  :herbie-target
  (/ 1 (+ (sqrt (+ x 1)) (sqrt x)))

  (- (sqrt (+ x 1)) (sqrt x)))