Average Error: 2.4 → 0.4
Time: 1.6m
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{\frac{i}{2}}{i \cdot 2 + 1.0} \cdot \frac{\frac{i}{2}}{i \cdot 2 - 1.0}\]
\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{\frac{i}{2}}{i \cdot 2 + 1.0} \cdot \frac{\frac{i}{2}}{i \cdot 2 - 1.0}
double f(double i) {
        double r2452353 = i;
        double r2452354 = r2452353 * r2452353;
        double r2452355 = r2452354 * r2452354;
        double r2452356 = 2.0;
        double r2452357 = /* ERROR: no posit support in C */;
        double r2452358 = r2452357 * r2452353;
        double r2452359 = r2452358 * r2452358;
        double r2452360 = r2452355 / r2452359;
        double r2452361 = 1.0;
        double r2452362 = /* ERROR: no posit support in C */;
        double r2452363 = r2452359 - r2452362;
        double r2452364 = r2452360 / r2452363;
        return r2452364;
}
↓
double f(double i) {
        double r2452365 = i;
        double r2452366 = 2.0;
        double r2452367 = r2452365 / r2452366;
        double r2452368 = r2452365 * r2452366;
        double r2452369 = 1.0;
        double r2452370 = r2452368 + r2452369;
        double r2452371 = r2452367 / r2452370;
        double r2452372 = r2452368 - r2452369;
        double r2452373 = r2452367 / r2452372;
        double r2452374 = r2452371 * r2452373;
        return r2452374;
}

Error

Bits error versus i

Derivation

  1. Initial program 2.4

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

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

  4. Applied associate-*r/1.1

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

  6. Applied /p16-rgt-identity-expand1.1

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

  7. Applied associate-/l/1.1

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

  8. Simplified1.1

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

  10. Applied associate-/r*0.8

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

  12. Applied p16-*-un-lft-identity0.8

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

  13. Applied difference-of-squares0.8

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

  14. Applied p16-times-frac0.8

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

  15. Applied p16-times-frac0.4

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

  16. Final simplification0.4

    \[\leadsto \frac{\frac{i}{2}}{i \cdot 2 + 1.0} \cdot \frac{\frac{i}{2}}{i \cdot 2 - 1.0}\]

Reproduce

herbie shell --seed 2019162 +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))))