Proofs: Radix tree

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

This proof shows: correctness.

We use the pseudocode and the invariant (R1) to (R4) of the page. For a node $x$, $str(x)$ is the concatenation of the labels from the root to $x$. Each node $y$ other than the root has a parent $p$, and $str(y) = str(p) \cdot e.label$ for the edge $e$ from $p$ to $y$, with $\lvert e.label \rvert \ge 1$ by (R1). So $\lvert str \rvert$ strictly increases down each path.

Lemma 1 (uniqueness and walk). Under (R1), for each string $s$ at most one node $x$ has $str(x) = s$. The loop of lines L1 to L5 returns at line L4 if no node has $str = s$, and it ends at that node otherwise.

Proof. Suppose $x \ne x'$ with $str(x) = str(x') = s$. Let $y$ be their lowest common ancestor. Since $\lvert str \rvert$ grows strictly down a path, neither node is an ancestor of the other, so $y$ has two distinct children $c, c'$ on the paths to $x$ and $x'$. Both labels are nonempty and both are followed in $s$ at position $\lvert str(y) \rvert$, so they start with the same symbol $s[\lvert str(y) \rvert]$, which (R1) forbids. For the walk: the loop keeps "$str(x) = s[0 \ldots i-1]$". At a node $x$, a node $z$ below $x$ with $s[0 \ldots i-1] \prec str(z) \preceq s$ must lie below the child edge whose label starts with $s[i]$; by (R1) that is at most the edge $e$ of line L3. If $e$ is NIL, no node lies below $x$ on the way to $s$. If $e.label$ is not a prefix of $s[i \ldots]$, then $str(e.child)$ is not a prefix of $s$, and neither is the $str$ of any node below $e.child$, since all of them extend $str(e.child)$. In both cases no node has $str = s$. Else line L5 moves to $e.child$ with $str(e.child) = s[0 \ldots i + \lvert e.label \rvert - 1]$. The quantity $\lvert s \rvert - i$ drops by at least 1 each round, so the loop ends. $\square$

GET. By Lemma 1 and (R2), line L6 returns the value of $s$ if $s$ is a key, and NIL otherwise (no node, or a node with no value).

PUT. The loop keeps "$str(x) = s[0 \ldots i-1]$, the invariant (R1) holds, and the multiset of keys and values is the old one". Line L10: no edge from $x$ starts with $s[i]$, so the new edge keeps (R1); the new leaf has $str = s$ and value $v$, and $s$ was not a key, since by Lemma 1 no node had $str = s$ (that node would lie below an edge of $x$ starting with $s[i]$). So (R2) and (R4) hold, and (R3) holds because the new node has a value. Line L11: $e$ starts with $s[i]$, so $j \ge 1$. If $j < \lvert e.label \rvert$, lines L13 and L14 replace the edge $x \to e.child$ with label $\ell$ by the edges $x \to z$ with label $\ell[0 \ldots j-1]$ and $z \to e.child$ with label $\ell[j \ldots]$. Both labels are nonempty, the first starts with the same symbol as $\ell$, and $z$ has one edge, so (R1) holds. The $str$ of each old node is the same, so the keys are the same. The new node $z$ has no value and one child, so (R3) fails at $z$ only. Line L15 moves to the child with $str = s[0 \ldots i + j - 1]$. We show that the same call repairs $z$. If $i + j = \lvert s \rvert$, the loop ends with $x = z$, and line L17 gives $z$ a value. Else $s[i + j] \ne \ell[j]$, by the choice of $j$ as the longest common prefix, so the next round finds no edge of $z$ starting with $s[i + j]$ and line L10 adds a second edge to $z$. If $j = \lvert e.label \rvert$, no split is done and the walk goes on. When the loop ends without line L10, $x$ is the node with $str(x) = s$. Lines L16 and L17 give it the value $v$ and count it if it had no value, so (R2) and (R4) hold, and (R3) holds at $x$ since it has a value.

DELETE. If line L19 returns, $s$ is not a key by Lemma 1 and (R2), and nothing changes. Else line L20 removes the value of the node $x$ with $str(x) = s$ and updates the count, so (R2) and (R4) hold for the keys without $s$. Now (R3) can fail only at $x$. Two cases.

• $x$ has no edge. If $x$ is the root, (R3) asks nothing. Else line L21 removes the leaf $x$, which has no value, so no key is lost. Its parent $p$ lost one child. If $p$ is not the root and has no value, then before the removal $p$ had at least two children by (R3), so it has at least one now. If it has two or more, (R3) holds. If it has exactly one, line L22 merges it as in the next case.
• $x$ has exactly one edge $f$, $x$ is not the root, and $x$ has no value. Let $e$ be the edge from the parent $q$ of $x$ to $x$. Line L22 replaces $e$ and $f$ by one edge from $q$ to $f.child$ with label $e.label \cdot f.label$. The new label starts with the first symbol of $e.label$, so (R1) holds at $q$. The $str$ of $f.child$ and of each node below it is unchanged, and the only removed node is $x$, which has no value. So the keys are unchanged, and (R3) holds, since $x$ is gone and no other node lost a child.
• $x$ has two or more edges. Then (R3) holds at $x$, and line L22 does nothing.

KEYS-WITH-PREFIX. Let $p$ be the query. Line L23 walks as in Lemma 1. If the walk ends exactly at a node $x$, then $str(x) = p$. If $p$ ends inside the label of an edge $e$ to a child $c$, so that $p \prec str(c)$, then each node $y$ with $p \preceq str(y)$ is $c$ or below $c$: its path from the root shares the part up to the parent of $c$, and by (R1) it then takes $e$. In both cases, the nodes $y$ with $p \preceq str(y)$ are exactly the nodes of the subtree of the reached node $x$. If the walk finds no edge, or a label that disagrees with $p$ before $p$ ends, then by the argument of Lemma 1 no node has $str$ with prefix $p$, and the empty list is right. The stack holds pairs $(y, str(y))$, because line L28 pushes $str(y) \cdot f.label = str(f.child)$. Each node of the subtree is pushed once. So by (R2), line L27 appends exactly the keys with prefix $p$. The children are popped in increasing order of their first symbol, and by (R1) the first symbols differ, so the preorder lists the strings in lexicographic order, as in the proof for the trie. $\blacksquare$

Node bound. If (R3) holds and the tree has $n \ge 1$ keys, then it has at most $2n$ nodes. Proof. Each leaf other than the root has a value, so there are at most $n$ leaves, or the root alone. In a rooted tree, let $L$, $U$ and $B$ be the numbers of nodes with zero, one, and two or more children. The tree has $L + U + B - 1$ edges, and each edge goes to a child, so the number of edges is the sum of the numbers of children, which is at least $U + 2B$. So $L + U + B - 1 \ge U + 2B$, that is, $B \le L - 1$. The nodes without a value other than the root have at least two children, so there are at most $n - 1$ of them, and with the root and the at most $n$ nodes with values the total is at most $2n$. $\square$