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 r2441278 = beta;
        double r2441279 = alpha;
        double r2441280 = r2441278 - r2441279;
        double r2441281 = r2441279 + r2441278;
        double r2441282 = 2.0;
        double r2441283 = /* ERROR: no posit support in C */;
        double r2441284 = r2441281 + r2441283;
        double r2441285 = r2441280 / r2441284;
        double r2441286 = 1.0;
        double r2441287 = /* ERROR: no posit support in C */;
        double r2441288 = r2441285 + r2441287;
        double r2441289 = r2441288 / r2441283;
        return r2441289;
}

double f(double alpha, double beta) {
        double r2441290 = 1.0;
        double r2441291 = 2.0;
        double r2441292 = /*Error: no posit support in C */;
        double r2441293 = alpha;
        double r2441294 = /*Error: no posit support in C */;
        double r2441295 = beta;
        double r2441296 = /*Error: no posit support in C */;
        double r2441297 = /*Error: no posit support in C */;
        double r2441298 = r2441295 - r2441293;
        double r2441299 = r2441297 / r2441298;
        double r2441300 = r2441290 / r2441299;
        double r2441301 = r2441300 + r2441290;
        double r2441302 = r2441301 / r2441291;
        return r2441302;
}

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