Average Error: 36.6 → 0.6
Time: 2.9m
Precision: 64
Internal Precision: 128
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[(\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)}\right) + \left(\frac{(\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos x}\right) + 1)_* \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot (e^{\log_* (1 + \frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x})} - 1)^*}\right))_* + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)} - \frac{\sin x}{\cos x}\right)\]

Error

Bits error versus x

Bits error versus eps

Target

Original36.6
Target14.9
Herbie0.6
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Initial program 36.6

    \[\tan \left(x + \varepsilon\right) - \tan x\]
  2. Using strategy rm

  3. Applied tan-sum21.6

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

  5. Applied flip--21.7

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

  6. Applied associate-/r/21.7

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

  7. Applied fma-neg21.6

    \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) + \left(-\tan x\right))_*}\]

  8. Simplified21.6

    \[\leadsto (\color{blue}{\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right)} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) + \left(-\tan x\right))_*\]

  9. Taylor expanded around -inf 21.8

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

  10. Simplified0.6

    \[\leadsto \color{blue}{(\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)}\right) + \left(\frac{(\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos x}\right) + 1)_* \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)}\right))_* + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)} - \frac{\sin x}{\cos x}\right)}\]
  11. Using strategy rm

  12. Applied expm1-log1p-u0.6

    \[\leadsto (\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)}\right) + \left(\frac{(\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos x}\right) + 1)_* \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \color{blue}{(e^{\log_* (1 + \frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x})} - 1)^*}}\right))_* + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)} - \frac{\sin x}{\cos x}\right)\]

  13. Final simplification0.6

    \[\leadsto (\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)}\right) + \left(\frac{(\left(\frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin x}{\cos x}\right) + 1)_* \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot (e^{\log_* (1 + \frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x})} - 1)^*}\right))_* + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos \varepsilon} \cdot \frac{\sin x}{\cos \varepsilon}\right) \cdot \left(\frac{\sin \varepsilon}{\cos x} \cdot \frac{\sin \varepsilon}{\cos x}\right)} - \frac{\sin x}{\cos x}\right)\]

Reproduce

herbie shell --seed 2019022 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))

Details

Time bar (total: 2.9m)Debug log

sample368.0ms

Algorithm
intervals
Results
162.0ms97×body1280valid
100.0ms66×body640valid
62.0ms21×body2560valid
15.0ms19×body320valid
9.0ms16×body160valid
8.0ms37×body80valid

simplify7.0ms

Counts
1 → 1
Calls
1 calls:
Slowest
7.0ms
(- (tan (+ x eps)) (tan x))

prune10.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 38.3b

localize26.0ms

Local error

Found 2 expressions with local error:

3.9b
(tan (+ x eps))
1.3b
(- (tan (+ x eps)) (tan x))

rewrite15.0ms

Algorithm
rewrite-expression-head
Rules
11×*-un-lft-identity
11×add-sqr-sqrt
9×add-cube-cbrt
9×prod-diff
4×add-log-exp
4×tan-quot
3×fma-neg
2×log1p-expm1-u
2×frac-sub
2×add-exp-log
2×add-cbrt-cube
2×tan-sum
2×pow1
2×expm1-log1p-u
1×difference-of-squares
1×distribute-lft-out--
1×flip--
1×diff-log
1×flip3--
1×sub-neg
Counts
2 → 41
Calls
2 calls:
Slowest
12.0ms
(- (tan (+ x eps)) (tan x))
3.0ms
(tan (+ x eps))

series184.0ms

Counts
2 → 6
Calls
2 calls:
Slowest
106.0ms
(- (tan (+ x eps)) (tan x))
76.0ms
(tan (+ x eps))

simplify1.1s

Counts
35 → 47
Calls
35 calls:
Slowest
241.0ms
(- (* (+ (tan x) (tan eps)) (cos x)) (* (- 1 (* (tan x) (tan eps))) (sin x)))
215.0ms
(+ (* x (pow eps 2)) (+ eps (* (pow x 2) eps)))
118.0ms
(* (- 1 (* (tan x) (tan eps))) (cos x))
74.0ms
(+ x (+ (* 1/3 (pow x 3)) eps))
39.0ms
(fma (sqrt (tan (+ x eps))) (sqrt (tan (+ x eps))) (- (* (sqrt (tan x)) (sqrt (tan x)))))

prune488.0ms

Pruning

8 alts after pruning (8 fresh and 0 done)

Merged error: 17.3b

localize33.0ms

Local error

Found 4 expressions with local error:

