Re: [isabelle] fun or function (sequential) command lasts long
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
Actually, this particular function was the reason for me to investigate
how the problem can be avoided. Short answer: It can't. Long answer:
This archive was generated by a fusion of
Pipermail (Mailman edition) and