Proofs: String B-tree

Blind search, one comparison and the passed lcp locate a pattern in the String B-tree full

This proof shows: correctness, complexity.

We use the pseudocode, the representation and the invariant (S1) to (S4) of the page. Strings are compared lexicographically, with the end of a string below every symbol; $lcp(u, v)$ is the length of the longest common prefix, and $u[i]$ for $i \ge \lvert u \rvert$ is the end symbol. For sorted strings $k_0 \le \cdots \le k_{c-1}$ and $a < b$, $lcp(k_a, k_b) = \min(adj[a+1], \ldots, adj[b])$ (Fact 0, the standard property of sorted strings).

Lemma 1 (blind search). Lines L1 and L2 return a key $s$ with $lcp(P, s) = \max_k lcp(P, k)$.

Proof. Let $\ell^* = \max_k lcp(P, k)$. We show that the range kept by the loop always contains a key $k$ with $lcp(P, k) = \ell^*$. It holds at the start. Take a range $[lo, hi]$ with this property, and let $d$ be the minimum of $adj$ in it, so all its keys share their first $d$ symbols (Fact 0), and the parts after the split are the groups of keys with the same symbol at position $d$, with distinct symbols. If $\ell^* \le d$, all keys of the range have the same lcp with $P$, namely $\min(lcp(P, k), d)$ for any of them, which is $\ell^*$; so every part keeps the property. If $\ell^* > d$, a best key agrees with $P$ at position $d$, so $P[d]$ is the symbol of its part, and line L2 keeps that part. When the range has one key, it is a best key. $\square$

Lemma 2 (the order from one comparison). Let $s$ be a key with $\ell = lcp(P, s)$ maximal among the keys. Then for every key $k$, $lcp(P, k) = \min(\ell, lcp(s, k))$, and line L4 decides $k \le P$ correctly.

Proof. Let $c = lcp(s, k)$. If $c < \ell$: $P$ and $s$ agree up to $\ell > c$, so $P$ and $k$ first differ at $c$, with the same symbols as $s$ and $k$; thus $lcp(P, k) = c$ and $k \le P$ exactly when $k \le s$, that is, when $k$ comes before $s$ in the node. If $c > \ell$: $k$ agrees with $s$ beyond $\ell$, so $lcp(P, k) = \ell$ and $k$ compares with $P$ like $s$ does, by $s[\ell]$ against $P[\ell]$. If $c = \ell$: $lcp(P, k) \ge \ell$ and, by the maximality of $\ell$, $lcp(P, k) = \ell$; then $k \le P$ is decided by $k[\ell]$ against $P[\ell]$, and $k[\ell]$ is a branching symbol of the trie: if $k$ is after $s$, it is $rc[j]$ for the last $j \le k$ with $adj[j] \le c$ (the keys from $j$ to $k$ share more than $c$ symbols, by Fact 0), and symmetrically $lc[j]$ for the first $j > k$ with $adj[j] \le c$ if $k$ is before $s$. The two symbols $k[\ell]$ and $P[\ell]$ are equal only if both are the end symbol, and then $k = P$, which counts as $k \le P$. $\square$

Lemma 3 (the passed lcp). In RANK, the value $\lambda$ passed to a node is at most $\max_k lcp(P, k)$ over the keys $k$ of that node, so line L3, which starts reading at $\lambda$, computes $lcp(P, s)$ correctly.

Proof. At the root $\lambda = 0$. At an internal node $x$, if $r = 2i + 1$, then by (S3) the keys of $x$ are $f_0, g_0, f_1, g_1, \ldots$ (first and last strings of the children), and exactly $f_0, \ldots, g_{i-1}, f_i$ are $\le P$. So $f_i \le P < g_i$. The value passed is $\max(lcp(P, f_i), lcp(P, g_i))$, computed exactly by Lemma 2. Both $f_i$ and $g_i$ are keys of child $i$: for a leaf they are its first and last strings, and for an internal child they are the first key of its first child and the last key of its last child, by (S3) applied to the child. So $\lambda$ is at most the maximum over the child's keys. By Lemma 1 the blind search in the child returns a key $s$ with $lcp(P, s)$ at least that maximum, hence at least $\lambda$, and the symbols before $\lambda$ need not be read. $\square$

RANK is correct. We show that the value returned is the number of stored strings $\le P$. At a node $x$ reached with $rank$ equal to the number of strings in the leaves to the left of $x$'s subtree, all of which are $\le P$, and with all strings to the right of the subtree $> P$: by Lemma 2, $r$ is the number of keys of $x$ that are $\le P$. If $x$ is a leaf, its keys are its strings, so the answer is $rank + r$. Otherwise, let $i = \lfloor r / 2 \rfloor$. If $r = 2i$, then $g_{i-1} \le P < f_i$, so by (S2) all strings of children $0, \ldots, i-1$ are $\le P$ and all strings of children $i, \ldots$ are $> P$; the answer is $rank$ plus their counts. If $r = 2i + 1$, then $f_i \le P < g_i$: the children before $i$ are all $\le P$, those after are all $> P$, and the descent into child $i$ keeps the claim. Lemma 3 makes each comparison correct. The loop ends at a leaf at the latest.

PREFIX-RANGE. With $\top$ above every symbol, a string $x$ is $\le P \top$ exactly when $x < P$ or $P$ is a prefix of $x$. So the strings in the returned range of ranks are those $\ge P$ with prefix $P$, which by sorted order are exactly the strings with prefix $P$.

INSERT keeps the invariant. The descent finds a leaf such that inserting $w$ at its rank in the leaf keeps the global order (S2): if $w$ falls inside the range of child $i$, it must go into that child; if it falls between children $i - 1$ and $i$, the end of child $i - 1$ (or the start of child 0) is a valid place. Line L9 inserts it at its rank among the leaf's strings, computed by Lemma 2. Line L10 restores the B-tree sizes (S1) by splitting an overfull child into two halves of at least $\lfloor b / 2 \rfloor$ entries, in order, and recomputes the boundary keys (S3), the counts and the tries (S4) of every node on the path. Nodes off the path keep their strings, hence their boundaries and tries. Line L11 adds a level only at the root, so all leaves keep the same depth.

The number of symbols read. Let $\ell_j$ be the value of $\ell$ at the $j$-th level of a search and $\lambda_j$ the value passed to it. Lemma 3 gives $\lambda_{j+1} = \max(lcp(P, f_i), lcp(P, g_i))$, and since $f_i$ and $g_i$ are the neighbors of $P$ among the keys of the parent, the best key of the parent is one of them, so $\lambda_{j+1} = \ell_j$. The comparison at level $j$ reads $\ell_j - \lambda_j$ matching symbols and at most one mismatching symbol. Summing, the search reads at most $\ell_h - \lambda_1 + h \le p + h$ symbols for a tree of height $h$. $\blacksquare$