Optimal binary search tree

DefinitionExpected search cost of a binary search tree#✓fully proved

Let \(R\) be an additive commutative monoid, let \(n\) be a natural number, and let \(p_0, \dots, p_{n-1} \in R\) (key weights) and \(q_0, \dots, q_n \in R\) (dummy-key weights) be given. Let \(T\) be a binary tree whose nodes are labelled by elements of \(\{0, \dots, n-1\}\) and whose inorder traversal is \(0, 1, \dots, n-1\), so each key labels exactly one node and \(T\) has exactly \(n + 1\) empty subtrees. The depth of a node or empty subtree is its distance from the root, the root having depth \(0\); write \(d(k)\) for the depth of the node labelled \(k\) and \(\ell_0, \dots, \ell_n\) for the depths of the empty subtrees listed from left to right. The expected search cost of \(T\) is

\[\sum_{k=0}^{n-1} (d(k) + 1) \cdot p_k + \sum_{i=0}^{n} (\ell_i + 1) \cdot q_i,\]

where \(m \cdot x\) denotes the \(m\)-fold sum of \(x\) in \(R\).

Cslib.Algorithms.Lean.OptimalBST.expectedSearchCost · 16 lines

public def expectedSearchCost [AddCommMonoid R] (n : Nat)
    (p : Vector R n) (q : Vector R (n + 1))
    (tree : BinaryTree (Fin n))
    (complete : inorder tree = List.finRange n) : R :=
  let depths := dummyDepths tree 0
  have nodes : tree.numNodes = n := by
    rw [numNodes_eq_length_inorder, complete]
    simp
  have leaves : tree.numLeaves = n + 1 := by
    rw [BinaryTree.numLeaves_eq_numNodes_succ, nodes]
  have depthCount : depths.length = n + 1 := by
    rw [dummyDepths_length, leaves]
  let depthVector : Vector Nat (n + 1) :=
    ⟨depths.toArray, by simp [depthCount]⟩
  keyCost p 0 tree +
    ∑ i : Fin (n + 1), (depthVector[i.val] + 1) • q[i.val]

Uses 2 · Used by 1

Statement usesInorder traversal of a binary tree · The length of the inorder traversal of a binary tree is its number of nodes

Used byThe optimal BST procedure finds the minimum expected search cost

DefinitionOptimal binary search tree procedure#✓fully proved

Let \(R\) be a linearly ordered additive commutative monoid in which addition is monotone, let \(n\) be a natural number, and let \(p_0, \dots, p_{n-1}, q_0, \dots, q_n \in R\). The procedure (CLRS OPTIMAL-BST, with keys indexed from \(0\)) fills a cost table \(e\) of size \((n+1) \times (n+1)\), an auxiliary weight table \(w\) of the same size, and a root table of size \(n \times n\) with entries in \(\{0, \dots, n-1\}\) or empty; all entries start as \(0\) or empty. First it sets \(e[a][a] = w[a][a] = q_a\) for \(a = 0, \dots, n\). Then for \(\ell = 1, \dots, n\) in increasing order and, for each \(\ell\), for \(a = 0, \dots, n - \ell\) in increasing order, with \(b = a + \ell\), it sets \(w[a][b] = w[a][b-1] + p_{b-1} + q_b\) and examines the candidate roots \(r = a, \dots, b-1\) in increasing order, replacing the current best only when the candidate value \(e[a][r] + e[r+1][b] + w[a][b]\) is strictly smaller. It stores the resulting minimum in \(e[a][b]\) and the earliest minimizing \(r\) at position \((a, b-1)\) of the root table. The procedure returns the cost table \(e\) and the root table, with running time equal to the total number of candidate roots examined.

public def optimalBST [AddCommMonoid R] [LinearOrder R]
    [IsOrderedAddMonoid R] {n : Nat} (p : Vector R n)
    (q : Vector R (n + 1)) : TimeM Nat
    (Vector (Vector R (n + 1)) (n + 1) ×
      Vector (Vector (Option (Fin n)) n) n) :=
  let result := execute p q
  ⟨(result.1, result.2.2.1), result.2.2.2⟩

