Average Error: 37.0 → 0.9
Time: 41.7s
Precision: 64
Internal Precision: 2368
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\begin{array}{l}
\mathbf{if}\;2 \cdot \left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \cos \left(\frac{x + \left(\varepsilon + x\right)}{2}\right)\right) \le -1.1689293128864387 \cdot 10^{-09}:\\
\;\;\;\;\sin x \cdot \cos \varepsilon + \left(\cos x \cdot \sin \varepsilon - \sin x\right)\\
\mathbf{if}\;2 \cdot \left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \cos \left(\frac{x + \left(\varepsilon + x\right)}{2}\right)\right) \le 1.790649928787888 \cdot 10^{-29}:\\
\;\;\;\;2 \cdot \left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \cos \left(\frac{x + \left(\varepsilon + x\right)}{2}\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x\\
\end{array}\]
Try it out
Enter valid numbers for all inputs
Target
| Original | 37.0 |
|---|
| Target | 15.3 |
|---|
| Herbie | 0.9 |
|---|
\[2 \cdot \left(\cos \left(x + \frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]
Derivation
- Split input into 3 regimes
if (* 2 (* (sin (/ eps 2)) (cos (/ (+ x (+ eps x)) 2)))) < -1.1689293128864387e-09
Initial program 29.9
\[\sin \left(x + \varepsilon\right) - \sin x\]
- Using strategy
rm Applied sin-sum0.5
\[\leadsto \color{blue}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - \sin x\]
Applied associate--l+0.5
\[\leadsto \color{blue}{\sin x \cdot \cos \varepsilon + \left(\cos x \cdot \sin \varepsilon - \sin x\right)}\]
if -1.1689293128864387e-09 < (* 2 (* (sin (/ eps 2)) (cos (/ (+ x (+ eps x)) 2)))) < 1.790649928787888e-29
Initial program 44.1
\[\sin \left(x + \varepsilon\right) - \sin x\]
- Using strategy
rm Applied diff-sin44.1
\[\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)}\]
Applied simplify0.2
\[\leadsto 2 \cdot \color{blue}{\left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \cos \left(\frac{x + \left(\varepsilon + x\right)}{2}\right)\right)}\]
if 1.790649928787888e-29 < (* 2 (* (sin (/ eps 2)) (cos (/ (+ x (+ eps x)) 2))))
Initial program 31.3
\[\sin \left(x + \varepsilon\right) - \sin x\]
- Using strategy
rm Applied sin-sum2.5
\[\leadsto \color{blue}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - \sin x\]
- Recombined 3 regimes into one program.
Runtime
herbie shell --seed 2018199
(FPCore (x eps)
:name "2sin (example 3.3)"
:herbie-target
(* 2 (* (cos (+ x (/ eps 2))) (sin (/ eps 2))))
(- (sin (+ x eps)) (sin x)))