Average Error: 0.4 → 0.4
Time: 17.3s
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{\left(\alpha + \beta\right) + \left(\beta \cdot \alpha + 1.0\right)}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\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{\frac{\left(\alpha + \beta\right) + \left(\beta \cdot \alpha + 1.0\right)}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\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 r1843698 = alpha;
        double r1843699 = beta;
        double r1843700 = r1843698 + r1843699;
        double r1843701 = r1843699 * r1843698;
        double r1843702 = r1843700 + r1843701;
        double r1843703 = 1.0;
        double r1843704 = /* ERROR: no posit support in C */;
        double r1843705 = r1843702 + r1843704;
        double r1843706 = 2.0;
        double r1843707 = /* ERROR: no posit support in C */;
        double r1843708 = 1.0;
        double r1843709 = /* ERROR: no posit support in C */;
        double r1843710 = r1843707 * r1843709;
        double r1843711 = r1843700 + r1843710;
        double r1843712 = r1843705 / r1843711;
        double r1843713 = r1843712 / r1843711;
        double r1843714 = r1843711 + r1843704;
        double r1843715 = r1843713 / r1843714;
        return r1843715;
}
↓
double f(double alpha, double beta) {
        double r1843716 = alpha;
        double r1843717 = beta;
        double r1843718 = r1843716 + r1843717;
        double r1843719 = r1843717 * r1843716;
        double r1843720 = 1.0;
        double r1843721 = r1843719 + r1843720;
        double r1843722 = r1843718 + r1843721;
        double r1843723 = 2.0;
        double r1843724 = 1.0;
        double r1843725 = r1843723 * r1843724;
        double r1843726 = r1843718 + r1843725;
        double r1843727 = r1843722 / r1843726;
        double r1843728 = r1843727 / r1843726;
        double r1843729 = r1843726 + r1843720;
        double r1843730 = r1843728 / r1843729;
        return r1843730;
}

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 associate-+l+0.4

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

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

Reproduce

herbie shell --seed 2019128 +o rules:numerics
(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))))