Average Error: 19.5 → 0.4
Time: 30.8s
Precision: 64
Internal Precision: 128
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{\frac{1}{1 + x}}{\frac{x}{\sqrt{1 + x}} + \frac{x}{\sqrt{x}}}\]

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

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

Derivation

  1. Initial program 19.5

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

  3. Applied flip--19.5

    \[\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-times24.5

    \[\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-times19.6

    \[\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.4

    \[\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.7

    \[\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.6

    \[\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 div-inv5.6

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

  12. Applied div-inv5.6

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

  13. Applied distribute-lft-out5.6

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

  14. Applied *-un-lft-identity5.6

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

  15. Applied times-frac5.6

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

  16. Simplified5.6

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

  17. Simplified0.4

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

  19. Applied *-un-lft-identity0.4

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

  20. Applied associate-/r*0.4

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

  21. Final simplification0.4

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

Reproduce

herbie shell --seed 2019021 
(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: 30.4s)Debug log

sample80.0ms

Algorithm
intervals
Results
16.0ms64×body640valid
14.0ms263×body80nan
11.0ms138×body80valid
9.0ms28×body1280valid
4.0ms21×body320valid
1.0ms6×body160valid

simplify10.0ms

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

prune5.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 19.4b

localize31.0ms

Local error

Found 4 expressions with local error:

2.3b
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
0.3b
(/ 1 (sqrt x))
0.2b
(/ 1 (sqrt (+ x 1)))
0.0b
(sqrt (+ x 1))

rewrite10.0ms

Algorithm
rewrite-expression-head
Rules
12×*-un-lft-identity
11×add-sqr-sqrt
9×associate-/r*
8×add-cube-cbrt
6×add-log-exp
6×div-inv
6×sqrt-prod
6×add-exp-log
6×pow1
4×distribute-lft-out--
4×pow-flip
4×sqrt-div
4×add-cbrt-cube
3×pow1/2
2×inv-pow
2×flip-+
2×associate-/r/
2×flip3-+
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
1×rem-sqrt-square
Counts
4 → 71
Calls
4 calls:
Slowest
7.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
1.0ms
(/ 1 (sqrt (+ x 1)))
1.0ms
(/ 1 (sqrt x))
1.0ms
(sqrt (+ x 1))

series65.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
27.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
16.0ms
(/ 1 (sqrt (+ x 1)))
12.0ms
(/ 1 (sqrt x))
10.0ms
(sqrt (+ x 1))

simplify376.0ms

Counts
42 → 83
Calls
42 calls:
Slowest
81.0ms
(- (+ (* 1/2 x) 1) (* 1/8 (pow x 2)))
73.0ms
(- (+ (* 3/8 (pow x 2)) 1) (* 1/2 x))
29.0ms
(sqrt (+ (* x x) (- (* 1 1) (* x 1))))
29.0ms
(sqrt (- (* x x) (* 1 1)))
26.0ms
(/ (exp (/ 1 (sqrt x))) (exp (/ 1 (sqrt (+ x 1)))))

prune606.0ms

Pruning

13 alts after pruning (13 fresh and 0 done)

Merged error: 18.8b

localize28.0ms

Local error

Found 4 expressions with local error:

2.3b
(- (* (/ 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))

rewrite47.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×prod-exp
4×pow-prod-down
4×associate-*l*
4×associate-*r*
3×associate-/r/
2×flip--
2×flip3--
2×frac-2neg
2×clear-num
1×flip-+
1×cbrt-unprod
1×*-commutative
1×frac-add
1×div-exp
1×div-sub
1×diff-log
1×pow-plus
1×flip3-+
1×sub-neg
1×cbrt-undiv
1×pow2
Counts
4 → 156
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)))))
12.0ms
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
4.0ms
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))
2.0ms
(/ 1 (sqrt x))

series89.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
48.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
20.0ms
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
11.0ms
(/ 1 (sqrt x))
9.0ms
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))

simplify15.9s

Counts
176 → 168
Calls
176 calls:
Slowest
620.0ms
(/ (* (cbrt (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))) (cbrt (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))))) (* (cbrt (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))) (cbrt (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))))
439.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
371.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
368.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
313.0ms
(- (log (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))) (log (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))))

prune961.0ms

