2cos (problem 3.3.5)

Average Error: 39.4 → 16.2

Time: 8.6s

Precision: 64

Math

\[\cos \left(x + \varepsilon\right) - \cos x\]

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.6681134187816791 \cdot 10^{-13}:\\ \;\;\;\;\cos x \cdot \cos \varepsilon + \log \left(e^{\left(-\sin x \cdot \sin \varepsilon\right) - \cos x}\right)\\ \mathbf{elif}\;\varepsilon \le 3.4911106815067981 \cdot 10^{-10}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} + {\left(\cos x\right)}^{3}\right)}{\left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos \varepsilon \cdot \cos x\right) + {\left(\cos \varepsilon\right)}^{2} \cdot {\left(\cos x\right)}^{2}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{2} + \cos x \cdot \left(\cos x - \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)\right)\right)} + \cos x \cdot \cos x}\\ \end{array}\]

C

double f(double x, double eps) {
        double r69892 = x;
        double r69893 = eps;
        double r69894 = r69892 + r69893;
        double r69895 = cos(r69894);
        double r69896 = cos(r69892);
        double r69897 = r69895 - r69896;
        return r69897;
}

↓

double f(double x, double eps) {
        double r69898 = eps;
        double r69899 = -8.668113418781679e-13;
        bool r69900 = r69898 <= r69899;
        double r69901 = x;
        double r69902 = cos(r69901);
        double r69903 = cos(r69898);
        double r69904 = r69902 * r69903;
        double r69905 = sin(r69901);
        double r69906 = sin(r69898);
        double r69907 = r69905 * r69906;
        double r69908 = -r69907;
        double r69909 = r69908 - r69902;
        double r69910 = exp(r69909);
        double r69911 = log(r69910);
        double r69912 = r69904 + r69911;
        double r69913 = 3.491110681506798e-10;
        bool r69914 = r69898 <= r69913;
        double r69915 = 0.16666666666666666;
        double r69916 = 3.0;
        double r69917 = pow(r69901, r69916);
        double r69918 = r69915 * r69917;
        double r69919 = r69918 - r69901;
        double r69920 = 0.5;
        double r69921 = r69898 * r69920;
        double r69922 = r69919 - r69921;
        double r69923 = r69898 * r69922;
        double r69924 = r69904 - r69907;
        double r69925 = pow(r69924, r69916);
        double r69926 = pow(r69902, r69916);
        double r69927 = r69925 - r69926;
        double r69928 = r69903 * r69902;
        double r69929 = pow(r69928, r69916);
        double r69930 = pow(r69907, r69916);
        double r69931 = r69929 - r69930;
        double r69932 = r69925 + r69926;
        double r69933 = r69931 * r69932;
        double r69934 = r69907 + r69928;
        double r69935 = r69907 * r69934;
        double r69936 = 2.0;
        double r69937 = pow(r69903, r69936);
        double r69938 = pow(r69902, r69936);
        double r69939 = r69937 * r69938;
        double r69940 = r69935 + r69939;
        double r69941 = pow(r69924, r69936);
        double r69942 = r69902 - r69924;
        double r69943 = r69902 * r69942;
        double r69944 = r69941 + r69943;
        double r69945 = r69940 * r69944;
        double r69946 = r69933 / r69945;
        double r69947 = r69902 * r69902;
        double r69948 = r69946 + r69947;
        double r69949 = r69927 / r69948;
        double r69950 = r69914 ? r69923 : r69949;
        double r69951 = r69900 ? r69912 : r69950;
        return r69951;
}

Error

Bits error versus x

Bits error versus eps

Derivation

1. Split input into 3 regimes

