Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] the complete and balanced of binary tree in HO...

Email Gateway (Aug 22 2022 at 17:43):

From: Tobias Nipkow <nipkow@in.tum.de>
The terminology in the literature is not canonical and the Tree theory reflects
that.

Does the "balanced" function define a height-balanced binary tree?

Depends on what you mean by height-balanced. If you think about it you will
realize that "height t - min_height t ≤ 1" means that leafs are at most one
level apart. This is weaker than what wikipedia calls "complete" but strong than
"avl".

You can always use quickcheck (eg by stating a conjecture) to test if some
definition implies anoter definition. For trees this tends to work very well.

Tobias
smime.p7s

Last updated: Apr 19 2024 at 16:20 UTC