Proofs: Region quadtree

The region quadtree operations keep a unique maximal tree of the image full

This proof shows: correctness, termination.

A block $\beta$ is uniform if all its pixels have one color. For a block $\beta$ and an image $I$, let $T(\beta)$ be the tree defined by: if $\beta$ is uniform with color $c$, a leaf of color $c$; else an internal node whose children are $T(\beta_0), \ldots, T(\beta_3)$ for the quadrants $\beta_0, \ldots, \beta_3$ of $\beta$. A block of side 1 is uniform, so $T(\beta)$ is well defined by induction on the side.

Lemma 1 (uniqueness). A tree for a block $\beta$ satisfies (Q) for $I$ exactly when it equals $T(\beta)$. Proof. By induction on the side $s$ of $\beta$. For $s = 1$, by part 1 the only tree is a leaf with the color of the pixel. Let $s \ge 2$ and let $R$ satisfy (Q). If $R$ is a leaf, part 1 says that $\beta$ is uniform, and $R = T(\beta)$. If $R$ is internal, each child satisfies (Q) for its quadrant, so by induction the children are $T(\beta_0), \ldots, T(\beta_3)$. If $\beta$ were uniform with color $c$, each quadrant would be uniform, each child a leaf of color $c$, and part 2 would fail. So $\beta$ is not uniform, and $R = T(\beta)$. Conversely, $T(\beta)$ satisfies part 1 by its definition, and part 2 because, if all four children of an internal node are leaves of color $c$, all four quadrants are uniform with color $c$, so $\beta$ is uniform, and $T(\beta)$ would be a leaf. $\square$

Lemma 2 (merge). If $R_0, \ldots, R_3$ equal $T(\beta_0), \ldots, T(\beta_3)$, the merge step of lines L4 and L5 returns $T(\beta)$. Proof. $\beta$ is uniform with color $c$ exactly when each $\beta_i$ is uniform with color $c$, that is, exactly when each $R_i$ is a leaf of color $c$. In that case the step returns a leaf of color $c$; else it returns the internal node with the $R_i$, and both cases are $T(\beta)$. $\square$

BUILD. Claim: after the round with side $s$ (and at the start, for $s = 1$, by line L1), the node kept for each block of side $s$ is $T$ of that block. The induction step is Lemma 2 applied in line L3 to each block of side $2s$. The loop stops when $s = N$, after $D$ rounds, and the node of the whole image is $T$ of the image. By Lemma 1 it satisfies (Q).

GET. The block of the child chosen in line L7 holds $(x, y)$: the pixel is in the right half exactly when $x \ge x_0 + s/2$, and in the bottom half exactly when $y \ge y_0 + s/2$. So each node on the path holds the pixel, and the side halves each step, so the loop stops at a leaf after at most $D$ steps. By part 1 of (Q), its color is the color of $(x, y)$.

SET. If the pixel already has color $c$, the image does not change and the tree is kept. Else, replacing a leaf of color $c'$ and side $s \ge 2$ by an internal node with four leaves of color $c'$ (line L11) keeps part 1, since each pixel keeps its color. Lines L10 and L11 go down to the leaf of side 1 at $(x, y)$, and line L12 sets it to $c$, so after line L12 part 1 holds for the new image $I'$. Part 2 can now fail only at nodes on the recorded path, since only they changed. Let the path be the blocks $\gamma_1 \supset \gamma_2 \supset \cdots \supset \gamma_D$, from the quadrant of the root down to the pixel's block of side 1. Each child that is not on the path is $T$ of its block for $I'$: it is a subtree that was not changed, or a leaf made by a split, which is uniform with its color in $I'$ since the only changed pixel is on the path; and in both cases it satisfies (Q), so it is $T$ of its block by Lemma 1. The node for $\gamma_D$ is a leaf of side 1, which is $T(\gamma_D)$. Line L13 goes up: if the node for $\gamma_{j+1}$ is $T(\gamma_{j+1})$, then the node for $\gamma_j$ has four children equal to $T$ of its quadrants, and the merge of Lemma 2 makes it $T(\gamma_j)$. By induction up to the root, the tree is $T$ of the image $I'$ and satisfies (Q). The path has $D$ blocks, so SET stops.

UNION. Claim: for nodes $A = T_I(\beta)$ and $B = T_J(\beta)$ of two images, UNION returns $T_{I \cup J}(\beta)$, where $I \cup J$ is the pixelwise OR. By induction on the side of $\beta$. If either is a black leaf, every pixel of $\beta$ is black in $I \cup J$, and a black leaf is $T$ (line L14). If $A$ is a white leaf, $I \cup J$ equals $J$ on $\beta$, and $B = T_J(\beta)$ is the answer (line L15); the same for $B$. Else both are internal, the side is at least 2, and by induction the four recursive results are $T_{I \cup J}$ of the quadrants; Lemma 2 gives $T_{I \cup J}(\beta)$ (line L16). INTERSECTION is the same with black and white swapped, since the AND with a white block is white and the AND with a black block is the other block (line L17). Each call goes down one level, and there are at most $D$ levels, so both stop. $\blacksquare$