Proofs: Linear quadtree

The linear quadtree keeps the list of maximal black blocks in Z-order full

This proof shows: correctness, termination.

We use the names of the pseudocode. For a block $b = (c, \ell)$ let $I(b) = [c, c + 4^\ell)$, the set of codes of its pixels. The invariant (L) asks: (1) $0 \le \ell \le D$ and $4^\ell \mid c$; (2) the intervals $I(b)$ are disjoint and the list is sorted by $c$; (3) no four blocks $(p + k 4^\ell, \ell)$, $k = 0, \ldots, 3$, with $4^{\ell+1} \mid p$, are all in the list. The image of the list is the set of pixels whose codes lie in some $I(b)$.

Lemma 1 (cells are intervals). For $4^\ell \mid c$, the codes $I(c, \ell)$ are exactly the codes of the pixels of one aligned square of side $2^\ell$, and $I(p, \ell + 1)$ is the disjoint union of $I(p + k 4^\ell, \ell)$, $k = 0, \ldots, 3$. Two such intervals are either disjoint or nested. Proof. The code of $(x, y)$ has the bits of $x$ and $y$ at the positions $2i$ and $2i + 1$. Fixing all bits of position $2\ell$ and above fixes the bits $i \ge \ell$ of $x$ and $y$, so it fixes an aligned square of side $2^\ell$, and leaves the lower $2\ell$ bits free, which is the interval $[c, c + 4^\ell)$. The bits at positions $2\ell$ and $2\ell + 1$ give the four children in order. Two intervals of the form $[c, c + 4^\ell)$ with $4^\ell \mid c$ are dyadic in base 4, so they are disjoint or nested. $\square$

Lemma 2 (uniqueness). For a set $P$ of black pixels, there is exactly one list satisfying (L) whose image is $P$: the black leaves of the region quadtree of $P$. Proof. Call a cell maximal black if it is all black and its parent is not (or it is the root). The maximal black cells are disjoint by Lemma 1, they cover $P$, and they are the black leaves of the region quadtree. Let a list satisfy (L) with image $P$. Each block is a black cell. Suppose some block $b$ is not maximal, so its parent $Q$ is all black. No block contains $Q$, since it would overlap $b$; so by Lemma 1 every block that meets $Q$ lies inside $Q$, and since $Q$ is black these blocks tile $Q$. Let $b'$ be one of them of the least level $m$; its parent $Q'$ lies inside $Q$. A block that meets a child of $Q'$ is inside $Q$, so it has level at least $m$; if its level were more than $m$ it would contain $Q'$, by Lemma 1, and overlap $b'$. So each of the four children of $Q'$ is tiled by blocks of level exactly $m$, that is, each child is a block, which part 3 forbids. Hence each block is maximal black. Each maximal black cell is tiled by blocks, which are maximal black cells and so cannot lie strictly inside it; so it is a block. $\square$

LOCATE. By part 2, the intervals are sorted and disjoint. If $z \in I(b_i)$, then $c_i \le z$ and every later block starts after $z$, so $i$ is the last index with $c_i \le z$, which line L7 finds, and line L8 accepts it. If line L8 accepts the last index with $c_i \le z$, then $z \in I(b_i)$. So LOCATE returns the block that holds $z$, or none if $z$ is white.

BUILD. We claim that after each pass of lines L1 to L6, the stack, read from bottom to top, satisfies parts 1 and 2, has as image the pixels read so far, and satisfies part 3. Each block on the stack ends at or before the last code read, since a block is pushed as one pixel and a merge replaces four consecutive intervals by their union (Lemma 1). Line L2 pushes $z$, which is larger than all earlier codes, so parts 1 and 2 hold. Line L4 merges the top four only when they are the four children of one cell, so the image does not change, and part 1 holds for the parent, and part 2 holds since the union of four consecutive intervals is an interval in the same place. For part 3, suppose four siblings $(p + k 4^\ell, \ell)$ are on the stack. They are consecutive in the sorted stack, since the blocks between them would lie in the parent's interval, and the last of them, by order of codes, was pushed or made last. At that moment the four were the top four, and lines L3 and L4 merged them. A merge makes one new block on top, and the loop goes on testing the new top four, so no complete group stays on the stack. Each code is pushed once and each merge removes three blocks, so the loop stops. By Lemma 2, the result is the list of black leaves.

INSERT. If line L10 finds $p$ black, nothing changes. Otherwise, $\{z\}$ is disjoint from all blocks, and line L11 adds $(z, 0)$ at its sorted place, so parts 1 and 2 hold and the image is $P \cup \{p\}$. Part 3 can now fail only for a group that contains a block that holds $z$, since every other group was in the list before. Line L12 checks the group of the current block $(c, \ell)$, which is the only block that holds $z$. If the group is complete, line L13 replaces the four blocks by their parent, which does not change the image and keeps parts 1 and 2 by Lemma 1, and the new block is the only one that holds $z$. If the group is not complete, or $\ell = D$, part 3 holds for all groups. Each pass raises $\ell$, so the loop stops after at most $D$ passes.

DELETE. If $p$ is white, nothing changes. Otherwise let $(c, \ell)$ be the block that holds $z$. For $j < \ell$, let $C_j$ be the cell of level $j$ that holds $z$, so $C_0 = \{z\}$ and $C_\ell = I(c, \ell)$. By Lemma 1, $C_{j+1} \setminus C_j$ is the union of the three other children of $C_{j+1}$, and so

a disjoint union of the $3\ell$ blocks that lines L16 and L17 add. They lie inside the removed block, so they are disjoint from the other blocks and from each other, parts 1 and 2 hold, and the image is $P \setminus \{p\}$. For part 3, a group made only of old blocks was there before. A group that contains a new block of level $j$ is the four children of $C_{j+1}$, and one of them, $C_j$, holds the white pixel $z$, so it is not a block. Any other group that changed would contain a part of the removed block, so it is one of these. Hence part 3 holds. The loop runs $\ell \le D$ times.

Blocks in a cell. For an aligned cell $C$ with codes $[lo, hi)$, Lemma 1 says each block is inside $C$, contains $C$, or is disjoint from it. If a block contains $C$, it holds $lo$, and LOCATE finds it. Otherwise the blocks inside $C$ are exactly those with $lo \le c < hi$, a run of the sorted list. $\blacksquare$