Average Error: 19.1 → 20.6
Time: 1.3m
Precision: 64
Internal Precision: 1152
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\begin{array}{l} \mathbf{if}\;{\left(\frac{1}{x}\right)}^{\frac{1}{2}} - \frac{1}{\sqrt{x + 1}} \le -4.450147717014403 \cdot 10^{-308}:\\ \;\;\;\;\sqrt{\frac{1}{\sqrt{x}}} \cdot \sqrt{\frac{1}{\sqrt{x}}} - \frac{1}{\sqrt{x + 1}}\\ \mathbf{if}\;{\left(\frac{1}{x}\right)}^{\frac{1}{2}} - \frac{1}{\sqrt{x + 1}} \le 0.0:\\ \;\;\;\;{\left(\frac{1}{x}\right)}^{\frac{1}{2}} - \frac{1}{\sqrt{x + 1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{\sqrt{\sqrt{x}}}}{\sqrt{\sqrt{x}}} - \frac{1}{\sqrt{x + 1}}\\ \end{array}\]

Error

Bits error versus x

Target

Original19.1
Target0.6
Herbie20.6
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Split input into 3 regimes

  2. if (- (pow (/ 1 x) 1/2) (/ 1 (sqrt (+ x 1)))) < -4.450147717014403e-308

    1. Initial program 40.8

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

    3. Applied add-sqr-sqrt50.0

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

    if -4.450147717014403e-308 < (- (pow (/ 1 x) 1/2) (/ 1 (sqrt (+ x 1)))) < 0.0

    1. Initial program 39.2

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

    3. Applied add-sqr-sqrt49.9

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

    5. Applied pow1/249.9

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

    6. Applied pow1/249.9

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

    7. Applied pow-prod-down39.2

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

    8. Applied simplify39.2

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

    if 0.0 < (- (pow (/ 1 x) 1/2) (/ 1 (sqrt (+ x 1))))

    1. Initial program 5.9

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

    3. Applied add-sqr-sqrt7.2

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

    4. Applied associate-/r*7.3

      \[\leadsto \color{blue}{\frac{\frac{1}{\sqrt{\sqrt{x}}}}{\sqrt{\sqrt{x}}}} - \frac{1}{\sqrt{x + 1}}\]
  3. Recombined 3 regimes into one program.

Runtime

Time bar (total: 1.3m)Debug logProfile

herbie shell --seed '#(1070991898 1055468627 4280279443 640792587 928206309 3646738750)' 
(FPCore (x)
  :name "2isqrt (example 3.6)"

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

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