Re: [isabelle] Creating ML data is slow. No sharing/caching?



Dear Cornelius,

isn't the problem merely that the expression

  "fold And (map Prim [1..10]) (Prim 0)"

is evaluated 1000 times? I guess you could speed-up things by using something like:

"let e = fold And (map Prim [1..10]) (Prim 0) in add_expr e (map Prim [1..1000]"

I did not yet test my intuition though.

cheers

chris

On 07/28/2015 08:13 PM, C. Diekmann wrote:

4) Adding bigger expressions to a list of expressions is more than 10
times slower than (2):
value[code] "add_expr (fold And (map Prim [1..10]) (Prim 0)) (map Prim
[1..1000])" (*5.853s elapsed time, 11.495s cpu time, 0.316s GC time*)

Why is (4) so slow, compared to (2)?

How can I speed this up? Currently, this renders my theory unusable.

Doesn't ML use sharing or caching? I always assumed that, if I have
expressions e1 and e2, then constructing "And e1 e2" would reuse the
values e1 and e2 and this operation would be independent of the sizes
of e1 and e2.

Best,
   Cornelius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.