2nthrt (problem 3.4.6)

Average Error: 29.8 → 19.6

Time: 32.4s

Precision: 64

• could not determine a ground truth for program body

  1. x = 4.804422053352139e+304
  2. n = 9.69669249590372e-232

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 -3.2155947364724913 \cdot 10^{-22}:\\ \;\;\;\;\mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \sqrt[3]{\left(\left({\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) \cdot \left({\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)\right) \cdot \left(\mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \mathsf{fma}\left(1, {\left(x + 1\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot \left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)\right)\right)}\\ \mathbf{elif}\;\frac{1}{n} \le 4.2228249751738446 \cdot 10^{-17}:\\ \;\;\;\;\left(\frac{\log x}{x \cdot \left(n \cdot n\right)} + \frac{1}{x \cdot n}\right) - \frac{\frac{\frac{1}{2}}{n}}{x \cdot x}\\ \mathbf{else}:\\ \;\;\;\;e^{\frac{\mathsf{log1p}\left(x\right)}{n}} - {x}^{\left(\frac{1}{n}\right)}\\ \end{array}\]

C

double f(double x, double n) {
        double r3487276 = x;
        double r3487277 = 1.0;
        double r3487278 = r3487276 + r3487277;
        double r3487279 = n;
        double r3487280 = r3487277 / r3487279;
        double r3487281 = pow(r3487278, r3487280);
        double r3487282 = pow(r3487276, r3487280);
        double r3487283 = r3487281 - r3487282;
        return r3487283;
}

↓

double f(double x, double n) {
        double r3487284 = 1.0;
        double r3487285 = n;
        double r3487286 = r3487284 / r3487285;
        double r3487287 = -3.2155947364724913e-22;
        bool r3487288 = r3487286 <= r3487287;
        double r3487289 = x;
        double r3487290 = cbrt(r3487289);
        double r3487291 = pow(r3487290, r3487286);
        double r3487292 = -r3487291;
        double r3487293 = r3487290 * r3487290;
        double r3487294 = pow(r3487293, r3487286);
        double r3487295 = r3487294 * r3487291;
        double r3487296 = fma(r3487292, r3487294, r3487295);
        double r3487297 = r3487289 + r3487284;
        double r3487298 = pow(r3487297, r3487286);
        double r3487299 = r3487298 - r3487295;
        double r3487300 = r3487299 * r3487299;
        double r3487301 = r3487294 * r3487292;
        double r3487302 = fma(r3487284, r3487298, r3487301);
        double r3487303 = r3487296 + r3487302;
        double r3487304 = r3487300 * r3487303;
        double r3487305 = cbrt(r3487304);
        double r3487306 = r3487296 + r3487305;
        double r3487307 = 4.2228249751738446e-17;
        bool r3487308 = r3487286 <= r3487307;
        double r3487309 = log(r3487289);
        double r3487310 = r3487285 * r3487285;
        double r3487311 = r3487289 * r3487310;
        double r3487312 = r3487309 / r3487311;
        double r3487313 = r3487289 * r3487285;
        double r3487314 = r3487284 / r3487313;
        double r3487315 = r3487312 + r3487314;
        double r3487316 = 0.5;
        double r3487317 = r3487316 / r3487285;
        double r3487318 = r3487289 * r3487289;
        double r3487319 = r3487317 / r3487318;
        double r3487320 = r3487315 - r3487319;
        double r3487321 = log1p(r3487289);
        double r3487322 = r3487321 / r3487285;
        double r3487323 = exp(r3487322);
        double r3487324 = pow(r3487289, r3487286);
        double r3487325 = r3487323 - r3487324;
        double r3487326 = r3487308 ? r3487320 : r3487325;
        double r3487327 = r3487288 ? r3487306 : r3487326;
        return r3487327;
}

Error

Bits error versus x

Bits error versus n

Derivation

1. Split input into 3 regimes

2. if (/ 1 n) < -3.2155947364724913e-22

   1. Initial program 2.7

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

   3. Applied add-cube-cbrt 2.7

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

   4. Applied unpow-prod-down 2.7

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

   5. Applied sqr-pow 2.7

      \[\leadsto \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[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\]

   6. Applied prod-diff 2.8

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

   8. Applied add-cbrt-cube 2.8

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

   9. Simplified 2.7

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

   11. Applied *-un-lft-identity 2.7

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

   12. Applied prod-diff 2.7

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

   if -3.2155947364724913e-22 < (/ 1 n) < 4.2228249751738446e-17

   1. Initial program 44.8

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

   2. Taylor expanded around inf 32.2

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

   3. Simplified 32.2

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

   if 4.2228249751738446e-17 < (/ 1 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-exp-log 26.6

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

   4. Applied pow-exp 26.6

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

   5. Simplified 4.8

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

4. Final simplification 19.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1}{n} \le -3.2155947364724913 \cdot 10^{-22}:\\ \;\;\;\;\mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \sqrt[3]{\left(\left({\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) \cdot \left({\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)\right) \cdot \left(\mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \mathsf{fma}\left(1, {\left(x + 1\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot \left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)\right)\right)}\\ \mathbf{elif}\;\frac{1}{n} \le 4.2228249751738446 \cdot 10^{-17}:\\ \;\;\;\;\left(\frac{\log x}{x \cdot \left(n \cdot n\right)} + \frac{1}{x \cdot n}\right) - \frac{\frac{\frac{1}{2}}{n}}{x \cdot x}\\ \mathbf{else}:\\ \;\;\;\;e^{\frac{\mathsf{log1p}\left(x\right)}{n}} - {x}^{\left(\frac{1}{n}\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019163 +o rules:numerics
(FPCore (x n)
  :name "2nthrt (problem 3.4.6)"
  (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))))