Given's Rotation SVD example

Average Error: 12.9 → 13.1

Time: 8.6s

Precision: 64

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

\[1.00000000000000001 \cdot 10^{-150} \lt \left|x\right| \lt 9.99999999999999981 \cdot 10^{149}\]

Math

\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]

↓

\[\sqrt{0.5 \cdot \left(1 + x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]

C

double f(double p, double x) {
        double r382478 = 0.5;
        double r382479 = 1.0;
        double r382480 = x;
        double r382481 = 4.0;
        double r382482 = p;
        double r382483 = r382481 * r382482;
        double r382484 = r382483 * r382482;
        double r382485 = r382480 * r382480;
        double r382486 = r382484 + r382485;
        double r382487 = sqrt(r382486);
        double r382488 = r382480 / r382487;
        double r382489 = r382479 + r382488;
        double r382490 = r382478 * r382489;
        double r382491 = sqrt(r382490);
        return r382491;
}

↓

double f(double p, double x) {
        double r382492 = 0.5;
        double r382493 = 1.0;
        double r382494 = x;
        double r382495 = 1.0;
        double r382496 = 4.0;
        double r382497 = p;
        double r382498 = r382496 * r382497;
        double r382499 = r382498 * r382497;
        double r382500 = r382494 * r382494;
        double r382501 = r382499 + r382500;
        double r382502 = sqrt(r382501);
        double r382503 = r382495 / r382502;
        double r382504 = r382494 * r382503;
        double r382505 = r382493 + r382504;
        double r382506 = r382492 * r382505;
        double r382507 = sqrt(r382506);
        return r382507;
}

Error

Bits error versus p

Bits error versus x

Target

Original	12.9
Target	12.9
Herbie	13.1

\[\sqrt{0.5 + \frac{\mathsf{copysign}\left(0.5, x\right)}{\mathsf{hypot}\left(1, \frac{2 \cdot p}{x}\right)}}\]

Derivation

1. Initial program 12.9

   \[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
2. Using strategy rm

3. Applied div-inv 13.1

   \[\leadsto \sqrt{0.5 \cdot \left(1 + \color{blue}{x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}\right)}\]

4. Final simplification 13.1

   \[\leadsto \sqrt{0.5 \cdot \left(1 + x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]

Reproduce

herbie shell --seed 2020047 
(FPCore (p x)
  :name "Given's Rotation SVD example"
  :precision binary64
  :pre (< 1e-150 (fabs x) 1e+150)

  :herbie-target
  (sqrt (+ 0.5 (/ (copysign 0.5 x) (hypot 1 (/ (* 2 p) x)))))

  (sqrt (* 0.5 (+ 1 (/ x (sqrt (+ (* (* 4 p) p) (* x x))))))))