Average Error: 15.5 → 0.0
Time: 18.7s
Precision: 64
\[1 - \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \le 1.000024131824829:\\ \;\;\;\;\mathsf{fma}\left(\left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \frac{69}{1024}, \left(\frac{1}{8} - \left(x \cdot x\right) \cdot \frac{11}{128}\right) \cdot \left(x \cdot x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} \cdot \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}{1 + \left(\left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right)}\\ \end{array}\]
1 - \sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\begin{array}{l}
\mathbf{if}\;\mathsf{hypot}\left(1, x\right) \le 1.000024131824829:\\
\;\;\;\;\mathsf{fma}\left(\left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \frac{69}{1024}, \left(\frac{1}{8} - \left(x \cdot x\right) \cdot \frac{11}{128}\right) \cdot \left(x \cdot x\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} \cdot \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}{1 + \left(\left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right)}\\

\end{array}
double f(double x) {
        double r3872085 = 1.0;
        double r3872086 = 0.5;
        double r3872087 = x;
        double r3872088 = hypot(r3872085, r3872087);
        double r3872089 = r3872085 / r3872088;
        double r3872090 = r3872085 + r3872089;
        double r3872091 = r3872086 * r3872090;
        double r3872092 = sqrt(r3872091);
        double r3872093 = r3872085 - r3872092;
        return r3872093;
}
↓
double f(double x) {
        double r3872094 = 1.0;
        double r3872095 = x;
        double r3872096 = hypot(r3872094, r3872095);
        double r3872097 = 1.000024131824829;
        bool r3872098 = r3872096 <= r3872097;
        double r3872099 = r3872095 * r3872095;
        double r3872100 = r3872099 * r3872095;
        double r3872101 = r3872100 * r3872100;
        double r3872102 = 0.0673828125;
        double r3872103 = 0.125;
        double r3872104 = 0.0859375;
        double r3872105 = r3872099 * r3872104;
        double r3872106 = r3872103 - r3872105;
        double r3872107 = r3872106 * r3872099;
        double r3872108 = fma(r3872101, r3872102, r3872107);
        double r3872109 = 0.5;
        double r3872110 = r3872109 / r3872096;
        double r3872111 = r3872109 + r3872110;
        double r3872112 = sqrt(r3872111);
        double r3872113 = r3872112 * r3872111;
        double r3872114 = r3872094 - r3872113;
        double r3872115 = r3872111 + r3872112;
        double r3872116 = r3872094 + r3872115;
        double r3872117 = r3872114 / r3872116;
        double r3872118 = r3872098 ? r3872108 : r3872117;
        return r3872118;
}

Error

Bits error versus x

Derivation

  1. Split input into 2 regimes

  2. if (hypot 1 x) < 1.000024131824829

    1. Initial program 29.9

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

    2. Simplified29.9

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

    4. Applied add-exp-log29.9

      \[\leadsto \color{blue}{e^{\log \left(1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right)}}\]

    5. Taylor expanded around 0 0.0

      \[\leadsto \color{blue}{\left(\frac{1}{8} \cdot {x}^{2} + \frac{69}{1024} \cdot {x}^{6}\right) - \frac{11}{128} \cdot {x}^{4}}\]

    6. Simplified0.0

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \frac{69}{1024}, \left(x \cdot x\right) \cdot \left(\frac{1}{8} - \frac{11}{128} \cdot \left(x \cdot x\right)\right)\right)}\]

    if 1.000024131824829 < (hypot 1 x)

    1. Initial program 1.0

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

    2. Simplified1.0

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

    4. Applied flip3--1.6

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

    5. Simplified1.0

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

    6. Simplified0.1

      \[\leadsto \frac{1 - \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}}{\color{blue}{\left(\left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right) + 1}}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification0.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \le 1.000024131824829:\\ \;\;\;\;\mathsf{fma}\left(\left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \frac{69}{1024}, \left(\frac{1}{8} - \left(x \cdot x\right) \cdot \frac{11}{128}\right) \cdot \left(x \cdot x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} \cdot \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}{1 + \left(\left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}\right)}\\ \end{array}\]

Reproduce

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