2nthrt (problem 3.4.6)

Average Error: 33.0 → 24.0

Time: 12.0s

Precision: 64

• could not determine a ground truth for program body

  1. x = 2160916163285.2522
  2. n = 8.244208103801466e-74

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;n \le -35447295026.760864 \lor \neg \left(n \le 604142.656624356867\right):\\ \;\;\;\;\frac{\frac{1 - \left(\frac{\frac{0.5}{n}}{x} \cdot n - x \cdot \frac{\log x \cdot 1}{x \cdot n}\right)}{x}}{n}\\ \mathbf{else}:\\ \;\;\;\;{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\\ \end{array}\]

C

double code(double x, double n) {
	return (pow((x + 1.0), (1.0 / n)) - pow(x, (1.0 / n)));
}

↓

double code(double x, double n) {
	double VAR;
	if (((n <= -35447295026.760864) || !(n <= 604142.6566243569))) {
		VAR = (((1.0 - ((((0.5 / n) / x) * n) - (x * ((log(x) * 1.0) / (x * n))))) / x) / n);
	} else {
		VAR = (pow((x + 1.0), (1.0 / n)) - pow(x, (1.0 / n)));
	}
	return VAR;
}

Error

Bits error versus x

Bits error versus n

Derivation

1. Split input into 2 regimes

2. if n < -35447295026.760864 or 604142.6566243569 < n

   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.8

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

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

   5. Applied unpow2 32.3

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

   6. Applied associate-*r* 32.3

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

   7. Applied associate-/r* 32.3

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

   8. Applied unpow2 32.3

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

   9. Applied associate-/r* 32.1

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

   10. Applied frac-sub 32.1

       \[\leadsto \frac{\frac{1}{n}}{x} - \color{blue}{\frac{\frac{\frac{0.5}{n}}{x} \cdot n - x \cdot \frac{\log x \cdot 1}{x \cdot n}}{x \cdot n}}\]

   11. Applied associate-/l/ 32.7

       \[\leadsto \color{blue}{\frac{1}{x \cdot n}} - \frac{\frac{\frac{0.5}{n}}{x} \cdot n - x \cdot \frac{\log x \cdot 1}{x \cdot n}}{x \cdot n}\]

   12. Applied sub-div 32.7

       \[\leadsto \color{blue}{\frac{1 - \left(\frac{\frac{0.5}{n}}{x} \cdot n - x \cdot \frac{\log x \cdot 1}{x \cdot n}\right)}{x \cdot n}}\]
   13. Using strategy rm

   14. Applied associate-/r* 32.3

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

   if -35447295026.760864 < n < 604142.6566243569

   1. Initial program 3.3

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

4. Final simplification 24.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;n \le -35447295026.760864 \lor \neg \left(n \le 604142.656624356867\right):\\ \;\;\;\;\frac{\frac{1 - \left(\frac{\frac{0.5}{n}}{x} \cdot n - x \cdot \frac{\log x \cdot 1}{x \cdot n}\right)}{x}}{n}\\ \mathbf{else}:\\ \;\;\;\;{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\\ \end{array}\]

Reproduce

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