Proofs: Grid file

The grid file keeps box-shaped bucket regions that partition the grid, and its operations are correct full

This proof shows: correctness, termination.

We use the names of the pseudocode. The scales $xs$ and $ys$ are sorted lists of distinct values, the column of $x$ is $c(x) = |\{v \in xs : v \le x\}|$ and the row of $y$ is $r(y) = |\{v \in ys : v \le y\}|$, so column $c$ holds the $x$ with $xs[c-1] \le x < xs[c]$, with $xs[-1] = -\infty$ and $xs[X - 1] = +\infty$. The invariant (G) asks: (1) the regions $[c_0, c_1) \times [r_0, r_1)$ of the buckets partition the cells $[0, X) \times [0, Y)$, and $G[c][r]$ is the bucket whose region holds $(c, r)$; (2) each point of a bucket has its cell in the region of that bucket; (3) each bucket holds at most $B$ points. Points are distinct.

LOOKUP. Lines L1 and L2 compute $c(x)$ and $r(y)$, and by part 1 line L3 returns the only bucket whose region holds the cell of $p$. By part 2, if $p$ is stored, it is in that bucket.

Lemma 1 (split at a line). Let $b$ have region $[c_0, c_1) \times R$ with $c_0 < a < c_1$. Replacing $b$ by $b_1$ with region $[c_0, a) \times R$ and the points with $x < xs[a-1]$, and $b_2$ with region $[a, c_1) \times R$ and the points with $x \ge xs[a-1]$, and setting $G$ to $b_2$ on its region, keeps parts 1 and 2. The same holds for rows. Proof. The two regions are boxes that partition the region of $b$, so part 1 holds. A point of $b$ has $c_0 \le c(x) < c_1$, and $c(x) \ge a$ if and only if $x \ge xs[a-1]$, so each point goes to the half whose region holds its cell. $\square$

Lemma 2 (refine). Let $b$ have a single cell $(c, r)$ and at least two points with distinct $x$ values, and let $v$ be the median of their distinct $x$ values, $v = d[\lfloor m/2 \rfloor]$ for the sorted distinct values $d_0 < \cdots < d_{m-1}$, $m \ge 2$. Inserting $v$ into $xs$, copying column $c$ of $G$ to a new column $c + 1$, and adding 1 to each $c_1 > c$ and each $c_0 > c$ keeps parts 1, 2 and 3, and then $b$ has columns $c$ and $c + 1$, each holding at least one point of $b$. Proof. All points of $b$ are in column $c$, so $xs[c-1] \le d_0 < v \le d_{m-1} < xs[c]$, and $v$ is a new value that goes to index $c$ of $xs$. The old column $c$ becomes the columns $c$, for $x < v$, and $c + 1$, for $x \ge v$, and every later column moves up by one. A region that did not contain column $c$ moves with its columns or stays; a region that contained it now contains both new columns. The regions are still boxes and still partition the grid, and the copied directory column names the same buckets, so part 1 holds. Each point's new cell lies in the moved region of its bucket, so part 2 holds; no bucket changes its points, so part 3 is unchanged. Finally, $d_0 < v$ is in column $c$ and $d_{m-1} \ge v$ is in column $c + 1$. The case of rows is the same. $\square$

INSERT. If $p$ is stored, line L4 finds it by LOOKUP. Otherwise line L5 adds it to the bucket of its cell, which keeps parts 1 and 2; part 3 can fail only at that bucket. Consider a pass of the loop with $b$ holding $k > B$ points, all other buckets within capacity. If the region of $b$ spans two or more columns or rows, lines L8 and L10 split it at a line inside its span by Lemma 1. Otherwise $b$ has one cell; its $k \ge 2$ distinct points differ on some axis, and the code refines an axis on which they differ, so by Lemma 2 line L9 keeps (G) up to part 3 at $b$, and line L10 then splits $b$ at the new line, by Lemma 1, into two nonempty halves. After line L10, at most one of the two halves can hold more than $B$ points, and $b$ becomes the larger one. For termination, look at the pair $(k, a)$, with $k$ the number of points of $b$ and $a$ the number of cells of its region. In a pass of the first kind, if both halves get points, the larger has at most $k - 1$ points; if all points go to one half, $k$ is the same and $a$ is smaller. In a pass of the second kind, both halves get points, so $k$ drops. Refining adds cells to the grid but the pair is taken for the new $b$ after line L10, so in every pass the pair drops in the lexicographic order, which has no infinite descending chain, since $k$ can drop at most $k$ times and between two drops $a$ only shrinks. Hence the loop stops, and then part 3 holds at every bucket.

DELETE. Line L12 finds the bucket of $p$, and line L13 removes $p$, which keeps (G). Line L14 merges $u$ into $b$ only when their regions are boxes with the same rows and adjacent columns, or the same columns and adjacent rows; their union is then a box, and the two regions are replaced by it, so part 1 holds after $G$ is set on the cells of $u$. Each point keeps a cell in the region of its bucket, so part 2 holds, and part 3 holds by the size test. The scan of line L14 is over a finite list.

RANGE-SEARCH. Let $q = (x, y)$ be stored with $lo \le q \le hi$. Then $c(lo_x) \le c(x) \le c(hi_x)$ and $r(lo_y) \le r(y) \le r(hi_y)$, since $c$ and $r$ do not decrease, so the cell of $q$ is in the block of line L15, and line L16 reads the bucket $G[c(x)][r(y)]$, which holds $q$ by parts 1 and 2. Line L17 reports exactly the points of the read buckets that lie in the box, and each bucket is read once, so each point is reported once. The block is finite, so the search stops. $\blacksquare$