Proofs: PR quadtree
These are the human proofs of PR quadtree, at full length.
The PR quadtree operations keep the compact invariant and report exactly the points in a box full
This proof shows: correctness, termination.
We use the names of the pseudocode. The root cell is , cells are half-open squares, and points have integer coordinates. For a node let be the set of points stored in the leaves below . The invariant (R) asks: (1) each point of the tree lies in the cell of its leaf and is stored once; (2) each leaf holds at most points; (3) each internal node has , and each leaf has ; and (4) the children of an internal node of side are its four quadrants, of side .
Lemma 1 (quadrants). For a cell of side , the four quadrants are disjoint, their union is , and the quadrant chosen for is the one that holds . Proof. On each axis, is the disjoint union of and , and the test picks the half that holds . The product of the halves gives the claim.
Lemma 2 (unit cells). A cell of side 1 holds at most one integer point. Proof. It is with integers , and the only integer point in it is .
Search. By Lemma 1 and (R) part 4, at each internal node the point lies in exactly one child cell, so there is exactly one leaf whose cell holds , and line L1 (and line L12) reaches it in at most steps, since the side halves at each step. By (R) part 1, is stored exactly when it is in that leaf's list.
INSERT. Let be a point of the root cell that is not stored. Lines L1 to L3 add to the only leaf whose cell holds it, and add 1 to the count of each node whose subtree now holds ; part 1 and part 3 hold. If , the loop does not run and (R) holds.
Otherwise the loop runs with a leaf that holds points, all in its cell, while (R) holds at every other node. By Lemma 2, the side of is at least 2, so line L5 can make the four quadrants. Line L6 moves each point into the quadrant that holds it (Lemma 1), with counts equal to the list sizes; now is internal with , so part 3 holds at and part 4 holds. The children's lists add up to points, so at most one child holds more than ; if none does, (R) holds everywhere and the loop stops. If one does, it holds exactly points, all in its cell, and the loop continues with it in the same situation. The side halves at each pass and is at least 2 at each pass, so the loop stops after at most passes.
DELETE. Let be stored, and let be its leaf, with path from the root down to the parent of . After line L13, is gone and each count on the path and at is one less, so the counts are correct, and parts 1, 2 and 4 hold. Part 3 can fail only at the nodes , and only when now, since before it was more than .
Line L14 treats in turn. Claim: when it reaches , (R) holds at every node except possibly , and the counts are correct. This holds for . If , then for each , since the count of a node is at least that of its child, so (R) holds everywhere and the loop can stop. If , each child of has ; by the claim (R) part 3 holds at , so is a leaf. Line L14 gathers the lists of the four leaves, at most points in total, all in the cell of by part 1 and Lemma 1, into one leaf with the same count. Parts 1 to 4 then hold at , and the claim holds for . The loop stops after at most steps. If it ends at the root, (R) holds everywhere.
Uniqueness. Let be the tree on a set of points of the cell that satisfies (R). If , part 3 forces a leaf with list . If , the root is internal, part 4 fixes its children as the quadrants, and by part 1 and Lemma 1 the child for quadrant is a tree on that satisfies (R); by induction on the side, it is . So the shape depends only on , not on the order of the operations.
RANGE-SEARCH. Let . Each reported point is stored and is in by the test of line L10, and each leaf is reached at most once, since the calls follow the tree, so by part 1 no point is reported twice. Let , with leaf . For each node on the path from the root to , lies in the cell of (by part 1 and Lemma 1, the cells along the path are nested) and in , so the cell of meets , and line L9 does not stop the search at . Line L11 calls every child, so the search reaches , and line L10 reports . The calls follow a finite tree, so the search stops.