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 r4041652 = beta;
        double r4041653 = alpha;
        double r4041654 = r4041652 - r4041653;
        double r4041655 = r4041653 + r4041652;
        double r4041656 = 2.0;
        double r4041657 = /* ERROR: no posit support in C */;
        double r4041658 = r4041655 + r4041657;
        double r4041659 = r4041654 / r4041658;
        double r4041660 = 1.0;
        double r4041661 = /* ERROR: no posit support in C */;
        double r4041662 = r4041659 + r4041661;
        double r4041663 = r4041662 / r4041657;
        return r4041663;
}
↓
double f(double alpha, double beta) {
        double r4041664 = 1.0;
        double r4041665 = 2.0;
        double r4041666 = /*Error: no posit support in C */;
        double r4041667 = alpha;
        double r4041668 = /*Error: no posit support in C */;
        double r4041669 = beta;
        double r4041670 = /*Error: no posit support in C */;
        double r4041671 = /*Error: no posit support in C */;
        double r4041672 = r4041669 - r4041667;
        double r4041673 = r4041671 / r4041672;
        double r4041674 = r4041664 / r4041673;
        double r4041675 = r4041674 + r4041664;
        double r4041676 = r4041675 / r4041665;
        return r4041676;
}

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