Average Error: 17.0 → 4.0
Time: 51.2s
Precision: 64
Internal Precision: 128
\[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\]
↓
\[R \cdot \log \left(e^{\cos^{-1} \left(\sin \phi_2 \cdot \sin \phi_1 + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right) + \left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)\right)\right)}\right)\]

Error

Bits error versus R

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 17.0

    \[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\]
  2. Using strategy rm

  3. Applied cos-diff4.0

    \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right) \cdot R\]
  4. Using strategy rm

  5. Applied distribute-rgt-in4.0

    \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \color{blue}{\left(\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right) + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)\right)}\right) \cdot R\]
  6. Using strategy rm

  7. Applied add-log-exp4.0

    \[\leadsto \color{blue}{\log \left(e^{\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right) + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)\right)\right)}\right)} \cdot R\]

  8. Final simplification4.0

    \[\leadsto R \cdot \log \left(e^{\cos^{-1} \left(\sin \phi_2 \cdot \sin \phi_1 + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\sin \lambda_2 \cdot \sin \lambda_1\right) + \left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)\right)\right)}\right)\]

Reproduce

herbie shell --seed 2019022 
(FPCore (R lambda1 lambda2 phi1 phi2)
  :name "Spherical law of cosines"
  (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))

Details

Time bar (total: 47.9s)Debug log

sample916.0ms

Algorithm
intervals
Results
733.0ms154×body1280valid
91.0ms65×body640valid
19.0ms18×body320valid
6.0ms10×body160valid
3.0ms9×body80valid

simplify26.0ms

Counts
1 → 1
Calls
1 calls:
Slowest
25.0ms
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R)

prune59.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 15.5b

localize69.0ms

Local error

Found 4 expressions with local error:

4.2b
(cos (- lambda1 lambda2))
0.6b
(acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))))
0.2b
(* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))
0.2b
(* (sin phi1) (sin phi2))

rewrite31.0ms

Algorithm
rewrite-expression-head
Rules
11×add-exp-log
11×add-cbrt-cube
11×pow1
7×add-cube-cbrt
7×*-un-lft-identity
7×add-sqr-sqrt
6×associate-*r*
4×add-log-exp
4×cbrt-unprod
4×prod-exp
4×pow-prod-down
4×associate-*l*
3×cos-diff
2×*-commutative
2×cos-sum
1×sin-mult
1×cos-mult
1×associate-*l/
1×distribute-lft-in
1×sub-neg
1×acos-asin
1×distribute-rgt-in
Counts
4 → 57
Calls
4 calls:
Slowest
11.0ms
(* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))
4.0ms
(cos (- lambda1 lambda2))
3.0ms
(* (sin phi1) (sin phi2))
1.0ms
(acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))))

series189.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
104.0ms
(* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))
52.0ms
(* (sin phi1) (sin phi2))
23.0ms
(cos (- lambda1 lambda2))
11.0ms
(acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))))

simplify984.0ms

Counts
37 → 69
Calls
37 calls:
Slowest
216.0ms
(* (* (* (* (cos phi1) (cos phi2)) (* (cos phi1) (cos phi2))) (* (cos phi1) (cos phi2))) (* (* (cos (- lambda1 lambda2)) (cos (- lambda1 lambda2))) (cos (- lambda1 lambda2))))
213.0ms
(* (* (* (* (cos phi1) (cos phi1)) (cos phi1)) (* (* (cos phi2) (cos phi2)) (cos phi2))) (* (* (cos (- lambda1 lambda2)) (cos (- lambda1 lambda2))) (cos (- lambda1 lambda2))))
140.0ms
(- 1 (+ (* 1/2 (pow phi2 2)) (* 1/2 (pow phi1 2))))
91.0ms
(* (* (* (sin phi1) (sin phi1)) (sin phi1)) (* (* (sin phi2) (sin phi2)) (sin phi2)))
49.0ms
(- (+ 1 (* lambda2 lambda1)) (* 1/2 (pow lambda1 2)))

prune1.3s

Pruning

13 alts after pruning (13 fresh and 0 done)

Merged error: 2.3b

localize70.0ms

Local error

Found 4 expressions with local error:

0.6b
(acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))
0.2b
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R)
0.2b
(* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))
0.2b
(* (sin phi1) (sin phi2))

rewrite50.0ms

Algorithm
rewrite-expression-head
Rules
11×add-exp-log
11×add-cbrt-cube
11×pow1
8×add-cube-cbrt
8×*-un-lft-identity
8×add-sqr-sqrt
7×associate-*l*
6×cos-mult
6×associate-*r*
4×add-log-exp
4×cbrt-unprod
4×prod-exp
4×pow-prod-down
3×sin-mult
3×*-commutative
3×associate-*r/
3×frac-times
2×flip-+
2×frac-add
2×flip3-+
1×associate-*l/
1×distribute-lft-in
1×acos-asin
1×distribute-rgt-in
Counts
4 → 64
Calls
4 calls:
Slowest
36.0ms
(* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))
7.0ms
(* (sin phi1) (sin phi2))
5.0ms
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R)
2.0ms
(acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))

series437.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
236.0ms
(* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))
106.0ms
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R)
68.0ms
(* (sin phi1) (sin phi2))
28.0ms
(acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))

simplify3.7s

