Average Error: 39.6 → 1.2
Time: 5.9s
Precision: binary64
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;x \leq -2.320785422446366 \cdot 10^{-124} \lor \neg \left(x \leq 6.203423099167994 \cdot 10^{-72}\right):\\ \;\;\;\;-2 \cdot \left(\sin x \cdot \left(\cos \left(\varepsilon \cdot 0.5\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right) + \cos x \cdot \sqrt[3]{{\left({\left(\sin \left(\varepsilon \cdot 0.5\right)\right)}^{2}\right)}^{3}}\right)\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \left(\sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)} \cdot \sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)}\right)\\ \end{array}\]
\cos \left(x + \varepsilon\right) - \cos x
↓
\begin{array}{l}
\mathbf{if}\;x \leq -2.320785422446366 \cdot 10^{-124} \lor \neg \left(x \leq 6.203423099167994 \cdot 10^{-72}\right):\\
\;\;\;\;-2 \cdot \left(\sin x \cdot \left(\cos \left(\varepsilon \cdot 0.5\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right) + \cos x \cdot \sqrt[3]{{\left({\left(\sin \left(\varepsilon \cdot 0.5\right)\right)}^{2}\right)}^{3}}\right)\\

\mathbf{else}:\\
\;\;\;\;-2 \cdot \left(\sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)} \cdot \sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)}\right)\\

\end{array}
double code(double x, double eps) {
	return ((double) (((double) cos(((double) (x + eps)))) - ((double) cos(x))));
}
↓
double code(double x, double eps) {
	double VAR;
	if (((x <= -2.320785422446366e-124) || !(x <= 6.203423099167994e-72))) {
		VAR = ((double) (-2.0 * ((double) (((double) (((double) sin(x)) * ((double) (((double) cos(((double) (eps * 0.5)))) * ((double) sin((eps / 2.0))))))) + ((double) (((double) cos(x)) * ((double) cbrt(((double) pow(((double) pow(((double) sin(((double) (eps * 0.5)))), 2.0)), 3.0))))))))));
	} else {
		VAR = ((double) (-2.0 * ((double) (((double) sqrt(((double) (((double) sin((eps / 2.0))) * ((double) sin(((double) (x + ((double) (eps * 0.5)))))))))) * ((double) sqrt(((double) (((double) sin((eps / 2.0))) * ((double) sin(((double) (x + ((double) (eps * 0.5))))))))))))));
	}
	return VAR;
}

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 2 regimes

  2. if x < -2.3207854224463659e-124 or 6.20342309916799379e-72 < x

    1. Initial program Error: 51.4 bits

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

    3. Applied diff-cosError: 50.4 bits

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

    4. SimplifiedError: 22.3 bits

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

    5. Taylor expanded around inf Error: 22.2 bits

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

    6. SimplifiedError: 22.2 bits

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

    8. Applied sin-sumError: 0.4 bits

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

    9. Applied distribute-lft-inError: 0.4 bits

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

    10. SimplifiedError: 0.4 bits

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

    11. SimplifiedError: 0.4 bits

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

    13. Applied add-cbrt-cubeError: 0.5 bits

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

    14. Applied add-cbrt-cubeError: 0.7 bits

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

    15. Applied cbrt-unprodError: 0.9 bits

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

    16. SimplifiedError: 0.9 bits

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

    if -2.3207854224463659e-124 < x < 6.20342309916799379e-72

    1. Initial program Error: 16.6 bits

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

    3. Applied diff-cosError: 2.1 bits

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

    4. SimplifiedError: 0.3 bits

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

    5. Taylor expanded around inf Error: 0.3 bits

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

    6. SimplifiedError: 0.3 bits

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

    8. Applied add-sqr-sqrtError: 1.8 bits

      \[\leadsto -2 \cdot \color{blue}{\left(\sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)} \cdot \sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)}\right)}\]

    9. SimplifiedError: 1.8 bits

      \[\leadsto -2 \cdot \left(\color{blue}{\sqrt{\sin \left(x + \varepsilon \cdot 0.5\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)}} \cdot \sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)}\right)\]

    10. SimplifiedError: 1.8 bits

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

  4. Final simplificationError: 1.2 bits

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -2.320785422446366 \cdot 10^{-124} \lor \neg \left(x \leq 6.203423099167994 \cdot 10^{-72}\right):\\ \;\;\;\;-2 \cdot \left(\sin x \cdot \left(\cos \left(\varepsilon \cdot 0.5\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right) + \cos x \cdot \sqrt[3]{{\left({\left(\sin \left(\varepsilon \cdot 0.5\right)\right)}^{2}\right)}^{3}}\right)\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \left(\sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)} \cdot \sqrt{\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(x + \varepsilon \cdot 0.5\right)}\right)\\ \end{array}\]

Reproduce

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