Average Error: 0.4 → 0.4
Time: 15.8s
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{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot 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{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot 1\right)}
double f(double alpha, double beta) {
        double r707521 = alpha;
        double r707522 = beta;
        double r707523 = r707521 + r707522;
        double r707524 = r707522 * r707521;
        double r707525 = r707523 + r707524;
        double r707526 = 1.0;
        double r707527 = /* ERROR: no posit support in C */;
        double r707528 = r707525 + r707527;
        double r707529 = 2.0;
        double r707530 = /* ERROR: no posit support in C */;
        double r707531 = 1.0;
        double r707532 = /* ERROR: no posit support in C */;
        double r707533 = r707530 * r707532;
        double r707534 = r707523 + r707533;
        double r707535 = r707528 / r707534;
        double r707536 = r707535 / r707534;
        double r707537 = r707534 + r707527;
        double r707538 = r707536 / r707537;
        return r707538;
}
↓
double f(double alpha, double beta) {
        double r707539 = alpha;
        double r707540 = beta;
        double r707541 = r707539 + r707540;
        double r707542 = r707540 * r707539;
        double r707543 = r707541 + r707542;
        double r707544 = 1.0;
        double r707545 = r707543 + r707544;
        double r707546 = 2.0;
        double r707547 = 1.0;
        double r707548 = r707546 * r707547;
        double r707549 = r707541 + r707548;
        double r707550 = r707545 / r707549;
        double r707551 = r707549 + r707544;
        double r707552 = r707551 * r707549;
        double r707553 = r707550 / r707552;
        return r707553;
}

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. Using strategy rm

  5. Applied associate-/l/0.4

    \[\leadsto \color{blue}{\frac{\left(\frac{\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(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot \left(1\right)\right)}\right)\right)}}\]
  6. Using strategy rm

  7. Applied associate-+r+0.4

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

  8. Final simplification0.4

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

Reproduce

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