Falkner and Boettcher, Appendix B, 1

Average Error: 0.6 → 0.6

Time: 21.5s

Precision: 64

Math

\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]

↓

\[\frac{{\left(\frac{\pi}{2}\right)}^{3} - {\left(\sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)\right)}^{3}}{\frac{\pi}{2} \cdot \frac{\pi}{2} + \left(\frac{\pi}{2} \cdot \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right) + \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right) \cdot \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)\right)}\]

C

double f(double v) {
        double r2673498 = 1.0;
        double r2673499 = 5.0;
        double r2673500 = v;
        double r2673501 = r2673500 * r2673500;
        double r2673502 = r2673499 * r2673501;
        double r2673503 = r2673498 - r2673502;
        double r2673504 = r2673501 - r2673498;
        double r2673505 = r2673503 / r2673504;
        double r2673506 = acos(r2673505);
        return r2673506;
}

↓

double f(double v) {
        double r2673507 = atan2(1.0, 0.0);
        double r2673508 = 2.0;
        double r2673509 = r2673507 / r2673508;
        double r2673510 = 3.0;
        double r2673511 = pow(r2673509, r2673510);
        double r2673512 = 1.0;
        double r2673513 = v;
        double r2673514 = r2673513 * r2673513;
        double r2673515 = r2673514 - r2673512;
        double r2673516 = 5.0;
        double r2673517 = r2673516 * r2673514;
        double r2673518 = r2673512 - r2673517;
        double r2673519 = r2673515 / r2673518;
        double r2673520 = r2673512 / r2673519;
        double r2673521 = asin(r2673520);
        double r2673522 = pow(r2673521, r2673510);
        double r2673523 = r2673511 - r2673522;
        double r2673524 = r2673509 * r2673509;
        double r2673525 = r2673509 * r2673521;
        double r2673526 = r2673521 * r2673521;
        double r2673527 = r2673525 + r2673526;
        double r2673528 = r2673524 + r2673527;
        double r2673529 = r2673523 / r2673528;
        return r2673529;
}

Error

Bits error versus v

Derivation

1. Initial program 0.6

   \[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
2. Using strategy rm

3. Applied acos-asin 0.6

   \[\leadsto \color{blue}{\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)}\]
4. Using strategy rm

5. Applied clear-num 0.6

   \[\leadsto \frac{\pi}{2} - \sin^{-1} \color{blue}{\left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)}\]
6. Using strategy rm

7. Applied flip3-- 0.6

   \[\leadsto \color{blue}{\frac{{\left(\frac{\pi}{2}\right)}^{3} - {\left(\sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)\right)}^{3}}{\frac{\pi}{2} \cdot \frac{\pi}{2} + \left(\sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right) \cdot \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right) + \frac{\pi}{2} \cdot \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)\right)}}\]

8. Final simplification 0.6

   \[\leadsto \frac{{\left(\frac{\pi}{2}\right)}^{3} - {\left(\sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)\right)}^{3}}{\frac{\pi}{2} \cdot \frac{\pi}{2} + \left(\frac{\pi}{2} \cdot \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right) + \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right) \cdot \sin^{-1} \left(\frac{1}{\frac{v \cdot v - 1}{1 - 5 \cdot \left(v \cdot v\right)}}\right)\right)}\]

Reproduce

herbie shell --seed 2019155 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 1"
  (acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))