Average Error: 19.9 → 5.7
Time: 44.3s
Precision: 64
Internal Precision: 128
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{\sqrt{\frac{1}{(x \cdot x + x)_*}}}{\frac{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}{\sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}}\]

Error

Bits error versus x

Target

Original19.9
Target0.7
Herbie5.7
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Initial program 19.9

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

  3. Applied flip--20.0

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

  5. Applied frac-times25.0

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

  6. Applied frac-times20.1

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

  7. Applied frac-sub19.8

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

  8. Simplified5.9

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

  9. Simplified5.8

    \[\leadsto \frac{\frac{1}{\color{blue}{(x \cdot x + x)_*}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
  10. Using strategy rm

  11. Applied add-sqr-sqrt5.8

    \[\leadsto \frac{\frac{1}{\color{blue}{\sqrt{(x \cdot x + x)_*} \cdot \sqrt{(x \cdot x + x)_*}}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]

  12. Applied associate-/r*5.8

    \[\leadsto \frac{\color{blue}{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
  13. Using strategy rm

  14. Applied add-sqr-sqrt5.8

    \[\leadsto \frac{\color{blue}{\sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}} \cdot \sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]

  15. Applied associate-/l*5.8

    \[\leadsto \color{blue}{\frac{\sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}{\frac{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}{\sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}}}\]

  16. Simplified5.7

    \[\leadsto \frac{\color{blue}{\sqrt{\frac{1}{(x \cdot x + x)_*}}}}{\frac{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}{\sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}}\]

  17. Final simplification5.7

    \[\leadsto \frac{\sqrt{\frac{1}{(x \cdot x + x)_*}}}{\frac{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}{\sqrt{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}}\]

Reproduce

herbie shell --seed 2019022 +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)))))

Details

Time bar (total: 43.9s)Debug log

sample104.0ms

Algorithm
intervals
Results
29.0ms58×body640valid
21.0ms270×body80nan
17.0ms36×body1280valid
12.0ms126×body80valid
7.0ms21×body320valid
3.0ms15×body160valid

simplify9.0ms

Counts
1 → 1
Calls
1 calls:
Slowest
9.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))

prune4.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 22.4b

localize13.0ms

Local error

Found 3 expressions with local error:

3.9b
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
0.3b
(/ 1 (sqrt x))
0.1b
(/ 1 (sqrt (+ x 1)))

rewrite10.0ms

Algorithm
rewrite-expression-head
Rules
24×prod-diff
21×*-un-lft-identity
19×add-sqr-sqrt
17×div-inv
17×add-cube-cbrt
10×associate-/r/
10×sqrt-div
9×associate-/r*
5×add-log-exp
5×flip-+
5×add-exp-log
5×flip3-+
5×pow1
4×distribute-lft-out--
4×pow-flip
4×fma-neg
3×log1p-expm1-u
3×sqrt-prod
3×add-cbrt-cube
3×expm1-log1p-u
2×inv-pow
2×pow1/2
2×frac-2neg
2×clear-num
2×rec-exp
1×difference-of-squares
1×flip--
1×frac-sub
1×diff-log
1×flip3--
1×sub-neg
Counts
3 → 91
Calls
3 calls:
Slowest
6.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
1.0ms
(/ 1 (sqrt (+ x 1)))
1.0ms
(/ 1 (sqrt x))

series77.0ms

Counts
3 → 9
Calls
3 calls:
Slowest
41.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
20.0ms
(/ 1 (sqrt (+ x 1)))
16.0ms
(/ 1 (sqrt x))

simplify3.1s

Counts
83 → 100
Calls
83 calls:
Slowest
171.0ms
(fma (- (sqrt (+ (* x x) (- (* 1 1) (* x 1))))) (/ 1 (sqrt (+ (pow x 3) (pow 1 3)))) (* (sqrt (+ (* x x) (- (* 1 1) (* x 1)))) (/ 1 (sqrt (+ (pow x 3) (pow 1 3))))))
155.0ms
(fma (- (sqrt (+ (* x x) (- (* 1 1) (* x 1))))) (/ 1 (sqrt (+ (pow x 3) (pow 1 3)))) (* (sqrt (+ (* x x) (- (* 1 1) (* x 1)))) (/ 1 (sqrt (+ (pow x 3) (pow 1 3))))))
152.0ms
(fma (- (sqrt (+ (* x x) (- (* 1 1) (* x 1))))) (/ 1 (sqrt (+ (pow x 3) (pow 1 3)))) (* (sqrt (+ (* x x) (- (* 1 1) (* x 1)))) (/ 1 (sqrt (+ (pow x 3) (pow 1 3))))))
152.0ms
(fma (- (sqrt (- x 1))) (/ 1 (sqrt (- (* x x) (* 1 1)))) (* (sqrt (- x 1)) (/ 1 (sqrt (- (* x x) (* 1 1))))))
149.0ms
(fma (* (cbrt (/ 1 (sqrt x))) (cbrt (/ 1 (sqrt x)))) (cbrt (/ 1 (sqrt x))) (- (* (sqrt (- x 1)) (/ 1 (sqrt (- (* x x) (* 1 1)))))))

prune746.0ms

Pruning

9 alts after pruning (9 fresh and 0 done)

Merged error: 21.7b

localize14.0ms

Local error

Found 4 expressions with local error:

4.0b
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
0.5b
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))
0.3b
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
0.3b
(/ 1 (sqrt x))

