Falkner and Boettcher, Appendix B, 2

Average Error: 0.0 → 0.0

Time: 2.1m

Precision: 64

Math

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

↓

\[\left(\sqrt{1 - v \cdot v} \cdot \frac{\sqrt{2}}{\frac{4}{\sqrt{1 - v \cdot v}}}\right) \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

C

double f(double v) {
        double r21770531 = 2.0;
        double r21770532 = sqrt(r21770531);
        double r21770533 = 4.0;
        double r21770534 = r21770532 / r21770533;
        double r21770535 = 1.0;
        double r21770536 = 3.0;
        double r21770537 = v;
        double r21770538 = r21770537 * r21770537;
        double r21770539 = r21770536 * r21770538;
        double r21770540 = r21770535 - r21770539;
        double r21770541 = sqrt(r21770540);
        double r21770542 = r21770534 * r21770541;
        double r21770543 = r21770535 - r21770538;
        double r21770544 = r21770542 * r21770543;
        return r21770544;
}

↓

double f(double v) {
        double r21770545 = 1.0;
        double r21770546 = v;
        double r21770547 = r21770546 * r21770546;
        double r21770548 = r21770545 - r21770547;
        double r21770549 = sqrt(r21770548);
        double r21770550 = 2.0;
        double r21770551 = sqrt(r21770550);
        double r21770552 = 4.0;
        double r21770553 = r21770552 / r21770549;
        double r21770554 = r21770551 / r21770553;
        double r21770555 = r21770549 * r21770554;
        double r21770556 = -3.0;
        double r21770557 = fma(r21770547, r21770556, r21770545);
        double r21770558 = sqrt(r21770557);
        double r21770559 = r21770555 * r21770558;
        return r21770559;
}

Error

Bits error versus v

Derivation

1. Initial program 0.0

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

2. Simplified 0.0

   \[\leadsto \color{blue}{\frac{\sqrt{2}}{\frac{4}{1 - v \cdot v}} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}}\]
3. Using strategy rm

4. Applied add-sqr-sqrt 0.0

   \[\leadsto \frac{\sqrt{2}}{\frac{4}{\color{blue}{\sqrt{1 - v \cdot v} \cdot \sqrt{1 - v \cdot v}}}} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

5. Applied *-un-lft-identity 0.0

   \[\leadsto \frac{\sqrt{2}}{\frac{\color{blue}{1 \cdot 4}}{\sqrt{1 - v \cdot v} \cdot \sqrt{1 - v \cdot v}}} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

6. Applied times-frac 0.0

   \[\leadsto \frac{\sqrt{2}}{\color{blue}{\frac{1}{\sqrt{1 - v \cdot v}} \cdot \frac{4}{\sqrt{1 - v \cdot v}}}} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

7. Applied *-un-lft-identity 0.0

   \[\leadsto \frac{\color{blue}{1 \cdot \sqrt{2}}}{\frac{1}{\sqrt{1 - v \cdot v}} \cdot \frac{4}{\sqrt{1 - v \cdot v}}} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

8. Applied times-frac 0.0

   \[\leadsto \color{blue}{\left(\frac{1}{\frac{1}{\sqrt{1 - v \cdot v}}} \cdot \frac{\sqrt{2}}{\frac{4}{\sqrt{1 - v \cdot v}}}\right)} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

9. Simplified 0.0

   \[\leadsto \left(\color{blue}{\sqrt{1 - v \cdot v}} \cdot \frac{\sqrt{2}}{\frac{4}{\sqrt{1 - v \cdot v}}}\right) \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

10. Final simplification 0.0

    \[\leadsto \left(\sqrt{1 - v \cdot v} \cdot \frac{\sqrt{2}}{\frac{4}{\sqrt{1 - v \cdot v}}}\right) \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}\]

Reproduce

herbie shell --seed 2019104 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))