Average Error: 36.7 → 0.2
Time: 6.1s
Precision: 64
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\sin x \cdot \left(\left(-\sin \varepsilon\right) \cdot \tan \left(\frac{\varepsilon}{2}\right)\right) + \cos x \cdot \sin \varepsilon\]
\sin \left(x + \varepsilon\right) - \sin x
↓
\sin x \cdot \left(\left(-\sin \varepsilon\right) \cdot \tan \left(\frac{\varepsilon}{2}\right)\right) + \cos x \cdot \sin \varepsilon
double f(double x, double eps) {
        double r98113 = x;
        double r98114 = eps;
        double r98115 = r98113 + r98114;
        double r98116 = sin(r98115);
        double r98117 = sin(r98113);
        double r98118 = r98116 - r98117;
        return r98118;
}
↓
double f(double x, double eps) {
        double r98119 = x;
        double r98120 = sin(r98119);
        double r98121 = eps;
        double r98122 = sin(r98121);
        double r98123 = -r98122;
        double r98124 = 2.0;
        double r98125 = r98121 / r98124;
        double r98126 = tan(r98125);
        double r98127 = r98123 * r98126;
        double r98128 = r98120 * r98127;
        double r98129 = cos(r98119);
        double r98130 = r98129 * r98122;
        double r98131 = r98128 + r98130;
        return r98131;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original36.7
Target15.0
Herbie0.2
\[2 \cdot \left(\cos \left(x + \frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]

Derivation

  1. Initial program 36.7

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

  3. Applied sin-sum21.5

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

  5. Applied *-un-lft-identity21.5

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

  6. Applied *-un-lft-identity21.5

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

  7. Applied distribute-lft-out--21.5

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

  8. Simplified0.4

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

  10. Applied flip--0.5

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

  11. Simplified0.4

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

  13. Applied *-un-lft-identity0.4

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

  14. Applied distribute-lft-neg-in0.4

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

  15. Applied times-frac0.4

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

  16. Simplified0.4

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

  17. Simplified0.2

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

  18. Final simplification0.2

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

Reproduce

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