Average Error: 0.7 → 0.7
Time: 19.3s
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 r2996336 = beta;
        double r2996337 = alpha;
        double r2996338 = r2996336 - r2996337;
        double r2996339 = r2996337 + r2996336;
        double r2996340 = 2.0;
        double r2996341 = /* ERROR: no posit support in C */;
        double r2996342 = r2996339 + r2996341;
        double r2996343 = r2996338 / r2996342;
        double r2996344 = 1.0;
        double r2996345 = /* ERROR: no posit support in C */;
        double r2996346 = r2996343 + r2996345;
        double r2996347 = r2996346 / r2996341;
        return r2996347;
}
↓
double f(double alpha, double beta) {
        double r2996348 = beta;
        double r2996349 = alpha;
        double r2996350 = r2996348 - r2996349;
        double r2996351 = 2.0;
        double r2996352 = r2996348 + r2996351;
        double r2996353 = r2996349 + r2996352;
        double r2996354 = r2996350 / r2996353;
        double r2996355 = 1.0;
        double r2996356 = r2996354 + r2996355;
        double r2996357 = r2996356 / r2996351;
        return r2996357;
}

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 2019128 +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)))