Average Error: 19.2 → 18.9
Time: 30.7s
Precision: 64
Internal Precision: 1088
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\begin{array}{l} \mathbf{if}\;\frac{(\left({x}^{\left(-\frac{1}{2}\right)}\right) \cdot \left({x}^{\left(-\frac{1}{2}\right)}\right) + \left(\frac{-1}{x + 1}\right))_*}{{x}^{\left(-\frac{1}{2}\right)} + \frac{1}{\sqrt{x + 1}}} \le 6.746107001627108 \cdot 10^{-82}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{\sqrt{x}} - \frac{\frac{1}{x + 1}}{\sqrt{x + 1}}}{\frac{\frac{1}{\sqrt{x}}}{\sqrt{x + 1}} + \left(\frac{1}{x} + \frac{1}{x + 1}\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{(\left({x}^{\left(-\frac{1}{2}\right)}\right) \cdot \left({x}^{\left(-\frac{1}{2}\right)}\right) + \left(\frac{-1}{x + 1}\right))_*}{{x}^{\left(-\frac{1}{2}\right)} + \frac{1}{\sqrt{x + 1}}}\\ \end{array}\]

Error

Bits error versus x

Target

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

Derivation

  1. Split input into 2 regimes

  2. if (/ (fma (pow x (- 1/2)) (pow x (- 1/2)) (/ (- 1) (+ x 1))) (+ (pow x (- 1/2)) (/ 1 (sqrt (+ x 1))))) < 6.746107001627108e-82

    1. Initial program 34.8

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

    3. Applied add-sqr-sqrt48.3

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

    5. Applied flip3--35.1

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

    6. Applied simplify34.8

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

    7. Applied simplify34.8

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

    if 6.746107001627108e-82 < (/ (fma (pow x (- 1/2)) (pow x (- 1/2)) (/ (- 1) (+ x 1))) (+ (pow x (- 1/2)) (/ 1 (sqrt (+ x 1)))))

    1. Initial program 9.6

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

    3. Applied pow1/29.6

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

    4. Applied pow-flip9.3

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

    6. Applied flip--9.3

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

    7. Applied simplify9.1

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

Runtime

Time bar (total: 30.7s)Debug logProfile

herbie shell --seed '#(1071246582 2318319007 2683472949 3810440501 3233274817 2724848749)' +o rules:numerics
(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)))))