Proofs: Ternary search tree

The ternary search tree operations keep the invariant and answer the string symbol table queries full

This proof shows: correctness.

We use the pseudocode, the sibling trees, the strings $str(x)$ and the invariant (S1) to (S4) of the page. The level of a sibling tree is the length of the strings of its nodes: the sibling tree of the root has level 1, and the one below $y.mid$ has level $\lvert str(y) \rvert + 1$. All nodes of one sibling tree share the same $str$ except for the last symbol.

Lemma 1 (uniqueness). Under (S1), each nonempty string $s$ is $str(x)$ for at most one node $x$.

Proof. By induction on $\lvert s \rvert$. A node with $str(x) = s$ lies in a sibling tree of level $\lvert s \rvert$ and has $x.c = s[\lvert s \rvert - 1]$. For $\lvert s \rvert = 1$ that sibling tree is the one of the root. For $\lvert s \rvert > 1$ it is the sibling tree below $y.mid$ for a node $y$ with $str(y) = s[0 \ldots \lvert s \rvert - 2]$, and $y$ is unique by the induction hypothesis. In either case the sibling tree is fixed, and by (S1) its symbols are distinct, so at most one of its nodes has the symbol $x.c$. $\square$

Lemma 2 (walk). The loop of lines L1 to L7 returns $x.val$ for the node $x$ with $str(x) = s$ if this node exists, and NIL otherwise.

Proof. The loop keeps this claim: $x$ is NIL or a node of the sibling tree of level $d + 1$ whose nodes have strings $s[0 \ldots d-1] \cdot c$, and if a node $z$ with $str(z) = s[0 \ldots d]$ exists, then $z$ is in the subtree of $x$ within that sibling tree. At the start, $x$ is the root and $d = 0$, so the claim holds. Lines L3 and L4 are one step of a BST search for the symbol $s[d]$: by (S1) a node with symbol $s[d]$ smaller than $x.c$ can only be in the left subtree, and one with a larger symbol only in the right subtree. If $s[d] = x.c$, then $str(x) = s[0 \ldots d]$. If $d = \lvert s \rvert - 1$, then $x$ is the node of $s$, and line L6 returns its value. Else line L5 moves to the sibling tree below $x.mid$, which by definition holds exactly the nodes with strings $s[0 \ldots d] \cdot c$, and the claim holds for $d + 1$. If $x$ becomes NIL, the subtree where $z$ must be is empty, so the node $z$ of $s[0 \ldots d]$ does not exist, and then no node of $s$ exists either (its sibling tree would be below $z.mid$). Line L7 returns NIL. Each round either moves one level down in a sibling tree or increases $d$; a sibling tree is finite and $d \le \lvert s \rvert - 1$, so the loop ends. $\square$

GET. By Lemma 2 and (S2), GET returns the value of $s$ if $s$ is a key and NIL otherwise.

PUT. The loop of lines L9 to L14 takes the same steps as the walk of Lemma 2, but where the walk would reach a NIL link, it creates a node there. A node created by a left or right step at level $d + 1$ gets the symbol $s[d]$, and it is put at the place where the BST search for $s[d]$ ended, so it is larger than each node where the search went right and smaller than each node where it went left. This is a BST insert, and (S1) holds in that sibling tree. A node created by a middle step starts a new sibling tree with one node, where (S1) holds. When the loop reaches line L13, $x$ is the node with $str(x) = s$. Lines L13 and L14 give it the value $v$ and count it if it was new as a key, so (S2) and (S4) hold. For (S3), each node created in this call lies on the path from the root to $x$, and each one other than $x$ was created just before a step into it, so the nodes created by middle steps have a middle child or are $x$; a node created by a left or right step at level $d + 1$ has the symbol $s[d]$, so the next step from it is a middle step (or it is $x$), which gives it a middle child. The value of $x$ covers $x$.

DELETE. If line L16 returns, $s$ is not a key by Lemma 2 and (S2), and nothing changes. Else line L17 removes the value of the node $x$ of $s$, so (S2) and (S4) hold for the keys other than $s$. Now (S3) can fail only at nodes of the path that lost their value or their middle child. The loop keeps this claim: (S1), (S2) and (S4) hold, and (S3) holds at each node except possibly the current node $y$. At $y$, if $y$ has a value or a middle child, (S3) holds everywhere, and the loop returns. Else no node lies below $y.mid$ and $y$ has no value, so $y$ carries no key and no other node's string depends on it. Line L20 removes $y$ from its sibling tree with a BST delete, which keeps the BST order of the other nodes of that sibling tree (this is the correctness of the BST delete) and does not change their strings, since the sibling tree and the symbols of its nodes stay the same. So (S1), (S2) and (S4) still hold. The only node whose links changed in a way that can break (S3) is the parent $q$ of the sibling tree, when $y$ was the root of the sibling tree below $q.mid$ and the sibling tree is now empty. Then $q$ is the next node of the path. If $y$ was reached by a left or right link, its parent in the path keeps its middle child and its value, so the next round returns. So the claim holds for the next node of the path. The loop ends at the root of the tree at the latest.

KEYS-WITH-PREFIX. If $p = \varepsilon$, the walk starts at the root with prefix $\varepsilon$. Else, by Lemma 2, line L21 finds the node $x$ with $str(x) = p$ or returns the empty list. In the second case no key starts with $p$: the node of a key $k$ with $p \preceq k$ has the node of $p$ as an ancestor through middle links, by the construction of $str$. In the first case, $p$ is reported if it is a key, and the other keys with prefix $p$ are the strings of the nodes with a value in the tree below $x.mid$, by (S2) and the definition of $str$.

The walk of lines L22 to L24 visits each node $y$ of the given tree once, with the prefix $t$ such that $str(y) = t \cdot y.c$: this holds at the start, a left or right step keeps $t$ (same sibling tree), and a middle step extends it by $y.c$ (line L24). So line L23 appends exactly the keys of the tree. Order. Within a sibling tree the in-order visit takes the symbols in increasing order, by (S1). At $y$, the string $str(y)$ is reported before the keys below $y.mid$, which extend it, and all of these come after the keys of the left subtree of $y$ and before those of the right subtree, whose last symbol at this level is smaller or larger. These are the rules of lexicographic order, so the list is sorted. $\blacksquare$