Average Error: 36.1 → 0.3
Time: 18.8s
Precision: 64
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[2 \cdot \left(\mathsf{fma}\left(\cos \left(\frac{1}{2} \cdot \varepsilon\right), \cos x, -\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin x\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]
\sin \left(x + \varepsilon\right) - \sin x
↓
2 \cdot \left(\mathsf{fma}\left(\cos \left(\frac{1}{2} \cdot \varepsilon\right), \cos x, -\sin \left(\frac{1}{2} \cdot \varepsilon\right) \cdot \sin x\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)
double f(double x, double eps) {
        double r4016297 = x;
        double r4016298 = eps;
        double r4016299 = r4016297 + r4016298;
        double r4016300 = sin(r4016299);
        double r4016301 = sin(r4016297);
        double r4016302 = r4016300 - r4016301;
        return r4016302;
}
↓
double f(double x, double eps) {
        double r4016303 = 2.0;
        double r4016304 = 0.5;
        double r4016305 = eps;
        double r4016306 = r4016304 * r4016305;
        double r4016307 = cos(r4016306);
        double r4016308 = x;
        double r4016309 = cos(r4016308);
        double r4016310 = sin(r4016306);
        double r4016311 = sin(r4016308);
        double r4016312 = r4016310 * r4016311;
        double r4016313 = -r4016312;
        double r4016314 = fma(r4016307, r4016309, r4016313);
        double r4016315 = r4016305 / r4016303;
        double r4016316 = sin(r4016315);
        double r4016317 = r4016314 * r4016316;
        double r4016318 = r4016303 * r4016317;
        return r4016318;
}

Error

Bits error versus x

Bits error versus eps

Target

Original36.1
Target14.2
Herbie0.3
\[2 \cdot \left(\cos \left(x + \frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]

Derivation

  1. Initial program 36.1

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

  3. Applied diff-sin36.4

    \[\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. Simplified14.2

    \[\leadsto 2 \cdot \color{blue}{\left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \cos \left(\frac{\mathsf{fma}\left(2, x, \varepsilon\right)}{2}\right)\right)}\]

  5. Taylor expanded around inf 14.2

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

  6. Simplified14.2

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

  8. Applied fma-udef14.2

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

  9. Applied cos-sum0.3

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

  11. Applied fma-neg0.3

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

  12. Final simplification0.3

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

Reproduce

herbie shell --seed 2019158 +o rules:numerics
(FPCore (x eps)
  :name "2sin (example 3.3)"

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

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