2isqrt (example 3.6)

Average Error: 19.4 → 0.4

Time: 6.9s

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 r144318 = 1.0;
        double r144319 = x;
        double r144320 = sqrt(r144319);
        double r144321 = r144318 / r144320;
        double r144322 = r144319 + r144318;
        double r144323 = sqrt(r144322);
        double r144324 = r144318 / r144323;
        double r144325 = r144321 - r144324;
        return r144325;
}

↓

double f(double x) {
        double r144326 = 1.0;
        double r144327 = r144326 * r144326;
        double r144328 = x;
        double r144329 = r144328 + r144326;
        double r144330 = r144327 / r144329;
        double r144331 = r144330 / r144326;
        double r144332 = r144326 / r144328;
        double r144333 = 1.0;
        double r144334 = sqrt(r144328);
        double r144335 = r144333 / r144334;
        double r144336 = sqrt(r144329);
        double r144337 = r144333 / r144336;
        double r144338 = r144335 + r144337;
        double r144339 = r144332 / r144338;
        double r144340 = r144331 * r144339;
        return r144340;
}

Error

Bits error versus x

Target

Original	19.4
Target	0.7
Herbie	0.4

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

Derivation

1. Initial program 19.4

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

3. Applied flip-- 19.4

   \[\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.6

   \[\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 19.5

   \[\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.2

   \[\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 18.9

   \[\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 18.8

   \[\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.8

    \[\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.8

    \[\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.8

    \[\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.8

    \[\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.4

    \[\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 2020020 +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)))))