Average Error: 0.7 → 0.7
Time: 1.1m
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{\left(\beta \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2.0} + \left(-\alpha\right) \cdot \frac{1.0}{\left(\alpha + \beta\right) + 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{\left(\beta \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2.0} + \left(-\alpha\right) \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2.0}\right) + 1.0}{2.0}
double f(double alpha, double beta) {
        double r1411968 = beta;
        double r1411969 = alpha;
        double r1411970 = r1411968 - r1411969;
        double r1411971 = r1411969 + r1411968;
        double r1411972 = 2.0;
        double r1411973 = /* ERROR: no posit support in C */;
        double r1411974 = r1411971 + r1411973;
        double r1411975 = r1411970 / r1411974;
        double r1411976 = 1.0;
        double r1411977 = /* ERROR: no posit support in C */;
        double r1411978 = r1411975 + r1411977;
        double r1411979 = r1411978 / r1411973;
        return r1411979;
}
↓
double f(double alpha, double beta) {
        double r1411980 = beta;
        double r1411981 = 1.0;
        double r1411982 = alpha;
        double r1411983 = r1411982 + r1411980;
        double r1411984 = 2.0;
        double r1411985 = r1411983 + r1411984;
        double r1411986 = r1411981 / r1411985;
        double r1411987 = r1411980 * r1411986;
        double r1411988 = -r1411982;
        double r1411989 = r1411988 * r1411986;
        double r1411990 = r1411987 + r1411989;
        double r1411991 = r1411990 + r1411981;
        double r1411992 = r1411991 / r1411984;
        return r1411992;
}

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 p16-*-un-lft-identity0.7

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

  4. Applied associate-/l*0.7

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

  6. Applied associate-/r/0.8

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

  8. Applied sub-neg0.8

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

  9. Applied distribute-rgt-in0.7

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

  10. Final simplification0.7

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

Reproduce

herbie shell --seed 2019153 
(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)))