2sin (example 3.3)

Average Error: 37.2 → 1.4

Time: 6.9s

Precision: binary64

Math

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

↓

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

C

double code(double x, double eps) {
	return ((double) (((double) sin(((double) (x + eps)))) - ((double) sin(x))));
}

↓

double code(double x, double eps) {
	return ((double) (2.0 * ((double) (((double) (((double) cbrt(((double) sin(((double) (eps * 0.5)))))) * ((double) cbrt(((double) sin(((double) (eps * 0.5)))))))) * ((double) (((double) cbrt(((double) sin(((double) (eps * 0.5)))))) * ((double) (((double) (((double) cos(x)) * ((double) cos(((double) (eps * 0.5)))))) - ((double) (((double) sin(((double) (eps * 0.5)))) * ((double) sin(x))))))))))));
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.2
Target	15.3
Herbie	1.4

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

Derivation

1. Initial program 37.2

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

3. Applied diff-sin 37.5

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

4. Simplified 15.3

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

6. Applied add-cube-cbrt 16.2

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

7. Applied associate-*l* 16.2

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

8. Simplified 16.2

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

10. Applied cos-sum 1.4

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

11. Final simplification 1.4

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

Reproduce

herbie shell --seed 2020184 
(FPCore (x eps)
  :name "2sin (example 3.3)"
  :precision binary64

  :herbie-target
  (* 2.0 (* (cos (+ x (/ eps 2.0))) (sin (/ eps 2.0))))

  (- (sin (+ x eps)) (sin x)))