2cos (problem 3.3.5)

Average Error: 39.7 → 15.9

Time: 9.3s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.4155618696900624 \cdot 10^{-10}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left(\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) - \cos x \cdot \cos x\right)}{\left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos \varepsilon \cdot \cos x\right) + {\left(\cos \varepsilon\right)}^{2} \cdot {\left(\cos x\right)}^{2}\right)} + \cos x \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 1.23057486602459758 \cdot 10^{-7}:\\ \;\;\;\;\frac{\frac{7}{8} \cdot {\varepsilon}^{4} - \left(3 \cdot \left(x \cdot \varepsilon\right) + \frac{3}{2} \cdot {\varepsilon}^{2}\right)}{\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}\\ \mathbf{else}:\\ \;\;\;\;\left(\cos x \cdot \cos \varepsilon - \left(\sqrt[3]{\sin x \cdot \sin \varepsilon} \cdot \sqrt[3]{\sin x \cdot \sin \varepsilon}\right) \cdot \sqrt[3]{\sin x \cdot \sin \varepsilon}\right) - \cos x\\ \end{array}\]

C

double f(double x, double eps) {
        double r41801 = x;
        double r41802 = eps;
        double r41803 = r41801 + r41802;
        double r41804 = cos(r41803);
        double r41805 = cos(r41801);
        double r41806 = r41804 - r41805;
        return r41806;
}

↓

double f(double x, double eps) {
        double r41807 = eps;
        double r41808 = -1.4155618696900624e-10;
        bool r41809 = r41807 <= r41808;
        double r41810 = x;
        double r41811 = cos(r41810);
        double r41812 = cos(r41807);
        double r41813 = r41811 * r41812;
        double r41814 = sin(r41810);
        double r41815 = sin(r41807);
        double r41816 = r41814 * r41815;
        double r41817 = r41813 - r41816;
        double r41818 = 3.0;
        double r41819 = pow(r41817, r41818);
        double r41820 = pow(r41811, r41818);
        double r41821 = r41819 - r41820;
        double r41822 = r41812 * r41811;
        double r41823 = pow(r41822, r41818);
        double r41824 = pow(r41816, r41818);
        double r41825 = r41823 - r41824;
        double r41826 = r41817 * r41817;
        double r41827 = r41811 * r41811;
        double r41828 = r41826 - r41827;
        double r41829 = r41825 * r41828;
        double r41830 = r41817 - r41811;
        double r41831 = r41816 + r41822;
        double r41832 = r41816 * r41831;
        double r41833 = 2.0;
        double r41834 = pow(r41812, r41833);
        double r41835 = pow(r41811, r41833);
        double r41836 = r41834 * r41835;
        double r41837 = r41832 + r41836;
        double r41838 = r41830 * r41837;
        double r41839 = r41829 / r41838;
        double r41840 = r41839 + r41827;
        double r41841 = r41821 / r41840;
        double r41842 = 1.2305748660245976e-07;
        bool r41843 = r41807 <= r41842;
        double r41844 = 0.875;
        double r41845 = 4.0;
        double r41846 = pow(r41807, r41845);
        double r41847 = r41844 * r41846;
        double r41848 = r41810 * r41807;
        double r41849 = r41818 * r41848;
        double r41850 = 1.5;
        double r41851 = pow(r41807, r41833);
        double r41852 = r41850 * r41851;
        double r41853 = r41849 + r41852;
        double r41854 = r41847 - r41853;
        double r41855 = r41822 - r41816;
        double r41856 = r41817 + r41811;
        double r41857 = r41855 * r41856;
        double r41858 = r41857 + r41827;
        double r41859 = r41854 / r41858;
        double r41860 = cbrt(r41816);
        double r41861 = r41860 * r41860;
        double r41862 = r41861 * r41860;
        double r41863 = r41813 - r41862;
        double r41864 = r41863 - r41811;
        double r41865 = r41843 ? r41859 : r41864;
        double r41866 = r41809 ? r41841 : r41865;
        return r41866;
}

Error

Bits error versus x

Bits error versus eps

Derivation

1. Split input into 3 regimes