Used by 5

Used byOptimal BST with no keys · The optimal BST procedure finds the minimum expected search cost · Optimal BST table recurrence · Exact running time of the optimal BST procedure · Cubic running time of the optimal BST procedure

TheoremOptimal BST with no keys#✓fully proved

Let \(R\) be a linearly ordered additive commutative monoid in which addition is monotone. For \(n = 0\) keys and a single dummy weight \(q_0 \in R\), the optimal binary search tree procedure returns the \(1 \times 1\) cost table whose only entry is \(q_0\), the empty \(0 \times 0\) root table, and running time \(0\).

public theorem optimalBST_empty [AddCommMonoid R] [LinearOrder R]
    [IsOrderedAddMonoid R] (p : Vector R 0) (q : Vector R 1) :
    optimalBST p q =
      ⟨(Vector.ofFn (fun _ : Fin 1 => Vector.ofFn (fun _ : Fin 1 => q[0])),
        Vector.replicate 0 (Vector.replicate 0 (none : Option (Fin 0)))), 0⟩

Uses 1

Statement usesOptimal binary search tree procedure

TheoremOptimal BST table recurrence#✓fully proved

Let \(R\) be a linearly ordered additive commutative monoid in which addition is monotone, let \(n\) be a natural number, let \(p_0, \dots, p_{n-1}, q_0, \dots, q_n \in R\), and let \(e\) and \(\rho\) be the cost table and the root table returned by the optimal binary search tree procedure on these weights. For \(a \le b \le n\) write \(w(a, b) = \sum_{i=a}^{b-1} p_i + \sum_{i=a}^{b} q_i\). Then \(e[a][a] = q_a\) for every \(a \le n\), and for all \(a < b \le n\) there is an \(r\) with \(a \le r < b\) such that \(\rho[a][b-1] = r\), \(e[a][b] = e[a][r] + e[r+1][b] + w(a, b)\), and for every \(t\) with \(a \le t < b\)

\[e[a][b] \le e[a][t] + e[t+1][b] + w(a, b),\]

with strict inequality when \(t < r\). So \(e[a][b]\) is the minimum of \(e[a][t] + e[t+1][b] + w(a, b)\) over \(a \le t < b\), and \(r\) is the earliest \(t\) attaining it.

Cslib.Algorithms.Lean.OptimalBST.optimalBST_table_spec · 23 lines

public theorem optimalBST_table_spec [AddCommMonoid R] [LinearOrder R]
    [IsOrderedAddMonoid R] :
    ∀ (n : Nat) (p : Vector R n) (q : Vector R (n + 1)),
      (∀ a : Fin (n + 1), (optimalBST p q).ret.1[a.val][a.val] = q[a.val]) ∧
      (∀ (a : Fin n) (b : Fin (n + 1)) (h : a.val < b.val),
        ∃ r : Fin n, a.val ≤ r.val ∧ r.val < b.val ∧
          (optimalBST p q).ret.2[a.val][b.val - 1]'(by omega) = some r ∧
          (optimalBST p q).ret.1[a.val][b.val] =
            (optimalBST p q).ret.1[a.val][r.val] +
            (optimalBST p q).ret.1[r.val + 1][b.val] +
            ((∑ i : Fin n, if a.val ≤ i.val ∧ i.val < b.val then p[i.val] else 0) +
              ∑ i : Fin (n + 1), if a.val ≤ i.val ∧ i.val ≤ b.val then q[i.val] else 0) ∧
          ∀ t : Fin n, a.val ≤ t.val → t.val < b.val →
            ((optimalBST p q).ret.1[a.val][b.val] ≤
              (optimalBST p q).ret.1[a.val][t.val] +
              (optimalBST p q).ret.1[t.val + 1][b.val] +
              ((∑ i : Fin n, if a.val ≤ i.val ∧ i.val < b.val then p[i.val] else 0) +
                ∑ i : Fin (n + 1), if a.val ≤ i.val ∧ i.val ≤ b.val then q[i.val] else 0)) ∧
            (t.val < r.val → (optimalBST p q).ret.1[a.val][b.val] <
              (optimalBST p q).ret.1[a.val][t.val] +
              (optimalBST p q).ret.1[t.val + 1][b.val] +
              ((∑ i : Fin n, if a.val ≤ i.val ∧ i.val < b.val then p[i.val] else 0) +
                ∑ i : Fin (n + 1), if a.val ≤ i.val ∧ i.val ≤ b.val then q[i.val] else 0)))

