Average Error: 2.3 → 0.5
Time: 1.1m
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 \cdot \frac{\frac{i}{2}}{i \cdot 2 + 1.0}}{\left(i \cdot 2 - 1.0\right) \cdot 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 \cdot \frac{\frac{i}{2}}{i \cdot 2 + 1.0}}{\left(i \cdot 2 - 1.0\right) \cdot 2}
double f(double i) {
        double r5457750 = i;
        double r5457751 = r5457750 * r5457750;
        double r5457752 = r5457751 * r5457751;
        double r5457753 = 2.0;
        double r5457754 = /* ERROR: no posit support in C */;
        double r5457755 = r5457754 * r5457750;
        double r5457756 = r5457755 * r5457755;
        double r5457757 = r5457752 / r5457756;
        double r5457758 = 1.0;
        double r5457759 = /* ERROR: no posit support in C */;
        double r5457760 = r5457756 - r5457759;
        double r5457761 = r5457757 / r5457760;
        return r5457761;
}
↓
double f(double i) {
        double r5457762 = i;
        double r5457763 = 2.0;
        double r5457764 = r5457762 / r5457763;
        double r5457765 = r5457762 * r5457763;
        double r5457766 = 1.0;
        double r5457767 = r5457765 + r5457766;
        double r5457768 = r5457764 / r5457767;
        double r5457769 = r5457762 * r5457768;
        double r5457770 = r5457765 - r5457766;
        double r5457771 = r5457770 * r5457763;
        double r5457772 = r5457769 / r5457771;
        return r5457772;
}

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. Simplified0.9

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

  4. Applied difference-of-sqr-10.9

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

  5. Applied associate-/r*0.6

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

  7. Applied associate-*r/0.5

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

  9. Applied associate-*l/0.5

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

  10. Applied associate-/l/0.5

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

  11. Final simplification0.5

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

Reproduce

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