2. if eps < -8.668113418781679e-13

   1. Initial program 31.0

      \[\cos \left(x + \varepsilon\right) - \cos x\]
   2. Using strategy rm

   3. Applied cos-sum 1.7

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
   4. Using strategy rm

   5. Applied sub-neg 1.7

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon + \left(-\sin x \cdot \sin \varepsilon\right)\right)} - \cos x\]

   6. Applied associate--l+ 1.7

      \[\leadsto \color{blue}{\cos x \cdot \cos \varepsilon + \left(\left(-\sin x \cdot \sin \varepsilon\right) - \cos x\right)}\]
   7. Using strategy rm

   8. Applied add-log-exp 1.8

      \[\leadsto \cos x \cdot \cos \varepsilon + \left(\left(-\sin x \cdot \sin \varepsilon\right) - \color{blue}{\log \left(e^{\cos x}\right)}\right)\]

   9. Applied add-log-exp 1.9

      \[\leadsto \cos x \cdot \cos \varepsilon + \left(\left(-\color{blue}{\log \left(e^{\sin x \cdot \sin \varepsilon}\right)}\right) - \log \left(e^{\cos x}\right)\right)\]

   10. Applied neg-log 1.9

       \[\leadsto \cos x \cdot \cos \varepsilon + \left(\color{blue}{\log \left(\frac{1}{e^{\sin x \cdot \sin \varepsilon}}\right)} - \log \left(e^{\cos x}\right)\right)\]

   11. Applied diff-log 2.0

       \[\leadsto \cos x \cdot \cos \varepsilon + \color{blue}{\log \left(\frac{\frac{1}{e^{\sin x \cdot \sin \varepsilon}}}{e^{\cos x}}\right)}\]

   12. Simplified 1.8

       \[\leadsto \cos x \cdot \cos \varepsilon + \log \color{blue}{\left(e^{\left(-\sin x \cdot \sin \varepsilon\right) - \cos x}\right)}\]

   if -8.668113418781679e-13 < eps < 3.491110681506798e-10

   1. Initial program 48.2

      \[\cos \left(x + \varepsilon\right) - \cos x\]

   2. Taylor expanded around 0 31.2

      \[\leadsto \color{blue}{\frac{1}{6} \cdot \left({x}^{3} \cdot \varepsilon\right) - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)}\]

   3. Simplified 31.2

      \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)}\]

   if 3.491110681506798e-10 < eps

   1. Initial program 30.7

      \[\cos \left(x + \varepsilon\right) - \cos x\]
   2. Using strategy rm

   3. Applied cos-sum 1.3

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
   4. Using strategy rm

   5. Applied flip3-- 1.5

      \[\leadsto \color{blue}{\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \left(\cos x \cdot \cos x + \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \cos x\right)}}\]

   6. Simplified 1.5

      \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x\right) + \cos x \cdot \cos x}}\]
   7. Using strategy rm

   8. Applied flip3-+ 1.6

      \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \color{blue}{\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} + {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \left(\cos x \cdot \cos x - \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \cos x\right)}} + \cos x \cdot \cos x}\]

   9. Applied flip3-- 1.6

      \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\frac{{\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right) + \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)}} \cdot \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} + {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \left(\cos x \cdot \cos x - \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \cos x\right)} + \cos x \cdot \cos x}\]

   10. Applied frac-times 1.6

       \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} + {\left(\cos x\right)}^{3}\right)}{\left(\left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right) + \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \left(\cos x \cdot \cos x - \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \cos x\right)\right)}} + \cos x \cdot \cos x}\]

   11. Simplified 1.6

       \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} + {\left(\cos x\right)}^{3}\right)}{\color{blue}{\left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos \varepsilon \cdot \cos x\right) + {\left(\cos \varepsilon\right)}^{2} \cdot {\left(\cos x\right)}^{2}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{2} + \cos x \cdot \left(\cos x - \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)\right)\right)}} + \cos x \cdot \cos x}\]
3. Recombined 3 regimes into one program.

4. Final simplification 16.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -8.6681134187816791 \cdot 10^{-13}:\\ \;\;\;\;\cos x \cdot \cos \varepsilon + \log \left(e^{\left(-\sin x \cdot \sin \varepsilon\right) - \cos x}\right)\\ \mathbf{elif}\;\varepsilon \le 3.4911106815067981 \cdot 10^{-10}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} + {\left(\cos x\right)}^{3}\right)}{\left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos \varepsilon \cdot \cos x\right) + {\left(\cos \varepsilon\right)}^{2} \cdot {\left(\cos x\right)}^{2}\right) \cdot \left({\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{2} + \cos x \cdot \left(\cos x - \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)\right)\right)} + \cos x \cdot \cos x}\\ \end{array}\]

Reproduce

herbie shell --seed 2020039 
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))