Average Error: 0.8 → 0.8
Time: 59.7s
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
↓
\[\frac{\frac{\beta - \alpha}{\alpha + \left(\beta + 2.0\right)} + 1.0}{2.0}\]
\frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
↓
\frac{\frac{\beta - \alpha}{\alpha + \left(\beta + 2.0\right)} + 1.0}{2.0}
double f(double alpha, double beta) {
        double r3055725 = beta;
        double r3055726 = alpha;
        double r3055727 = r3055725 - r3055726;
        double r3055728 = r3055726 + r3055725;
        double r3055729 = 2.0;
        double r3055730 = /* ERROR: no posit support in C */;
        double r3055731 = r3055728 + r3055730;
        double r3055732 = r3055727 / r3055731;
        double r3055733 = 1.0;
        double r3055734 = /* ERROR: no posit support in C */;
        double r3055735 = r3055732 + r3055734;
        double r3055736 = r3055735 / r3055730;
        return r3055736;
}
↓
double f(double alpha, double beta) {
        double r3055737 = beta;
        double r3055738 = alpha;
        double r3055739 = r3055737 - r3055738;
        double r3055740 = 2.0;
        double r3055741 = r3055737 + r3055740;
        double r3055742 = r3055738 + r3055741;
        double r3055743 = r3055739 / r3055742;
        double r3055744 = 1.0;
        double r3055745 = r3055743 + r3055744;
        double r3055746 = r3055745 / r3055740;
        return r3055746;
}

Error

Bits error versus alpha

Bits error versus beta

Derivation

  1. Initial program 0.8

    \[\frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  2. Using strategy rm

  3. Applied associate-+l+0.8

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

  4. Final simplification0.8

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

Reproduce

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