Email Gateway (Aug 12 2020 at 17:50): Email Gateway (Aug 12 2020 at 17:50):From: Martin Raszyk <m.raszyk@gmail.com>
Dear Tobias,
thank you very much for pointing me towards the existing theory
Set2_Join_RBT. Unfortunately, I could not use it directly, because its
RBTs use the tree datatype from the Tree theory in the HOL-Library
while the RBTs from Containers use the rbt datatype from the RBT_Impl
theory in the HOL-Library. Since registering a new set implementation
in Containers would be tedious and the algorithm from the
Set2_Join_RBT theory is only faster in particular cases (for two sets
that are not of "roughly" equal size and none of which is small), I've
decided to port the definitions and proofs from the existing theory
Set2_Join_RBT into a new theory called RBT_set_opt that can be found
in the GitHub repository [1].
As you can easily check using the code exported with the old and
optimized code equations, the performance of my counter-example did
improve significantly. I've also added checks for the cases of one RBT
being "small", but the case of both RBTs being of "roughly" equal size
is still pending. I believe that storing the black height and/or the
size of an RBT in its nodes could help to guide the decision of which
algorithm to use. Yet it is not clear how to set the thresholds for an
RBT being "small" or two RBTs being of "roughly" equal size. Here an
empirical evaluation of the performance seems inevitable to me.
Now I would be interested in your opinion again on how to proceed with
the integration of my theory RBT_set_opt into Containers. In
particular, with regard to storing the black height and/or the size of
an RBT in its nodes and setting the thresholds.
Best regards,
Martin
[1] https://github.com/mraszyk/RBT_height
Email Gateway (Aug 13 2020 at 11:17):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Martin,
The theories in Data_Structure have more of a textbook quality and thus I am not
suprised you needed to make a copy.
Concerning the integration with Containers - what do you mean by "Containers"?
Peter Lammich's Collections Framework? In which case you have to talk to him. If
you meant "Data_Structures", I don't think it would be the right place, but we
can discuss that privately.
Tobias
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC