Given's Rotation SVD example, simplified

Average Error: 15.6 → 15.2

Time: 1.3m

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r9757794 = 1.0;
        double r9757795 = 0.5;
        double r9757796 = x;
        double r9757797 = hypot(r9757794, r9757796);
        double r9757798 = r9757794 / r9757797;
        double r9757799 = r9757794 + r9757798;
        double r9757800 = r9757795 * r9757799;
        double r9757801 = sqrt(r9757800);
        double r9757802 = r9757794 - r9757801;
        return r9757802;
}

↓

double f(double x) {
        double r9757803 = 1.0;
        double r9757804 = r9757803 * r9757803;
        double r9757805 = r9757803 * r9757804;
        double r9757806 = 0.5;
        double r9757807 = x;
        double r9757808 = hypot(r9757803, r9757807);
        double r9757809 = r9757803 / r9757808;
        double r9757810 = r9757803 + r9757809;
        double r9757811 = r9757806 * r9757810;
        double r9757812 = sqrt(r9757811);
        double r9757813 = r9757812 * r9757811;
        double r9757814 = r9757805 - r9757813;
        double r9757815 = fma(r9757803, r9757812, r9757811);
        double r9757816 = fma(r9757803, r9757803, r9757815);
        double r9757817 = r9757814 / r9757816;
        double r9757818 = sqrt(r9757817);
        double r9757819 = r9757818 * r9757818;
        return r9757819;
}

Error

Bits error versus x

Derivation

1. Initial program 15.6

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

3. Applied flip3-- 15.9

   \[\leadsto \color{blue}{\frac{{1}^{3} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{1 \cdot 1 + \left(\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 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}}\]

4. Simplified 15.6

   \[\leadsto \frac{\color{blue}{1 \cdot \left(1 \cdot 1\right) - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}{1 \cdot 1 + \left(\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 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}\]

5. Simplified 15.2

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

7. Applied add-sqr-sqrt 15.2

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

8. Final simplification 15.2

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

Reproduce

herbie shell --seed 2019172 +o rules:numerics
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))