Publication at Faculty of Mathematics and Physics |
2012
Abstract
We present a correctness proof of Adams' trees of bounded balance, which are used in Haskell to implement Data.Map and Data.Set. Our analysis includes the previously ignored join operation, and also guarantees trees with smaller depth than the original one.
Because the Adams' trees can be parametrized, we use benchmarking to find the best choice of parameters. Finally, a saving memory technique based on introducing additional data constructor is evaluated.