Average Error: 0.7 → 0.8
Time: 3.5m
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 - \alpha\right) \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2.0} + 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 - \alpha\right) \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2.0} + 1.0}{2.0}
double f(double alpha, double beta) {
        double r3772577 = beta;
        double r3772578 = alpha;
        double r3772579 = r3772577 - r3772578;
        double r3772580 = r3772578 + r3772577;
        double r3772581 = 2.0;
        double r3772582 = /* ERROR: no posit support in C */;
        double r3772583 = r3772580 + r3772582;
        double r3772584 = r3772579 / r3772583;
        double r3772585 = 1.0;
        double r3772586 = /* ERROR: no posit support in C */;
        double r3772587 = r3772584 + r3772586;
        double r3772588 = r3772587 / r3772582;
        return r3772588;
}
↓
double f(double alpha, double beta) {
        double r3772589 = beta;
        double r3772590 = alpha;
        double r3772591 = r3772589 - r3772590;
        double r3772592 = 1.0;
        double r3772593 = r3772590 + r3772589;
        double r3772594 = 2.0;
        double r3772595 = r3772593 + r3772594;
        double r3772596 = r3772592 / r3772595;
        double r3772597 = r3772591 * r3772596;
        double r3772598 = r3772597 + r3772592;
        double r3772599 = r3772598 / r3772594;
        return r3772599;
}

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{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2.0\right)\right)}}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  4. Applied p16-*-un-lft-identity0.7

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

  5. Applied distribute-lft-out0.7

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

  6. Applied *p16-rgt-identity-expand0.7

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

  7. Applied p16-times-frac0.8

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

  8. Simplified0.8

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

  9. Final simplification0.8

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

Reproduce

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