2nthrt (problem 3.4.6)

Average Error: 33.0 → 24.0

Time: 19.7s

Precision: 64

• could not determine a ground truth for program body

  1. x = 1.199947025871061e+147
  2. n = 1.4433187213430084e-221

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 -7.7456503819782359 \cdot 10^{-30}:\\ \;\;\;\;\left(\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}\right) \cdot \left(\left(1 \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{\frac{1}{n}}{2}\right)} + {\left(\sqrt{x}\right)}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt[3]{\left(\sqrt{{\left(x + 1\right)}^{\left(\frac{\frac{1}{n}}{2}\right)}} + {\left(\sqrt{\sqrt{x}}\right)}^{\left(\frac{1}{n}\right)}\right) \cdot \left(\sqrt{{\left(x + 1\right)}^{\left(\frac{\frac{1}{n}}{2}\right)}} - {\left(\sqrt{\sqrt{x}}\right)}^{\left(\frac{1}{n}\right)}\right)}\right)\\ \mathbf{elif}\;\frac{1}{n} \le 3.6323271639935607 \cdot 10^{-11}:\\ \;\;\;\;\frac{1}{x} \cdot \left(\frac{1}{n} - \frac{\log \left(\frac{1}{x}\right)}{{n}^{2}}\right) + \frac{-0.5}{{x}^{2} \cdot n}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(x + 1\right)}^{\left(2 \cdot \frac{1}{n}\right)} + \left(-{x}^{\left(2 \cdot \frac{1}{n}\right)}\right)}{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} + {x}^{\left(\frac{1}{n}\right)}}\\ \end{array}\]

C

double f(double x, double n) {
        double r116356 = x;
        double r116357 = 1.0;
        double r116358 = r116356 + r116357;
        double r116359 = n;
        double r116360 = r116357 / r116359;
        double r116361 = pow(r116358, r116360);
        double r116362 = pow(r116356, r116360);
        double r116363 = r116361 - r116362;
        return r116363;
}

↓

double f(double x, double n) {
        double r116364 = 1.0;
        double r116365 = n;
        double r116366 = r116364 / r116365;
        double r116367 = -7.745650381978236e-30;
        bool r116368 = r116366 <= r116367;
        double r116369 = x;
        double r116370 = r116369 + r116364;
        double r116371 = pow(r116370, r116366);
        double r116372 = pow(r116369, r116366);
        double r116373 = r116371 - r116372;
        double r116374 = cbrt(r116373);
        double r116375 = r116374 * r116374;
        double r116376 = 1.0;
        double r116377 = 2.0;
        double r116378 = r116366 / r116377;
        double r116379 = pow(r116370, r116378);
        double r116380 = sqrt(r116369);
        double r116381 = pow(r116380, r116366);
        double r116382 = r116379 + r116381;
        double r116383 = cbrt(r116382);
        double r116384 = r116376 * r116383;
        double r116385 = sqrt(r116379);
        double r116386 = sqrt(r116380);
        double r116387 = pow(r116386, r116366);
        double r116388 = r116385 + r116387;
        double r116389 = r116385 - r116387;
        double r116390 = r116388 * r116389;
        double r116391 = cbrt(r116390);
        double r116392 = r116384 * r116391;
        double r116393 = r116375 * r116392;
        double r116394 = 3.6323271639935607e-11;
        bool r116395 = r116366 <= r116394;
        double r116396 = r116364 / r116369;
        double r116397 = r116376 / r116365;
        double r116398 = r116376 / r116369;
        double r116399 = log(r116398);
        double r116400 = pow(r116365, r116377);
        double r116401 = r116399 / r116400;
        double r116402 = r116397 - r116401;
        double r116403 = r116396 * r116402;
        double r116404 = 0.5;
        double r116405 = -r116404;
        double r116406 = pow(r116369, r116377);
        double r116407 = r116406 * r116365;
        double r116408 = r116405 / r116407;
        double r116409 = r116403 + r116408;
        double r116410 = r116377 * r116366;
        double r116411 = pow(r116370, r116410);
        double r116412 = pow(r116369, r116410);
        double r116413 = -r116412;
        double r116414 = r116411 + r116413;
        double r116415 = r116371 + r116372;
        double r116416 = r116414 / r116415;
        double r116417 = r116395 ? r116409 : r116416;
        double r116418 = r116368 ? r116393 : r116417;
        return r116418;
}

Error

Bits error versus x

Bits error versus n

Derivation

1. Split input into 3 regimes

2. if (/ 1.0 n) < -7.745650381978236e-30

   1. Initial program 7.6

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

   3. Applied add-cube-cbrt 7.6

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

   5. Applied add-sqr-sqrt 7.6

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

   6. Applied unpow-prod-down 7.6

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

   7. Applied sqr-pow 7.6

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

   8. Applied difference-of-squares 7.6

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

   9. Applied cbrt-prod 7.6

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

   11. Applied add-sqr-sqrt 7.6

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

   12. Applied sqrt-prod 7.6

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

   13. Applied unpow-prod-down 7.6

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

   14. Applied add-sqr-sqrt 7.6

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

   15. Applied difference-of-squares 7.6

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

   17. Applied *-un-lft-identity 7.6

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

   if -7.745650381978236e-30 < (/ 1.0 n) < 3.6323271639935607e-11

   1. Initial program 44.9

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

   2. Taylor expanded around inf 32.4

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

   3. Simplified 31.8

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

   if 3.6323271639935607e-11 < (/ 1.0 n)

   1. Initial program 7.4

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

   3. Applied flip-- 7.4

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

   4. Simplified 7.3

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

4. Final simplification 24.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1}{n} \le -7.7456503819782359 \cdot 10^{-30}:\\ \;\;\;\;\left(\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}\right) \cdot \left(\left(1 \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{\frac{1}{n}}{2}\right)} + {\left(\sqrt{x}\right)}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt[3]{\left(\sqrt{{\left(x + 1\right)}^{\left(\frac{\frac{1}{n}}{2}\right)}} + {\left(\sqrt{\sqrt{x}}\right)}^{\left(\frac{1}{n}\right)}\right) \cdot \left(\sqrt{{\left(x + 1\right)}^{\left(\frac{\frac{1}{n}}{2}\right)}} - {\left(\sqrt{\sqrt{x}}\right)}^{\left(\frac{1}{n}\right)}\right)}\right)\\ \mathbf{elif}\;\frac{1}{n} \le 3.6323271639935607 \cdot 10^{-11}:\\ \;\;\;\;\frac{1}{x} \cdot \left(\frac{1}{n} - \frac{\log \left(\frac{1}{x}\right)}{{n}^{2}}\right) + \frac{-0.5}{{x}^{2} \cdot n}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(x + 1\right)}^{\left(2 \cdot \frac{1}{n}\right)} + \left(-{x}^{\left(2 \cdot \frac{1}{n}\right)}\right)}{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} + {x}^{\left(\frac{1}{n}\right)}}\\ \end{array}\]

Reproduce

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