Average Error: 39.4 → 16.0
Time: 8.6s
Precision: 64
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.38475982226319313 \cdot 10^{-20}:\\ \;\;\;\;\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right) - \left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right) \cdot \frac{1}{\cos x \cdot \cos \varepsilon + \sin x \cdot \sin \varepsilon} - \cos x\\ \mathbf{elif}\;\varepsilon \le 1.04788299952919091 \cdot 10^{-7}:\\ \;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x}\right)\\ \end{array}\]
\cos \left(x + \varepsilon\right) - \cos x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.38475982226319313 \cdot 10^{-20}:\\
\;\;\;\;\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right) - \left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right) \cdot \frac{1}{\cos x \cdot \cos \varepsilon + \sin x \cdot \sin \varepsilon} - \cos x\\

\mathbf{elif}\;\varepsilon \le 1.04788299952919091 \cdot 10^{-7}:\\
\;\;\;\;\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {x}^{3} - x\right) - \varepsilon \cdot \frac{1}{2}\right)\\

\mathbf{else}:\\
\;\;\;\;\log \left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x}\right)\\

\end{array}
double f(double x, double eps) {
        double r34855 = x;
        double r34856 = eps;
        double r34857 = r34855 + r34856;
        double r34858 = cos(r34857);
        double r34859 = cos(r34855);
        double r34860 = r34858 - r34859;
        return r34860;
}
↓
double f(double x, double eps) {
        double r34861 = eps;
        double r34862 = -2.384759822263193e-20;
        bool r34863 = r34861 <= r34862;
        double r34864 = x;
        double r34865 = cos(r34864);
        double r34866 = cos(r34861);
        double r34867 = r34865 * r34866;
        double r34868 = r34867 * r34867;
        double r34869 = sin(r34864);
        double r34870 = sin(r34861);
        double r34871 = r34869 * r34870;
        double r34872 = r34871 * r34871;
        double r34873 = r34868 - r34872;
        double r34874 = 1.0;
        double r34875 = r34867 + r34871;
        double r34876 = r34874 / r34875;
        double r34877 = r34873 * r34876;
        double r34878 = r34877 - r34865;
        double r34879 = 1.0478829995291909e-07;
        bool r34880 = r34861 <= r34879;
        double r34881 = 0.16666666666666666;
        double r34882 = 3.0;
        double r34883 = pow(r34864, r34882);
        double r34884 = r34881 * r34883;
        double r34885 = r34884 - r34864;
        double r34886 = 0.5;
        double r34887 = r34861 * r34886;
        double r34888 = r34885 - r34887;
        double r34889 = r34861 * r34888;
        double r34890 = r34867 - r34871;
        double r34891 = r34890 - r34865;
        double r34892 = exp(r34891);
        double r34893 = log(r34892);
        double r34894 = r34880 ? r34889 : r34893;
        double r34895 = r34863 ? r34878 : r34894;
        return r34895;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.384759822263193e-20

    1. Initial program 31.5

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

    3. Applied cos-sum3.1

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

    5. Applied flip--3.2

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

    7. Applied div-inv3.3

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

    if -2.384759822263193e-20 < eps < 1.0478829995291909e-07

    1. Initial program 49.2

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

    2. Taylor expanded around 0 31.4

      \[\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. Simplified31.4

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

    if 1.0478829995291909e-07 < eps

    1. Initial program 29.9

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

    3. Applied cos-sum1.1

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

    5. Applied add-log-exp1.2

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

    6. Applied add-log-exp1.3

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

    7. Applied add-log-exp1.5

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

    8. Applied diff-log1.5

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

    9. Applied diff-log1.5

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

    10. Simplified1.2

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

  4. Final simplification16.0

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

Reproduce

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