2isqrt (example 3.6)

Average Error: 19.4 → 0.3

Time: 20.3s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r6017062 = 1.0;
        double r6017063 = x;
        double r6017064 = sqrt(r6017063);
        double r6017065 = r6017062 / r6017064;
        double r6017066 = r6017063 + r6017062;
        double r6017067 = sqrt(r6017066);
        double r6017068 = r6017062 / r6017067;
        double r6017069 = r6017065 - r6017068;
        return r6017069;
}

↓

double f(double x) {
        double r6017070 = 1.0;
        double r6017071 = x;
        double r6017072 = sqrt(r6017071);
        double r6017073 = r6017070 / r6017072;
        double r6017074 = r6017071 + r6017070;
        double r6017075 = sqrt(r6017074);
        double r6017076 = r6017070 / r6017075;
        double r6017077 = r6017073 + r6017076;
        double r6017078 = r6017070 / r6017077;
        double r6017079 = r6017078 / r6017071;
        double r6017080 = r6017070 / r6017074;
        double r6017081 = r6017079 * r6017080;
        return r6017081;
}

Error

Bits error versus x

Target

Original	19.4
Target	0.7
Herbie	0.3

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

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

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

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

   \[\leadsto \frac{\frac{\color{blue}{\left(x + 1\right) - x}}{\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.0

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

10. Taylor expanded around 0 5.4

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

12. Applied *-un-lft-identity 5.4

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

13. Applied add-sqr-sqrt 5.4

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

14. Applied times-frac 5.0

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

15. Applied times-frac 0.4

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

16. Simplified 0.4

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

17. Simplified 0.3

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

18. Final simplification 0.3

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

Reproduce

herbie shell --seed 2019164 
(FPCore (x)
  :name "2isqrt (example 3.6)"

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

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