Average Error: 39.7 → 0.7
Time: 49.0s
Precision: 64
Internal Precision: 2368
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^{3} - {\left((\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_*\right)}^{3}}{(\left((\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left((\left(\cos x\right) \cdot \left(\cos \varepsilon\right) + \left(\cos x\right))_*\right))_*\right) \cdot \left((\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_*\right) + \left(\left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right)\right))_*} \le -0.00020617047311532276:\\ \;\;\;\;(\left(\cos x\right) \cdot \left(\cos \varepsilon\right) + \left(-(\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_*\right))_*\\ \mathbf{if}\;\frac{{\left(\cos x \cdot \cos \varepsilon\right)}^{3} - {\left((\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_*\right)}^{3}}{(\left((\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left((\left(\cos x\right) \cdot \left(\cos \varepsilon\right) + \left(\cos x\right))_*\right))_*\right) \cdot \left((\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_*\right) + \left(\left(\cos \varepsilon \cdot \cos x\right) \cdot \left(\cos \varepsilon \cdot \cos x\right)\right))_*} \le 0.0:\\ \;\;\;\;-2 \cdot \left(\sin \left(\frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{x + \left(\varepsilon + x\right)}{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;(\left(\cos x\right) \cdot \left(\cos \varepsilon\right) + \left(-(\left(\sin \varepsilon\right) \cdot \left(\sin x\right) + \left(\cos x\right))_*\right))_*\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Derivation

  1. Split input into 2 regimes

  2. if (/ (- (pow (* (cos x) (cos eps)) 3) (pow (fma (sin eps) (sin x) (cos x)) 3)) (fma (fma (sin eps) (sin x) (fma (cos x) (cos eps) (cos x))) (fma (sin eps) (sin x) (cos x)) (* (* (cos eps) (cos x)) (* (cos eps) (cos x))))) < -0.00020617047311532276 or 0.0 < (/ (- (pow (* (cos x) (cos eps)) 3) (pow (fma (sin eps) (sin x) (cos x)) 3)) (fma (fma (sin eps) (sin x) (fma (cos x) (cos eps) (cos x))) (fma (sin eps) (sin x) (cos x)) (* (* (cos eps) (cos x)) (* (cos eps) (cos x)))))

    1. Initial program 30.9

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

    3. Applied cos-sum1.0

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

    4. Applied associate--l-1.0

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

    5. Applied simplify1.0

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

    7. Applied fma-neg1.0

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

    if -0.00020617047311532276 < (/ (- (pow (* (cos x) (cos eps)) 3) (pow (fma (sin eps) (sin x) (cos x)) 3)) (fma (fma (sin eps) (sin x) (fma (cos x) (cos eps) (cos x))) (fma (sin eps) (sin x) (cos x)) (* (* (cos eps) (cos x)) (* (cos eps) (cos x))))) < 0.0

    1. Initial program 48.6

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

    3. Applied diff-cos37.2

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

    4. Applied simplify0.4

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

Runtime

Time bar (total: 49.0s)Debug logProfile

herbie shell --seed '#(1072840222 1305617769 1692503039 1353360431 4178980589 1488672652)' +o rules:numerics
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  (- (cos (+ x eps)) (cos x)))