Average Error: 0.4 → 0.3
Time: 3.7m
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(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \beta, \alpha\right)\right), 1.0, 1.0\right)\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(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \beta, \alpha\right)\right), 1.0, 1.0\right)\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 r1853916 = alpha;
        double r1853917 = beta;
        double r1853918 = r1853916 + r1853917;
        double r1853919 = r1853917 * r1853916;
        double r1853920 = r1853918 + r1853919;
        double r1853921 = 1.0;
        double r1853922 = /* ERROR: no posit support in C */;
        double r1853923 = r1853920 + r1853922;
        double r1853924 = 2.0;
        double r1853925 = /* ERROR: no posit support in C */;
        double r1853926 = 1.0;
        double r1853927 = /* ERROR: no posit support in C */;
        double r1853928 = r1853925 * r1853927;
        double r1853929 = r1853918 + r1853928;
        double r1853930 = r1853923 / r1853929;
        double r1853931 = r1853930 / r1853929;
        double r1853932 = r1853929 + r1853922;
        double r1853933 = r1853931 / r1853932;
        return r1853933;
}
↓
double f(double alpha, double beta) {
        double r1853934 = alpha;
        double r1853935 = beta;
        double r1853936 = r1853934 + r1853935;
        double r1853937 = /*Error: no posit support in C */;
        double r1853938 = /*Error: no posit support in C */;
        double r1853939 = 1.0;
        double r1853940 = /*Error: no posit support in C */;
        double r1853941 = /*Error: no posit support in C */;
        double r1853942 = 2.0;
        double r1853943 = 1.0;
        double r1853944 = r1853942 * r1853943;
        double r1853945 = r1853936 + r1853944;
        double r1853946 = r1853941 / r1853945;
        double r1853947 = r1853946 / r1853945;
        double r1853948 = r1853945 + r1853939;
        double r1853949 = r1853947 / r1853948;
        return r1853949;
}

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{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\beta \cdot \alpha\right)}\right)}{\color{blue}{\left(\left(1.0\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{\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 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(\left(1.0\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{\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-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(\left(1.0\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{\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. Applied insert-quire-fdp-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)}\]

  7. Final simplification0.3

    \[\leadsto \frac{\frac{\frac{\left(\mathsf{qma}\left(\left(\mathsf{qma}\left(\left(\left(\alpha + \beta\right)\right), \beta, \alpha\right)\right), 1.0, 1.0\right)\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 2019153 
(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))))