sqrtexp (problem 3.4.4)

Average Error: 4.7 → 0.1

Time: 20.2s

Precision: 64

• could not determine a ground truth for program body

  1. x = 4.940605716246613e+111

Math

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

↓

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

C

double f(double x) {
        double r19658 = 2.0;
        double r19659 = x;
        double r19660 = r19658 * r19659;
        double r19661 = exp(r19660);
        double r19662 = 1.0;
        double r19663 = r19661 - r19662;
        double r19664 = exp(r19659);
        double r19665 = r19664 - r19662;
        double r19666 = r19663 / r19665;
        double r19667 = sqrt(r19666);
        return r19667;
}

↓

double f(double x) {
        double r19668 = x;
        double r19669 = -1.115913044114018e-11;
        bool r19670 = r19668 <= r19669;
        double r19671 = 2.0;
        double r19672 = r19671 * r19668;
        double r19673 = exp(r19672);
        double r19674 = sqrt(r19673);
        double r19675 = sqrt(r19674);
        double r19676 = r19675 * r19675;
        double r19677 = 1.0;
        double r19678 = sqrt(r19677);
        double r19679 = r19676 + r19678;
        double r19680 = exp(r19671);
        double r19681 = 2.0;
        double r19682 = r19668 / r19681;
        double r19683 = pow(r19680, r19682);
        double r19684 = r19683 - r19678;
        double r19685 = exp(r19668);
        double r19686 = r19685 - r19677;
        double r19687 = r19684 / r19686;
        double r19688 = r19679 * r19687;
        double r19689 = sqrt(r19688);
        double r19690 = 1.1250860145338832e-16;
        bool r19691 = r19668 <= r19690;
        double r19692 = 0.5;
        double r19693 = r19692 * r19668;
        double r19694 = r19677 + r19693;
        double r19695 = r19668 * r19694;
        double r19696 = r19695 + r19671;
        double r19697 = sqrt(r19696);
        double r19698 = r19671 + r19671;
        double r19699 = exp(r19698);
        double r19700 = r19682 / r19681;
        double r19701 = pow(r19699, r19700);
        double r19702 = r19701 + r19678;
        double r19703 = r19702 * r19687;
        double r19704 = sqrt(r19703);
        double r19705 = r19691 ? r19697 : r19704;
        double r19706 = r19670 ? r19689 : r19705;
        return r19706;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -1.115913044114018e-11

   1. Initial program 0.5

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

   3. Applied *-un-lft-identity 0.5

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

   4. Applied add-sqr-sqrt 0.5

      \[\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.5

      \[\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.1

      \[\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.1

      \[\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.1

      \[\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.1

       \[\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.1

       \[\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. Using strategy rm

   14. Applied add-sqr-sqrt 0.0

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

   15. Applied sqrt-prod 0.0

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

   if -1.115913044114018e-11 < x < 1.1250860145338832e-16

   1. Initial program 54.6

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

   2. Taylor expanded around 0 0.0

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

   3. Simplified 0.0

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

   if 1.1250860145338832e-16 < x

   1. Initial program 17.4

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

   3. Applied *-un-lft-identity 17.4

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

   4. Applied add-sqr-sqrt 17.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 14.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 7.4

      \[\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 7.4

      \[\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 7.4

      \[\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 7.4

       \[\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 7.5

       \[\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 2.1

       \[\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. Using strategy rm

   14. Applied add-sqr-sqrt 2.1

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

   15. Applied sqrt-prod 2.2

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

   17. Applied add-log-exp 2.2

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

   18. Applied exp-to-pow 2.2

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

   19. Applied sqrt-pow1 2.2

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

   20. Applied sqrt-pow1 2.2

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

   21. Applied add-log-exp 2.2

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

   22. Applied exp-to-pow 2.2

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

   23. Applied sqrt-pow1 1.3

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

   24. Applied sqrt-pow1 1.3

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

   25. Applied pow-prod-down 1.3

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

   26. Simplified 1.1

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

4. Final simplification 0.1

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

Reproduce

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