Average Error: 0.4 → 0.3
Time: 41.4s
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{\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{\beta}{\left(\frac{\alpha}{\left(\left(1\right) \cdot \left(2\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)}\]
\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{\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{\beta}{\left(\frac{\alpha}{\left(\left(1\right) \cdot \left(2\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)}
double f(double alpha, double beta) {
        double r4490167 = alpha;
        double r4490168 = beta;
        double r4490169 = r4490167 + r4490168;
        double r4490170 = r4490168 * r4490167;
        double r4490171 = r4490169 + r4490170;
        double r4490172 = 1.0;
        double r4490173 = /* ERROR: no posit support in C */;
        double r4490174 = r4490171 + r4490173;
        double r4490175 = 2.0;
        double r4490176 = /* ERROR: no posit support in C */;
        double r4490177 = 1.0;
        double r4490178 = /* ERROR: no posit support in C */;
        double r4490179 = r4490176 * r4490178;
        double r4490180 = r4490169 + r4490179;
        double r4490181 = r4490174 / r4490180;
        double r4490182 = r4490181 / r4490180;
        double r4490183 = r4490180 + r4490173;
        double r4490184 = r4490182 / r4490183;
        return r4490184;
}
↓
double f(double alpha, double beta) {
        double r4490185 = alpha;
        double r4490186 = beta;
        double r4490187 = r4490185 + r4490186;
        double r4490188 = r4490186 * r4490185;
        double r4490189 = r4490187 + r4490188;
        double r4490190 = 1.0;
        double r4490191 = /* ERROR: no posit support in C */;
        double r4490192 = r4490189 + r4490191;
        double r4490193 = 1.0;
        double r4490194 = /* ERROR: no posit support in C */;
        double r4490195 = 2.0;
        double r4490196 = /* ERROR: no posit support in C */;
        double r4490197 = r4490194 * r4490196;
        double r4490198 = r4490185 + r4490197;
        double r4490199 = r4490186 + r4490198;
        double r4490200 = r4490192 / r4490199;
        double r4490201 = r4490196 * r4490194;
        double r4490202 = r4490187 + r4490201;
        double r4490203 = r4490200 / r4490202;
        double r4490204 = r4490202 + r4490191;
        double r4490205 = r4490203 / r4490204;
        return r4490205;
}

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 *p16-rgt-identity-expand0.4

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

    \[\leadsto \frac{\left(\frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\left(1.0\right)}\right) \cdot \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 associate-/l*0.4

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

  6. Simplified0.3

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

  7. Final simplification0.3

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

Reproduce

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