Octave 3.8, jcobi/1

Average Error: 0.7 → 0.7

Time: 30.1s

Precision: 64

\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right)\]

Math

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

C

double f(double alpha, double beta) {
        double r1526418 = beta;
        double r1526419 = alpha;
        double r1526420 = r1526418 - r1526419;
        double r1526421 = r1526419 + r1526418;
        double r1526422 = 2.0;
        double r1526423 = /* ERROR: no posit support in C */;
        double r1526424 = r1526421 + r1526423;
        double r1526425 = r1526420 / r1526424;
        double r1526426 = 1.0;
        double r1526427 = /* ERROR: no posit support in C */;
        double r1526428 = r1526425 + r1526427;
        double r1526429 = r1526428 / r1526423;
        return r1526429;
}

↓

double f(double alpha, double beta) {
        double r1526430 = beta;
        double r1526431 = alpha;
        double r1526432 = r1526430 - r1526431;
        double r1526433 = 2.0;
        double r1526434 = r1526431 + r1526433;
        double r1526435 = r1526430 + r1526434;
        double r1526436 = r1526432 / r1526435;
        double r1526437 = /*Error: no posit support in C */;
        double r1526438 = 1.0;
        double r1526439 = /*Error: no posit support in C */;
        double r1526440 = /*Error: no posit support in C */;
        double r1526441 = r1526440 / r1526433;
        return r1526441;
}

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-identity 0.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-identity 0.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-out 0.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-expand 0.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-frac 0.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. Simplified 0.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. Using strategy rm

10. Applied introduce-quire 0.8

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

11. Applied insert-quire-add 0.8

    \[\leadsto \frac{\color{blue}{\left(\left(\mathsf{qma}\left(\left(\left(\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)\right), \left(1.0\right), \left(1.0\right)\right)\right)\right)}}{\left(2.0\right)}\]

12. Simplified 0.7

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

13. Final simplification 0.7

    \[\leadsto \frac{\left(\mathsf{qma}\left(\left(\left(\frac{\beta - \alpha}{\beta + \left(\alpha + 2.0\right)}\right)\right), 1.0, 1.0\right)\right)}{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)))