Given's Rotation SVD example, simplified

Average Error: 15.6 → 15.1

Time: 7.4s

Precision: binary64

Cost: 40192

Math

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

↓

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

FPCore

(FPCore (x)
 :precision binary64
 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))

↓

(FPCore (x)
 :precision binary64
 (/
  (/
   (+ 0.125 (/ -0.125 (pow (hypot 1.0 x) 3.0)))
   (+ 0.25 (/ (+ 0.25 (/ 0.25 (hypot 1.0 x))) (hypot 1.0 x))))
  (+ 1.0 (sqrt (+ 0.5 (/ 0.5 (hypot 1.0 x)))))))

C

double code(double x) {
	return 1.0 - sqrt(0.5 * (1.0 + (1.0 / hypot(1.0, x))));
}

↓

double code(double x) {
	return ((0.125 + (-0.125 / pow(hypot(1.0, x), 3.0))) / (0.25 + ((0.25 + (0.25 / hypot(1.0, x))) / hypot(1.0, x)))) / (1.0 + sqrt(0.5 + (0.5 / hypot(1.0, x))));
}

Error

Bits error versus x

Alternatives

Alternative 1
Error	15.1
Cost	20160

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

Alternative 2
Error	15.6
Cost	13312

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

Alternative 3
Error	41.7
Cost	706

\[\begin{array}{l} \mathbf{if}\;x \leq -3.0152608065398887 \cdot 10^{-77}:\\ \;\;\;\;1\\ \mathbf{elif}\;x \leq 3.0033332679397286 \cdot 10^{-77}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array}\]

Alternative 4
Error	57.1
Cost	64

\[1\]

Derivation

1. Initial program 15.6

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

2. Simplified 15.6

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

4. Applied flip--_binary64_1076 15.6

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

5. Simplified 15.1

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

7. Applied flip3--_binary64_1105 15.1

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

8. Simplified 15.1

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

9. Simplified 15.1

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

11. Applied sub-neg_binary64_1094 15.1

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

12. Simplified 15.1

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

13. Simplified 15.1

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

14. Final simplification 15.1

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

Reproduce

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