2isqrt (example 3.6)

Average Error: 19.9 → 0.4

Time: 7.1s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r165469 = 1.0;
        double r165470 = x;
        double r165471 = sqrt(r165470);
        double r165472 = r165469 / r165471;
        double r165473 = r165470 + r165469;
        double r165474 = sqrt(r165473);
        double r165475 = r165469 / r165474;
        double r165476 = r165472 - r165475;
        return r165476;
}

↓

double f(double x) {
        double r165477 = 1.0;
        double r165478 = r165477 * r165477;
        double r165479 = x;
        double r165480 = r165479 + r165477;
        double r165481 = r165478 / r165480;
        double r165482 = r165481 / r165477;
        double r165483 = r165477 / r165479;
        double r165484 = 1.0;
        double r165485 = sqrt(r165479);
        double r165486 = r165484 / r165485;
        double r165487 = sqrt(r165480);
        double r165488 = r165484 / r165487;
        double r165489 = r165486 + r165488;
        double r165490 = r165483 / r165489;
        double r165491 = r165482 * r165490;
        return r165491;
}

Error

Bits error versus x

Target

Original	19.9
Target	0.6
Herbie	0.4

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

Derivation

1. Initial program 19.9

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

3. Applied flip-- 19.9

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

5. Applied frac-times 24.8

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

6. Applied frac-times 20.0

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

7. Applied frac-sub 19.8

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

8. Simplified 19.3

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

9. Simplified 19.3

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

10. Taylor expanded around 0 5.6

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

12. Applied div-inv 5.6

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

13. Applied div-inv 5.6

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

14. Applied distribute-lft-out 5.6

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

15. Applied times-frac 5.2

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

16. Applied times-frac 0.4

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

17. Final simplification 0.4

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

Reproduce

herbie shell --seed 2020065 +o rules:numerics
(FPCore (x)
  :name "2isqrt (example 3.6)"
  :precision binary64

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

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