Average Error: 2.3 → 0.4
Time: 30.6s
Precision: 64
\[i \gt \left(0\right)\]
\[\frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right)}\right)}{\left(\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right) - \left(1.0\right)\right)}\]
↓
\[\frac{i}{i \cdot 2 + 1.0} \cdot \frac{\frac{i}{\left(i \cdot 2 - 1.0\right) \cdot 2}}{2}\]
\frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right)}\right)}{\left(\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right) - \left(1.0\right)\right)}
↓
\frac{i}{i \cdot 2 + 1.0} \cdot \frac{\frac{i}{\left(i \cdot 2 - 1.0\right) \cdot 2}}{2}
double f(double i) {
        double r1428451 = i;
        double r1428452 = r1428451 * r1428451;
        double r1428453 = r1428452 * r1428452;
        double r1428454 = 2.0;
        double r1428455 = /* ERROR: no posit support in C */;
        double r1428456 = r1428455 * r1428451;
        double r1428457 = r1428456 * r1428456;
        double r1428458 = r1428453 / r1428457;
        double r1428459 = 1.0;
        double r1428460 = /* ERROR: no posit support in C */;
        double r1428461 = r1428457 - r1428460;
        double r1428462 = r1428458 / r1428461;
        return r1428462;
}
↓
double f(double i) {
        double r1428463 = i;
        double r1428464 = 2.0;
        double r1428465 = r1428463 * r1428464;
        double r1428466 = 1.0;
        double r1428467 = r1428465 + r1428466;
        double r1428468 = r1428463 / r1428467;
        double r1428469 = r1428465 - r1428466;
        double r1428470 = r1428469 * r1428464;
        double r1428471 = r1428463 / r1428470;
        double r1428472 = r1428471 / r1428464;
        double r1428473 = r1428468 * r1428472;
        return r1428473;
}

Error

Bits error versus i

Derivation

  1. Initial program 2.3

    \[\frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right)}\right)}{\left(\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right) - \left(1.0\right)\right)}\]
  2. Using strategy rm

  3. Applied p16-*-un-lft-identity2.3

    \[\leadsto \frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right)}\right)}{\left(\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right) - \color{blue}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}\right)}\]

  4. Applied difference-of-squares2.3

    \[\leadsto \frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right)}\right)}{\color{blue}{\left(\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right) \cdot \left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)\right)}}\]

  5. Applied p16-times-frac1.0

    \[\leadsto \frac{\color{blue}{\left(\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right) \cdot \left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}}{\left(\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right) \cdot \left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)\right)}\]

  6. Applied p16-times-frac1.0

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)}\]
  7. Using strategy rm

  8. Applied *p16-rgt-identity-expand1.0

    \[\leadsto \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\color{blue}{\left(\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right) \cdot \left(1.0\right)\right)}}\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\]

  9. Applied p16-times-frac0.7

    \[\leadsto \left(\frac{\color{blue}{\left(\left(\frac{i}{\left(2\right)}\right) \cdot \left(\frac{i}{i}\right)\right)}}{\left(\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right) \cdot \left(1.0\right)\right)}\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\]

  10. Applied p16-times-frac0.7

    \[\leadsto \color{blue}{\left(\left(\frac{\left(\frac{i}{\left(2\right)}\right)}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right)}\right) \cdot \left(\frac{\left(\frac{i}{i}\right)}{\left(1.0\right)}\right)\right)} \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\]

  11. Simplified0.7

    \[\leadsto \left(\color{blue}{\left(\frac{i}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) \cdot \left(2\right)\right)}{\left(2\right)}\right)}\right)} \cdot \left(\frac{\left(\frac{i}{i}\right)}{\left(1.0\right)}\right)\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\]

  12. Simplified0.7

    \[\leadsto \left(\left(\frac{i}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) \cdot \left(2\right)\right)}{\left(2\right)}\right)}\right) \cdot \color{blue}{\left(1.0\right)}\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\]
  13. Using strategy rm

  14. Applied associate-*l/0.7

    \[\leadsto \color{blue}{\left(\frac{\left(i \cdot \left(1.0\right)\right)}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) \cdot \left(2\right)\right)}{\left(2\right)}\right)}\right)} \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\]

  15. Applied associate-*l/0.7

    \[\leadsto \color{blue}{\frac{\left(\left(i \cdot \left(1.0\right)\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)\right)}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) \cdot \left(2\right)\right)}{\left(2\right)}\right)}}\]

  16. Simplified0.5

    \[\leadsto \frac{\color{blue}{\left(i \cdot \left(\frac{i}{\left(\left(\left(i \cdot \left(2\right)\right) - \left(1.0\right)\right) \cdot \left(2\right)\right)}\right)\right)}}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) \cdot \left(2\right)\right)}{\left(2\right)}\right)}\]
  17. Using strategy rm

  18. Applied distribute-lft1-in0.5

    \[\leadsto \frac{\left(i \cdot \left(\frac{i}{\left(\left(\left(i \cdot \left(2\right)\right) - \left(1.0\right)\right) \cdot \left(2\right)\right)}\right)\right)}{\color{blue}{\left(\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right) \cdot \left(2\right)\right)}}\]

  19. Applied p16-times-frac0.4

    \[\leadsto \color{blue}{\left(\frac{i}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(1.0\right)}\right)}\right) \cdot \left(\frac{\left(\frac{i}{\left(\left(\left(i \cdot \left(2\right)\right) - \left(1.0\right)\right) \cdot \left(2\right)\right)}\right)}{\left(2\right)}\right)}\]

  20. Simplified0.4

    \[\leadsto \color{blue}{\left(\frac{i}{\left(\frac{\left(i \cdot \left(2\right)\right)}{\left(1.0\right)}\right)}\right)} \cdot \left(\frac{\left(\frac{i}{\left(\left(\left(i \cdot \left(2\right)\right) - \left(1.0\right)\right) \cdot \left(2\right)\right)}\right)}{\left(2\right)}\right)\]

  21. Final simplification0.4

    \[\leadsto \frac{i}{i \cdot 2 + 1.0} \cdot \frac{\frac{i}{\left(i \cdot 2 - 1.0\right) \cdot 2}}{2}\]

Reproduce

herbie shell --seed 2019153 +o rules:numerics
(FPCore (i)
  :name "Octave 3.8, jcobi/4, as called"
  :pre (and (>.p16 i (real->posit16 0)))
  (/.p16 (/.p16 (*.p16 (*.p16 i i) (*.p16 i i)) (*.p16 (*.p16 (real->posit16 2) i) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (*.p16 (real->posit16 2) i) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))