2sin (example 3.3)

Average Error: 37.3 → 0.4

Time: 6.3s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r133760 = x;
        double r133761 = eps;
        double r133762 = r133760 + r133761;
        double r133763 = sin(r133762);
        double r133764 = sin(r133760);
        double r133765 = r133763 - r133764;
        return r133765;
}

↓

double f(double x, double eps) {
        double r133766 = eps;
        double r133767 = cos(r133766);
        double r133768 = x;
        double r133769 = sin(r133768);
        double r133770 = r133767 * r133769;
        double r133771 = -r133769;
        double r133772 = r133770 + r133771;
        double r133773 = cos(r133768);
        double r133774 = sin(r133766);
        double r133775 = r133773 * r133774;
        double r133776 = r133772 + r133775;
        return r133776;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.3
Target	15.7
Herbie	0.4

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

Derivation

1. Initial program 37.3

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

3. Applied sin-sum 21.5

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

4. Applied associate--l+ 21.6

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

5. Taylor expanded around inf 21.5

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

6. Simplified 0.4

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

8. Applied add-log-exp 0.4

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

9. Applied add-log-exp 0.4

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

10. Applied diff-log 0.5

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

11. Simplified 0.4

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

13. Applied sub-neg 0.4

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

14. Applied exp-sum 0.4

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

15. Applied log-prod 0.4

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

16. Applied distribute-lft-in 0.4

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

17. Simplified 0.4

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

18. Simplified 0.4

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

19. Final simplification 0.4

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

Reproduce

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