Search-tree node-visit costs

The cost model counts visits to internal nodes. Empty-child tests, allocation, reconstruction, order-comparison implementation, and pure client computation are not charged. In particular, inserting into an empty tree costs zero in this model. These are not RAM instruction counts.

Each traversal below follows exactly the branch decisions of its corresponding operation. Search and insertion follow the same path; minimum follows left children; successor follows one child and retains a candidate when descending left. No operation scans both subtrees.

Main definitions

• searchVisits, minimumVisits, successorVisits: node visits along the selected path.

Main results

• searchVisits_le_height, minimumVisits_le_height, successorVisits_le_height: shape-dependent upper bounds, without any balancing assumption.
• height_insert_le: insertion increases height by at most one.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 12

def Cslib.Algorithms.Lean.SearchTree.searchVisits {α : Type u_1} [LinearOrder α] (x : α) : BinaryTree α → ℕ

Internal-node visits shared by membership and insertion.

def Cslib.Algorithms.Lean.SearchTree.minimumVisits {α : Type u_1} : BinaryTree α → ℕ

Internal-node visits of leftmost descent.

def Cslib.Algorithms.Lean.SearchTree.successorVisits {α : Type u_1} [LinearOrder α] (x : α) : BinaryTree α → ℕ

Internal-node visits of strict successor, including failed searches.

theorem Cslib.Algorithms.Lean.SearchTree.searchVisits_le_height {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : searchVisits x t ≤ t.height

theorem Cslib.Algorithms.Lean.SearchTree.minimumVisits_le_height {α : Type u_1} (t : BinaryTree α) : minimumVisits t ≤ t.height

theorem Cslib.Algorithms.Lean.SearchTree.successorVisits_le_height {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : successorVisits x t ≤ t.height

theorem Cslib.Algorithms.Lean.SearchTree.height_insert_le {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : (insert x t).height ≤ t.height + 1

This permits linear height growth; it is not a balancing theorem.