Average Error: 36.6 → 0.4
Time: 6.0s
Precision: 64
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\frac{\sin x \cdot \left({\left(\cos \varepsilon\right)}^{3} - 1\right)}{\cos \varepsilon \cdot \cos \varepsilon + \left(1 + \cos \varepsilon \cdot 1\right)} + \cos x \cdot \sin \varepsilon\]
\sin \left(x + \varepsilon\right) - \sin x
↓
\frac{\sin x \cdot \left({\left(\cos \varepsilon\right)}^{3} - 1\right)}{\cos \varepsilon \cdot \cos \varepsilon + \left(1 + \cos \varepsilon \cdot 1\right)} + \cos x \cdot \sin \varepsilon
double f(double x, double eps) {
        double r101520 = x;
        double r101521 = eps;
        double r101522 = r101520 + r101521;
        double r101523 = sin(r101522);
        double r101524 = sin(r101520);
        double r101525 = r101523 - r101524;
        return r101525;
}
↓
double f(double x, double eps) {
        double r101526 = x;
        double r101527 = sin(r101526);
        double r101528 = eps;
        double r101529 = cos(r101528);
        double r101530 = 3.0;
        double r101531 = pow(r101529, r101530);
        double r101532 = 1.0;
        double r101533 = r101531 - r101532;
        double r101534 = r101527 * r101533;
        double r101535 = r101529 * r101529;
        double r101536 = r101529 * r101532;
        double r101537 = r101532 + r101536;
        double r101538 = r101535 + r101537;
        double r101539 = r101534 / r101538;
        double r101540 = cos(r101526);
        double r101541 = sin(r101528);
        double r101542 = r101540 * r101541;
        double r101543 = r101539 + r101542;
        return r101543;
}

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.6
Target15.3
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.6

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

  3. Applied sin-sum21.2

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

  4. Taylor expanded around inf 21.2

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

  5. Simplified0.4

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

  7. Applied flip3--0.4

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

  8. Applied associate-*r/0.4

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

  9. Final simplification0.4

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

Reproduce

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