2cos (problem 3.3.5)

Average Error: 39.5 → 0.4

Time: 13.5s

Precision: 64

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

Math

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

↓

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

C

double f(double x, double eps) {
        double r51754 = x;
        double r51755 = eps;
        double r51756 = r51754 + r51755;
        double r51757 = cos(r51756);
        double r51758 = cos(r51754);
        double r51759 = r51757 - r51758;
        return r51759;
}

↓

double f(double x, double eps) {
        double r51760 = -2.0;
        double r51761 = x;
        double r51762 = cos(r51761);
        double r51763 = 0.5;
        double r51764 = eps;
        double r51765 = r51763 * r51764;
        double r51766 = sin(r51765);
        double r51767 = r51762 * r51766;
        double r51768 = sin(r51761);
        double r51769 = cos(r51765);
        double r51770 = r51768 * r51769;
        double r51771 = r51767 + r51770;
        double r51772 = r51771 * r51766;
        double r51773 = r51760 * r51772;
        return r51773;
}

Error

Bits error versus x

Bits error versus eps

Derivation

1. Initial program 39.5

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

3. Applied diff-cos 34.0

   \[\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 15.1

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

5. Taylor expanded around inf 15.1

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

7. Applied distribute-lft-in 15.1

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

8. Applied sin-sum 0.4

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

9. Simplified 0.4

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

10. Simplified 0.4

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

12. Applied +-commutative 0.4

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

13. Final simplification 0.4

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

Reproduce

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