2nthrt (problem 3.4.6)

Average Error: 29.5 → 22.2

Time: 19.2s

Precision: 64

• could not determine a ground truth for program body

  1. x = 1.6987679971172172e+148
  2. n = 8.851090425825177e-257

Math

\[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1}{n} \le -2.154325354581484357283788222403586587461 \cdot 10^{-5} \lor \neg \left(\frac{1}{n} \le 3.198641373964683341512287228572030275955 \cdot 10^{-22}\right):\\ \;\;\;\;\left(\sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} - \sqrt{{x}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt{{x}^{\left(\frac{1}{n}\right)}} + \left(\sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} - \sqrt{{x}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} + \sqrt{{x}^{\left(\frac{1}{n}\right)}}\right) \cdot \left(\left(-0.25 \cdot \left(\frac{1}{{x}^{2} \cdot n} + \frac{\log \left(\frac{1}{x}\right)}{x \cdot {n}^{2}}\right)\right) + \frac{\frac{0.5}{n}}{x}\right)\\ \end{array}\]

C

double f(double x, double n) {
        double r63700 = x;
        double r63701 = 1.0;
        double r63702 = r63700 + r63701;
        double r63703 = n;
        double r63704 = r63701 / r63703;
        double r63705 = pow(r63702, r63704);
        double r63706 = pow(r63700, r63704);
        double r63707 = r63705 - r63706;
        return r63707;
}

↓

double f(double x, double n) {
        double r63708 = 1.0;
        double r63709 = n;
        double r63710 = r63708 / r63709;
        double r63711 = -2.1543253545814844e-05;
        bool r63712 = r63710 <= r63711;
        double r63713 = 3.1986413739646833e-22;
        bool r63714 = r63710 <= r63713;
        double r63715 = !r63714;
        bool r63716 = r63712 || r63715;
        double r63717 = x;
        double r63718 = r63717 + r63708;
        double r63719 = pow(r63718, r63710);
        double r63720 = sqrt(r63719);
        double r63721 = pow(r63717, r63710);
        double r63722 = sqrt(r63721);
        double r63723 = r63720 - r63722;
        double r63724 = r63723 * r63722;
        double r63725 = r63723 * r63720;
        double r63726 = r63724 + r63725;
        double r63727 = r63720 + r63722;
        double r63728 = 0.25;
        double r63729 = 1.0;
        double r63730 = 2.0;
        double r63731 = pow(r63717, r63730);
        double r63732 = r63731 * r63709;
        double r63733 = r63729 / r63732;
        double r63734 = r63729 / r63717;
        double r63735 = log(r63734);
        double r63736 = pow(r63709, r63730);
        double r63737 = r63717 * r63736;
        double r63738 = r63735 / r63737;
        double r63739 = r63733 + r63738;
        double r63740 = r63728 * r63739;
        double r63741 = -r63740;
        double r63742 = 0.5;
        double r63743 = r63742 / r63709;
        double r63744 = r63743 / r63717;
        double r63745 = r63741 + r63744;
        double r63746 = r63727 * r63745;
        double r63747 = r63716 ? r63726 : r63746;
        return r63747;
}

Error

Bits error versus x

Bits error versus n

Derivation

1. Split input into 3 regimes

2. if (/ 1.0 n) < -2.1543253545814844e-05

   1. Initial program 0.5

      \[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 0.5

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

   4. Applied add-sqr-sqrt 0.5

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

   5. Applied difference-of-squares 0.5

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

   7. Applied add-cbrt-cube 0.5

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

   8. Simplified 0.5

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

   10. Applied add-cube-cbrt 0.5

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

   if -2.1543253545814844e-05 < (/ 1.0 n) < 3.1986413739646833e-22

   1. Initial program 44.9

      \[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 45.0

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

   4. Applied add-sqr-sqrt 45.0

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

   5. Applied difference-of-squares 45.0

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

   6. Taylor expanded around inf 32.6

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

   7. Simplified 32.1

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

   if 3.1986413739646833e-22 < (/ 1.0 n)

   1. Initial program 26.6

      \[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 26.7

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

   4. Applied add-sqr-sqrt 26.7

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

   5. Applied difference-of-squares 26.7

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

   7. Applied add-cbrt-cube 26.7

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

   8. Simplified 26.7

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

   10. Applied add-cube-cbrt 26.7

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

   12. Applied add-cube-cbrt 26.7

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

4. Final simplification 22.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1}{n} \le -2.154325354581484357283788222403586587461 \cdot 10^{-5} \lor \neg \left(\frac{1}{n} \le 3.198641373964683341512287228572030275955 \cdot 10^{-22}\right):\\ \;\;\;\;\left(\sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} - \sqrt{{x}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt{{x}^{\left(\frac{1}{n}\right)}} + \left(\sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} - \sqrt{{x}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} + \sqrt{{x}^{\left(\frac{1}{n}\right)}}\right) \cdot \left(\left(-0.25 \cdot \left(\frac{1}{{x}^{2} \cdot n} + \frac{\log \left(\frac{1}{x}\right)}{x \cdot {n}^{2}}\right)\right) + \frac{\frac{0.5}{n}}{x}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019308 
(FPCore (x n)
  :name "2nthrt (problem 3.4.6)"
  :precision binary64
  (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))))