Average Error: 0.8 → 0.8
Time: 2.8m
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{1.0}{\frac{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(2.0\right), \alpha, 1.0\right)\right), \beta, 1.0\right)\right)}{\beta - \alpha}} + 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{1.0}{\frac{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(2.0\right), \alpha, 1.0\right)\right), \beta, 1.0\right)\right)}{\beta - \alpha}} + 1.0}{2.0}
double f(double alpha, double beta) {
        double r3071715 = beta;
        double r3071716 = alpha;
        double r3071717 = r3071715 - r3071716;
        double r3071718 = r3071716 + r3071715;
        double r3071719 = 2.0;
        double r3071720 = /* ERROR: no posit support in C */;
        double r3071721 = r3071718 + r3071720;
        double r3071722 = r3071717 / r3071721;
        double r3071723 = 1.0;
        double r3071724 = /* ERROR: no posit support in C */;
        double r3071725 = r3071722 + r3071724;
        double r3071726 = r3071725 / r3071720;
        return r3071726;
}
↓
double f(double alpha, double beta) {
        double r3071727 = 1.0;
        double r3071728 = 2.0;
        double r3071729 = /*Error: no posit support in C */;
        double r3071730 = alpha;
        double r3071731 = /*Error: no posit support in C */;
        double r3071732 = beta;
        double r3071733 = /*Error: no posit support in C */;
        double r3071734 = /*Error: no posit support in C */;
        double r3071735 = r3071732 - r3071730;
        double r3071736 = r3071734 / r3071735;
        double r3071737 = r3071727 / r3071736;
        double r3071738 = r3071737 + r3071727;
        double r3071739 = r3071738 / r3071728;
        return r3071739;
}

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. Using strategy rm

  5. Applied *p16-rgt-identity-expand0.8

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

  6. Applied associate-/l*0.8

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

  7. Simplified0.8

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

  9. Applied introduce-quire0.8

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

  10. Applied insert-quire-add0.8

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

  11. Applied insert-quire-add0.7

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

  13. 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(\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(2.0\right)\right), \alpha, \left(1.0\right)\right)\right), \beta, \left(1.0\right)\right)\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  14. Applied associate-/l*0.8

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

  15. Final simplification0.8

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

Reproduce

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