2. if eps < -1.4155618696900624e-10

   1. Initial program 31.0

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

   3. Applied cos-sum 1.5

      \[\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.7

      \[\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.7

      \[\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 flip-+ 1.7

      \[\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}{\frac{\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) - \cos x \cdot \cos x}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x}} + \cos x \cdot \cos x}\]

   9. Applied flip3-- 1.7

      \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\frac{{\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right) + \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)}} \cdot \frac{\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) - \cos x \cdot \cos x}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x} + \cos x \cdot \cos x}\]

   10. Applied frac-times 1.7

       \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left(\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) - \cos x \cdot \cos x\right)}{\left(\left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right) + \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon\right) + \left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\sin x \cdot \sin \varepsilon\right)\right)\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x\right)}} + \cos x \cdot \cos x}\]

   11. Simplified 1.7

       \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left(\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) - \cos x \cdot \cos x\right)}{\color{blue}{\left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos \varepsilon \cdot \cos x\right) + {\left(\cos \varepsilon\right)}^{2} \cdot {\left(\cos x\right)}^{2}\right)}} + \cos x \cdot \cos x}\]

   if -1.4155618696900624e-10 < eps < 1.2305748660245976e-07

   1. Initial program 49.1

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

   3. Applied cos-sum 48.8

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

   5. Applied flip3-- 48.8

      \[\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 48.8

      \[\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. Taylor expanded around inf 48.8

      \[\leadsto \frac{\color{blue}{\left({\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3} + 3 \cdot \left(\cos \varepsilon \cdot \left({\left(\sin x\right)}^{2} \cdot \left({\left(\sin \varepsilon\right)}^{2} \cdot \cos x\right)\right)\right)\right) - \left({\left(\cos x\right)}^{3} + \left(3 \cdot \left({\left(\cos \varepsilon\right)}^{2} \cdot \left(\sin x \cdot \left(\sin \varepsilon \cdot {\left(\cos x\right)}^{2}\right)\right)\right) + {\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}\right)\right)}}{\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}\]

   8. Simplified 48.8

      \[\leadsto \frac{\color{blue}{{\left(\cos \varepsilon \cdot \cos x\right)}^{3} + \left(3 \cdot \left(\cos x \cdot \left({\left(\sin x\right)}^{2} \cdot \left({\left(\sin \varepsilon\right)}^{2} \cdot \cos \varepsilon\right)\right)\right) - \left(\left({\left(\cos x\right)}^{3} + 3 \cdot \left({\left(\cos x\right)}^{2} \cdot \left(\sin x \cdot \left(\sin \varepsilon \cdot {\left(\cos \varepsilon\right)}^{2}\right)\right)\right)\right) + {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right)\right)}}{\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}\]

   9. Taylor expanded around 0 30.8

      \[\leadsto \frac{\color{blue}{\frac{7}{8} \cdot {\varepsilon}^{4} - \left(3 \cdot \left(x \cdot \varepsilon\right) + \frac{3}{2} \cdot {\varepsilon}^{2}\right)}}{\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}\]

   if 1.2305748660245976e-07 < eps

   1. Initial program 30.3

      \[\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. Using strategy rm

   5. Applied add-cube-cbrt 1.4

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

4. Final simplification 15.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.4155618696900624 \cdot 10^{-10}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\frac{\left({\left(\cos \varepsilon \cdot \cos x\right)}^{3} - {\left(\sin x \cdot \sin \varepsilon\right)}^{3}\right) \cdot \left(\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) - \cos x \cdot \cos x\right)}{\left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x\right) \cdot \left(\left(\sin x \cdot \sin \varepsilon\right) \cdot \left(\sin x \cdot \sin \varepsilon + \cos \varepsilon \cdot \cos x\right) + {\left(\cos \varepsilon\right)}^{2} \cdot {\left(\cos x\right)}^{2}\right)} + \cos x \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 1.23057486602459758 \cdot 10^{-7}:\\ \;\;\;\;\frac{\frac{7}{8} \cdot {\varepsilon}^{4} - \left(3 \cdot \left(x \cdot \varepsilon\right) + \frac{3}{2} \cdot {\varepsilon}^{2}\right)}{\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}\\ \mathbf{else}:\\ \;\;\;\;\left(\cos x \cdot \cos \varepsilon - \left(\sqrt[3]{\sin x \cdot \sin \varepsilon} \cdot \sqrt[3]{\sin x \cdot \sin \varepsilon}\right) \cdot \sqrt[3]{\sin x \cdot \sin \varepsilon}\right) - \cos x\\ \end{array}\]

Reproduce

herbie shell --seed 2020062 
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))