Verified Root-Balanced Trees

Tobias Nipkow

Andersson introduced general balanced trees, search trees based on the design principle of partial rebuilding: perform update operations naively until the tree becomes too unbalanced, at which point you rebalance a whole subtree. We define and analyze a functional version of general balanced trees which we call root-balanced trees. Using a lightweight model of execution time, amortized logarithmic complexity is verified in the theorem prover Isabelle. Experimental results show competitiveness of root-balanced with AVL and red-black trees.

pdf

BibTeX:

@InProceedings{Nipkow-APLAS17,
  author ={Tobias Nipkow},
  title ={Verified Root-Balanced Trees},
  booktitle ={Asian Symposium on Programming Languages and Systems, APLAS 2017},
  pages ={255--272},
  series ={LNCS},
  year ={2017},
  volume ={10695},
  editor ={Bor-Yuh Evan Chang},
  publisher ={Springer},
}

Online article

Isabelle theories in the Archive of Formal Proofs