Average Error: 2.4 → 0.4
Time: 29.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} \cdot \frac{\frac{i}{2}}{2 \cdot i - 1.0}}{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} \cdot \frac{\frac{i}{2}}{2 \cdot i - 1.0}}{2 \cdot i + 1.0}
double f(double i) {
        double r4169224 = i;
        double r4169225 = r4169224 * r4169224;
        double r4169226 = r4169225 * r4169225;
        double r4169227 = 2.0;
        double r4169228 = /* ERROR: no posit support in C */;
        double r4169229 = r4169228 * r4169224;
        double r4169230 = r4169229 * r4169229;
        double r4169231 = r4169226 / r4169230;
        double r4169232 = 1.0;
        double r4169233 = /* ERROR: no posit support in C */;
        double r4169234 = r4169230 - r4169233;
        double r4169235 = r4169231 / r4169234;
        return r4169235;
}
↓
double f(double i) {
        double r4169236 = i;
        double r4169237 = 2.0;
        double r4169238 = r4169236 / r4169237;
        double r4169239 = r4169237 * r4169236;
        double r4169240 = 1.0;
        double r4169241 = r4169239 - r4169240;
        double r4169242 = r4169238 / r4169241;
        double r4169243 = r4169238 * r4169242;
        double r4169244 = r4169239 + r4169240;
        double r4169245 = r4169243 / r4169244;
        return r4169245;
}

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

  10. Applied associate-*l/0.4

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

  11. Final simplification0.4

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

Reproduce

herbie shell --seed 2019125 
(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))))