Proofs: k-d-B tree

The k-d-B tree keeps a balanced partition of the plane into page regions, and its operations are correct full

This proof shows: correctness, termination.

We use the names of the pseudocode. Regions are half-open boxes $[lo, hi)$, possibly unbounded, and the root's region is the plane. The invariant (K) asks: (1) the regions of the children of each region page partition its region; (2) each point lies in the region of its point page and is stored once; (3) all point pages are at the same depth; (4) a point page holds at most $B$ points and a region page between 1 and $M$ children. We also use (G): the children of each region page form a guillotine partition, that is, either there is one child, or some line $x_a = v$ at a child boundary crosses no child and both sides are again guillotine partitions.

Lemma 1 (SPLIT). Let $u$ satisfy (K) and (G) below it, and let the line $x_a = v$ have $lo_a(u) < v < hi_a(u)$. Then SPLIT$(u, a, v)$ returns two pages $\ell$ and $r$ at the level of $u$, with regions $R(u) \cap \{x_a < v\}$ and $R(u) \cap \{x_a \ge v\}$, such that (K) parts 1 to 3 and (G) hold below each, the points of $u$ are divided between them by the side of the line, and each has at most as many children as $u$ and at least one, if $u$ is a region page. Proof. By induction on the height of $u$. For a point page, the two lists are the points on each side, and each lies in its half region. For a region page, each child $c$ lies left of the line ($hi_a(c) \le v$), right of it ($lo_a(c) \ge v$), or crosses it; a crossing child has $lo_a(c) < v < hi_a(c)$, and by induction it splits into two halves at its own level. The children of $\ell$ are the left children and the left halves; their regions are the parts left of the line of the regions of the children of $u$, which partition $R(u) \cap \{x_a < v\}$, so part 1 holds. Part 3 holds since every half is at the level of the page it came from. Each child of $u$ gives at most one child to each side, so neither side has more than $u$. The region of $u$ has points on both sides of the line, so some child of $u$ meets each side, and each side has a child. For (G), a guillotine partition cut by a line gives a guillotine partition on each side: cut the tree of cuts by the line, and remove the cuts that fall outside. $\square$

Lemma 2 (a cut exists). Let a region page $u$ have $M + 1 \ge 3$ children in a guillotine partition. Then some line at a child boundary leaves at most $M$ entries on each side, counting each crossed child on both sides. Proof. By (G) there is a line that crosses no child, with both sides nonempty; its sides have $L$ and $R$ children with $L + R = M + 1$ and $L, R \ge 1$, so $L, R \le M$. It is at a child boundary $v$ with $v > lo_a(u)$. $\square$

So line L5 always finds a cut for a region page; for a point page with $B + 1$ distinct points, the points differ on some axis, and the median $v$ of the $m \ge 2$ distinct values on it has a value below it, so both sides of $x_a = v$ get a point.

Search. By part 1 and induction, for each point $p$ and each level, exactly one page on the path from the root has a region that holds $p$, so line L1 and line L14 follow one path, and by part 2 the point is stored exactly when it is in the point page reached.

INSERT. Line L2 adds $p$ to the point page that holds it, so part 2 holds, and part 4 can fail only on the path. We claim that when the loop of lines L3 to L9 reaches $u$ on the path, (K) and (G) hold except for part 4 at $u$, where $u$ has one entry or point too many. This is true for the point page. If $u$ is within capacity, line L4 stops with (K) and (G) everywhere. Otherwise line L5 chooses a cut that, by Lemma 2 or the point page argument, puts at most $M$ entries, or at most $B$ points, on each side; line L6 applies SPLIT, which by Lemma 1 gives two pages at the level of $u$ that satisfy (K) and (G) below them. If $u$ is the root, line L7 makes a new root with two children whose regions partition the plane along one line, which is guillotine; every point page gets one level deeper, so part 3 holds, and the loop stops. Otherwise line L8 replaces $u$ by $\ell$ and $r$ in its parent. Their regions partition the region of $u$, so part 1 and (G) hold at the parent, which now has one entry more, as in the claim. The loop goes up one level per pass, so it stops after at most $h + 1$ passes, and then (K) holds.

DELETE. Lines L14 and L15 remove $p$ from the only page where it can be. This keeps parts 1 to 4, since part 4 has no lower bound for point pages.

RANGE-SEARCH. Each page is pushed once, by its parent, so the loop stops, and by part 2 no point is reported twice. Each reported point is in the box by the test of line L12. Let $q$ be stored and in the box, at the point page $w$. Every page on the path from the root to $w$ has a region that holds $q$, by part 1, so it meets the box, line L11 does not skip it, and line L13 pushes the next page of the path. So $w$ is visited, and line L12 reports $q$. $\blacksquare$