Weight-Balanced Trees (Q7361513)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Weight_Balanced_Trees
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Weight-Balanced Trees |
AFP entry Weight_Balanced_Trees |
Statements
13 March 2018
0 references
Tobias Nipkow
0 references
Stefan Dirix
0 references
Weight-Balanced Trees (English)
0 references
This theory provides a verified implementation of weight-balanced trees following the work of Hirai and Yamamoto who proved that all parameters in a certain range are valid, i.e. guarantee that insertion and deletion preserve weight-balance. Instead of a general theorem we provide parameterized proofs of preservation of the invariant that work for many (all?) valid parameters.
0 references
