Average Error: 0.4 → 0.3
Time: 24.5s
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
↓
\[\frac{\frac{\frac{1.0}{\frac{\left(\alpha + \beta\right) + 2 \cdot 1}{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \beta, \alpha\right)\right), 1.0, 1.0\right)\right)}}}{\beta + \left(2 \cdot 1 + \alpha\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]
\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}
↓
\frac{\frac{\frac{1.0}{\frac{\left(\alpha + \beta\right) + 2 \cdot 1}{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \beta, \alpha\right)\right), 1.0, 1.0\right)\right)}}}{\beta + \left(2 \cdot 1 + \alpha\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}
double f(double alpha, double beta) {
        double r915486 = alpha;
        double r915487 = beta;
        double r915488 = r915486 + r915487;
        double r915489 = r915487 * r915486;
        double r915490 = r915488 + r915489;
        double r915491 = 1.0;
        double r915492 = /* ERROR: no posit support in C */;
        double r915493 = r915490 + r915492;
        double r915494 = 2.0;
        double r915495 = /* ERROR: no posit support in C */;
        double r915496 = 1.0;
        double r915497 = /* ERROR: no posit support in C */;
        double r915498 = r915495 * r915497;
        double r915499 = r915488 + r915498;
        double r915500 = r915493 / r915499;
        double r915501 = r915500 / r915499;
        double r915502 = r915499 + r915492;
        double r915503 = r915501 / r915502;
        return r915503;
}
↓
double f(double alpha, double beta) {
        double r915504 = 1.0;
        double r915505 = alpha;
        double r915506 = beta;
        double r915507 = r915505 + r915506;
        double r915508 = 2.0;
        double r915509 = 1.0;
        double r915510 = r915508 * r915509;
        double r915511 = r915507 + r915510;
        double r915512 = /*Error: no posit support in C */;
        double r915513 = /*Error: no posit support in C */;
        double r915514 = /*Error: no posit support in C */;
        double r915515 = /*Error: no posit support in C */;
        double r915516 = r915511 / r915515;
        double r915517 = r915504 / r915516;
        double r915518 = r915510 + r915505;
        double r915519 = r915506 + r915518;
        double r915520 = r915517 / r915519;
        double r915521 = r915511 + r915504;
        double r915522 = r915520 / r915521;
        return r915522;
}

Error

Bits error versus alpha

Bits error versus beta

Derivation

  1. Initial program 0.4

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

  3. Applied introduce-quire0.4

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

  4. Applied insert-quire-fdp-add0.4

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

  5. Applied insert-quire-add0.3

    \[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\frac{\alpha}{\beta}\right)\right), \beta, \alpha\right)\right), \left(1.0\right), \left(1.0\right)\right)\right)\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
  6. Using strategy rm

  7. Applied p16-*-un-lft-identity0.3

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

  8. Applied associate-/l*0.3

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\frac{\alpha}{\beta}\right)\right), \beta, \alpha\right)\right), \left(1.0\right), \left(1.0\right)\right)\right)\right)}\right)}\right)}}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right)}\]
  9. Using strategy rm

  10. Applied /p16-rgt-identity-expand0.3

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

  11. Applied associate-/r/0.3

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

  12. Applied p16-*-un-lft-identity0.3

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

  13. Applied p16-times-frac0.3

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

  14. Applied associate-/l*0.3

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

  15. Simplified0.3

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

  16. Final simplification0.3

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

Reproduce

herbie shell --seed 2019156 
(FPCore (alpha beta)
  :name "Octave 3.8, jcobi/3"
  :pre (and (>.p16 alpha (real->posit16 -1)) (>.p16 beta (real->posit16 -1)))
  (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))