Re: [isabelle] fun or function (sequential) command lasts long



Hi Peter,

I have a problem with the following function definition:

  fun balance:: "'a tree => 'a tree" where
  [...]

isabelle seems to need really long to process this command, I have
waited for several minutes and finally had to kill isabelle because it
used 1.5GB of memory and my computer started getting unusable due to
very high response times.
Is their any standard approach how speed this command up ?

Eating 1,5G of memory sounds a bit too much (64 bit? proof terms?), but in general, it is perfectly normal that the balance function blows up the function package: Isabelle tries to make the patterns non-overlapping (this is necessary, because they are not valid as they are written), which leads to an exponential explosion of cases. The rest of the package again has an n^2 complexity in the number of equations...

Note that there is already a formalization of red-black trees in HOL/Library/RBT.thy. Maybe that can save you some work... In that formalization, the definition of balance is slow, but works.

There is no general way of fixing this explosion. You can only try to avoid such evil pattern matching. If you really really need it, good old recdef may be faster, since it has a less general handling of pattern matching.

Actually, this particular function was the reason for me to investigate how the problem can be avoided. Short answer: It can't. Long answer:
http://www4.in.tum.de/~krauss/patterns/

Alex






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