Average Error: 2.4 → 0.4
Time: 26.0s
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}}{2 \cdot i + 1.0} \cdot \frac{\frac{i}{2}}{2 \cdot i - 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}}{2 \cdot i + 1.0} \cdot \frac{\frac{i}{2}}{2 \cdot i - 1.0}
double f(double i) {
        double r3074387 = i;
        double r3074388 = r3074387 * r3074387;
        double r3074389 = r3074388 * r3074388;
        double r3074390 = 2.0;
        double r3074391 = /* ERROR: no posit support in C */;
        double r3074392 = r3074391 * r3074387;
        double r3074393 = r3074392 * r3074392;
        double r3074394 = r3074389 / r3074393;
        double r3074395 = 1.0;
        double r3074396 = /* ERROR: no posit support in C */;
        double r3074397 = r3074393 - r3074396;
        double r3074398 = r3074394 / r3074397;
        return r3074398;
}
↓
double f(double i) {
        double r3074399 = i;
        double r3074400 = 2.0;
        double r3074401 = r3074399 / r3074400;
        double r3074402 = r3074400 * r3074399;
        double r3074403 = 1.0;
        double r3074404 = r3074402 + r3074403;
        double r3074405 = r3074401 / r3074404;
        double r3074406 = r3074402 - r3074403;
        double r3074407 = r3074401 / r3074406;
        double r3074408 = r3074405 * r3074407;
        return r3074408;
}

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. Using strategy rm

  3. Applied associate-/l*1.0

    \[\leadsto \frac{\color{blue}{\left(\frac{\left(i \cdot i\right)}{\left(\frac{\left(\left(\left(2\right) \cdot i\right) \cdot \left(\left(2\right) \cdot i\right)\right)}{\left(i \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)}\]

  4. Simplified0.8

    \[\leadsto \frac{\left(\frac{\left(i \cdot i\right)}{\color{blue}{\left(\left(2\right) \cdot \left(2\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)}\]
  5. Using strategy rm

  6. Applied difference-of-sqr-10.7

    \[\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(\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)}}\]

  7. 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(\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)}\]

  8. Applied p16-times-frac0.4

    \[\leadsto \color{blue}{\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}{\left(2\right)}\right)}{\left(\left(\left(2\right) \cdot i\right) - \left(1.0\right)\right)}\right)}\]

  9. Final simplification0.4

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

Reproduce

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