### 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.

### License

BSD License

### Topics

- Computer science/Data structures

### Related publications

- Nipkow, T. (2017). Verified Root-Balanced Trees. Lecture Notes in Computer Science, 255–272. https://doi.org/10.1007/978-3-319-71237-6_13
- Open access

### Session Root_Balanced_Tree

- Time_Monad
- Root_Balanced_Tree
- Root_Balanced_Tree_Tab

### Depends on

- Amortized Complexity Verified

### Used by

- Schönhage-Strassen Multiplication
- Karatsuba Multiplication on Integers
- Closest Pair of Points Algorithms
- A Verified Code Generator from Isabelle/HOL to CakeML

### Auto-related entries

- A Fully Verified Executable LTL Model Checker

## Cite

×

Root_Balanced_Tree-AFP

    @article{Root_Balanced_Tree-AFP,
      author  = {Tobias Nipkow},
      title   = {Root-Balanced Tree},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Root_Balanced_Tree.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Aug 20, 2017 : Isabelle2016-1