Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Height Bounds for Height-Balan...

Email Gateway (Jul 07 2026 at 19:57):

From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: Height Bounds for Height-Balanced Trees

Height Bounds for Height-Balanced Trees
Manuel Eberl

This article takes a fresh look at the class of binary trees known as
height-balanced trees, where for each node, the height difference between the
left and right subtree is bounded by some fixed integer d > 0. An interesting
question from an algorithmic perspective is how bad the imbalance of such trees
can be in the worst case. Luccio and Pagli showed that the worst-case size of a
tree of height h is roughly B_d * C_d^h for large h for some specific real
numbers B_d, C_d > 1.

This formalisation contains:

• A simpler proof that the worst-case size is at least C_d^h for all h
• An explicit closed-form expression for the worst-case size
• A closed-form expression for B_d in terms of C_d and vice versa
• Explicit bounds for C_d in terms of d
• Asymptotic expansions for C_d and B_d as d -> infinity.

https://isa-afp.org/entries/Height_Balanced_Tree_Bounds.html

Enjoy!

smime.p7s

Last updated: Jul 22 2026 at 14:00 UTC