sqrtexp (problem 3.4.4)

Average Error: 4.4 → 0.1

Time: 12.8s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

• could not determine a ground truth for program body

  1. x = 1.3481840315279074e+121

Math

\[\sqrt{\frac{e^{2 \cdot x} - 1}{e^{x} - 1}}\]

↓

\[\sqrt{1} \cdot \sqrt{\mathsf{fma}\left(\sqrt{e^{x}}, \sqrt{e^{x}}, 1\right)}\]

C

double f(double x) {
        double r11172 = 2.0;
        double r11173 = x;
        double r11174 = r11172 * r11173;
        double r11175 = exp(r11174);
        double r11176 = 1.0;
        double r11177 = r11175 - r11176;
        double r11178 = exp(r11173);
        double r11179 = r11178 - r11176;
        double r11180 = r11177 / r11179;
        double r11181 = sqrt(r11180);
        return r11181;
}

↓

double f(double x) {
        double r11182 = 1.0;
        double r11183 = sqrt(r11182);
        double r11184 = x;
        double r11185 = exp(r11184);
        double r11186 = sqrt(r11185);
        double r11187 = fma(r11186, r11186, r11182);
        double r11188 = sqrt(r11187);
        double r11189 = r11183 * r11188;
        return r11189;
}

Error

Bits error versus x

Derivation

1. Initial program 4.4

   \[\sqrt{\frac{e^{2 \cdot x} - 1}{e^{x} - 1}}\]
2. Using strategy rm

3. Applied flip-- 4.0

   \[\leadsto \sqrt{\frac{e^{2 \cdot x} - 1}{\color{blue}{\frac{e^{x} \cdot e^{x} - 1 \cdot 1}{e^{x} + 1}}}}\]

4. Applied associate-/r/ 4.0

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

5. Applied sqrt-prod 4.0

   \[\leadsto \color{blue}{\sqrt{\frac{e^{2 \cdot x} - 1}{e^{x} \cdot e^{x} - 1 \cdot 1}} \cdot \sqrt{e^{x} + 1}}\]

6. Simplified 2.9

   \[\leadsto \color{blue}{\sqrt{\frac{e^{2 \cdot x} - 1}{e^{x + x} - 1 \cdot 1}}} \cdot \sqrt{e^{x} + 1}\]

7. Taylor expanded around 0 0.1

   \[\leadsto \sqrt{\color{blue}{1}} \cdot \sqrt{e^{x} + 1}\]
8. Using strategy rm

9. Applied add-sqr-sqrt 0.1

   \[\leadsto \sqrt{1} \cdot \sqrt{\color{blue}{\sqrt{e^{x}} \cdot \sqrt{e^{x}}} + 1}\]

10. Applied fma-def 0.1

    \[\leadsto \sqrt{1} \cdot \sqrt{\color{blue}{\mathsf{fma}\left(\sqrt{e^{x}}, \sqrt{e^{x}}, 1\right)}}\]

11. Final simplification 0.1

    \[\leadsto \sqrt{1} \cdot \sqrt{\mathsf{fma}\left(\sqrt{e^{x}}, \sqrt{e^{x}}, 1\right)}\]

Reproduce

herbie shell --seed 2019350 +o rules:numerics
(FPCore (x)
  :name "sqrtexp (problem 3.4.4)"
  :precision binary64
  (sqrt (/ (- (exp (* 2 x)) 1) (- (exp x) 1))))