2sin (example 3.3)

Average Error: 37.1 → 0.4

Time: 8.7s

Precision: binary64

Cost: 26176

Math

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

↓

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

FPCore

(FPCore (x eps) :precision binary64 (- (sin (+ x eps)) (sin x)))

↓

(FPCore (x eps)
 :precision binary64
 (+ (* (sin eps) (cos x)) (* (sin x) (+ (cos eps) -1.0))))

C

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

↓

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

Error

Bits error versus x

Bits error versus eps

Target

Original	37.1
Target	15.1
Herbie	0.4

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

Alternatives

Alternative 1
Error	1.6
Cost	123968

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

Alternative 2
Error	1.6
Cost	136768

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

Alternative 3
Error	1.9
Cost	182336

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

Alternative 4
Error	21.6
Cost	182592

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

Derivation

1. Initial program 37.1

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

3. Applied sin-sum_binary64_2257 21.8

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

4. Taylor expanded around inf 21.8

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

5. Simplified 0.4

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

6. Simplified 0.4

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

7. Final simplification 0.4

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

Reproduce

herbie shell --seed 2021043 
(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)))