rewrite44.0ms

Algorithm
rewrite-expression-head
Rules
40×*-un-lft-identity
32×frac-sub
28×times-frac
24×div-inv
20×distribute-lft-out
20×add-cube-cbrt
20×add-sqr-sqrt
18×associate-/l/
17×un-div-inv
17×associate-*r/
17×associate-*l/
17×frac-times
16×pow1
15×add-exp-log
12×pow-flip
10×associate-/r*
9×difference-of-squares
8×add-cbrt-cube
7×inv-pow
6×add-log-exp
6×pow-prod-up
5×pow1/2
5×rec-exp
4×associate-/l*
4×log1p-expm1-u
4×prod-exp
4×pow-prod-down
4×associate-*l*
4×associate-*r*
4×expm1-log1p-u
3×associate-/r/
2×flip--
2×flip3--
2×frac-2neg
2×clear-num
1×flip-+
1×cbrt-unprod
1×*-commutative
1×frac-add
1×prod-diff
1×div-exp
1×div-sub
1×diff-log
1×fma-neg
1×pow-plus
1×flip3-+
1×sub-neg
1×cbrt-undiv
1×pow2
Counts
4 → 166
Calls
4 calls:
Slowest
25.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
7.0ms
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
7.0ms
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))
1.0ms
(/ 1 (sqrt x))

series98.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
54.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
23.0ms
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
11.0ms
(/ 1 (sqrt x))
10.0ms
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))

simplify15.7s

Counts
179 → 178
Calls
179 calls:
Slowest
432.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
399.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
385.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
367.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
363.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))

prune1.0s

Pruning

5 alts after pruning (5 fresh and 0 done)

Merged error: 6.9b

localize11.0ms

Local error

Found 4 expressions with local error:

6.5b
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
0.5b
(/ 1 (fma x x x))
0.3b
(/ 1 (sqrt x))
0.1b
(/ 1 (sqrt (+ x 1)))

rewrite13.0ms

Algorithm
rewrite-expression-head
Rules
41×*-un-lft-identity
32×div-inv
28×times-frac
21×add-cube-cbrt
21×add-sqr-sqrt
20×distribute-lft-out
19×associate-/r*
11×add-exp-log
7×pow1
6×add-cbrt-cube
5×pow-flip
5×associate-/r/
4×add-log-exp
4×associate-/l*
4×log1p-expm1-u
4×frac-2neg
4×clear-num
4×rec-exp
4×expm1-log1p-u
3×inv-pow
3×sqrt-prod
2×flip-+
2×div-exp
2×sqrt-div
2×pow1/2
2×flip3-+
1×associate-/l/
1×frac-add
1×cbrt-undiv
Counts
4 → 119
Calls
4 calls:
Slowest
9.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
1.0ms
(/ 1 (sqrt (+ x 1)))
1.0ms
(/ 1 (sqrt x))
1.0ms
(/ 1 (fma x x x))

