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

Average Error: 0.4 → 0.1

Time: 13.0s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

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)}\]

↓

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

C

double f(double v, double t) {
        double r195557 = 1.0;
        double r195558 = 5.0;
        double r195559 = v;
        double r195560 = r195559 * r195559;
        double r195561 = r195558 * r195560;
        double r195562 = r195557 - r195561;
        double r195563 = atan2(1.0, 0.0);
        double r195564 = t;
        double r195565 = r195563 * r195564;
        double r195566 = 2.0;
        double r195567 = 3.0;
        double r195568 = r195567 * r195560;
        double r195569 = r195557 - r195568;
        double r195570 = r195566 * r195569;
        double r195571 = sqrt(r195570);
        double r195572 = r195565 * r195571;
        double r195573 = r195557 - r195560;
        double r195574 = r195572 * r195573;
        double r195575 = r195562 / r195574;
        return r195575;
}

↓

double f(double v, double t) {
        double r195576 = 1.0;
        double r195577 = atan2(1.0, 0.0);
        double r195578 = r195576 / r195577;
        double r195579 = v;
        double r195580 = r195579 / r195577;
        double r195581 = 5.0;
        double r195582 = r195581 * r195579;
        double r195583 = r195580 * r195582;
        double r195584 = r195578 - r195583;
        double r195585 = 2.0;
        double r195586 = r195576 * r195576;
        double r195587 = 4.0;
        double r195588 = pow(r195579, r195587);
        double r195589 = 3.0;
        double r195590 = r195589 * r195589;
        double r195591 = r195588 * r195590;
        double r195592 = r195586 - r195591;
        double r195593 = r195585 * r195592;
        double r195594 = sqrt(r195593);
        double r195595 = r195584 / r195594;
        double r195596 = t;
        double r195597 = r195595 / r195596;
        double r195598 = r195579 * r195579;
        double r195599 = r195576 - r195598;
        double r195600 = r195597 / r195599;
        double r195601 = r195589 * r195598;
        double r195602 = r195576 + r195601;
        double r195603 = sqrt(r195602);
        double r195604 = r195600 * r195603;
        return r195604;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.4

   \[\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 flip-- 0.4

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

4. Applied associate-*r/ 0.4

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

5. Applied sqrt-div 0.4

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

6. Applied associate-*r/ 0.4

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

7. Applied associate-*l/ 0.4

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

8. Applied associate-/r/ 0.4

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

9. Simplified 0.4

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

11. Applied div-sub 0.4

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

12. Simplified 0.3

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

13. Simplified 0.3

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

15. Applied associate-*r/ 0.3

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

16. Applied sub-div 0.3

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

17. Applied associate-/l/ 0.3

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

19. Applied associate-/r* 0.1

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

20. Final simplification 0.1

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

Reproduce

herbie shell --seed 2020043 
(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)))))