2atan (example 3.5)

Average Error: 15.1 → 0.4

Time: 13.1s

Precision: 64

Math

\[\tan^{-1} \left(N + 1\right) - \tan^{-1} N\]

↓

\[\tan^{-1}_* \frac{1}{(N \cdot \left(N + 1\right) + 1)_*}\]

C

double f(double N) {
        double r11197133 = N;
        double r11197134 = 1.0;
        double r11197135 = r11197133 + r11197134;
        double r11197136 = atan(r11197135);
        double r11197137 = atan(r11197133);
        double r11197138 = r11197136 - r11197137;
        return r11197138;
}

↓

double f(double N) {
        double r11197139 = 1.0;
        double r11197140 = N;
        double r11197141 = r11197140 + r11197139;
        double r11197142 = fma(r11197140, r11197141, r11197139);
        double r11197143 = atan2(r11197139, r11197142);
        return r11197143;
}

Error

Bits error versus N

Target

Original	15.1
Target	0.4
Herbie	0.4

\[\tan^{-1} \left(\frac{1}{1 + N \cdot \left(N + 1\right)}\right)\]

Derivation

1. Initial program 15.1

   \[\tan^{-1} \left(N + 1\right) - \tan^{-1} N\]
2. Using strategy rm

3. Applied diff-atan 13.8

   \[\leadsto \color{blue}{\tan^{-1}_* \frac{\left(N + 1\right) - N}{1 + \left(N + 1\right) \cdot N}}\]

4. Simplified 0.4

   \[\leadsto \tan^{-1}_* \frac{\color{blue}{1}}{1 + \left(N + 1\right) \cdot N}\]

5. Simplified 0.4

   \[\leadsto \tan^{-1}_* \frac{1}{\color{blue}{(N \cdot \left(N + 1\right) + 1)_*}}\]

6. Final simplification 0.4

   \[\leadsto \tan^{-1}_* \frac{1}{(N \cdot \left(N + 1\right) + 1)_*}\]

Reproduce

herbie shell --seed 2019107 +o rules:numerics
(FPCore (N)
  :name "2atan (example 3.5)"

  :herbie-target
  (atan (/ 1 (+ 1 (* N (+ N 1)))))

  (- (atan (+ N 1)) (atan N)))