Average Error: 2.3 → 0.4
Time: 3.3m
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}{1.0 + i \cdot 2} \cdot \frac{1.0}{\frac{i \cdot 2 - 1.0}{\frac{i}{2 \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}{1.0 + i \cdot 2} \cdot \frac{1.0}{\frac{i \cdot 2 - 1.0}{\frac{i}{2 \cdot 2}}}
double f(double i) {
        double r2096932 = i;
        double r2096933 = r2096932 * r2096932;
        double r2096934 = r2096933 * r2096933;
        double r2096935 = 2.0;
        double r2096936 = /* ERROR: no posit support in C */;
        double r2096937 = r2096936 * r2096932;
        double r2096938 = r2096937 * r2096937;
        double r2096939 = r2096934 / r2096938;
        double r2096940 = 1.0;
        double r2096941 = /* ERROR: no posit support in C */;
        double r2096942 = r2096938 - r2096941;
        double r2096943 = r2096939 / r2096942;
        return r2096943;
}
↓
double f(double i) {
        double r2096944 = i;
        double r2096945 = 1.0;
        double r2096946 = 2.0;
        double r2096947 = r2096944 * r2096946;
        double r2096948 = r2096945 + r2096947;
        double r2096949 = r2096944 / r2096948;
        double r2096950 = r2096947 - r2096945;
        double r2096951 = r2096946 * r2096946;
        double r2096952 = r2096944 / r2096951;
        double r2096953 = r2096950 / r2096952;
        double r2096954 = r2096945 / r2096953;
        double r2096955 = r2096949 * r2096954;
        return r2096955;
}

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. Simplified1.1

    \[\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.0

    \[\leadsto i \cdot \color{blue}{\left(\frac{\left(\frac{i}{\left(2\right)}\right)}{\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 associate-/r*0.9

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

  7. Simplified0.9

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

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

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

  10. Applied difference-of-squares0.8

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

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

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

  12. Applied p16-times-frac0.6

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

  13. Applied associate-*r*0.4

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

  14. Simplified0.3

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

  16. Applied p16-*-un-lft-identity0.3

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

  17. Applied associate-/l*0.4

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

  18. Final simplification0.4

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

Reproduce

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