2isqrt (example 3.6)

Average Error: 20.2 → 0.3

Time: 4.0s

Precision: 64

Math

\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]

↓

\[\frac{\frac{1 \cdot 1}{x + \sqrt{x} \cdot \sqrt{x + 1}}}{\sqrt{x + 1}}\]

C

double code(double x) {
	return ((1.0 / sqrt(x)) - (1.0 / sqrt((x + 1.0))));
}

↓

double code(double x) {
	return (((1.0 * 1.0) / (x + (sqrt(x) * sqrt((x + 1.0))))) / sqrt((x + 1.0)));
}

Error

Bits error versus x

Target

Original	20.2
Target	0.7
Herbie	0.3

\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

1. Initial program 20.2

   \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
2. Using strategy rm

3. Applied frac-sub 20.2

   \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}}}\]

4. Simplified 20.2

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

6. Applied flip-- 19.9

   \[\leadsto \frac{1 \cdot \color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - \sqrt{x} \cdot \sqrt{x}}{\sqrt{x + 1} + \sqrt{x}}}}{\sqrt{x} \cdot \sqrt{x + 1}}\]

7. Simplified 0.4

   \[\leadsto \frac{1 \cdot \frac{\color{blue}{1 + 0}}{\sqrt{x + 1} + \sqrt{x}}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
8. Using strategy rm

9. Applied associate-/r* 0.4

   \[\leadsto \color{blue}{\frac{\frac{1 \cdot \frac{1 + 0}{\sqrt{x + 1} + \sqrt{x}}}{\sqrt{x}}}{\sqrt{x + 1}}}\]

10. Simplified 0.3

    \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1}{x + \sqrt{x} \cdot \sqrt{x + 1}}}}{\sqrt{x + 1}}\]

11. Final simplification 0.3

    \[\leadsto \frac{\frac{1 \cdot 1}{x + \sqrt{x} \cdot \sqrt{x + 1}}}{\sqrt{x + 1}}\]

Reproduce

herbie shell --seed 2020078 
(FPCore (x)
  :name "2isqrt (example 3.6)"
  :precision binary64

  :herbie-target
  (/ 1 (+ (* (+ x 1) (sqrt x)) (* x (sqrt (+ x 1)))))

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))