Abstract: |
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 a whole subtree is rebalanced. This article
defines and analyzes 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.
This is the Isabelle formalization of the material decribed in the APLAS 2017 article
Verified Root-Balanced Trees
by the same author, which also presents experimental results that show
competitiveness of root-balanced with AVL and red-black trees.
|
BibTeX: |
@article{Root_Balanced_Tree-AFP,
author = {Tobias Nipkow},
title = {Root-Balanced Tree},
journal = {Archive of Formal Proofs},
month = aug,
year = 2017,
note = {\url{http://isa-afp.org/entries/Root_Balanced_Tree.html},
Formal proof development},
ISSN = {2150-914x},
}
|