Average Error: 15.3 → 14.9
Time: 16.5s
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{\log \left(e^{\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{fma}\left(1, 1, \left(-0.5\right) \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)\right)}\right)}{\sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5} + 1}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{\log \left(e^{\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{fma}\left(1, 1, \left(-0.5\right) \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)\right)}\right)}{\sqrt{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5} + 1}
double f(double x) {
        double r176346 = 1.0;
        double r176347 = 0.5;
        double r176348 = x;
        double r176349 = hypot(r176346, r176348);
        double r176350 = r176346 / r176349;
        double r176351 = r176346 + r176350;
        double r176352 = r176347 * r176351;
        double r176353 = sqrt(r176352);
        double r176354 = r176346 - r176353;
        return r176354;
}
↓
double f(double x) {
        double r176355 = 1.0;
        double r176356 = 0.5;
        double r176357 = -r176356;
        double r176358 = x;
        double r176359 = hypot(r176355, r176358);
        double r176360 = r176355 / r176359;
        double r176361 = r176355 + r176360;
        double r176362 = r176357 * r176361;
        double r176363 = fma(r176355, r176355, r176362);
        double r176364 = log1p(r176363);
        double r176365 = expm1(r176364);
        double r176366 = exp(r176365);
        double r176367 = log(r176366);
        double r176368 = r176361 * r176356;
        double r176369 = sqrt(r176368);
        double r176370 = r176369 + r176355;
        double r176371 = r176367 / r176370;
        return r176371;
}

Error

Bits error versus x

Derivation

  1. Initial program 15.3

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

  3. Applied flip--15.3

    \[\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. Simplified14.8

    \[\leadsto \frac{\color{blue}{1 \cdot 1 - 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)}}\]

  5. Simplified14.8

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

  7. Applied add-log-exp14.9

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

  8. Applied add-log-exp14.9

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

  9. Applied diff-log15.3

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

  10. Simplified14.9

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

  12. Applied expm1-log1p-u14.9

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

  13. Simplified14.9

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

  14. Final simplification14.9

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

Reproduce

herbie shell --seed 2019196 +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)))))))