Average Error: 36.9 → 0.4
Time: 6.6s
Precision: 64
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\mathsf{fma}\left(\sin x, {\left({\left(\cos \varepsilon - 1\right)}^{2}\right)}^{\frac{1}{3}} \cdot \sqrt[3]{\cos \varepsilon - 1}, \cos x \cdot \sin \varepsilon\right) + \mathsf{fma}\left(-\sin x, 1, \sin x \cdot 1\right)\]
\sin \left(x + \varepsilon\right) - \sin x
↓
\mathsf{fma}\left(\sin x, {\left({\left(\cos \varepsilon - 1\right)}^{2}\right)}^{\frac{1}{3}} \cdot \sqrt[3]{\cos \varepsilon - 1}, \cos x \cdot \sin \varepsilon\right) + \mathsf{fma}\left(-\sin x, 1, \sin x \cdot 1\right)
double f(double x, double eps) {
        double r152127 = x;
        double r152128 = eps;
        double r152129 = r152127 + r152128;
        double r152130 = sin(r152129);
        double r152131 = sin(r152127);
        double r152132 = r152130 - r152131;
        return r152132;
}
↓
double f(double x, double eps) {
        double r152133 = x;
        double r152134 = sin(r152133);
        double r152135 = eps;
        double r152136 = cos(r152135);
        double r152137 = 1.0;
        double r152138 = r152136 - r152137;
        double r152139 = 2.0;
        double r152140 = pow(r152138, r152139);
        double r152141 = 0.3333333333333333;
        double r152142 = pow(r152140, r152141);
        double r152143 = cbrt(r152138);
        double r152144 = r152142 * r152143;
        double r152145 = cos(r152133);
        double r152146 = sin(r152135);
        double r152147 = r152145 * r152146;
        double r152148 = fma(r152134, r152144, r152147);
        double r152149 = -r152134;
        double r152150 = r152134 * r152137;
        double r152151 = fma(r152149, r152137, r152150);
        double r152152 = r152148 + r152151;
        return r152152;
}

Error

Bits error versus x

Bits error versus eps

Target

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

Derivation

  1. Initial program 36.9

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

  3. Applied sin-sum22.0

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

  4. Applied associate--l+22.0

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

  6. Applied *-un-lft-identity22.0

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

  7. Applied prod-diff22.0

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

  8. Applied associate-+r+22.0

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

  9. Simplified0.4

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

  11. Applied add-cube-cbrt0.5

    \[\leadsto \mathsf{fma}\left(\sin x, \color{blue}{\left(\sqrt[3]{\cos \varepsilon - 1} \cdot \sqrt[3]{\cos \varepsilon - 1}\right) \cdot \sqrt[3]{\cos \varepsilon - 1}}, \cos x \cdot \sin \varepsilon\right) + \mathsf{fma}\left(-\sin x, 1, \sin x \cdot 1\right)\]
  12. Using strategy rm

  13. Applied pow1/332.7

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

  14. Applied pow1/332.7

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

  15. Applied pow-prod-down0.4

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

  16. Simplified0.4

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

  17. Final simplification0.4

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

Reproduce

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

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

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