2.9b
(- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))
0.2b
(* (tan x) (tan eps))
0.1b
(+ (tan x) (tan eps))
0.1b
(/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))

rewrite88.0ms

Algorithm
rewrite-expression-head
Rules
102×*-un-lft-identity
71×add-sqr-sqrt
66×add-cube-cbrt
61×times-frac
54×prod-diff
18×fma-neg
17×distribute-lft-out
10×associate-/r/
9×tan-quot
8×add-log-exp
8×add-exp-log
8×add-cbrt-cube
6×flip--
6×flip3--
6×pow1
5×div-inv
4×associate-/l*
4×log1p-expm1-u
4×expm1-log1p-u
3×associate-/l/
3×associate-*l*
3×associate-*r*
3×fma-def
3×associate-/r*
2×difference-of-squares
2×flip-+
2×frac-add
2×flip3-+
1×distribute-lft-out--
1×cbrt-unprod
1×frac-sub
1×*-commutative
1×associate-*r/
1×prod-exp
1×associate-*l/
1×pow-prod-down
1×div-exp
1×diff-log
1×frac-2neg
1×sub-neg
1×sum-log
1×clear-num
1×+-commutative
1×cbrt-undiv
1×frac-times
Counts
4 → 168
Calls
4 calls:
Slowest
44.0ms
(- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))
24.0ms
(/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))
8.0ms
(* (tan x) (tan eps))
7.0ms
(+ (tan x) (tan eps))

series849.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
402.0ms
(- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))
239.0ms
(/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))
108.0ms
(* (tan x) (tan eps))
101.0ms
(+ (tan x) (tan eps))

simplify13.3s

Counts
199 → 180
Calls
199 calls:
Slowest
472.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan x) (tan eps)))) (cbrt (- 1 (* (tan x) (tan eps)))))) (/ (+ (tan x) (tan eps)) (cbrt (- 1 (* (tan x) (tan eps))))) (- (* (sqrt (tan x)) (sqrt (tan x)))))
463.0ms
(fma (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (+ (* 1 1) (+ (* (* (tan x) (tan eps)) (* (tan x) (tan eps))) (* 1 (* (tan x) (tan eps))))) (- (* (cbrt (tan x)) (* (cbrt (tan x)) (cbrt (tan x))))))
435.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan x) (tan eps)))) (cbrt (- 1 (* (tan x) (tan eps)))))) (/ (+ (tan x) (tan eps)) (cbrt (- 1 (* (tan x) (tan eps))))) (- (* (sqrt (tan x)) (sqrt (tan x)))))
428.0ms
(fma (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (+ (* 1 1) (+ (* (* (tan x) (tan eps)) (* (tan x) (tan eps))) (* 1 (* (tan x) (tan eps))))) (- (* (tan x) 1)))
421.0ms
(fma (/ 1 1) (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (- (* (sqrt (tan x)) (sqrt (tan x)))))

prune1.8s

Pruning

13 alts after pruning (13 fresh and 0 done)

Merged error: 17.2b

localize33.0ms

Local error

Found 4 expressions with local error:

2.9b
(fma (/ (+ (tan x) (tan eps)) (- 1 (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (+ 1 (* (tan x) (tan eps))) (- (tan x)))
0.3b
(* (* (tan eps) (tan x)) (* (tan eps) (tan x)))
0.2b
(* (tan x) (tan eps))
0.2b
(* (tan eps) (tan x))

rewrite30.0ms

Algorithm
rewrite-expression-head
Rules
40×tan-quot
35×pow1
20×add-exp-log
20×add-cbrt-cube
19×frac-times
15×pow-prod-down
13×associate-*r/
13×associate-*l/
10×cbrt-unprod
10×prod-exp
8×add-cube-cbrt
8×*-un-lft-identity
8×add-sqr-sqrt
7×associate-*l*
7×associate-*r*
4×add-log-exp
4×log1p-expm1-u
4×pow-prod-up
4×expm1-log1p-u
3×*-commutative
2×pow-plus
1×fma-udef
1×pow2
Counts
4 → 100
Calls
4 calls:
Slowest
21.0ms
(* (* (tan eps) (tan x)) (* (tan eps) (tan x)))
4.0ms
(* (tan x) (tan eps))
4.0ms
(* (tan eps) (tan x))
0.0ms
(fma (/ (+ (tan x) (tan eps)) (- 1 (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (+ 1 (* (tan x) (tan eps))) (- (tan x)))

series833.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
559.0ms
(fma (/ (+ (tan x) (tan eps)) (- 1 (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (+ 1 (* (tan x) (tan eps))) (- (tan x)))
102.0ms
(* (* (tan eps) (tan x)) (* (tan eps) (tan x)))
90.0ms
(* (tan eps) (tan x))
82.0ms
(* (tan x) (tan eps))

simplify4.3s

Counts
84 → 112
Calls
84 calls:
Slowest
518.0ms
(* (* (* (* (tan eps) (tan eps)) (tan eps)) (* (* (tan x) (tan x)) (tan x))) (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))))
469.0ms
(* (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))) (* (* (* (tan eps) (tan eps)) (tan eps)) (* (* (tan x) (tan x)) (tan x))))
460.0ms
(* (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))) (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))))
411.0ms
(/ (* (pow (sin x) 2) (pow (sin eps) 2)) (* (pow (cos x) 2) (pow (cos eps) 2)))
304.0ms
(/ (* (pow (sin x) 2) (pow (sin eps) 2)) (* (pow (cos x) 2) (pow (cos eps) 2)))

prune1.4s

Pruning

9 alts after pruning (9 fresh and 0 done)

Merged error: 0.2b

localize82.0ms

Local error

Found 4 expressions with local error:

0.8b
(- (/ (/ (sin x) (cos x)) (- 1 (* (* (/ (sin x) (cos eps)) (/ (sin x) (cos eps))) (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))))) (/ (sin x) (cos x)))
0.3b
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))
0.3b
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))
0.3b
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))

