Trigonometry A

Average Error: 0.1 → 0.1

Time: 9.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

\[0.0 \le e \le 1\]

Math

\[\frac{e \cdot \sin v}{1 + e \cdot \cos v}\]

↓

\[\frac{e \cdot \sin v}{1 + e \cdot \cos v}\]

C

double f(double e, double v) {
        double r13898 = e;
        double r13899 = v;
        double r13900 = sin(r13899);
        double r13901 = r13898 * r13900;
        double r13902 = 1.0;
        double r13903 = cos(r13899);
        double r13904 = r13898 * r13903;
        double r13905 = r13902 + r13904;
        double r13906 = r13901 / r13905;
        return r13906;
}

↓

double f(double e, double v) {
        double r13907 = e;
        double r13908 = v;
        double r13909 = sin(r13908);
        double r13910 = r13907 * r13909;
        double r13911 = 1.0;
        double r13912 = cos(r13908);
        double r13913 = r13907 * r13912;
        double r13914 = r13911 + r13913;
        double r13915 = r13910 / r13914;
        return r13915;
}

Error

Bits error versus e

Bits error versus v

Derivation

1. Initial program 0.1

   \[\frac{e \cdot \sin v}{1 + e \cdot \cos v}\]
2. Using strategy rm

3. Applied *-un-lft-identity 0.1

   \[\leadsto \frac{e \cdot \sin v}{\color{blue}{1 \cdot \left(1 + e \cdot \cos v\right)}}\]

4. Applied times-frac 0.1

   \[\leadsto \color{blue}{\frac{e}{1} \cdot \frac{\sin v}{1 + e \cdot \cos v}}\]

5. Simplified 0.1

   \[\leadsto \color{blue}{e} \cdot \frac{\sin v}{1 + e \cdot \cos v}\]
6. Using strategy rm

7. Applied add-sqr-sqrt 0.4

   \[\leadsto \color{blue}{\left(\sqrt{e} \cdot \sqrt{e}\right)} \cdot \frac{\sin v}{1 + e \cdot \cos v}\]

8. Applied associate-*l* 0.4

   \[\leadsto \color{blue}{\sqrt{e} \cdot \left(\sqrt{e} \cdot \frac{\sin v}{1 + e \cdot \cos v}\right)}\]
9. Using strategy rm

10. Applied add-sqr-sqrt 0.4

    \[\leadsto \sqrt{e} \cdot \left(\sqrt{\color{blue}{\sqrt{e} \cdot \sqrt{e}}} \cdot \frac{\sin v}{1 + e \cdot \cos v}\right)\]

11. Applied sqrt-prod 0.6

    \[\leadsto \sqrt{e} \cdot \left(\color{blue}{\left(\sqrt{\sqrt{e}} \cdot \sqrt{\sqrt{e}}\right)} \cdot \frac{\sin v}{1 + e \cdot \cos v}\right)\]

12. Applied associate-*l* 0.5

    \[\leadsto \sqrt{e} \cdot \color{blue}{\left(\sqrt{\sqrt{e}} \cdot \left(\sqrt{\sqrt{e}} \cdot \frac{\sin v}{1 + e \cdot \cos v}\right)\right)}\]
13. Using strategy rm

14. Applied *-un-lft-identity 0.5

    \[\leadsto \color{blue}{\left(1 \cdot \sqrt{e}\right)} \cdot \left(\sqrt{\sqrt{e}} \cdot \left(\sqrt{\sqrt{e}} \cdot \frac{\sin v}{1 + e \cdot \cos v}\right)\right)\]

15. Applied associate-*l* 0.5

    \[\leadsto \color{blue}{1 \cdot \left(\sqrt{e} \cdot \left(\sqrt{\sqrt{e}} \cdot \left(\sqrt{\sqrt{e}} \cdot \frac{\sin v}{1 + e \cdot \cos v}\right)\right)\right)}\]

16. Simplified 0.1

    \[\leadsto 1 \cdot \color{blue}{\frac{e \cdot \sin v}{1 + e \cdot \cos v}}\]

17. Final simplification 0.1

    \[\leadsto \frac{e \cdot \sin v}{1 + e \cdot \cos v}\]

Reproduce

herbie shell --seed 2020046 
(FPCore (e v)
  :name "Trigonometry A"
  :precision binary64
  :pre (<= 0.0 e 1)
  (/ (* e (sin v)) (+ 1 (* e (cos v)))))