Uses 1

Statement usesOptimal binary search tree procedure

TheoremThe optimal BST procedure finds the minimum expected search cost#✓fully proved

Let \(R\) be a linearly ordered additive commutative monoid in which addition is monotone, let \(n\) be a natural number, and let \(p_0, \dots, p_{n-1}, q_0, \dots, q_n \in R\). Let \(e\) be the cost table returned by the optimal binary search tree procedure on these weights. Then \(e[0][n]\) is the least expected search cost, with key weights \(p\) and dummy-key weights \(q\), of a binary tree whose nodes are labelled by elements of \(\{0, \dots, n-1\}\) and whose inorder traversal is \(0, 1, \dots, n-1\): some such tree has expected search cost \(e[0][n]\), and every such tree has expected search cost at least \(e[0][n]\).

public theorem optimalBST_minimal [AddCommMonoid R] [LinearOrder R]
    [IsOrderedAddMonoid R] :
    ∀ (n : Nat) (p : Vector R n) (q : Vector R (n + 1)),
      IsLeast {z : R | ∃ (tree : BinaryTree (Fin n))
        (h : inorder tree = List.finRange n), expectedSearchCost n p q tree h = z}
        (optimalBST p q).ret.1[0][n]

Uses 5

Statement usesInorder traversal of a binary tree · Expected search cost of a binary search tree · Optimal binary search tree procedure

Proof usesInorder traversal of a binary tree with an accumulator · The length of the inorder traversal of a binary tree is its number of nodes

TheoremExact running time of the optimal BST procedure#✓fully proved

Let \(R\) be a linearly ordered additive commutative monoid in which addition is monotone. For every natural number \(n\) and all \(p_0, \dots, p_{n-1}, q_0, \dots, q_n \in R\), the running time of the optimal binary search tree procedure on these weights, which is the number of candidate roots it examines, equals \(\binom{n+2}{3}\).

public theorem optimalBST_time [AddCommMonoid R] [LinearOrder R]
    [IsOrderedAddMonoid R] :
    ∀ (n : Nat) (p : Vector R n) (q : Vector R (n + 1)),
      (optimalBST p q).time = Nat.choose (n + 2) 3

Uses 1 · Used by 1

Statement usesOptimal binary search tree procedure

Used byCubic running time of the optimal BST procedure

TheoremCubic running time of the optimal BST procedure#✓fully proved

Let \(R\) be a linearly ordered additive commutative monoid in which addition is monotone. For every natural number \(n\) and all \(p_0, \dots, p_{n-1}, q_0, \dots, q_n \in R\), the running time \(T\) of the optimal binary search tree procedure on these weights, which is the number of candidate roots it examines, satisfies \(n^3 \le 6T\) and \(T \le n^3\).

public theorem optimalBST_time_bounds [AddCommMonoid R] [LinearOrder R]
    [IsOrderedAddMonoid R] :
    ∀ (n : Nat) (p : Vector R n) (q : Vector R (n + 1)),
      n ^ 3 ≤ 6 * (optimalBST p q).time ∧ (optimalBST p q).time ≤ n ^ 3

Uses 2

Statement usesOptimal binary search tree procedure

Proof usesExact running time of the optimal BST procedure

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.