sqrtexp (problem 3.4.4)

Average Error: 4.7 → 0.2

Time: 5.7s

Precision: 64

• could not determine a ground truth for program body

  1. x = 9.924781450718653e+287

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -8.128074973713997003282004383262204783023 \cdot 10^{-6}:\\ \;\;\;\;\sqrt{\left(\sqrt{e^{2 \cdot x}} + \sqrt{1}\right) \cdot \frac{\sqrt[3]{{\left({\left(e^{2}\right)}^{\left(\frac{1}{2} \cdot x\right)} - \sqrt{1}\right)}^{3}}}{e^{x} - 1}}\\ \mathbf{elif}\;x \le 4.626269415052568020683340637978732054481 \cdot 10^{-10}:\\ \;\;\;\;\sqrt{x \cdot \left(1 + 0.5 \cdot x\right) + 2}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(\sqrt{e^{2 \cdot x}} + \sqrt{1}\right) \cdot \frac{\sqrt{e^{2 \cdot x}} - \sqrt{1}}{e^{x} - 1}}\\ \end{array}\]

C

double f(double x) {
        double r11362 = 2.0;
        double r11363 = x;
        double r11364 = r11362 * r11363;
        double r11365 = exp(r11364);
        double r11366 = 1.0;
        double r11367 = r11365 - r11366;
        double r11368 = exp(r11363);
        double r11369 = r11368 - r11366;
        double r11370 = r11367 / r11369;
        double r11371 = sqrt(r11370);
        return r11371;
}

↓

double f(double x) {
        double r11372 = x;
        double r11373 = -8.128074973713997e-06;
        bool r11374 = r11372 <= r11373;
        double r11375 = 2.0;
        double r11376 = r11375 * r11372;
        double r11377 = exp(r11376);
        double r11378 = sqrt(r11377);
        double r11379 = 1.0;
        double r11380 = sqrt(r11379);
        double r11381 = r11378 + r11380;
        double r11382 = exp(r11375);
        double r11383 = 0.5;
        double r11384 = r11383 * r11372;
        double r11385 = pow(r11382, r11384);
        double r11386 = r11385 - r11380;
        double r11387 = 3.0;
        double r11388 = pow(r11386, r11387);
        double r11389 = cbrt(r11388);
        double r11390 = exp(r11372);
        double r11391 = r11390 - r11379;
        double r11392 = r11389 / r11391;
        double r11393 = r11381 * r11392;
        double r11394 = sqrt(r11393);
        double r11395 = 4.626269415052568e-10;
        bool r11396 = r11372 <= r11395;
        double r11397 = 0.5;
        double r11398 = r11397 * r11372;
        double r11399 = r11379 + r11398;
        double r11400 = r11372 * r11399;
        double r11401 = r11400 + r11375;
        double r11402 = sqrt(r11401);
        double r11403 = r11378 - r11380;
        double r11404 = r11403 / r11391;
        double r11405 = r11381 * r11404;
        double r11406 = sqrt(r11405);
        double r11407 = r11396 ? r11402 : r11406;
        double r11408 = r11374 ? r11394 : r11407;
        return r11408;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -8.128074973713997e-06

   1. Initial program 0.1

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

   3. Applied *-un-lft-identity 0.1

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

   4. Applied add-sqr-sqrt 0.1

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

   5. Applied add-sqr-sqrt 0.1

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

   6. Applied difference-of-squares 0.0

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

   7. Applied times-frac 0.0

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

   8. Simplified 0.0

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

   10. Applied add-log-exp 0.0

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

   11. Applied exp-to-pow 0.0

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

   12. Applied sqrt-pow1 0.0

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

   13. Simplified 0.0

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

   15. Applied add-cbrt-cube 0.0

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

   16. Simplified 0.0

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

   if -8.128074973713997e-06 < x < 4.626269415052568e-10

   1. Initial program 44.6

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

   2. Taylor expanded around 0 0.1

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

   3. Simplified 0.1

      \[\leadsto \sqrt{\color{blue}{x \cdot \left(1 + 0.5 \cdot x\right) + 2}}\]

   if 4.626269415052568e-10 < x

   1. Initial program 12.4

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

   3. Applied *-un-lft-identity 12.4

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

   4. Applied add-sqr-sqrt 12.4

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

   5. Applied add-sqr-sqrt 12.0

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

   6. Applied difference-of-squares 4.5

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

   7. Applied times-frac 4.5

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

   8. Simplified 4.5

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

4. Final simplification 0.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -8.128074973713997003282004383262204783023 \cdot 10^{-6}:\\ \;\;\;\;\sqrt{\left(\sqrt{e^{2 \cdot x}} + \sqrt{1}\right) \cdot \frac{\sqrt[3]{{\left({\left(e^{2}\right)}^{\left(\frac{1}{2} \cdot x\right)} - \sqrt{1}\right)}^{3}}}{e^{x} - 1}}\\ \mathbf{elif}\;x \le 4.626269415052568020683340637978732054481 \cdot 10^{-10}:\\ \;\;\;\;\sqrt{x \cdot \left(1 + 0.5 \cdot x\right) + 2}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\left(\sqrt{e^{2 \cdot x}} + \sqrt{1}\right) \cdot \frac{\sqrt{e^{2 \cdot x}} - \sqrt{1}}{e^{x} - 1}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019356 
(FPCore (x)
  :name "sqrtexp (problem 3.4.4)"
  :precision binary64
  (sqrt (/ (- (exp (* 2 x)) 1) (- (exp x) 1))))