Email Gateway (Aug 18 2022 at 12:48): Email Gateway (Aug 18 2022 at 12:48):From: Peter Lammich <peter.lammich@uni-muenster.de>
HI all,
I have a problem with the following function definition:
fun balance:: "'a tree => 'a tree" where
"balance (T B (T R (T R a x b) y c) z d) = T R (T B a x b) y (T B c
z d)" |
"balance (T B (T R a x (T R b y c)) z d) = T R (T B a x b) y (T B c
z d)" |
"balance (T B a x (T R (T R b y c) z d)) = T R (T B a x b) y (T B c
z d)" |
"balance (T B a x (T R b y (T R c z d))) = T R (T B a x b) y (T B c
z d)" |
"balance t = t"
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 ?
Best regards,
Peter
Email Gateway (Aug 18 2022 at 12:48):From: Alexander Krauss <krauss@in.tum.de>
Hi Peter,
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
Last updated: May 03 2024 at 04:19 UTC