_multiplyComplex, real part

Average Error: 0.0 → 0.0

Time: 2.7s

Precision: 64

Math

\[x.re \cdot y.re - x.im \cdot y.im\]

↓

\[x.re \cdot y.re - x.im \cdot y.im\]

C

double f(double x_re, double x_im, double y_re, double y_im) {
        double r37662 = x_re;
        double r37663 = y_re;
        double r37664 = r37662 * r37663;
        double r37665 = x_im;
        double r37666 = y_im;
        double r37667 = r37665 * r37666;
        double r37668 = r37664 - r37667;
        return r37668;
}

↓

double f(double x_re, double x_im, double y_re, double y_im) {
        double r37669 = x_re;
        double r37670 = y_re;
        double r37671 = r37669 * r37670;
        double r37672 = x_im;
        double r37673 = y_im;
        double r37674 = r37672 * r37673;
        double r37675 = r37671 - r37674;
        return r37675;
}

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 0.0

   \[x.re \cdot y.re - x.im \cdot y.im\]
2. Using strategy rm

3. Applied flip-- 27.2

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

5. Applied *-un-lft-identity 27.2

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

6. Applied difference-of-squares 27.2

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

7. Applied times-frac 1.0

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

8. Simplified 1.0

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

9. Taylor expanded around inf 0.0

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

10. Simplified 0.0

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

11. Final simplification 0.0

    \[\leadsto x.re \cdot y.re - x.im \cdot y.im\]

Reproduce

herbie shell --seed 2019353 
(FPCore (x.re x.im y.re y.im)
  :name "_multiplyComplex, real part"
  :precision binary64
  (- (* x.re y.re) (* x.im y.im)))