rewrite91.0ms

Algorithm
rewrite-expression-head
Rules
1394×times-frac
872×add-sqr-sqrt
857×*-un-lft-identity
851×add-cube-cbrt
585×prod-diff
107×div-inv
45×fma-neg
40×add-exp-log
40×add-cbrt-cube
39×associate-*l*
39×associate-*r*
28×associate-/r/
19×pow1
15×flip--
15×flip3--
12×cbrt-unprod
12×prod-exp
12×div-exp
12×cbrt-undiv
6×difference-of-squares
6×add-log-exp
4×log1p-expm1-u
4×expm1-log1p-u
3×pow-prod-up
3×*-commutative
3×associate-*r/
3×associate-*l/
3×pow-prod-down
3×pow-plus
3×frac-times
3×pow2
2×distribute-lft-out--
1×frac-sub
1×diff-log
1×sub-neg
Counts
4 → 806
Calls
4 calls:
Slowest
36.0ms
(- (/ (/ (sin x) (cos x)) (- 1 (* (* (/ (sin x) (cos eps)) (/ (sin x) (cos eps))) (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))))) (/ (sin x) (cos x)))
7.0ms
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))
7.0ms
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))
7.0ms
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))

series413.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
243.0ms
(- (/ (/ (sin x) (cos x)) (- 1 (* (* (/ (sin x) (cos eps)) (/ (sin x) (cos eps))) (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))))) (/ (sin x) (cos x)))
58.0ms
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))
56.0ms
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))
56.0ms
(* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))

simplify2.1m

Counts
1367 → 818
Calls
1367 calls:
Slowest
527.0ms
(* (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))) (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))))
523.0ms
(* (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))) (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))))
522.0ms
(* (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))) (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))))
466.0ms
(fma (/ (/ 1 1) (* (cbrt (- 1 (* (* (/ (sin x) (cos eps)) (/ (sin x) (cos eps))) (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))))) (cbrt (- 1 (* (* (/ (sin x) (cos eps)) (/ (sin x) (cos eps))) (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x)))))))) (/ (/ (sin x) (cos x)) (cbrt (- 1 (* (* (/ (sin x) (cos eps)) (/ (sin x) (cos eps))) (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))))))) (- (* (/ (sqrt (sin x)) (sqrt (cos x))) (/ (sqrt (sin x)) (sqrt (cos x))))))
465.0ms
(* (* (* (/ (sin eps) (cos x)) (/ (sin eps) (cos x))) (/ (sin eps) (cos x))) (/ (* (* (sin eps) (sin eps)) (sin eps)) (* (* (cos x) (cos x)) (cos x))))

prune12.2s

Pruning

11 alts after pruning (11 fresh and 0 done)

Merged error: 0.2b

regimes185.0ms

Accuracy

0% (0.3b remaining)

Error of 0.6b against oracle of 0.3b and baseline of 0.6b

bsearch3.0ms

end0.0ms

sample9.3s

Algorithm
intervals
Results
5.0s3261×body1280valid
1.7s1824×body640valid
1.6s651×body2560valid
528.0ms790×body320valid
264.0ms1115×body80valid
121.0ms359×body160valid