Proofs: Hilbert R-tree

The Hilbert R-tree keeps a balanced tree of sorted keys with correct bounding rectangles, and its operations are correct full

This proof shows: correctness, termination.

We use the names of the pseudocode. Keys are pairs $(H(r), r)$ and are totally ordered and distinct for distinct rectangles. The invariant (H) asks: (1) all leaves are at the same depth; (2) the leaf keys, read from left to right, are strictly increasing; (3) every node other than the root has between $m$ and $C$ entries, the root at most $C$, and at least 2 if it is internal; (4) the MBR of each node is the bounding rectangle of the rectangles below it, and its LHV is the largest key below it. Here $C \ge 4$ and $m = \lfloor C/2 \rfloor \ge 2$.

Lemma 1 (runs). Under (H), the keys below each node form a run of consecutive leaf keys, and the runs of the children of a node are consecutive and in the order of the children. Proof. By induction on the height: the leaf keys are read from left to right, so the keys below a node are the keys of its children read in order. $\square$

Lemma 2 (descent). Under (H), lines L2 and L3 reach the only leaf $u$ such that $k$, if stored, is in $u$, and such that inserting $k$ into $u$ keeps part 2. Proof. At an internal node with children $c_1, \dots, c_t$, by Lemma 1 and part 4 the keys of $c_i$ are greater than LHV$(c_{i-1})$ and at most LHV$(c_i)$. Let $i$ be the first index with LHV$(c_i) \ge k$, or $t$ if there is none. Every key below $c_j$ with $j < i$ is less than $k$, and every key below $c_j$ with $j > i$ is greater than LHV$(c_i) \ge k$ (or there is no such $j$). So $k$ can only be below $c_i$, and putting it in order below $c_i$ keeps the whole sequence sorted. By induction on the depth the claim holds at the leaf. $\square$

Lemma 3 (dealing). If $j$ items in order are dealt among $t$ adjacent nodes that hold them as consecutive runs, the leaf order is kept, and each node gets $\lfloor j/t \rfloor$ or $\lceil j/t \rceil$ items. Proof. The items keep their order and the nodes keep theirs; the counts are those of divmod. $\square$

INSERT. By Lemma 2, line L4 keeps part 2, and part 3 can fail only at $u$, which has $C + 1$ entries. We claim that at each test of line L5, (H) parts 1 and 2 hold and part 3 holds except that $u$ may have $C + 1$ entries. If $u$ has at most $C$, the loop stops. If $u$ is the root (line L6), its $C + 1 \ge 5$ entries are dealt into two nodes of at least $\lfloor (C+1)/2 \rfloor \ge m$ and at most $C$ entries under a new root with two children; all leaves get one level deeper, so part 1 holds. Otherwise $u$ has a sibling next to it, since its parent has at least 2 children by part 3. The two hold $j$ entries with $m + C + 1 \le j \le 2C + 1$. If $j \le 2C$ (line L8), Lemma 3 gives each at least $\lfloor j/2 \rfloor \ge m$ and at most $\lceil 2C/2 \rceil = C$, and the parent is unchanged, so the loop stops. If $j = 2C + 1$ (line L9), the three nodes get $\lfloor (2C+1)/3 \rfloor$ or $\lceil (2C+1)/3 \rceil$ entries; since $C \ge 4$, $\lfloor (2C+1)/3 \rfloor \ge \lfloor C/2 \rfloor = m$ and $\lceil (2C+1)/3 \rceil \le C$. The new node is placed next to the two in the parent, so Lemma 1 and part 2 still hold, all three are at the same level, and the parent has one more child (line L10), as in the claim. Each pass goes up one level, so the loop stops after at most $h + 1$ passes, and then parts 1 to 3 hold.

Part 4 may now be wrong only at nodes whose entries changed: the leaf, the nodes that shared or split, which are on the path or children of nodes on the path, and the new root. Every node that received entries is refreshed by _deal from its own entries, and the entries of a sibling leaf or node are themselves correct, since only nodes at the same level or lower were changed before it. Line L11 then refreshes the leaf and each ancestor from the bottom up, so each is computed from children that are already correct. Hence part 4 holds.

DELETE. By Lemma 2, line L12 finds $k$ if it is stored. Line L13 keeps part 2. The loop of lines L14 to L16 has the same form: $u$ has $m - 1$ entries and its sibling between $m$ and $C$, so $j$ is between $2m - 1$ and $C + m - 1$. If $j \ge 2m$, Lemma 3 gives each at least $m$ and at most $\lceil (C + m - 1)/2 \rceil \le C$, and the loop stops. Otherwise $j = 2m - 1 \le C$ and the merged node fits; the parent loses one child and may fall below $m$, and the loop goes on with it. At the root no lower bound is needed, except that an internal root with one child is replaced by that child in line L17, which removes one level from every leaf, so parts 1 and 3 hold. Part 4 is restored as for insertion. Each pass goes up one level, so the loop stops.

WINDOW. By part 4, every rectangle below a node lies in its MBR, so if the MBR misses $q$, no rectangle below meets $q$, and line L19 skips nothing that must be reported. Every other node is pushed by its parent, so every leaf whose MBR meets $q$ is reached, and line L20 tests each of its rectangles. Each node is pushed once, so the loop stops after at most as many passes as there are nodes.

So each operation stops, keeps (H), and gives the right answer. $\blacksquare$