2isqrt (example 3.6)

Average Error: 19.7 → 10.8

Time: 36.1s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le 8090.627331149180463398806750774383544922:\\ \;\;\;\;\frac{\left(\sqrt{1} \cdot \sqrt{\sqrt{x + 1}} + \sqrt{\sqrt{x}} \cdot \sqrt{1}\right) \cdot \mathsf{fma}\left(\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}}, \sqrt{\frac{1}{\sqrt{x}}}, -{\left(\sqrt{\frac{1}{\sqrt{x + 1}}}\right)}^{3}\right)}{\left(\sqrt{\sqrt{x}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \left(\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}} + \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}} + \sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\left(0.3125 \cdot \left(\sqrt{\frac{1}{{x}^{7}}} \cdot {\left(\sqrt{1}\right)}^{2}\right) + 0.5 \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)\right) - 0.375 \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)\\ \end{array}\]

C

double f(double x) {
        double r353522 = 1.0;
        double r353523 = x;
        double r353524 = sqrt(r353523);
        double r353525 = r353522 / r353524;
        double r353526 = r353523 + r353522;
        double r353527 = sqrt(r353526);
        double r353528 = r353522 / r353527;
        double r353529 = r353525 - r353528;
        return r353529;
}

↓

double f(double x) {
        double r353530 = x;
        double r353531 = 8090.6273311491805;
        bool r353532 = r353530 <= r353531;
        double r353533 = 1.0;
        double r353534 = sqrt(r353533);
        double r353535 = r353530 + r353533;
        double r353536 = sqrt(r353535);
        double r353537 = sqrt(r353536);
        double r353538 = r353534 * r353537;
        double r353539 = sqrt(r353530);
        double r353540 = sqrt(r353539);
        double r353541 = r353540 * r353534;
        double r353542 = r353538 + r353541;
        double r353543 = r353533 / r353539;
        double r353544 = sqrt(r353543);
        double r353545 = r353544 * r353544;
        double r353546 = r353533 / r353536;
        double r353547 = sqrt(r353546);
        double r353548 = 3.0;
        double r353549 = pow(r353547, r353548);
        double r353550 = -r353549;
        double r353551 = fma(r353545, r353544, r353550);
        double r353552 = r353542 * r353551;
        double r353553 = r353540 * r353537;
        double r353554 = r353547 * r353547;
        double r353555 = r353544 * r353547;
        double r353556 = r353554 + r353555;
        double r353557 = r353545 + r353556;
        double r353558 = r353553 * r353557;
        double r353559 = r353552 / r353558;
        double r353560 = 0.3125;
        double r353561 = 1.0;
        double r353562 = 7.0;
        double r353563 = pow(r353530, r353562);
        double r353564 = r353561 / r353563;
        double r353565 = sqrt(r353564);
        double r353566 = 2.0;
        double r353567 = pow(r353534, r353566);
        double r353568 = r353565 * r353567;
        double r353569 = r353560 * r353568;
        double r353570 = 0.5;
        double r353571 = pow(r353530, r353548);
        double r353572 = r353561 / r353571;
        double r353573 = sqrt(r353572);
        double r353574 = r353573 * r353567;
        double r353575 = r353570 * r353574;
        double r353576 = r353569 + r353575;
        double r353577 = 0.375;
        double r353578 = 5.0;
        double r353579 = pow(r353530, r353578);
        double r353580 = r353561 / r353579;
        double r353581 = sqrt(r353580);
        double r353582 = r353581 * r353567;
        double r353583 = r353577 * r353582;
        double r353584 = r353576 - r353583;
        double r353585 = r353532 ? r353559 : r353584;
        return r353585;
}

Error

Bits error versus x

Target

Original	19.7
Target	0.6
Herbie	10.8

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

Derivation

1. Split input into 2 regimes

2. if x < 8090.6273311491805

   1. Initial program 0.3

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

   3. Applied add-sqr-sqrt 0.4

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

   4. Applied add-sqr-sqrt 0.7

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

   5. Applied difference-of-squares 0.7

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

   7. Applied flip3-- 0.7

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

   8. Applied sqrt-div 0.7

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

   9. Applied sqrt-div 0.7

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

   10. Applied frac-add 0.7

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

   11. Applied frac-times 0.7

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

   13. Applied unpow3 0.6

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

   14. Applied fma-neg 0.6

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

   if 8090.6273311491805 < x

   1. Initial program 39.5

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

   3. Applied add-sqr-sqrt 49.3

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

   4. Applied add-sqr-sqrt 39.5

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

   5. Applied difference-of-squares 39.5

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

   6. Taylor expanded around inf 21.2

      \[\leadsto \color{blue}{\left(0.3125 \cdot \left(\sqrt{\frac{1}{{x}^{7}}} \cdot {\left(\sqrt{1}\right)}^{2}\right) + 0.5 \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)\right) - 0.375 \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 10.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 8090.627331149180463398806750774383544922:\\ \;\;\;\;\frac{\left(\sqrt{1} \cdot \sqrt{\sqrt{x + 1}} + \sqrt{\sqrt{x}} \cdot \sqrt{1}\right) \cdot \mathsf{fma}\left(\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}}, \sqrt{\frac{1}{\sqrt{x}}}, -{\left(\sqrt{\frac{1}{\sqrt{x + 1}}}\right)}^{3}\right)}{\left(\sqrt{\sqrt{x}} \cdot \sqrt{\sqrt{x + 1}}\right) \cdot \left(\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}} + \left(\sqrt{\frac{1}{\sqrt{x + 1}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}} + \sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x + 1}}}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\left(0.3125 \cdot \left(\sqrt{\frac{1}{{x}^{7}}} \cdot {\left(\sqrt{1}\right)}^{2}\right) + 0.5 \cdot \left(\sqrt{\frac{1}{{x}^{3}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)\right) - 0.375 \cdot \left(\sqrt{\frac{1}{{x}^{5}}} \cdot {\left(\sqrt{1}\right)}^{2}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019354 +o rules:numerics
(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)))))