Proofs: R+-tree

The R+-tree operations keep the partition invariant, stop, and search reports each rectangle that meets the query exactly once full

This proof shows: correctness, termination.

Regions are half-open, $[x_0, x_1) \times [y_0, y_1)$ with $x_0 < x_1$ and $y_0 < y_1$, where the ends may be infinite; stored rectangles and the query are closed and not empty. A closed rectangle $r$ meets a region $R$ if $r \cap R \ne \emptyset$. We prove that the invariant (R+) holds after every operation, that every operation stops, and that SEARCH is correct.

Lemma 1 (cut of a region). For a region $R$ and a line $x = c$ with $x_0 < c < x_1$, the halves $R_L = [x_0, c) \times [y_0, y_1)$ and $R_R = [c, x_1) \times [y_0, y_1)$ are regions, disjoint, with union $R$. A closed rectangle $r$ meets $R$ if and only if it meets $R_L$ or $R_R$. The same holds for $y$.

Proof. Each point of $R$ has $x < c$ or $x \ge c$, not both. Since $R = R_L \cup R_R$, $r \cap R = (r \cap R_L) \cup (r \cap R_R)$. $\square$

Lemma 2 (CUT). Let $u$ satisfy parts (1) to (3) of (R+) in its subtree, for some set $S$ of rectangles: each leaf below $u$ holds the rectangles of $S$ that meet its region. Then CUT$(u, \text{axis}, c)$ returns nodes $u_L$ and $u_R$ with regions $R_L$ and $R_R$ of Lemma 1, whose subtrees satisfy (1) to (3) for $S$, with leaves at the depth of the leaves of $u$ relative to $u$, and each with at most as many entries as $u$.

Proof. By induction on the height of $u$. A leaf (line L12) gives two leaves with regions $R_L$ and $R_R$, each with the entries of $u$ that meet it. A rectangle of $S$ that meets $R_L$ meets $R$, so it is in $u$, and so it is in $u_L$: part (2) holds. Each half keeps at most the entries of $u$. For an internal node (line L13), a child $v$ with region $[a, b) \times \ldots$ goes left if $b \le c$, right if $a \ge c$, and otherwise, since $a < c < b$, is cut by induction into $v_L$ and $v_R$ with regions $\text{reg}(v) \cap R_L$ and $\text{reg}(v) \cap R_R$. The regions of the children of $u$ partition $R$, so the regions of the new children of $u_L$ partition $R \cap R_L = R_L$, and the same for $u_R$: part (1) holds. Parts (2) and (3) hold in each child by induction. The number of children of $u_L$ is the number of children of $u$ with $a < c$, which is at most the number of children of $u$. $\square$

Guillotine partitions. A partition of a region $R$ into regions is guillotine if it is $\{R\}$, or if a line cuts $R$ into the halves $R_L$ and $R_R$ of Lemma 1 so that every part lies in $R_L$ or in $R_R$, and the parts in each half form a guillotine partition of that half. We call the line the top cut.

Lemma 3 (guillotine facts). (a) If a guillotine partition of $R$ has $s \ge 2$ parts, its top cut is at a side of a part, lies strictly inside $R$, crosses no part, and has $n_L, n_R \ge 1$ parts on its sides with $n_L + n_R = s$. (b) The intersection of a guillotine partition of $R$ with a half $R_L$ given by any line strictly inside $R$ (parts that cross the line replaced by their two halves, parts outside dropped) is a guillotine partition of $R_L$. (c) Replacing one part of a guillotine partition by a guillotine partition of that part gives a guillotine partition.

Proof. (a) The parts in $R_L$ cover $R_L$, which is not empty, so at least one part lies on each side; a part in $R_L$ that touches the line has its upper side at the line. (b) By induction on the number of parts. If the top cut is parallel to the new line, or the new line misses one of its halves, the new line meets one or both halves, and we apply induction in each; otherwise the top cut, restricted to $R_L$, is a cut of $R_L$, and we apply induction to each half. In every case the result is built by cuts. (c) By induction on the cut tree: the replaced part is a leaf of the tree, and we hang the tree of its partition below that leaf. $\square$

Lemma 4 (children are guillotine). In every internal node, the regions of the children form a guillotine partition of the region of the node.

Proof. We show that every operation keeps this. A new root made at line L8 has as children the pieces of a SPLIT-ALL of a node of the same region, and SPLIT-ALL makes its pieces by cuts, so they form a guillotine partition. At line L7, a child is replaced by the pieces of its SPLIT-ALL, a guillotine partition of the child, which keeps the property by Lemma 3(c). A CUT of an internal node $u$ (line L13) gives to $u_L$ the children of $u$ intersected with $R_L$, which is guillotine by Lemma 3(b); a child cut downward is itself an internal node or a leaf, and its own children are treated the same way, by induction. DELETE does not change regions. $\square$

