Average Error: 0.4 → 0.4
Time: 37.2s
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{1.0}{\frac{\left(\alpha + \beta\right) + 2 \cdot 1}{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \left(\beta \cdot \alpha\right), 1.0\right)\right), 1.0, 1.0\right)\right)}} \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\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{1.0}{\frac{\left(\alpha + \beta\right) + 2 \cdot 1}{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \left(\beta \cdot \alpha\right), 1.0\right)\right), 1.0, 1.0\right)\right)}} \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}
double f(double alpha, double beta) {
        double r3809624 = alpha;
        double r3809625 = beta;
        double r3809626 = r3809624 + r3809625;
        double r3809627 = r3809625 * r3809624;
        double r3809628 = r3809626 + r3809627;
        double r3809629 = 1.0;
        double r3809630 = /* ERROR: no posit support in C */;
        double r3809631 = r3809628 + r3809630;
        double r3809632 = 2.0;
        double r3809633 = /* ERROR: no posit support in C */;
        double r3809634 = 1.0;
        double r3809635 = /* ERROR: no posit support in C */;
        double r3809636 = r3809633 * r3809635;
        double r3809637 = r3809626 + r3809636;
        double r3809638 = r3809631 / r3809637;
        double r3809639 = r3809638 / r3809637;
        double r3809640 = r3809637 + r3809630;
        double r3809641 = r3809639 / r3809640;
        return r3809641;
}
↓
double f(double alpha, double beta) {
        double r3809642 = 1.0;
        double r3809643 = alpha;
        double r3809644 = beta;
        double r3809645 = r3809643 + r3809644;
        double r3809646 = 2.0;
        double r3809647 = 1.0;
        double r3809648 = r3809646 * r3809647;
        double r3809649 = r3809645 + r3809648;
        double r3809650 = /*Error: no posit support in C */;
        double r3809651 = r3809644 * r3809643;
        double r3809652 = /*Error: no posit support in C */;
        double r3809653 = /*Error: no posit support in C */;
        double r3809654 = /*Error: no posit support in C */;
        double r3809655 = r3809649 / r3809654;
        double r3809656 = r3809642 / r3809655;
        double r3809657 = r3809642 / r3809649;
        double r3809658 = r3809656 * r3809657;
        double r3809659 = r3809649 + r3809642;
        double r3809660 = r3809658 / r3809659;
        return r3809660;
}

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-add0.4

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\mathsf{qma}\left(\left(\left(\frac{\alpha}{\beta}\right)\right), \left(\beta \cdot \alpha\right), \left(1.0\right)\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), \left(\beta \cdot \alpha\right), \left(1.0\right)\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{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\frac{\alpha}{\beta}\right)\right), \left(\beta \cdot \alpha\right), \left(1.0\right)\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)\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.4

    \[\leadsto \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(\frac{\left(\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\frac{\alpha}{\beta}\right)\right), \left(\beta \cdot \alpha\right), \left(1.0\right)\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)}\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 associate-/r/0.4

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

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

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

  12. Applied p16-times-frac0.4

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

  13. Final simplification0.4

    \[\leadsto \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), \left(\beta \cdot \alpha\right), 1.0\right)\right), 1.0, 1.0\right)\right)}} \cdot \frac{1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]

Reproduce

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