Average Error: 37.3 → 15.2
Time: 1.6m
Precision: 64
Internal Precision: 2368
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon - \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot x\right) + \left(\varepsilon \cdot {x}^{2}\right) \cdot \frac{1}{2}\right) \le -2.0851602488011864 \cdot 10^{-45}:\\ \;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin x \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x \cdot \sin x\right) + \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}\\ \mathbf{elif}\;\varepsilon - \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot x\right) + \left(\varepsilon \cdot {x}^{2}\right) \cdot \frac{1}{2}\right) \le 1.1136541482848599 \cdot 10^{-08}:\\ \;\;\;\;\varepsilon - \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot x\right) + \left(\varepsilon \cdot {x}^{2}\right) \cdot \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin x \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x \cdot \sin x\right) + \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original37.3
Target15.2
Herbie15.2
\[2 \cdot \left(\cos \left(x + \frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]

Derivation

  1. Split input into 2 regimes

  2. if (- eps (+ (* 1/2 (* eps (pow x 2))) (* 1/2 (* (pow eps 2) x)))) < -2.0851602488011864e-45 or 1.1136541482848599e-08 < (- eps (+ (* 1/2 (* eps (pow x 2))) (* 1/2 (* (pow eps 2) x))))

    1. Initial program 37.8

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

    3. Applied sin-sum16.5

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

    5. Applied flip3--16.7

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

    if -2.0851602488011864e-45 < (- eps (+ (* 1/2 (* eps (pow x 2))) (* 1/2 (* (pow eps 2) x)))) < 1.1136541482848599e-08

    1. Initial program 36.1

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

    2. Taylor expanded around 0 11.2

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

  4. Final simplification15.2

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon - \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot x\right) + \left(\varepsilon \cdot {x}^{2}\right) \cdot \frac{1}{2}\right) \le -2.0851602488011864 \cdot 10^{-45}:\\ \;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin x \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x \cdot \sin x\right) + \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}\\ \mathbf{elif}\;\varepsilon - \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot x\right) + \left(\varepsilon \cdot {x}^{2}\right) \cdot \frac{1}{2}\right) \le 1.1136541482848599 \cdot 10^{-08}:\\ \;\;\;\;\varepsilon - \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot x\right) + \left(\varepsilon \cdot {x}^{2}\right) \cdot \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin x \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x \cdot \sin x\right) + \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}\\ \end{array}\]

Runtime

Time bar (total: 1.6m)Debug logProfile

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

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

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