Lemma 5 (SPLIT-ALL). Let $u$ satisfy (1) to (3) for $S$. Then SPLIT-ALL$(u)$ stops and returns nodes whose regions partition the region of $u$ by cuts, each satisfying (1) to (3) for $S$. Every internal node returned has at most $M$ children, and every leaf returned with more than $M$ entries has no good cut. With clean cuts only, on an internal node with $s > M \ge 2$ children, it returns fewer than $s$ pieces, each with at most $M$ children.

Proof. A good cut found by CHOOSE-CUT (lines L10 and L11) has $0 < n_L, n_R < \text{size}(u)$, where $n_L$ and $n_R$ count exactly the entries that go to each side by Lemma 2: the leaf entries with $x_1 < c$ meet $R_L$ and those with $x_2 \ge c$ meet $R_R$, and the children with $a < c$ go left and with $b > c$ go right. So both pieces are strictly smaller than $u$, and the recursion stops. By Lemmas 1 and 2, the pieces partition the region of $u$ and satisfy (1) to (3). A node is returned unchanged only if it has at most $M$ entries or no good cut. An internal node with more than $M$ children has a good cut, by Lemma 4 and Lemma 3(a), so it is never returned with more than $M$ children; a leaf with more than $M$ entries is returned only with no good cut. With clean cuts only, the internal nodes in the recursion stay guillotine by Lemma 3(b), so a clean good cut exists while a node has more than $M$ children, and every cut splits the $t$ children of a node into two groups with sizes summing to $t$. The pieces are the leaves of a binary tree of cuts in which each cut node has more than $M \ge 2$ children. The two pieces of the last cut on any branch have sizes summing to more than $2$, so not every piece has one child, and the number of pieces is less than $s$. $\square$

The nodes below a returned node keep their properties. A piece of an internal node made by a downward cut has at most as many children as the node, by Lemma 2, so at most $M$. A piece of a leaf $w$ with no good cut also has no good cut: its region lies in that of $w$, so every candidate line strictly inside the piece is a candidate for $w$, and if all entries of $w$ reach one side of the line, so do all entries of the piece. A piece of a leaf with at most $M$ entries has at most $M$. So part (4) holds in the whole tree after each SPLIT-ALL, given that it held before.

INSERT. Let (R+) hold for $S$ and insert $r$. Claim: the call on a node $u$ returns nodes whose regions partition the region of $u$ by cuts, whose subtrees satisfy (R+) for $S \cup \{r\}$, with leaves at the old depth. By induction on height. At a leaf, $r$ is added if and only if the walk reached it. The walk goes into every child whose region meets $r$ (line L5), and by part (1) the union of the regions of the children is the region of the parent, so the leaves reached are exactly those whose regions meet $r$. So each leaf holds the rectangles of $S \cup \{r\}$ that meet it (line L6). At an internal node, each child that $r$ meets is replaced by the pieces of the recursive call, whose regions partition the region of the child; so the children still partition the region of $u$. Then SPLIT-ALL (line L7) keeps (R+) by Lemma 5 and the remark after it. At the root, if $q \ge 2$ pieces come back, line L8 makes a new root over them. Its region is the plane, the pieces partition it, and every leaf goes one level deeper, so (1) to (3) hold. If $q \le M$ the loop ends. Otherwise SPLIT-ALL with clean cuts returns fewer than $q$ pieces, each with at most $M$ children, by Lemma 5 with Lemma 4. So the number of pieces strictly decreases from one pass of line L8 to the next, and the loop ends with one root, and (R+) holds for $S \cup \{r\}$.

DELETE. The walk of line L14 reaches every leaf whose region meets $r$, by the argument above, and those are exactly the leaves that hold $r$ by part (2). Removing $r$ from each gives part (2) for $S \setminus \{r\}$; parts (1) and (3) do not change, and a smaller node still satisfies (4).

SEARCH. Let $r \in S$ meet $q$, and let $p = (\max(q.x_1, r.x_1), \max(q.y_1, r.y_1))$. Since $r$ and $q$ are closed and meet, $p \in r \cap q$. By part (1), applied from the root down, exactly one leaf $\lambda$ has $p$ in its region. Its region meets $r$ and $q$ at $p$, so $r$ is stored in $\lambda$ by part (2), and every ancestor of $\lambda$ has a region that contains $p$, so it meets $q$ and the search goes into it (line L2). At $\lambda$, line L3 sees $r$, and line L4 finds $p$ in the region and reports $r$. In every other leaf the search sees $r$, $p$ is not in the region, since the leaf regions are disjoint, so $r$ is not reported there. A rectangle that does not meet $q$ is never reported, by the test of line L3. So the output is exactly the rectangles of $S$ that meet $q$, each once.

Termination. SEARCH and DELETE visit each node at most once, since the tree is finite. INSERT stops by Lemma 5 and the argument for line L8. $\blacksquare$