sqrtexp (problem 3.4.4)

Average Error: 4.4 → 0.9

Time: 10.5s

Precision: 64

• could not determine a ground truth for program body

  1. x = 6.49265952778414e+132

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -5.52196569000031793 \cdot 10^{-7}:\\ \;\;\;\;\sqrt{\frac{1}{\frac{\sqrt{e^{x}} + \sqrt{1}}{\sqrt{\sqrt{e^{2 \cdot x}}} + \sqrt{\sqrt{1}}}}} \cdot \sqrt{\frac{\sqrt{e^{2 \cdot x}} + \sqrt{1}}{\frac{\sqrt{e^{x}} - \sqrt{1}}{\sqrt{\sqrt{e^{2 \cdot x}}} - \sqrt{\sqrt{1}}}}}\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot \frac{x}{\sqrt{2}} + \left(\sqrt{2} + \frac{{x}^{2}}{\sqrt{2}} \cdot \left(0.25 - \frac{0.125}{2}\right)\right)\\ \end{array}\]

C

double f(double x) {
        double r45585 = 2.0;
        double r45586 = x;
        double r45587 = r45585 * r45586;
        double r45588 = exp(r45587);
        double r45589 = 1.0;
        double r45590 = r45588 - r45589;
        double r45591 = exp(r45586);
        double r45592 = r45591 - r45589;
        double r45593 = r45590 / r45592;
        double r45594 = sqrt(r45593);
        return r45594;
}

↓

double f(double x) {
        double r45595 = x;
        double r45596 = -5.521965690000318e-07;
        bool r45597 = r45595 <= r45596;
        double r45598 = 1.0;
        double r45599 = exp(r45595);
        double r45600 = sqrt(r45599);
        double r45601 = 1.0;
        double r45602 = sqrt(r45601);
        double r45603 = r45600 + r45602;
        double r45604 = 2.0;
        double r45605 = r45604 * r45595;
        double r45606 = exp(r45605);
        double r45607 = sqrt(r45606);
        double r45608 = sqrt(r45607);
        double r45609 = sqrt(r45602);
        double r45610 = r45608 + r45609;
        double r45611 = r45603 / r45610;
        double r45612 = r45598 / r45611;
        double r45613 = sqrt(r45612);
        double r45614 = r45607 + r45602;
        double r45615 = r45600 - r45602;
        double r45616 = r45608 - r45609;
        double r45617 = r45615 / r45616;
        double r45618 = r45614 / r45617;
        double r45619 = sqrt(r45618);
        double r45620 = r45613 * r45619;
        double r45621 = 0.5;
        double r45622 = sqrt(r45604);
        double r45623 = r45595 / r45622;
        double r45624 = r45621 * r45623;
        double r45625 = 2.0;
        double r45626 = pow(r45595, r45625);
        double r45627 = r45626 / r45622;
        double r45628 = 0.25;
        double r45629 = 0.125;
        double r45630 = r45629 / r45604;
        double r45631 = r45628 - r45630;
        double r45632 = r45627 * r45631;
        double r45633 = r45622 + r45632;
        double r45634 = r45624 + r45633;
        double r45635 = r45597 ? r45620 : r45634;
        return r45635;
}

Error

Bits error versus x

Derivation

1. Split input into 2 regimes

2. if x < -5.521965690000318e-07

   1. Initial program 0.1

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

   3. Applied add-sqr-sqrt 0.1

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

   4. 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}}{e^{x} - 1}}\]

   5. 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)}}{e^{x} - 1}}\]

   6. Applied associate-/l* 0.0

      \[\leadsto \sqrt{\color{blue}{\frac{\sqrt{e^{2 \cdot x}} + \sqrt{1}}{\frac{e^{x} - 1}{\sqrt{e^{2 \cdot x}} - \sqrt{1}}}}}\]
   7. Using strategy rm

   8. Applied add-sqr-sqrt 0.0

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

   9. Applied sqrt-prod 0.0

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

   10. Applied add-sqr-sqrt 0.0

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

   11. Applied sqrt-prod 0.1

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

   12. Applied difference-of-squares 0.2

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

   13. Applied add-sqr-sqrt 0.2

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

   14. Applied add-sqr-sqrt 0.1

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

   15. Applied difference-of-squares 0.0

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

   16. Applied times-frac 0.0

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

   17. Applied *-un-lft-identity 0.0

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

   18. Applied times-frac 0.0

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

   19. Applied sqrt-prod 0.0

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

   if -5.521965690000318e-07 < x

   1. Initial program 34.9

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

   2. Taylor expanded around 0 7.2

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

   3. Simplified 7.2

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

4. Final simplification 0.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -5.52196569000031793 \cdot 10^{-7}:\\ \;\;\;\;\sqrt{\frac{1}{\frac{\sqrt{e^{x}} + \sqrt{1}}{\sqrt{\sqrt{e^{2 \cdot x}}} + \sqrt{\sqrt{1}}}}} \cdot \sqrt{\frac{\sqrt{e^{2 \cdot x}} + \sqrt{1}}{\frac{\sqrt{e^{x}} - \sqrt{1}}{\sqrt{\sqrt{e^{2 \cdot x}}} - \sqrt{\sqrt{1}}}}}\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot \frac{x}{\sqrt{2}} + \left(\sqrt{2} + \frac{{x}^{2}}{\sqrt{2}} \cdot \left(0.25 - \frac{0.125}{2}\right)\right)\\ \end{array}\]

Reproduce

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