Average Error: 1.1 → 1.1
Time: 10.7s
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 r1778153 = x_im;
        double r1778154 = y_re;
        double r1778155 = r1778153 * r1778154;
        double r1778156 = x_re;
        double r1778157 = y_im;
        double r1778158 = r1778156 * r1778157;
        double r1778159 = r1778155 - r1778158;
        double r1778160 = r1778154 * r1778154;
        double r1778161 = r1778157 * r1778157;
        double r1778162 = r1778160 + r1778161;
        double r1778163 = r1778159 / r1778162;
        return r1778163;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1778164 = 1.0;
        double r1778165 = y_re;
        double r1778166 = r1778165 * r1778165;
        double r1778167 = y_im;
        double r1778168 = r1778167 * r1778167;
        double r1778169 = r1778166 + r1778168;
        double r1778170 = x_im;
        double r1778171 = r1778170 * r1778165;
        double r1778172 = x_re;
        double r1778173 = r1778172 * r1778167;
        double r1778174 = r1778171 - r1778173;
        double r1778175 = r1778169 / r1778174;
        double r1778176 = r1778164 / r1778175;
        return r1778176;
}

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.1

    \[\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-squares2.0

    \[\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 2019104 +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))))