Average Error: 16.1 → 0.0
Time: 29.5s
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.0000277305282526:\\ \;\;\;\;\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{e^{\log \left(\frac{1}{2} - \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\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.0000277305282526:\\
\;\;\;\;\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{e^{\log \left(\frac{1}{2} - \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}}\\

\end{array}
double f(double x) {
        double r5351047 = 1.0;
        double r5351048 = 0.5;
        double r5351049 = x;
        double r5351050 = hypot(r5351047, r5351049);
        double r5351051 = r5351047 / r5351050;
        double r5351052 = r5351047 + r5351051;
        double r5351053 = r5351048 * r5351052;
        double r5351054 = sqrt(r5351053);
        double r5351055 = r5351047 - r5351054;
        return r5351055;
}
↓
double f(double x) {
        double r5351056 = 1.0;
        double r5351057 = x;
        double r5351058 = hypot(r5351056, r5351057);
        double r5351059 = 1.0000277305282526;
        bool r5351060 = r5351058 <= r5351059;
        double r5351061 = r5351057 * r5351057;
        double r5351062 = r5351061 * r5351057;
        double r5351063 = r5351062 * r5351062;
        double r5351064 = 0.0673828125;
        double r5351065 = 0.125;
        double r5351066 = 0.0859375;
        double r5351067 = r5351061 * r5351066;
        double r5351068 = r5351065 - r5351067;
        double r5351069 = r5351068 * r5351061;
        double r5351070 = fma(r5351063, r5351064, r5351069);
        double r5351071 = 0.5;
        double r5351072 = r5351071 / r5351058;
        double r5351073 = r5351071 - r5351072;
        double r5351074 = log(r5351073);
        double r5351075 = exp(r5351074);
        double r5351076 = r5351071 + r5351072;
        double r5351077 = sqrt(r5351076);
        double r5351078 = r5351056 + r5351077;
        double r5351079 = r5351075 / r5351078;
        double r5351080 = r5351060 ? r5351070 : r5351079;
        return r5351080;
}

Error

Bits error versus x

Derivation

  1. Split input into 2 regimes

  2. if (hypot 1 x) < 1.0000277305282526

    1. Initial program 30.9

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

    2. Simplified30.9

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

    3. 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}}\]

    4. 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.0000277305282526 < (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 flip--1.0

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

    5. Simplified0.0

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

    7. Applied add-exp-log0.0

      \[\leadsto \frac{\color{blue}{e^{\log \left(\frac{1}{2} - \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}}}{1 + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}}\]
  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.0000277305282526:\\ \;\;\;\;\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{e^{\log \left(\frac{1}{2} - \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}}}\\ \end{array}\]

Reproduce

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