Average Error: 1.0 → 0.6
Time: 1.6m
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right) \land i \gt \left(0\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
↓
\[\frac{\frac{\left(\beta + \alpha\right) \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2 \cdot i}}{\frac{\left(\alpha + \left(\beta + 2 \cdot i\right)\right) + 2.0}{\beta - \alpha}} + 1.0}{2.0}\]
\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
↓
\frac{\frac{\left(\beta + \alpha\right) \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2 \cdot i}}{\frac{\left(\alpha + \left(\beta + 2 \cdot i\right)\right) + 2.0}{\beta - \alpha}} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r1685556 = alpha;
        double r1685557 = beta;
        double r1685558 = r1685556 + r1685557;
        double r1685559 = r1685557 - r1685556;
        double r1685560 = r1685558 * r1685559;
        double r1685561 = 2.0;
        double r1685562 = /* ERROR: no posit support in C */;
        double r1685563 = i;
        double r1685564 = r1685562 * r1685563;
        double r1685565 = r1685558 + r1685564;
        double r1685566 = r1685560 / r1685565;
        double r1685567 = 2.0;
        double r1685568 = /* ERROR: no posit support in C */;
        double r1685569 = r1685565 + r1685568;
        double r1685570 = r1685566 / r1685569;
        double r1685571 = 1.0;
        double r1685572 = /* ERROR: no posit support in C */;
        double r1685573 = r1685570 + r1685572;
        double r1685574 = r1685573 / r1685568;
        return r1685574;
}
↓
double f(double alpha, double beta, double i) {
        double r1685575 = beta;
        double r1685576 = alpha;
        double r1685577 = r1685575 + r1685576;
        double r1685578 = 1.0;
        double r1685579 = r1685576 + r1685575;
        double r1685580 = 2.0;
        double r1685581 = i;
        double r1685582 = r1685580 * r1685581;
        double r1685583 = r1685579 + r1685582;
        double r1685584 = r1685578 / r1685583;
        double r1685585 = r1685577 * r1685584;
        double r1685586 = r1685575 + r1685582;
        double r1685587 = r1685576 + r1685586;
        double r1685588 = 2.0;
        double r1685589 = r1685587 + r1685588;
        double r1685590 = r1685575 - r1685576;
        double r1685591 = r1685589 / r1685590;
        double r1685592 = r1685585 / r1685591;
        double r1685593 = r1685592 + r1685578;
        double r1685594 = r1685593 / r1685588;
        return r1685594;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 1.0

    \[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  2. Using strategy rm

  3. Applied *p16-rgt-identity-expand1.0

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

  4. Applied p16-times-frac0.6

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

  5. Simplified0.6

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

  7. Applied associate-+l+0.6

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

  9. Applied associate-/l*0.6

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

  11. Applied p16-*-un-lft-identity0.6

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

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

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

  13. Applied p16-times-frac0.6

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

  14. Simplified0.6

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

  15. Final simplification0.6

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

Reproduce

herbie shell --seed 2019152 +o rules:numerics
(FPCore (alpha beta i)
  :name "Octave 3.8, jcobi/2"
  :pre (and (>.p16 alpha (real->posit16 -1)) (>.p16 beta (real->posit16 -1)) (>.p16 i (real->posit16 0)))
  (/.p16 (+.p16 (/.p16 (/.p16 (*.p16 (+.p16 alpha beta) (-.p16 beta alpha)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)))