Average Error: 0.9 → 0.6
Time: 49.4s
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right) \land i \gt \left(0\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
↓
\[\frac{\frac{\frac{\beta - \alpha}{2 \cdot i + \left(\beta + \alpha\right)}}{\frac{\left(2.0 + \left(\beta + \alpha\right)\right) + 2 \cdot i}{\beta + \alpha}} + 1.0}{2.0}\]
\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
↓
\frac{\frac{\frac{\beta - \alpha}{2 \cdot i + \left(\beta + \alpha\right)}}{\frac{\left(2.0 + \left(\beta + \alpha\right)\right) + 2 \cdot i}{\beta + \alpha}} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r3907874 = alpha;
        double r3907875 = beta;
        double r3907876 = r3907874 + r3907875;
        double r3907877 = r3907875 - r3907874;
        double r3907878 = r3907876 * r3907877;
        double r3907879 = 2.0;
        double r3907880 = /* ERROR: no posit support in C */;
        double r3907881 = i;
        double r3907882 = r3907880 * r3907881;
        double r3907883 = r3907876 + r3907882;
        double r3907884 = r3907878 / r3907883;
        double r3907885 = 2.0;
        double r3907886 = /* ERROR: no posit support in C */;
        double r3907887 = r3907883 + r3907886;
        double r3907888 = r3907884 / r3907887;
        double r3907889 = 1.0;
        double r3907890 = /* ERROR: no posit support in C */;
        double r3907891 = r3907888 + r3907890;
        double r3907892 = r3907891 / r3907886;
        return r3907892;
}
↓
double f(double alpha, double beta, double i) {
        double r3907893 = beta;
        double r3907894 = alpha;
        double r3907895 = r3907893 - r3907894;
        double r3907896 = 2.0;
        double r3907897 = i;
        double r3907898 = r3907896 * r3907897;
        double r3907899 = r3907893 + r3907894;
        double r3907900 = r3907898 + r3907899;
        double r3907901 = r3907895 / r3907900;
        double r3907902 = 2.0;
        double r3907903 = r3907902 + r3907899;
        double r3907904 = r3907903 + r3907898;
        double r3907905 = r3907904 / r3907899;
        double r3907906 = r3907901 / r3907905;
        double r3907907 = 1.0;
        double r3907908 = r3907906 + r3907907;
        double r3907909 = r3907908 / r3907902;
        return r3907909;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 0.9

    \[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  2. Simplified0.9

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

  4. Applied p16-times-frac0.6

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

  6. Applied associate-*r/0.6

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

  8. Applied associate-/l*0.6

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

  9. Final simplification0.6

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

Reproduce

herbie shell --seed 2019134 +o rules:numerics
(FPCore (alpha beta i)
  :name "Octave 3.8, jcobi/2"
  :pre (and (>.p16 alpha (real->posit16 -1)) (>.p16 beta (real->posit16 -1)) (>.p16 i (real->posit16 0)))
  (/.p16 (+.p16 (/.p16 (/.p16 (*.p16 (+.p16 alpha beta) (-.p16 beta alpha)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)))