Proofs: R-tree

The R-tree operations keep the invariant, and search reports exactly the rectangles that meet the query full

This proof shows: correctness, termination.

We use the names of the pseudocode. A rectangle is closed. For a node $u$ let $\operatorname{Obj}(u)$ be the set of leaf entries in the subtree of $u$. The invariant (R) says: (1) all leaves are at one depth; (2) each non-root node has between $m$ and $M$ entries, and an internal root has between 2 and $M$; (3) the rectangle of each internal entry $(r, c)$ is $\operatorname{MBR}(c)$.

Lemma 1 (containment). Under (R) part 3, for each internal entry $(r, c)$ and each leaf entry $(s, id)$ in $\operatorname{Obj}(c)$, $s \subseteq r$. Proof. By induction on the height of $c$. If $c$ is a leaf, $s$ is the rectangle of an entry of $c$, and $\operatorname{MBR}(c)$ contains it. If $c$ is internal, $(s, id)$ is below some entry $(r', c')$ of $c$; by induction $s \subseteq r'$, and $r' \subseteq \operatorname{MBR}(c) = r$. $\square$

SEARCH. Each reported entry is a leaf entry whose rectangle meets $q$ (lines L1 and L2). Each node is reached by one path from the root, so no entry is reported twice. Conversely, let $(s, id)$ be stored with $s \cap q \ne \emptyset$, and let $(r_1, c_1), \ldots, (r_h, c_h)$ be the internal entries on the path from the root to its leaf. By Lemma 1, $s \subseteq r_i$, so $r_i \cap q \supseteq s \cap q \ne \emptyset$ for each $i$. By induction on $i$, line L3 enters $c_i$: the root is reached, and if the node holding $(r_i, c_i)$ is reached, the test of line L1 passes. In the leaf, line L1 passes for $(s, id)$ and line L2 reports it. The tree is finite and each node is entered once, so SEARCH stops.

Lemma 2 (split). The quadratic split of $M + 1$ entries returns two disjoint groups whose union is the input, each with at least $m$ entries. Proof. Each step moves one entry from the rest to a group, so the groups stay disjoint and the union is kept. Each group starts with one seed. Before each step, if a group $g$ has $|g| + |\text{rest}| = m$, all of the rest goes to $g$, which then has $m$ entries. Otherwise both groups satisfy $|g| + |\text{rest}| > m$, and one entry is moved, which lowers $|g| + |\text{rest}|$ by at most 1 for each group, so both sums stay at least $m$. When the rest is empty, each group has $|g| \ge m$. At the start $|g| + |\text{rest}| = 1 + (M - 1) = M \ge 2m \ge m$, so the induction starts. The other group has at least $m$ entries because $M + 1 - m \ge m$. $\square$

INSERT. Assume (R) holds before the call, and let $h$ be the height. CHOOSE-LEAF follows one entry per level to a leaf $u$ (lines L4 and L5), and line L6 adds the new entry. Only the nodes on the path from $u$ to the root can now break (R): $u$ may hold $M + 1$ entries, and the rectangles on the path may no longer be MBRs.

Claim: at the start of each pass of line L7 with node $u$ at height $j$, (R) holds at every node except that $u$ may have $M + 1$ entries and the rectangles of the entries for $u$ and its ancestors may be wrong; all rectangles inside the subtree of $u$ are correct, and all leaves are at depth $h$. This holds for the leaf. If $u$ has $M + 1$ entries, line L8 splits them by Lemma 2 into $u$ and a new node $v$ of the same kind, each with $m$ to $M$ entries; the children moved to $v$ keep their subtrees, so all rectangles inside the subtrees of $u$ and $v$ stay correct, and the leaves below $v$ keep their depth. If $u$ is the root, line L10 makes a root with two correct entries for $u$ and $v$; the new root is internal with 2 entries, and every leaf is now at depth $h + 1$, so (R) holds everywhere and INSERT stops. Otherwise line L9 adds a correct entry for $v$ to the parent $p$, so $p$ may hold $M + 1$ entries. In both cases line L11 sets the rectangle of the entry for $u$ in $p$ to $\operatorname{MBR}(u)$, so all rectangles inside the subtree of $p$ are correct, and the claim holds for $p$ at height $j + 1$. When line L7 passes the root, the root has at most $M$ entries and all rectangles are correct, so (R) holds. Each pass goes up one level, so INSERT stops after at most $h + 1$ passes.

The same argument holds when INSERT is called by line L15 to put an entry $(r, c)$ at height $j \ge 1$: CHOOSE-LEAF stops at a node of height $j$, the subtree of $c$ has height $j - 1$, so its leaves land at depth $h$, and the rest of the claim is the same.

DELETE. By Lemma 1, the leaf that holds $(r, id)$ is below entries whose rectangles contain $r$, so line L12 finds it if it is stored, and it answers false only when the entry is not stored. Line L13 removes the entry. CONDENSE-TREE (line L14) goes up the path from that leaf. At each non-root node $u$ on the path: if $u$ has fewer than $m$ entries, it is removed from its parent, and its subtree is kept in $Q$ with its height; else the rectangle for $u$ in its parent is set to $\operatorname{MBR}(u)$, which is correct, since the rectangles below $u$ are correct by induction from the leaf up. After line L14, each remaining node has a correct rectangle, each remaining non-root node has between $m$ and $M$ entries (the nodes on the path that kept at least $m$ were not underfull, and the other nodes did not change), and all remaining leaves are at depth $h$. The root may now have only one entry, and if the root is a leaf it may have fewer.

Line L15 reinserts each entry of each node of $Q$ at the height of that node. By the claim above, each such INSERT keeps parts 1 to 3, except for the possible root with one entry, which INSERT does not create but does not repair either. Each entry of a removed node goes back once, so the set of stored objects is the old set minus $(r, id)$. Line L16 replaces an internal root with one entry by its child, which lowers every leaf depth by one and keeps parts 1 and 3; it stops because the height drops by one each time. After it, an internal root has at least 2 entries, and (R) holds.

Termination of DELETE. Line L12 visits each node at most once. Line L14 makes one step per level. Line L15 runs finitely many INSERTs, each of which stops. Line L16 runs at most $h$ times. $\blacksquare$