Counts
45 → 76
Calls
45 calls:
Slowest
369.0ms
(* (+ (cos (+ phi1 phi2)) (cos (- phi1 phi2))) (+ (* (+ (cos (+ lambda1 lambda2)) (cos (- lambda1 lambda2))) 2) (* 2 (- (cos (- lambda1 lambda2)) (cos (+ lambda1 lambda2))))))
368.0ms
(+ (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (- (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))
251.0ms
(* 2 (+ (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (- (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))
244.0ms
(* (+ (cos (+ phi1 phi2)) (cos (- phi1 phi2))) (- (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2)))))
187.0ms
(* (* (* (* (cos phi1) (cos phi1)) (cos phi1)) (* (* (cos phi2) (cos phi2)) (cos phi2))) (* (* (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))

prune1.8s

Pruning

16 alts after pruning (16 fresh and 0 done)

Merged error: 2.2b

localize39.0ms

Local error

Found 4 expressions with local error:

0.6b
(acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))
0.3b
(* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))
0.2b
(* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2)))
0.2b
(* (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))) R)

rewrite71.0ms

Algorithm
rewrite-expression-head
Rules
28×add-exp-log
28×add-cbrt-cube
28×pow1
16×cbrt-unprod
16×prod-exp
16×pow-prod-down
6×cos-mult
5×add-cube-cbrt
5×associate-*l*
5×*-un-lft-identity
5×add-sqr-sqrt
4×add-log-exp
3×*-commutative
2×sin-mult
2×associate-*r/
2×associate-*l/
2×associate-*r*
2×frac-times
1×acos-asin
Counts
4 → 69
Calls
4 calls:
Slowest
33.0ms
(* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))
29.0ms
(* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2)))
4.0ms
(* (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))) R)
2.0ms
(acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))

series432.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
149.0ms
(* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2)))
147.0ms
(* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))
108.0ms
(* (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))) R)
27.0ms
(acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))

simplify4.1s

Counts
48 → 81
Calls
48 calls:
Slowest
670.0ms
(* (* (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (* (cos lambda1) (cos lambda2))) (* (* (* (cos phi1) (cos phi2)) (* (cos phi1) (cos phi2))) (* (cos phi1) (cos phi2))))
612.0ms
(* (* (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (sin lambda1) (sin lambda2))) (* (* (* (cos phi1) (cos phi2)) (* (cos phi1) (cos phi2))) (* (cos phi1) (cos phi2))))
138.0ms
(* R (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))))
137.0ms
(* (+ (cos (+ lambda1 lambda2)) (cos (- lambda1 lambda2))) (+ (cos (+ phi1 phi2)) (cos (- phi1 phi2))))
134.0ms
(* (- (cos (- lambda1 lambda2)) (cos (+ lambda1 lambda2))) (+ (cos (+ phi1 phi2)) (cos (- phi1 phi2))))

prune2.1s

Pruning

15 alts after pruning (15 fresh and 0 done)

Merged error: 2.1b

localize19.0ms

Local error

Found 4 expressions with local error:

0.7b
(log (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))))
0.6b
(acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))
0.3b
(* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))
0.2b
(* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2)))

rewrite31.0ms

Algorithm
rewrite-expression-head
Rules
29×add-exp-log
29×pow1
28×add-cbrt-cube
16×cbrt-unprod
16×prod-exp
16×pow-prod-down
6×cos-mult
5×add-cube-cbrt
5×*-un-lft-identity
5×add-sqr-sqrt
4×add-log-exp
3×log-prod
2×sin-mult
2×*-commutative
2×associate-*r/
2×associate-*l/
2×associate-*l*
2×associate-*r*
2×frac-times
1×log-pow
1×rem-log-exp
1×acos-asin
Counts
4 → 70
Calls
4 calls:
Slowest
15.0ms
(* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))
13.0ms
(* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2)))
1.0ms
(acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))
1.0ms
(log (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))))

series302.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
124.0ms
(* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2)))
112.0ms
(* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))
50.0ms
(log (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))))
15.0ms
(acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))

simplify3.9s

Counts
50 → 82
Calls
50 calls:
Slowest
670.0ms
(* (* (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (sin lambda1) (sin lambda2))) (* (* (* (cos phi1) (cos phi2)) (* (cos phi1) (cos phi2))) (* (cos phi1) (cos phi2))))
572.0ms
(* (* (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (* (cos lambda1) (cos lambda2))) (* (* (* (cos phi1) (cos phi2)) (* (cos phi1) (cos phi2))) (* (cos phi1) (cos phi2))))
132.0ms
(* (- (cos (- lambda1 lambda2)) (cos (+ lambda1 lambda2))) (+ (cos (+ phi1 phi2)) (cos (- phi1 phi2))))
120.0ms
(log (* (cbrt (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2))))))) (cbrt (acos (+ (* (sin phi1) (sin phi2)) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos phi1) (cos phi2))) (* (* (sin lambda1) (sin lambda2)) (* (cos phi1) (cos phi2)))))))))
118.0ms
(log (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))))

prune2.2s

Pruning

13 alts after pruning (13 fresh and 0 done)

Merged error: 2.1b

regimes1.1s

Accuracy

0% (0.3b remaining)

Error of 4.0b against oracle of 3.7b and baseline of 4.0b

bsearch6.0ms

end0.0ms

sample24.0s

Algorithm
intervals
Results
17.6s4739×body1280valid
4.8s2083×body640valid
897.0ms731×body320valid
257.0ms294×body160valid
79.0ms147×body80valid
44.0ms8×body2560valid