Re: [isabelle] No tail-recursive code equation for List.map



Hi Florian,

> Andreas Lochbihler a few months ago also showed funny surprises in
> PolyML of obviously equivalent function definitions with dramatic
> differences in runtime behaviour.

For completeness, here are the figures that I had mentioned to you. I have tested different code equations for fold on a red-black tree with 100 000 000 entries from theory HOL/Library/RBT_Impl.

The equation for Empty is always the same

fold f rbt.Empty = id

but I tried three versions for the branch case:

a) fold f (rbt.Branch c l k v r) = fold f r ◦ f k v ◦ fold f l
b) fold f (rbt.Branch c l k v r) = (λb. fold f r (f k v (fold f l b)))
c) fold f (rbt.Branch c l k v r) b = fold f r (f k v (fold f l b))

Under PolyML, I got the following timings, i.e., the eta-expanded version performed best.

a) 0.54 s
b) 0.38 s
c) 0.15 s

Andreas




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