Average Error: 0.7 → 0.7
Time: 22.0s
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 r1617756 = beta;
        double r1617757 = alpha;
        double r1617758 = r1617756 - r1617757;
        double r1617759 = r1617757 + r1617756;
        double r1617760 = 2.0;
        double r1617761 = /* ERROR: no posit support in C */;
        double r1617762 = r1617759 + r1617761;
        double r1617763 = r1617758 / r1617762;
        double r1617764 = 1.0;
        double r1617765 = /* ERROR: no posit support in C */;
        double r1617766 = r1617763 + r1617765;
        double r1617767 = r1617766 / r1617761;
        return r1617767;
}
↓
double f(double alpha, double beta) {
        double r1617768 = beta;
        double r1617769 = alpha;
        double r1617770 = r1617768 - r1617769;
        double r1617771 = 2.0;
        double r1617772 = r1617768 + r1617771;
        double r1617773 = r1617769 + r1617772;
        double r1617774 = r1617770 / r1617773;
        double r1617775 = 1.0;
        double r1617776 = r1617774 + r1617775;
        double r1617777 = r1617776 / r1617771;
        return r1617777;
}

Error

Bits error versus alpha

Bits error versus beta

Derivation

  1. Initial program 0.7

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

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

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

Reproduce

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