2isqrt (example 3.6)

Average Error: 19.3 → 0.6

Time: 27.0s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r3085116 = 1.0;
        double r3085117 = x;
        double r3085118 = sqrt(r3085117);
        double r3085119 = r3085116 / r3085118;
        double r3085120 = r3085117 + r3085116;
        double r3085121 = sqrt(r3085120);
        double r3085122 = r3085116 / r3085121;
        double r3085123 = r3085119 - r3085122;
        return r3085123;
}

↓

double f(double x) {
        double r3085124 = 1.0;
        double r3085125 = x;
        double r3085126 = r3085125 + r3085124;
        double r3085127 = sqrt(r3085126);
        double r3085128 = sqrt(r3085125);
        double r3085129 = r3085127 + r3085128;
        double r3085130 = cbrt(r3085129);
        double r3085131 = r3085130 * r3085130;
        double r3085132 = r3085124 / r3085131;
        double r3085133 = r3085132 / r3085128;
        double r3085134 = r3085125 - r3085125;
        double r3085135 = r3085124 + r3085134;
        double r3085136 = r3085135 / r3085130;
        double r3085137 = r3085136 / r3085127;
        double r3085138 = r3085133 * r3085137;
        return r3085138;
}

Error

Bits error versus x

Target

Original	19.3
Target	0.6
Herbie	0.6

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

Derivation

1. Initial program 19.3

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

3. Applied frac-sub 19.3

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

4. Simplified 19.3

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

6. Applied flip-- 19.1

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

7. Simplified 0.4

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

9. Applied add-cube-cbrt 0.6

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

10. Applied *-un-lft-identity 0.6

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

11. Applied *-un-lft-identity 0.6

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

12. Applied distribute-lft-out 0.6

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

13. Applied times-frac 0.6

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

14. Applied times-frac 0.6

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

15. Final simplification 0.6

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

Reproduce

herbie shell --seed 2019133 +o rules:numerics
(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)))))