Average Error: 2.3 → 0.4
Time: 30.7s
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}{\left(2 \cdot i + 1.0\right) \cdot \frac{2}{1.0}} \cdot \frac{\frac{i}{\frac{2}{1.0}}}{\left(\mathsf{qms}\left(\left(\left(2 \cdot i\right)\right), 1.0, 1.0\right)\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}{\left(2 \cdot i + 1.0\right) \cdot \frac{2}{1.0}} \cdot \frac{\frac{i}{\frac{2}{1.0}}}{\left(\mathsf{qms}\left(\left(\left(2 \cdot i\right)\right), 1.0, 1.0\right)\right)}
double f(double i) {
        double r2743340 = i;
        double r2743341 = r2743340 * r2743340;
        double r2743342 = r2743341 * r2743341;
        double r2743343 = 2.0;
        double r2743344 = /* ERROR: no posit support in C */;
        double r2743345 = r2743344 * r2743340;
        double r2743346 = r2743345 * r2743345;
        double r2743347 = r2743342 / r2743346;
        double r2743348 = 1.0;
        double r2743349 = /* ERROR: no posit support in C */;
        double r2743350 = r2743346 - r2743349;
        double r2743351 = r2743347 / r2743350;
        return r2743351;
}
↓
double f(double i) {
        double r2743352 = i;
        double r2743353 = 2.0;
        double r2743354 = r2743353 * r2743352;
        double r2743355 = 1.0;
        double r2743356 = r2743354 + r2743355;
        double r2743357 = r2743353 / r2743355;
        double r2743358 = r2743356 * r2743357;
        double r2743359 = r2743352 / r2743358;
        double r2743360 = r2743352 / r2743357;
        double r2743361 = /*Error: no posit support in C */;
        double r2743362 = /*Error: no posit support in C */;
        double r2743363 = /*Error: no posit support in C */;
        double r2743364 = r2743360 / r2743363;
        double r2743365 = r2743359 * r2743364;
        return r2743365;
}

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

  4. Applied associate-/r*2.3

    \[\leadsto \color{blue}{\frac{\left(\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(1.0\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. Simplified0.9

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

  7. Applied p16-*-un-lft-identity0.9

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

  8. Applied difference-of-squares0.8

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

  9. Applied p16-times-frac0.4

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

  11. Applied introduce-quire0.4

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

  12. Applied insert-quire-sub0.4

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

  14. Applied associate-/l/0.4

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

  15. Final simplification0.4

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

Reproduce

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