Email Gateway (Aug 22 2022 at 15:54): Email Gateway (Aug 22 2022 at 15:54):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Root-Balanced Tree
by 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 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.
More details at https://www.isa-afp.org/entries/Root_Balanced_Tree.html
Enjoy,
René
Last updated: Apr 18 2024 at 01:05 UTC