Proofs: X-tree

The X-tree operations keep the invariant, stop, and the searches return the right rectangles full

This proof shows: correctness, termination.

Let $M \ge 2$ and $1 \le m \le M/2$. Heights count from the leaves: a leaf has height 0. The capacity of a leaf is $M$, and of a directory node of $b$ blocks $bM$. For a node $u$, let $E(u)$ be the multiset of stored entries below $u$ and $R_u$ the rectangle kept at $u$. We use the invariant (X): (1) all leaves at one depth; (2) every non-root node has at least $m$ entries and at most its capacity, and an internal root has at least 2 children and at most its capacity; leaves have one block; (3) $R_u$ is the MBR of the rectangles of the entries of $u$, and so, by induction from the leaves, of the rectangles in $E(u)$.

Lemma 1 (recompute). If (3) holds at every child of $u$, recomputing $u$ makes (3) hold at $u$.

Proof. The MBR of a set is, axis by axis, the least lower end and the greatest upper end. For a union of sets, these are the least and the greatest over the parts, so the MBR of the children's rectangles is the MBR of $E(u)$. $\square$

Lemma 2 (split sizes). Let $u$ have $N$ entries, more than its capacity $C$. If SPLIT returns two groups, they partition the entries, each has at least $m$ entries, and each fits in the blocks it is given. If it returns none, $u$ gains a block and then has capacity $C + M \ge N$.

Proof. A topological split cuts a sorted list at $k$ with $g \le k \le N - g$, where $g = \max(m, \lfloor 0.4 N \rfloor)$. The range is not empty: $2m \le M \le C < N$, and $2\lfloor 0.4N \rfloor \le 0.8N \le N$. An overlap-minimal split cuts at $k$ with $g' \le k \le N - g'$ and $g' \ge m$, if any such $k$ exists. So in both cases each group has at least $m$ entries. A new leaf gets one block and at most $N - m \le M$ entries, since a leaf has $N = M + 1$. A directory group of $s$ entries gets $\lceil s/M \rceil$ blocks, whose capacity is at least $s$. If no split is taken, which happens only at a directory node, $u$ had $N = C + 1$ entries, since entries arrive one at a time and $u$ was within capacity before, so the new capacity $C + M \ge C + 1 = N$. $\square$

Lemma 3 (INSERT). Let (X) hold and let $e$ be a stored entry (level 0) or a node of height $\ell - 1$ whose subtree satisfies (X) inside, with $\ell$ at most the height of the tree. Then INSERT$(e, \ell)$ stops, and afterwards (X) holds for the old entries plus those of $e$.

Proof. Lines L1 and L2 follow one child per level, from the root down to a node $u$ of height $\ell$, in at most $h$ steps. Line L3 adds $e$ to $u$, so the leaves of $e$ are at the same depth as the others. Line L4 walks from $u$ to the root, one level per step, so it stops. At each node on the walk, only one entry has been added since it was last within capacity: $e$ for $u$, or the new sibling from a split of the child below. If it is over capacity, Lemma 2 applies. If two groups are made, $u$ and the new node $v$ have the same height and at least $m$ entries each, and either $v$ is added to the parent, the next node of the walk, or a new root with the two children $u$ and $v$ is made, which puts every leaf one level deeper and keeps (1). If no split is made, $u$ is a supernode within its new capacity and the parent gains nothing. Nodes off the walk keep their entries. So (1) and (2) hold at the end. For (3): the nodes whose entries change are those on the walk, the new nodes of splits, and a new root. Each is recomputed after its children are final: the groups of a split when they are made, the nodes of the walk at line L4, and the new root when it is made. By Lemma 1 and induction on height, (3) holds everywhere. $\square$

Lemma 4 (DELETE). Let (X) hold. DELETE$(\text{id}, r)$ stops, returns false if $(r, \text{id})$ is not stored, and otherwise leaves (X) for the entries without it.

Proof. If $(r, \text{id})$ is stored in a leaf $L$, then by (3), $r \subseteq R_v$ for every node $v$ on the path to $L$, so every such $R_v$ meets $r$ and the search of line L14 reaches $L$; it visits each node at most once, so it stops, and it reports the entry only if it is stored. Line L15 walks from $L$ to the root. A node with fewer than $m$ entries is removed from its parent, and its entries are kept with its height; a node that stays has at least $m$ entries, at most as many as before, and its blocks are set to $\lceil s/M \rceil$, which keeps its capacity at least its size; it is recomputed by Lemma 1, the root last. Now (1) and (3) hold for the entries in the tree, and every non-root node satisfies (2). The root keeps an entry unless it was a leaf and is now empty, since a child of an internal root off the path is unchanged. Each kept entry came from a node of height $h_u$ below the root, so the tree still has height more than $h_u$ when it is reinserted, the height only growing during reinsertion, and Lemma 3 applies. Line L16 removes roots with one child, each step lowering every leaf by one level, which keeps (1) and gives an internal root at least 2 children. Every loop moves up a level or handles one of finitely many entries, so DELETE stops. $\square$

Theorem. SEARCH$(q)$ reports exactly the stored rectangles that meet $q$. KNN$(q, k)$ returns $\min(k, n)$ entries in order of distance from $q$, whose distances are the $\min(k, n)$ smallest. Both stop.

Proof. SEARCH. An entry is reported only if it meets $q$. If a stored rectangle $r$ meets $q$, then $r \subseteq R_v$ for every node $v$ above it, by (3), so every such $R_v$ meets $q$, line L17 skips none of them, and the search reaches the leaf of $r$ and reports it. Each node is visited once, so the search stops.

KNN. A node $v$ has the key $\operatorname{dist}(q, R_v)$ and an entry its distance $\operatorname{dist}(q, r)$. For every entry $r$ in $E(v)$, $r \subseteq R_v$, so $\operatorname{dist}(q, r) \ge \operatorname{dist}(q, R_v)$: the key of a node is a lower bound on the distances of the entries below it. When an entry $r$ is popped, every entry $r'$ not yet output is in the queue, with key at least that of $r$, or below a node $v$ in the queue, with $\operatorname{dist}(q, r') \ge \operatorname{dist}(q, R_v) \ge \operatorname{dist}(q, r)$, since the root starts the queue and every popped node pushes all its entries. So the entries come out in order of distance, each at most once, and the first $\min(k, n)$ are the nearest. Each node and entry is pushed once, so line L18 stops. $\blacksquare$