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 = [0]"
| "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
```

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

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

Of course, I am stupid

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: Aug 13 2022 at 05:18 UTC