_divideComplex, imaginary part

Average Error: 26.3 → 26.3

Time: 3.4s

Precision: 64

Math

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

↓

\[\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]

C

double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	return (((x_46_im * y_46_re) - (x_46_re * y_46_im)) / ((y_46_re * y_46_re) + (y_46_im * y_46_im)));
}

↓

double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	return ((1.0 / sqrt(((y_46_re * y_46_re) + (y_46_im * y_46_im)))) * (((x_46_im * y_46_re) - (x_46_re * y_46_im)) / sqrt(((y_46_re * y_46_re) + (y_46_im * y_46_im)))));
}

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 26.3

   \[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
2. Using strategy rm

3. Applied add-sqr-sqrt 26.3

   \[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]

4. Applied *-un-lft-identity 26.3

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

5. Applied times-frac 26.3

   \[\leadsto \color{blue}{\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]

6. Final simplification 26.3

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

Reproduce

herbie shell --seed 2020066 
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  :precision binary64
  (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))))