Main:bigenough3 from C

Average Error: 30.1 → 0.2

Time: 9.9s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

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

C

double f(double x) {
        double r583425 = x;
        double r583426 = 1.0;
        double r583427 = r583425 + r583426;
        double r583428 = sqrt(r583427);
        double r583429 = sqrt(r583425);
        double r583430 = r583428 - r583429;
        return r583430;
}

↓

double f(double x) {
        double r583431 = 1.0;
        double r583432 = r583431 * r583431;
        double r583433 = x;
        double r583434 = r583433 + r583431;
        double r583435 = sqrt(r583434);
        double r583436 = sqrt(r583433);
        double r583437 = r583435 * r583436;
        double r583438 = r583434 + r583437;
        double r583439 = r583437 + r583433;
        double r583440 = r583438 + r583439;
        double r583441 = r583432 / r583440;
        double r583442 = sqrt(r583441);
        return r583442;
}

Error

Bits error versus x

Target

Original	30.1
Target	0.2
Herbie	0.2

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

Derivation

1. Initial program 30.1

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

3. Applied flip-- 29.8

   \[\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}}{\sqrt{x + 1} + \sqrt{x}}\]
5. Using strategy rm

6. Applied add-sqr-sqrt 0.3

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

8. Applied sqrt-unprod 0.2

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

9. Simplified 0.2

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

11. Applied distribute-lft-in 0.2

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

12. Simplified 0.2

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

13. Simplified 0.2

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

14. Final simplification 0.2

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

Reproduce

herbie shell --seed 2020043 
(FPCore (x)
  :name "Main:bigenough3 from C"
  :precision binary64

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

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