Average Error: 13.4 → 13.9
Time: 18.5s
Precision: 64
\[10^{-150} \lt \left|x\right| \lt 10^{+150}\]
\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
↓
\[\sqrt{\frac{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(\frac{x}{4 \cdot \left(p \cdot p\right) + x \cdot x} \cdot x\right) \cdot \left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right)\right) \cdot \frac{x}{\sqrt{4 \cdot \left(p \cdot p\right) + x \cdot x}}}{\left(0.5 \cdot \frac{x}{\sqrt{4 \cdot \left(p \cdot p\right) + x \cdot x}} - 0.5\right) \cdot \left(0.5 \cdot \frac{x}{\sqrt{4 \cdot \left(p \cdot p\right) + x \cdot x}}\right) + 0.5 \cdot 0.5}}\]
\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
↓
\sqrt{\frac{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(\frac{x}{4 \cdot \left(p \cdot p\right) + x \cdot x} \cdot x\right) \cdot \left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right)\right) \cdot \frac{x}{\sqrt{4 \cdot \left(p \cdot p\right) + x \cdot x}}}{\left(0.5 \cdot \frac{x}{\sqrt{4 \cdot \left(p \cdot p\right) + x \cdot x}} - 0.5\right) \cdot \left(0.5 \cdot \frac{x}{\sqrt{4 \cdot \left(p \cdot p\right) + x \cdot x}}\right) + 0.5 \cdot 0.5}}
double f(double p, double x) {
        double r8575700 = 0.5;
        double r8575701 = 1.0;
        double r8575702 = x;
        double r8575703 = 4.0;
        double r8575704 = p;
        double r8575705 = r8575703 * r8575704;
        double r8575706 = r8575705 * r8575704;
        double r8575707 = r8575702 * r8575702;
        double r8575708 = r8575706 + r8575707;
        double r8575709 = sqrt(r8575708);
        double r8575710 = r8575702 / r8575709;
        double r8575711 = r8575701 + r8575710;
        double r8575712 = r8575700 * r8575711;
        double r8575713 = sqrt(r8575712);
        return r8575713;
}
↓
double f(double p, double x) {
        double r8575714 = 0.5;
        double r8575715 = r8575714 * r8575714;
        double r8575716 = r8575714 * r8575715;
        double r8575717 = x;
        double r8575718 = 4.0;
        double r8575719 = p;
        double r8575720 = r8575719 * r8575719;
        double r8575721 = r8575718 * r8575720;
        double r8575722 = r8575717 * r8575717;
        double r8575723 = r8575721 + r8575722;
        double r8575724 = r8575717 / r8575723;
        double r8575725 = r8575724 * r8575717;
        double r8575726 = r8575725 * r8575716;
        double r8575727 = sqrt(r8575723);
        double r8575728 = r8575717 / r8575727;
        double r8575729 = r8575726 * r8575728;
        double r8575730 = r8575716 + r8575729;
        double r8575731 = r8575714 * r8575728;
        double r8575732 = r8575731 - r8575714;
        double r8575733 = r8575732 * r8575731;
        double r8575734 = r8575733 + r8575715;
        double r8575735 = r8575730 / r8575734;
        double r8575736 = sqrt(r8575735);
        return r8575736;
}

Error

Bits error versus p

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original13.4
Target13.4
Herbie13.9
\[\sqrt{\frac{1}{2} + \frac{\mathsf{copysign}\left(\frac{1}{2}, x\right)}{\mathsf{hypot}\left(1, \frac{2 \cdot p}{x}\right)}}\]

Derivation

  1. Initial program 13.4

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

  2. Simplified13.4

    \[\leadsto \color{blue}{\sqrt{0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot p\right) \cdot 4}} + 0.5}}\]
  3. Using strategy rm

  4. Applied div-inv13.6

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

  6. Applied flip3-+13.7

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

  7. Simplified13.4

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

  8. Simplified13.4

    \[\leadsto \sqrt{\frac{\left(0.5 \cdot 0.5\right) \cdot 0.5 + \left(\left(\left(0.5 \cdot 0.5\right) \cdot 0.5\right) \cdot \frac{x \cdot x}{x \cdot x + \left(p \cdot p\right) \cdot 4}\right) \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot p\right) \cdot 4}}}{\color{blue}{\left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot p\right) \cdot 4}}\right) \cdot \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot p\right) \cdot 4}} - 0.5\right) + 0.5 \cdot 0.5}}}\]
  9. Using strategy rm

  10. Applied *-un-lft-identity13.4

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

  11. Applied times-frac13.9

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

  12. Simplified13.9

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

  13. Final simplification13.9

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

Reproduce

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

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

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