Falkner and Boettcher, Equation (20:1,3)

Average Error: 0.5 → 0.1

Time: 24.0s

Precision: 64

Math

\[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]

↓

\[\left(\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5} \cdot \frac{\frac{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{\pi}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}}{t}\right) \cdot \frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]

C

double f(double v, double t) {
        double r188043 = 1.0;
        double r188044 = 5.0;
        double r188045 = v;
        double r188046 = r188045 * r188045;
        double r188047 = r188044 * r188046;
        double r188048 = r188043 - r188047;
        double r188049 = atan2(1.0, 0.0);
        double r188050 = t;
        double r188051 = r188049 * r188050;
        double r188052 = 2.0;
        double r188053 = 3.0;
        double r188054 = r188053 * r188046;
        double r188055 = r188043 - r188054;
        double r188056 = r188052 * r188055;
        double r188057 = sqrt(r188056);
        double r188058 = r188051 * r188057;
        double r188059 = r188043 - r188046;
        double r188060 = r188058 * r188059;
        double r188061 = r188048 / r188060;
        return r188061;
}

↓

double f(double v, double t) {
        double r188062 = 1.0;
        double r188063 = v;
        double r188064 = r188063 * r188063;
        double r188065 = 5.0;
        double r188066 = r188064 * r188065;
        double r188067 = r188062 - r188066;
        double r188068 = cbrt(r188067);
        double r188069 = atan2(1.0, 0.0);
        double r188070 = r188068 / r188069;
        double r188071 = 2.0;
        double r188072 = 3.0;
        double r188073 = r188072 * r188064;
        double r188074 = r188062 - r188073;
        double r188075 = r188071 * r188074;
        double r188076 = sqrt(r188075);
        double r188077 = r188070 / r188076;
        double r188078 = t;
        double r188079 = r188077 / r188078;
        double r188080 = r188068 * r188079;
        double r188081 = r188062 - r188064;
        double r188082 = r188068 / r188081;
        double r188083 = r188080 * r188082;
        return r188083;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.5

   \[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
2. Using strategy rm

3. Applied add-log-exp 0.5

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

5. Applied add-cube-cbrt 0.5

   \[\leadsto \frac{\color{blue}{\left(\sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)} \cdot \sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)}\right) \cdot \sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)}}}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]

6. Applied times-frac 0.5

   \[\leadsto \color{blue}{\frac{\sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)} \cdot \sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)}}{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}} \cdot \frac{\sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)}}{1 - v \cdot v}}\]

7. Simplified 0.5

   \[\leadsto \color{blue}{\frac{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5} \cdot \sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{t \cdot \pi}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}} \cdot \frac{\sqrt[3]{1 - \log \left(e^{5 \cdot \left(v \cdot v\right)}\right)}}{1 - v \cdot v}\]

8. Simplified 0.5

   \[\leadsto \frac{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5} \cdot \sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{t \cdot \pi}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}} \cdot \color{blue}{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}}\]
9. Using strategy rm

10. Applied *-un-lft-identity 0.5

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

11. Applied times-frac 0.4

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

12. Applied times-frac 0.3

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

13. Simplified 0.3

    \[\leadsto \left(\color{blue}{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{t}} \cdot \frac{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{\pi}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}\right) \cdot \frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
14. Using strategy rm

15. Applied div-inv 0.3

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

16. Applied associate-*l* 0.3

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

17. Simplified 0.1

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

18. Final simplification 0.1

    \[\leadsto \left(\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5} \cdot \frac{\frac{\frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{\pi}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}}{t}\right) \cdot \frac{\sqrt[3]{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]

Reproduce

herbie shell --seed 2019326 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  :precision binary64
  (/ (- 1 (* 5 (* v v))) (* (* (* PI t) (sqrt (* 2 (- 1 (* 3 (* v v)))))) (- 1 (* v v)))))