Migdal et al, Equation (64)

Average Error: 0.5 → 0.4

Time: 13.9s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]

↓

\[\frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\left(\frac{\cos th}{\sqrt{\left|\sqrt[3]{2}\right|}} \cdot \frac{\frac{1}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{\sqrt[3]{2}}}}\right) \cdot a2\right) \cdot a2\]

C

double f(double a1, double a2, double th) {
        double r85830 = th;
        double r85831 = cos(r85830);
        double r85832 = 2.0;
        double r85833 = sqrt(r85832);
        double r85834 = r85831 / r85833;
        double r85835 = a1;
        double r85836 = r85835 * r85835;
        double r85837 = r85834 * r85836;
        double r85838 = a2;
        double r85839 = r85838 * r85838;
        double r85840 = r85834 * r85839;
        double r85841 = r85837 + r85840;
        return r85841;
}

↓

double f(double a1, double a2, double th) {
        double r85842 = th;
        double r85843 = cos(r85842);
        double r85844 = 2.0;
        double r85845 = sqrt(r85844);
        double r85846 = sqrt(r85845);
        double r85847 = r85843 / r85846;
        double r85848 = r85847 / r85846;
        double r85849 = a1;
        double r85850 = r85849 * r85849;
        double r85851 = r85848 * r85850;
        double r85852 = cbrt(r85844);
        double r85853 = fabs(r85852);
        double r85854 = sqrt(r85853);
        double r85855 = r85843 / r85854;
        double r85856 = 1.0;
        double r85857 = r85856 / r85846;
        double r85858 = sqrt(r85852);
        double r85859 = sqrt(r85858);
        double r85860 = r85857 / r85859;
        double r85861 = r85855 * r85860;
        double r85862 = a2;
        double r85863 = r85861 * r85862;
        double r85864 = r85863 * r85862;
        double r85865 = r85851 + r85864;
        return r85865;
}

Error

Bits error versus a1

Bits error versus a2

Bits error versus th

Derivation

1. Initial program 0.5

   \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]
2. Using strategy rm

3. Applied add-sqr-sqrt 0.5

   \[\leadsto \frac{\cos th}{\sqrt{\color{blue}{\sqrt{2} \cdot \sqrt{2}}}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]

4. Applied sqrt-prod 0.5

   \[\leadsto \frac{\cos th}{\color{blue}{\sqrt{\sqrt{2}} \cdot \sqrt{\sqrt{2}}}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]

5. Applied associate-/r* 0.5

   \[\leadsto \color{blue}{\frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]
6. Using strategy rm

7. Applied associate-*r* 0.5

   \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \color{blue}{\left(\frac{\cos th}{\sqrt{2}} \cdot a2\right) \cdot a2}\]
8. Using strategy rm

9. Applied add-sqr-sqrt 0.5

   \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\frac{\cos th}{\sqrt{\color{blue}{\sqrt{2} \cdot \sqrt{2}}}} \cdot a2\right) \cdot a2\]

10. Applied sqrt-prod 0.5

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\frac{\cos th}{\color{blue}{\sqrt{\sqrt{2}} \cdot \sqrt{\sqrt{2}}}} \cdot a2\right) \cdot a2\]

11. Applied associate-/r* 0.5

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\color{blue}{\frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}}} \cdot a2\right) \cdot a2\]
12. Using strategy rm

13. Applied add-cube-cbrt 0.5

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{\color{blue}{\left(\sqrt[3]{2} \cdot \sqrt[3]{2}\right) \cdot \sqrt[3]{2}}}}} \cdot a2\right) \cdot a2\]

14. Applied sqrt-prod 0.5

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\color{blue}{\sqrt{\sqrt[3]{2} \cdot \sqrt[3]{2}} \cdot \sqrt{\sqrt[3]{2}}}}} \cdot a2\right) \cdot a2\]

15. Applied sqrt-prod 0.5

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\color{blue}{\sqrt{\sqrt{\sqrt[3]{2} \cdot \sqrt[3]{2}}} \cdot \sqrt{\sqrt{\sqrt[3]{2}}}}} \cdot a2\right) \cdot a2\]

16. Applied div-inv 0.5

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\frac{\color{blue}{\cos th \cdot \frac{1}{\sqrt{\sqrt{2}}}}}{\sqrt{\sqrt{\sqrt[3]{2} \cdot \sqrt[3]{2}}} \cdot \sqrt{\sqrt{\sqrt[3]{2}}}} \cdot a2\right) \cdot a2\]

17. Applied times-frac 0.4

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\color{blue}{\left(\frac{\cos th}{\sqrt{\sqrt{\sqrt[3]{2} \cdot \sqrt[3]{2}}}} \cdot \frac{\frac{1}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{\sqrt[3]{2}}}}\right)} \cdot a2\right) \cdot a2\]

18. Simplified 0.4

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\left(\color{blue}{\frac{\cos th}{\sqrt{\left|\sqrt[3]{2}\right|}}} \cdot \frac{\frac{1}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{\sqrt[3]{2}}}}\right) \cdot a2\right) \cdot a2\]

19. Final simplification 0.4

    \[\leadsto \frac{\frac{\cos th}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{2}}} \cdot \left(a1 \cdot a1\right) + \left(\left(\frac{\cos th}{\sqrt{\left|\sqrt[3]{2}\right|}} \cdot \frac{\frac{1}{\sqrt{\sqrt{2}}}}{\sqrt{\sqrt{\sqrt[3]{2}}}}\right) \cdot a2\right) \cdot a2\]

Reproduce

herbie shell --seed 2020045 +o rules:numerics
(FPCore (a1 a2 th)
  :name "Migdal et al, Equation (64)"
  :precision binary64
  (+ (* (/ (cos th) (sqrt 2)) (* a1 a1)) (* (/ (cos th) (sqrt 2)) (* a2 a2))))