Stream: Beginner Questions

Topic: Complexity proofs with logarithm


view this post on Zulip 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 = [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

view this post on Zulip Lukas Stevens (Apr 29 2021 at 09:08):

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

view this post on Zulip Lukas Stevens (Apr 29 2021 at 09:09):

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

view this post on Zulip Jan van Brügge (Apr 29 2021 at 09:17):

Of course, I am stupid

view this post on Zulip 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: Aug 13 2022 at 05:18 UTC