2cos (problem 3.3.5)

Average Error: 39.8 → 0.9

Time: 16.5s

Precision: 64

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

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -9.63544918678768572 \cdot 10^{-4} \lor \neg \left(\varepsilon \le 95617.0838819038909\right):\\ \;\;\;\;\cos x \cdot \cos \varepsilon - \mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(-2 \cdot \sin \left(\frac{\varepsilon}{2}\right)\right) \cdot \sin \left(\frac{\mathsf{fma}\left(x, 2, \varepsilon\right)}{2}\right)\\ \end{array}\]

C

double f(double x, double eps) {
        double r53355 = x;
        double r53356 = eps;
        double r53357 = r53355 + r53356;
        double r53358 = cos(r53357);
        double r53359 = cos(r53355);
        double r53360 = r53358 - r53359;
        return r53360;
}

↓

double f(double x, double eps) {
        double r53361 = eps;
        double r53362 = -0.0009635449186787686;
        bool r53363 = r53361 <= r53362;
        double r53364 = 95617.08388190389;
        bool r53365 = r53361 <= r53364;
        double r53366 = !r53365;
        bool r53367 = r53363 || r53366;
        double r53368 = x;
        double r53369 = cos(r53368);
        double r53370 = cos(r53361);
        double r53371 = r53369 * r53370;
        double r53372 = sin(r53368);
        double r53373 = sin(r53361);
        double r53374 = fma(r53372, r53373, r53369);
        double r53375 = r53371 - r53374;
        double r53376 = -2.0;
        double r53377 = 2.0;
        double r53378 = r53361 / r53377;
        double r53379 = sin(r53378);
        double r53380 = r53376 * r53379;
        double r53381 = fma(r53368, r53377, r53361);
        double r53382 = r53381 / r53377;
        double r53383 = sin(r53382);
        double r53384 = r53380 * r53383;
        double r53385 = r53367 ? r53375 : r53384;
        return r53385;
}

Error

Bits error versus x

Bits error versus eps

Derivation

1. Split input into 2 regimes

2. if eps < -0.0009635449186787686 or 95617.08388190389 < eps

   1. Initial program 30.3

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

   3. Applied cos-sum 0.8

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

   4. Applied associate--l- 0.8

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

   5. Simplified 0.8

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

   if -0.0009635449186787686 < eps < 95617.08388190389

   1. Initial program 49.5

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

   3. Applied diff-cos 38.6

      \[\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. Simplified 1.0

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

   6. Applied pow1 1.0

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

   7. Applied pow1 1.0

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

   8. Applied pow-prod-down 1.0

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

   9. Applied pow1 1.0

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

   10. Applied pow-prod-down 1.0

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

   11. Simplified 1.0

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

4. Final simplification 0.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -9.63544918678768572 \cdot 10^{-4} \lor \neg \left(\varepsilon \le 95617.0838819038909\right):\\ \;\;\;\;\cos x \cdot \cos \varepsilon - \mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(-2 \cdot \sin \left(\frac{\varepsilon}{2}\right)\right) \cdot \sin \left(\frac{\mathsf{fma}\left(x, 2, \varepsilon\right)}{2}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020043 +o rules:numerics
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))