Pruning

4 alts after pruning (4 fresh and 0 done)

Merged error: 5.3b

localize10.0ms

Local error

Found 4 expressions with local error:

4.8b
(/ (/ 1 (+ (* x x) x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
0.7b
(/ 1 (+ (* x x) x))
0.3b
(/ 1 (sqrt x))
0.2b
(/ 1 (sqrt (+ x 1)))

rewrite15.0ms

Algorithm
rewrite-expression-head
Rules
51×*-un-lft-identity
42×times-frac
40×div-inv
28×distribute-lft-out
23×add-cube-cbrt
23×associate-/r/
23×add-sqr-sqrt
20×associate-/r*
11×flip-+
11×add-exp-log
11×flip3-+
7×pow1
6×associate-/l*
6×add-cbrt-cube
5×pow-flip
4×add-log-exp
4×frac-2neg
4×clear-num
4×rec-exp
3×inv-pow
3×sqrt-prod
2×div-exp
2×sqrt-div
2×pow1/2
1×associate-/l/
1×frac-add
1×distribute-lft1-in
1×cbrt-undiv
Counts
4 → 130
Calls
4 calls:
Slowest
10.0ms
(/ (/ 1 (+ (* x x) x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
2.0ms
(/ 1 (+ (* x x) x))
1.0ms
(/ 1 (sqrt (+ x 1)))
1.0ms
(/ 1 (sqrt x))

series81.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
50.0ms
(/ (/ 1 (+ (* x x) x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
12.0ms
(/ 1 (sqrt (+ x 1)))
11.0ms
(/ 1 (sqrt x))
8.0ms
(/ 1 (+ (* x x) x))

simplify5.7s

Counts
134 → 142
Calls
134 calls:
Slowest
316.0ms
(+ (* (* x x) (* x x)) (- (* x x) (* (* x x) x)))
219.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)
218.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)
215.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)
215.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)

prune812.0ms

Pruning

5 alts after pruning (5 fresh and 0 done)

Merged error: 0.0b

localize17.0ms

Local error

Found 4 expressions with local error:

0.5b
(/ x (sqrt x))
0.3b
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
0.2b
(/ x (sqrt (+ x 1)))
0.0b
(/ 1 (+ x 1))

rewrite12.0ms

Algorithm
rewrite-expression-head
Rules
35×*-un-lft-identity
30×times-frac
24×div-inv
21×add-cube-cbrt
21×add-sqr-sqrt
19×associate-/r/
17×associate-/r*
14×distribute-lft-out
9×flip-+
9×add-exp-log
9×flip3-+
6×associate-/l*
6×add-cbrt-cube
5×pow1
4×add-log-exp
4×frac-2neg
4×clear-num
3×sqrt-prod
2×div-exp
2×sqrt-div
2×rec-exp
1×associate-/l/
1×inv-pow
1×pow-flip
1×frac-add
1×cbrt-undiv
Counts
4 → 107
Calls
4 calls:
Slowest
9.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
1.0ms
(/ 1 (+ x 1))
1.0ms
(/ x (sqrt (+ x 1)))
0.0ms
(/ x (sqrt x))

series94.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
52.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
19.0ms
(/ x (sqrt (+ x 1)))
16.0ms
(/ x (sqrt x))
6.0ms
(/ 1 (+ x 1))

simplify2.6s

Counts
104 → 119
Calls
104 calls:
Slowest
175.0ms
(+ (* (/ x (sqrt x)) (/ x (sqrt x))) (- (* (/ x (sqrt (+ x 1))) (/ x (sqrt (+ x 1)))) (* (/ x (sqrt x)) (/ x (sqrt (+ x 1))))))
167.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
167.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
167.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
166.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))

prune667.0ms

Pruning

6 alts after pruning (6 fresh and 0 done)

Merged error: 0.0b

regimes28.0ms

Accuracy

0% (0.3b remaining)

Error of 0.4b against oracle of 0.0b and baseline of 0.4b

bsearch2.0ms

end0.0ms

sample2.1s

Algorithm
intervals
Results
738.0ms7849×body80nan
476.0ms1830×body640valid
403.0ms1091×body1280valid
230.0ms4145×body80valid
123.0ms612×body320valid
35.0ms323×body160valid