2frac (problem 3.3.1)

Average Error: 14.4 → 0.1

Time: 3.0s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r25179 = 1.0;
        double r25180 = x;
        double r25181 = r25180 + r25179;
        double r25182 = r25179 / r25181;
        double r25183 = r25179 / r25180;
        double r25184 = r25182 - r25183;
        return r25184;
}

↓

double f(double x) {
        double r25185 = 0.0;
        double r25186 = 1.0;
        double r25187 = sqrt(r25186);
        double r25188 = r25185 + r25187;
        double r25189 = x;
        double r25190 = r25186 / r25189;
        double r25191 = r25188 * r25190;
        double r25192 = r25189 + r25186;
        double r25193 = sqrt(r25185);
        double r25194 = r25193 - r25187;
        double r25195 = r25192 / r25194;
        double r25196 = r25191 / r25195;
        return r25196;
}

Error

Bits error versus x

Derivation

1. Initial program 14.4

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

3. Applied frac-sub 13.7

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

4. Simplified 13.7

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

6. Applied associate-/r* 13.7

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

7. Simplified 0.1

   \[\leadsto \frac{\color{blue}{\frac{1}{\frac{x + 1}{0 - 1}}}}{x}\]
8. Using strategy rm

9. Applied div-inv 0.1

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

10. Applied associate-/l* 0.4

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

11. Simplified 0.4

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

13. Applied add-sqr-sqrt 0.4

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

14. Applied add-sqr-sqrt 0.4

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

15. Applied difference-of-squares 0.4

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

16. Applied times-frac 0.4

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

17. Applied associate-/r* 0.1

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

18. Simplified 0.1

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

19. Final simplification 0.1

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

Reproduce

herbie shell --seed 2020057 +o rules:numerics
(FPCore (x)
  :name "2frac (problem 3.3.1)"
  :precision binary64
  (- (/ 1 (+ x 1)) (/ 1 x)))