Average Error: 1.1 → 1.1
Time: 10.4s
Precision: 64
\[\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
↓
\[\frac{1.0}{\frac{y.re \cdot y.re + y.im \cdot y.im}{x.im \cdot y.re - x.re \cdot y.im}}\]
\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}
↓
\frac{1.0}{\frac{y.re \cdot y.re + y.im \cdot y.im}{x.im \cdot y.re - x.re \cdot y.im}}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1027162 = x_im;
        double r1027163 = y_re;
        double r1027164 = r1027162 * r1027163;
        double r1027165 = x_re;
        double r1027166 = y_im;
        double r1027167 = r1027165 * r1027166;
        double r1027168 = r1027164 - r1027167;
        double r1027169 = r1027163 * r1027163;
        double r1027170 = r1027166 * r1027166;
        double r1027171 = r1027169 + r1027170;
        double r1027172 = r1027168 / r1027171;
        return r1027172;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1027173 = 1.0;
        double r1027174 = y_re;
        double r1027175 = r1027174 * r1027174;
        double r1027176 = y_im;
        double r1027177 = r1027176 * r1027176;
        double r1027178 = r1027175 + r1027177;
        double r1027179 = x_im;
        double r1027180 = r1027179 * r1027174;
        double r1027181 = x_re;
        double r1027182 = r1027181 * r1027176;
        double r1027183 = r1027180 - r1027182;
        double r1027184 = r1027178 / r1027183;
        double r1027185 = r1027173 / r1027184;
        return r1027185;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Derivation

  1. Initial program 1.1

    \[\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
  2. Using strategy rm

  3. Applied p16-flip--2.0

    \[\leadsto \frac{\color{blue}{\left(\frac{\left(\left(\left(x.im \cdot y.re\right) \cdot \left(x.im \cdot y.re\right)\right) - \left(\left(x.re \cdot y.im\right) \cdot \left(x.re \cdot y.im\right)\right)\right)}{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}\right)}}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
  4. Using strategy rm

  5. Applied difference-of-squares1.9

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right) \cdot \left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)\right)}}{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]

  6. Applied associate-/l*1.1

    \[\leadsto \frac{\color{blue}{\left(\frac{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}{\left(\frac{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}\right)}\right)}}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
  7. Using strategy rm

  8. Applied associate-/r/1.1

    \[\leadsto \frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}\right) \cdot \left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)\right)}}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]

  9. Applied associate-/l*1.1

    \[\leadsto \color{blue}{\frac{\left(\frac{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}{\left(\frac{\left(x.im \cdot y.re\right)}{\left(x.re \cdot y.im\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}\right)}}\]

  10. Simplified1.1

    \[\leadsto \frac{\color{blue}{\left(1.0\right)}}{\left(\frac{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}\right)}\]

  11. Final simplification1.1

    \[\leadsto \frac{1.0}{\frac{y.re \cdot y.re + y.im \cdot y.im}{x.im \cdot y.re - x.re \cdot y.im}}\]

Reproduce

herbie shell --seed 2019124 +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  (/.p16 (-.p16 (*.p16 x.im y.re) (*.p16 x.re y.im)) (+.p16 (*.p16 y.re y.re) (*.p16 y.im y.im))))