series84.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
49.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
12.0ms
(/ 1 (sqrt x))
12.0ms
(/ 1 (sqrt (+ x 1)))
10.0ms
(/ 1 (fma x x x))

simplify4.6s

Counts
102 → 131
Calls
102 calls:
Slowest
553.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
319.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
318.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
315.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
313.0ms
(/ (/ 1 (fma x x x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))

prune776.0ms

Pruning

7 alts after pruning (7 fresh and 0 done)

Merged error: 6.8b

localize9.0ms

Local error

Found 4 expressions with local error:

14.6b
(sqrt (fma x x x))
14.6b
(sqrt (fma x x x))
6.5b
(/ (/ (/ 1 (sqrt (fma x x x))) (sqrt (fma x x x))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
0.3b
(/ 1 (sqrt x))

rewrite23.0ms

Algorithm
rewrite-expression-head
Rules
388×times-frac
272×*-un-lft-identity
174×div-inv
158×add-sqr-sqrt
156×add-cube-cbrt
116×distribute-lft-out
102×sqrt-prod
28×associate-/l*
13×add-exp-log
10×associate-/r*
9×add-cbrt-cube
5×div-exp
5×pow1
4×add-log-exp
4×log1p-expm1-u
4×expm1-log1p-u
3×associate-/r/
3×pow1/2
3×cbrt-undiv
2×pow-flip
2×frac-2neg
2×clear-num
2×rec-exp
2×rem-sqrt-square
1×associate-/l/
1×inv-pow
1×flip-+
1×frac-add
1×flip3-+
Counts
4 → 299
Calls
4 calls:
Slowest
15.0ms
(/ (/ (/ 1 (sqrt (fma x x x))) (sqrt (fma x x x))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
1.0ms
(sqrt (fma x x x))
1.0ms
(/ 1 (sqrt x))
1.0ms
(sqrt (fma x x x))

series89.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
51.0ms
(/ (/ (/ 1 (sqrt (fma x x x))) (sqrt (fma x x x))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
14.0ms
(sqrt (fma x x x))
14.0ms
(sqrt (fma x x x))
10.0ms
(/ 1 (sqrt x))

simplify12.8s

Counts
460 → 311
Calls
460 calls:
Slowest
184.0ms
(+ (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (- (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))) (* (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))))
158.0ms
(/ (/ (* (cbrt (/ 1 (sqrt (fma x x x)))) (cbrt (/ 1 (sqrt (fma x x x))))) (* (cbrt (sqrt (fma x x x))) (cbrt (sqrt (fma x x x))))) (* (cbrt (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))) (cbrt (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))))
136.0ms
(/ (/ (* (cbrt (/ 1 (sqrt (fma x x x)))) (cbrt (/ 1 (sqrt (fma x x x))))) 1) (* (cbrt (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))) (cbrt (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))))
133.0ms
(/ (/ (* (cbrt (/ 1 (sqrt (fma x x x)))) (cbrt (/ 1 (sqrt (fma x x x))))) (* (cbrt (sqrt (fma x x x))) (cbrt (sqrt (fma x x x))))) 1)
133.0ms
(/ (/ (* (cbrt (/ 1 (sqrt (fma x x x)))) (cbrt (/ 1 (sqrt (fma x x x))))) (* (cbrt (sqrt (fma x x x))) (cbrt (sqrt (fma x x x))))) 1)

prune2.2s

Pruning

5 alts after pruning (4 fresh and 1 done)

Merged error: 6.8b

regimes28.0ms

Accuracy

0% (0.2b remaining)

Error of 5.7b against oracle of 5.5b and baseline of 5.7b

bsearch2.0ms

end0.0ms

sample2.2s

Algorithm
intervals
Results
691.0ms1775×body640valid
524.0ms8004×body80nan
385.0ms1165×body1280valid
293.0ms4065×body80valid
126.0ms654×body320valid
39.0ms341×body160valid