Average Error: 0.9 → 0.6
Time: 47.0s
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{\frac{\beta + \alpha}{\beta + \left(\alpha + i \cdot 2\right)} \cdot \left(\beta - \alpha\right)}{2.0 + \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) + 0.0 \cdot i\right)} + 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{\frac{\beta + \alpha}{\beta + \left(\alpha + i \cdot 2\right)} \cdot \left(\beta - \alpha\right)}{2.0 + \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) + 0.0 \cdot i\right)} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r1087642 = alpha;
        double r1087643 = beta;
        double r1087644 = r1087642 + r1087643;
        double r1087645 = r1087643 - r1087642;
        double r1087646 = r1087644 * r1087645;
        double r1087647 = 2.0;
        double r1087648 = /* ERROR: no posit support in C */;
        double r1087649 = i;
        double r1087650 = r1087648 * r1087649;
        double r1087651 = r1087644 + r1087650;
        double r1087652 = r1087646 / r1087651;
        double r1087653 = 2.0;
        double r1087654 = /* ERROR: no posit support in C */;
        double r1087655 = r1087651 + r1087654;
        double r1087656 = r1087652 / r1087655;
        double r1087657 = 1.0;
        double r1087658 = /* ERROR: no posit support in C */;
        double r1087659 = r1087656 + r1087658;
        double r1087660 = r1087659 / r1087654;
        return r1087660;
}
↓
double f(double alpha, double beta, double i) {
        double r1087661 = beta;
        double r1087662 = alpha;
        double r1087663 = r1087661 + r1087662;
        double r1087664 = i;
        double r1087665 = 2.0;
        double r1087666 = r1087664 * r1087665;
        double r1087667 = r1087662 + r1087666;
        double r1087668 = r1087661 + r1087667;
        double r1087669 = r1087663 / r1087668;
        double r1087670 = r1087661 - r1087662;
        double r1087671 = r1087669 * r1087670;
        double r1087672 = 2.0;
        double r1087673 = r1087661 + r1087666;
        double r1087674 = r1087662 + r1087673;
        double r1087675 = 0.0;
        double r1087676 = r1087675 * r1087664;
        double r1087677 = r1087674 + r1087676;
        double r1087678 = r1087672 + r1087677;
        double r1087679 = r1087671 / r1087678;
        double r1087680 = 1.0;
        double r1087681 = r1087679 + r1087680;
        double r1087682 = r1087681 / r1087672;
        return r1087682;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 0.9

    \[\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-*-un-lft-identity0.9

    \[\leadsto \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)}{\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-identity0.9

    \[\leadsto \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{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\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-out0.9

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

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

    \[\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(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  7. 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(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  8. Applied p16-times-frac0.6

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

  9. Simplified0.6

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

  10. Simplified0.6

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

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

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

  13. Applied distribute-rgt-in0.6

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

  14. Applied associate-+r+0.6

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

  15. Simplified0.6

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

  17. Applied associate-*r/0.6

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

  19. Applied associate-+l+0.6

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

  20. Final simplification0.6

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

Reproduce

herbie shell --seed 2019154 +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)))