Given's Rotation SVD example, simplified

Average Error: 15.1 → 14.6

Time: 14.0s

Precision: 64

Math

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

↓

\[\frac{{\left(1 \cdot \left(1 - 0.5\right)\right)}^{4} - \left(\left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right) \cdot \left(\left(1 \cdot \left(1 - 0.5\right)\right) \cdot \left(1 \cdot \left(1 - 0.5\right)\right)\right) - \left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right) \cdot \left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right)\right)}{\frac{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\frac{{\left(1 \cdot \left(1 - 0.5\right)\right)}^{3} - {\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}^{3}}{{\left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right)}^{3} + {\left(\left(1 \cdot \left(1 - 0.5\right)\right) \cdot \left(1 \cdot \left(1 - 0.5\right)\right)\right)}^{3}}}}\]

C

double f(double x) {
        double r219693 = 1.0;
        double r219694 = 0.5;
        double r219695 = x;
        double r219696 = hypot(r219693, r219695);
        double r219697 = r219693 / r219696;
        double r219698 = r219693 + r219697;
        double r219699 = r219694 * r219698;
        double r219700 = sqrt(r219699);
        double r219701 = r219693 - r219700;
        return r219701;
}

↓

double f(double x) {
        double r219702 = 1.0;
        double r219703 = 0.5;
        double r219704 = r219702 - r219703;
        double r219705 = r219702 * r219704;
        double r219706 = 4.0;
        double r219707 = pow(r219705, r219706);
        double r219708 = x;
        double r219709 = hypot(r219702, r219708);
        double r219710 = r219702 / r219709;
        double r219711 = r219703 * r219710;
        double r219712 = r219711 + r219705;
        double r219713 = r219711 * r219712;
        double r219714 = r219705 * r219705;
        double r219715 = r219713 * r219714;
        double r219716 = r219713 * r219713;
        double r219717 = r219715 - r219716;
        double r219718 = r219707 - r219717;
        double r219719 = r219702 + r219710;
        double r219720 = r219703 * r219719;
        double r219721 = sqrt(r219720);
        double r219722 = r219702 + r219721;
        double r219723 = 3.0;
        double r219724 = pow(r219705, r219723);
        double r219725 = pow(r219711, r219723);
        double r219726 = r219724 - r219725;
        double r219727 = pow(r219713, r219723);
        double r219728 = pow(r219714, r219723);
        double r219729 = r219727 + r219728;
        double r219730 = r219726 / r219729;
        double r219731 = r219722 / r219730;
        double r219732 = r219718 / r219731;
        return r219732;
}

Error

Bits error versus x

Derivation

1. Initial program 15.1

   \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
2. Using strategy rm

3. Applied flip-- 15.1

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

4. Simplified 14.6

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

6. Applied flip3-- 14.7

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

7. Simplified 14.7

   \[\leadsto \frac{\frac{{\left(1 \cdot \left(1 - 0.5\right)\right)}^{3} - {\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}^{3}}{\color{blue}{\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right) + \left(1 \cdot \left(1 - 0.5\right)\right) \cdot \left(1 \cdot \left(1 - 0.5\right)\right)}}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\]
8. Using strategy rm

9. Applied flip3-+ 14.7

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

10. Applied associate-/r/ 14.6

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

11. Final simplification 14.6

    \[\leadsto \frac{{\left(1 \cdot \left(1 - 0.5\right)\right)}^{4} - \left(\left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right) \cdot \left(\left(1 \cdot \left(1 - 0.5\right)\right) \cdot \left(1 \cdot \left(1 - 0.5\right)\right)\right) - \left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right) \cdot \left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right)\right)}{\frac{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\frac{{\left(1 \cdot \left(1 - 0.5\right)\right)}^{3} - {\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}^{3}}{{\left(\left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \left(0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)} + 1 \cdot \left(1 - 0.5\right)\right)\right)}^{3} + {\left(\left(1 \cdot \left(1 - 0.5\right)\right) \cdot \left(1 \cdot \left(1 - 0.5\right)\right)\right)}^{3}}}}\]

Reproduce

herbie shell --seed 2019297 
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  :precision binary64
  (- 1 (sqrt (* 0.5 (+ 1 (/ 1 (hypot 1 x)))))))