## Stream: Beginner Questions

### Topic: Complexity proofs with logarithm

#### Jan van Brügge (Apr 29 2021 at 09:04):

How would I prove logarithmic complexity of a data structure? E.g. for example that a complete binary tree has a height that is logarithmic to the number of nodes, or that search takes at maximum log steps?

datatype 'a bst = Leaf | Node "'a bst" 'a "'a bst"

fun heights :: "'a bst ⇒ nat list" where
"heights Leaf = "
| "heights (Node a _ b) = map (λx. x + 1) (heights a) @ map (λx. x + 1) (heights b)"

definition maximum :: "nat list ⇒ nat" where
"maximum xs ≡ foldl max 0 xs"

definition complete :: "'a bst ⇒ bool" where
"complete t ≡ (∃n. set (heights t) = { n, Suc n }) ∨ (∃n. set (heights t) = { n })"

lemma height_log: "complete t ⟹ ceil (log2 (size t)) = maximum (heights t)"
sorry

fun valid_bst :: "'a::linorder bst ⇒ bool" where
"valid_bst Leaf = True"
| "valid_bst (Node l a r) ⟷ (∀x∈set_bst l. x < a) ∧ (∀x∈set_bst r. a < x) ∧ valid_bst l ∧ valid_bst r"

fun isin :: "'a::linorder ⇒ 'a bst ⇒ bool" where
"isin _ Leaf = False"
| "isin x (Node l a r) = (if a = x then True else
if x < a then isin x l else isin x r
)"
fun isin_t :: "'a::linorder ⇒ 'a bst ⇒ nat" where
"isin_t _ Leaf = 1"
| "isin_t x (Node l a r) = (if a = x then 1 else
if x < a then 1 + isin_t x l else 1 + isin_t x r
)"

lemma "⟦ complete t ; valid_bst t ⟧ ⟹ isin_t x t ≤ ceil (log2 (size t))"
sorry


#### Lukas Stevens (Apr 29 2021 at 09:08):

It's probably easier to prove that a tree of height $n$ has $2^n$ nodes.

#### Lukas Stevens (Apr 29 2021 at 09:09):

If it is complete then it should be easy to prove by induction on $n$.

#### Jan van Brügge (Apr 29 2021 at 09:17):

Of course, I am stupid

#### Manuel Eberl (Apr 29 2021 at 09:46):

Indeed, that's usually the preferred way: reduce a property about the logarithm to a property about exponentiation.

But one can also show with some effort (pretty sure I did that at some point somewhere) that if we define f n = ceil (log 2 n)then f n = 1 + f ((n + 1) div 2) or something like that, then you can do the induction like that. But the other way is probably nicer (pretty sure that's also how it's done in @Tobias Nipkow's FDS lecture).

Last updated: Sep 25 2022 at 23:25 UTC