2cos (problem 3.3.5)

Average Error: 40.0 → 15.8

Time: 7.7s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.6443088649730258 \cdot 10^{-8}:\\ \;\;\;\;\mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)\right)\right)\\ \mathbf{elif}\;\varepsilon \le 4.8831367818885993 \cdot 10^{-8}:\\ \;\;\;\;\varepsilon \cdot \left({\varepsilon}^{3} \cdot \frac{1}{24} - \mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \log \left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x}\right) + \cos x \cdot \cos x}\\ \end{array}\]

C

double f(double x, double eps) {
        double r56854 = x;
        double r56855 = eps;
        double r56856 = r56854 + r56855;
        double r56857 = cos(r56856);
        double r56858 = cos(r56854);
        double r56859 = r56857 - r56858;
        return r56859;
}

↓

double f(double x, double eps) {
        double r56860 = eps;
        double r56861 = -8.644308864973026e-08;
        bool r56862 = r56860 <= r56861;
        double r56863 = cos(r56860);
        double r56864 = x;
        double r56865 = cos(r56864);
        double r56866 = sin(r56864);
        double r56867 = sin(r56860);
        double r56868 = fma(r56866, r56867, r56865);
        double r56869 = expm1(r56868);
        double r56870 = log1p(r56869);
        double r56871 = -r56870;
        double r56872 = fma(r56863, r56865, r56871);
        double r56873 = 4.883136781888599e-08;
        bool r56874 = r56860 <= r56873;
        double r56875 = 3.0;
        double r56876 = pow(r56860, r56875);
        double r56877 = 0.041666666666666664;
        double r56878 = r56876 * r56877;
        double r56879 = 0.5;
        double r56880 = fma(r56879, r56860, r56864);
        double r56881 = r56878 - r56880;
        double r56882 = r56860 * r56881;
        double r56883 = r56865 * r56863;
        double r56884 = r56866 * r56867;
        double r56885 = r56883 - r56884;
        double r56886 = pow(r56885, r56875);
        double r56887 = pow(r56865, r56875);
        double r56888 = r56886 - r56887;
        double r56889 = r56863 * r56865;
        double r56890 = r56889 - r56884;
        double r56891 = r56885 + r56865;
        double r56892 = exp(r56891);
        double r56893 = log(r56892);
        double r56894 = r56890 * r56893;
        double r56895 = r56865 * r56865;
        double r56896 = r56894 + r56895;
        double r56897 = r56888 / r56896;
        double r56898 = r56874 ? r56882 : r56897;
        double r56899 = r56862 ? r56872 : r56898;
        return r56899;
}

Error

Bits error versus x

Bits error versus eps

Derivation

1. Split input into 3 regimes

2. if eps < -8.644308864973026e-08

   1. Initial program 30.6

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

   3. Applied cos-sum 1.1

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

   4. Taylor expanded around inf 1.1

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

   5. Simplified 1.1

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

   7. Applied log1p-expm1-u 1.1

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

   if -8.644308864973026e-08 < eps < 4.883136781888599e-08

   1. Initial program 49.9

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

   3. Applied cos-sum 49.5

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

   4. Taylor expanded around inf 49.5

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

   5. Simplified 49.5

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

   6. Taylor expanded around 0 31.0

      \[\leadsto \color{blue}{\frac{1}{24} \cdot {\varepsilon}^{4} - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)}\]

   7. Simplified 31.0

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

   if 4.883136781888599e-08 < eps

   1. Initial program 30.4

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

   3. Applied cos-sum 1.2

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

   5. Applied flip3-- 1.4

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

   6. Simplified 1.4

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

   8. Applied add-log-exp 1.4

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

   9. Applied add-log-exp 1.4

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

   10. Applied add-log-exp 1.5

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

   11. Applied diff-log 1.5

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

   12. Applied sum-log 1.5

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

   13. Simplified 1.4

       \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \log \color{blue}{\left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x}\right)} + \cos x \cdot \cos x}\]
3. Recombined 3 regimes into one program.

4. Final simplification 15.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -8.6443088649730258 \cdot 10^{-8}:\\ \;\;\;\;\mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)\right)\right)\\ \mathbf{elif}\;\varepsilon \le 4.8831367818885993 \cdot 10^{-8}:\\ \;\;\;\;\varepsilon \cdot \left({\varepsilon}^{3} \cdot \frac{1}{24} - \mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \log \left(e^{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x}\right) + \cos x \cdot \cos x}\\ \end{array}\]

Reproduce

herbie shell --seed 2020027 +o rules:numerics
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))