Average Error: 1.0 → 0.6
Time: 45.8s
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{\beta + \alpha}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 2.0} \cdot \frac{\beta - \alpha}{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(2 \cdot i\right)\right), \alpha, 1.0\right)\right), \beta, 1.0\right)\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{\beta + \alpha}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 2.0} \cdot \frac{\beta - \alpha}{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(2 \cdot i\right)\right), \alpha, 1.0\right)\right), \beta, 1.0\right)\right)} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r1055635 = alpha;
        double r1055636 = beta;
        double r1055637 = r1055635 + r1055636;
        double r1055638 = r1055636 - r1055635;
        double r1055639 = r1055637 * r1055638;
        double r1055640 = 2.0;
        double r1055641 = /* ERROR: no posit support in C */;
        double r1055642 = i;
        double r1055643 = r1055641 * r1055642;
        double r1055644 = r1055637 + r1055643;
        double r1055645 = r1055639 / r1055644;
        double r1055646 = 2.0;
        double r1055647 = /* ERROR: no posit support in C */;
        double r1055648 = r1055644 + r1055647;
        double r1055649 = r1055645 / r1055648;
        double r1055650 = 1.0;
        double r1055651 = /* ERROR: no posit support in C */;
        double r1055652 = r1055649 + r1055651;
        double r1055653 = r1055652 / r1055647;
        return r1055653;
}
↓
double f(double alpha, double beta, double i) {
        double r1055654 = beta;
        double r1055655 = alpha;
        double r1055656 = r1055654 + r1055655;
        double r1055657 = r1055655 + r1055654;
        double r1055658 = 2.0;
        double r1055659 = i;
        double r1055660 = r1055658 * r1055659;
        double r1055661 = r1055657 + r1055660;
        double r1055662 = 2.0;
        double r1055663 = r1055661 + r1055662;
        double r1055664 = r1055656 / r1055663;
        double r1055665 = r1055654 - r1055655;
        double r1055666 = /*Error: no posit support in C */;
        double r1055667 = 1.0;
        double r1055668 = /*Error: no posit support in C */;
        double r1055669 = /*Error: no posit support in C */;
        double r1055670 = /*Error: no posit support in C */;
        double r1055671 = r1055665 / r1055670;
        double r1055672 = r1055664 * r1055671;
        double r1055673 = r1055672 + r1055667;
        double r1055674 = r1055673 / r1055662;
        return r1055674;
}

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-*-un-lft-identity1.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(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}{\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(1.0\right)}\right) \cdot \left(\frac{\left(\beta - \alpha\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}{\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(\color{blue}{\left(\frac{\beta}{\alpha}\right)} \cdot \left(\frac{\left(\beta - \alpha\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}{\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 *p16-rgt-identity-expand0.6

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

  9. Simplified0.6

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

  11. Applied introduce-quire0.6

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

  12. Applied insert-quire-add0.6

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

  13. Applied insert-quire-add0.6

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

  14. Final simplification0.6

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

Reproduce

herbie shell --seed 2019156 
(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)))