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

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original19.9
Target0.7
Herbie0.4
\[\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 *-un-lft-identity5.8

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

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

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

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

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

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

  17. Simplified0.3

    \[\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 add-sqr-sqrt0.3

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

  20. Applied sqrt-prod0.4

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

  21. Applied associate-/r*0.4

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

  22. Final simplification0.4

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

Reproduce

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

sample96.0ms

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

simplify10.0ms

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

prune29.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 22.4b

localize29.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)))

rewrite15.0ms

Algorithm
rewrite-expression-head
Rules
10×*-un-lft-identity
9×associate-/r*
8×add-sqr-sqrt
6×div-inv
6×add-cube-cbrt
5×add-log-exp
5×add-exp-log
5×pow1
4×distribute-lft-out--
4×pow-flip
3×sqrt-prod
3×add-cbrt-cube
2×inv-pow
2×associate-/r/
2×sqrt-div
2×pow1/2
2×frac-2neg
2×clear-num
2×rec-exp
1×difference-of-squares
1×flip--
1×flip-+
1×frac-sub
1×diff-log
1×flip3--
1×flip3-+
1×sub-neg
Counts
3 → 57
Calls
3 calls:
Slowest
10.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
2.0ms
(/ 1 (sqrt (+ x 1)))
1.0ms
(/ 1 (sqrt x))

series65.0ms

Counts
3 → 9
Calls
3 calls:
Slowest
30.0ms
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
18.0ms
(/ 1 (sqrt x))
17.0ms
(/ 1 (sqrt (+ x 1)))

simplify184.0ms

Counts
33 → 66
Calls
33 calls:
Slowest
43.0ms
(- (+ (* 3/8 (pow x 2)) 1) (* 1/2 x))
33.0ms
(sqrt (+ (* x x) (- (* 1 1) (* x 1))))
20.0ms
(- (* 1 (sqrt (+ x 1))) (* (sqrt x) 1))
19.0ms
(/ (exp (/ 1 (sqrt x))) (exp (/ 1 (sqrt (+ x 1)))))
11.0ms
(- (sqrt (/ 1 (sqrt x))) (sqrt (/ 1 (sqrt (+ x 1)))))

prune495.0ms

Pruning

10 alts after pruning (10 fresh and 0 done)

Merged error: 21.7b

localize24.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))

rewrite62.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
37.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
13.0ms
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
9.0ms
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))
1.0ms
(/ 1 (sqrt x))

series97.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
53.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
19.0ms
(- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1)))))
13.0ms
(* (/ 1 (sqrt x)) (/ 1 (sqrt x)))
12.0ms
(/ 1 (sqrt x))

simplify15.0s

Counts
176 → 168
Calls
176 calls:
Slowest
401.0ms
(- (* (* 1 1) (sqrt (+ x 1))) (* (* (sqrt x) (sqrt x)) (/ 1 (sqrt (+ x 1)))))
398.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
383.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
376.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
360.0ms
(/ (- (* (/ 1 (sqrt x)) (/ 1 (sqrt x))) (* (/ 1 (sqrt (+ x 1))) (/ 1 (sqrt (+ x 1))))) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))

prune1.4s

Pruning

5 alts after pruning (5 fresh and 0 done)

Merged error: 6.9b

localize10.0ms

Local error

Found 4 expressions with local error:

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

rewrite18.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
12.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))

series107.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
62.0ms
(/ (/ 1 (+ (* x x) x)) (+ (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))
19.0ms
(/ 1 (sqrt (+ x 1)))
15.0ms
(/ 1 (sqrt x))
11.0ms
(/ 1 (+ (* x x) x))

simplify5.3s

Counts
134 → 142
Calls
134 calls:
Slowest
322.0ms
(+ (* (* x x) (* x x)) (- (* x x) (* (* x x) x)))
210.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)
208.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)
207.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)
205.0ms
(/ (/ 1 (- (* (* x x) (* x x)) (* x x))) 1)

prune932.0ms

Pruning

7 alts after pruning (7 fresh and 0 done)

Merged error: 0.1b

localize15.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.3b
(/ x (sqrt (+ x 1)))
0.0b
(+ (/ x (sqrt x)) (/ x (sqrt (+ x 1))))

rewrite19.0ms

Algorithm
rewrite-expression-head
Rules
36×*-un-lft-identity
30×times-frac
25×div-inv
20×add-cube-cbrt
20×add-sqr-sqrt
17×associate-/r/
16×distribute-lft-out
14×associate-/r*
9×flip-+
9×flip3-+
8×add-exp-log
6×add-log-exp
6×associate-/l*
6×add-cbrt-cube
4×pow1
3×sqrt-prod
3×frac-2neg
3×clear-num
2×frac-add
2×div-exp
2×sqrt-div
1×associate-/l/
1×sum-log
1×rec-exp
1×+-commutative
1×cbrt-undiv
Counts
4 → 103
Calls
4 calls:
Slowest
9.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
5.0ms
(+ (/ x (sqrt x)) (/ x (sqrt (+ x 1))))
1.0ms
(/ x (sqrt (+ x 1)))
0.0ms
(/ x (sqrt x))

series124.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
51.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
35.0ms
(+ (/ x (sqrt x)) (/ x (sqrt (+ x 1))))
21.0ms
(/ x (sqrt (+ x 1)))
16.0ms
(/ x (sqrt x))

simplify2.4s

Counts
103 → 115
Calls
103 calls:
Slowest
163.0ms
(+ (* (/ x (sqrt x)) (/ x (sqrt x))) (- (* (/ x (sqrt (+ x 1))) (/ x (sqrt (+ x 1)))) (* (/ x (sqrt x)) (/ x (sqrt (+ x 1))))))
163.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
162.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
162.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))
162.0ms
(/ (/ 1 (+ x 1)) (+ (/ x (sqrt x)) (/ x (sqrt (+ x 1)))))

prune654.0ms

Pruning

9 alts after pruning (9 fresh and 0 done)

Merged error: 0b

regimes43.0ms

Accuracy

0% (0.3b remaining)

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

bsearch1.0ms

end0.0ms

sample2.2s

Algorithm
intervals
Results
786.0ms1775×body640valid
449.0ms1165×body1280valid
436.0ms8004×body80nan
236.0ms4065×body80valid
129.0ms654×body320valid
39.0ms341×body160valid