Proofs: Fully persistent array

The path-copying array returns the right value in every version and uses O(log n) time and space per write full

This proof shows: correctness, termination, complexity.

We use the definitions of the page, with $n \ge 1$. For integers $lo < hi$, a tree for $[lo, hi)$ is a leaf if $hi - lo = 1$, and otherwise a node whose left child is a tree for $[lo, mid)$ and whose right child is a tree for $[mid, hi)$, with $mid = \lfloor (lo + hi)/2 \rfloor$. Since $hi - lo \ge 2$ gives $lo < mid < hi$, both ranges are non-empty and shorter than $[lo, hi)$. For a tree $v$ for $[lo, hi)$ and an index $i \in [lo, hi)$, let $\text{leaf}(v, i)$ be the leaf reached from $v$ by going to the left child when $i < mid$ and to the right child otherwise, and let $\text{val}(v, i)$ be its value. The invariant of the page says that $\text{val}(\text{roots}[t], i) = A_t[i]$ for every version $t$ and index $i \in [0, n)$.

Lemma 1 (BUILD). For $lo < hi$, BUILD$(a, lo, hi)$ returns a tree for $[lo, hi)$ with $\text{val}(v, i) = a[i]$ for every $i \in [lo, hi)$, made of $2(hi - lo) - 1$ new nodes.

Proof. By induction on $hi - lo$. If it is 1, line L1 returns a leaf for $[lo, lo + 1)$ that holds $a[lo]$. Otherwise, by the hypothesis, line L3 returns a node whose children are trees for $[lo, mid)$ and $[mid, hi)$ with the right values. For $i < mid$, $\text{leaf}(v, i)$ is the leaf of $i$ in the left child, which holds $a[i]$, and likewise for $i \ge mid$ on the right. The number of nodes is $1 + (2(mid - lo) - 1) + (2(hi - mid) - 1) = 2(hi - lo) - 1$. $\square$

Lemma 2 (GET). If $v$ is a tree for $[0, n)$ and $0 \le i < n$, GET$(v, i)$ returns $\text{val}(v, i)$ after at most $\lceil \lg n \rceil$ iterations.

Proof. At the start of each iteration of line L5, $v$ is the node for $[lo, hi)$ on the path to $\text{leaf}(v_0, i)$ from the root $v_0$, and $lo \le i < hi$. This holds at line L4. If $hi - lo > 1$, lines L6 and L7 move to the child whose range contains $i$, which is the next node on the path by the definition of leaf, and keep $lo \le i < hi$. Each iteration replaces $hi - lo$ by $\lfloor (hi - lo)/2 \rfloor$ or $\lceil (hi - lo)/2 \rceil$, so after $j$ iterations $hi - lo \le \lceil n / 2^j \rceil$, and the loop stops after at most $\lceil \lg n \rceil$ iterations with $hi - lo = 1$. Then $v$ is $\text{leaf}(v_0, i)$, and line L8 returns its value. $\square$

Lemma 3 (SET). If $v$ is a tree for $[lo, hi)$ and $lo \le i < hi$, then SET$(v, lo, hi, i, x)$ returns a tree $v'$ for $[lo, hi)$ such that $\text{val}(v', i) = x$ and $\text{leaf}(v', j) = \text{leaf}(v, j)$ for every $j \in [lo, hi)$ with $j \ne i$. It changes no existing node and builds one new node for each node on the path from $v$ to $\text{leaf}(v, i)$, which is at most $\lceil \lg(hi - lo) \rceil + 1$ nodes.

Proof. By induction on $hi - lo$. If it is 1, then $j \ne i$ is impossible in $[lo, hi)$, and line L9 returns a new leaf holding $x$. Otherwise suppose $i < mid$; the case $i \ge mid$ is symmetric with line L12. By the hypothesis applied to the left child, which is a tree for $[lo, mid)$ that contains $i$, the call returns a tree $\ell'$ for $[lo, mid)$ with $\text{val}(\ell', i) = x$ that agrees with the old left child on every other leaf. Line L11 returns a new node with children $\ell'$ and the old right child, which is a tree for $[lo, hi)$. For $j = i$ or $j < mid$, the path goes left and the claim follows from the hypothesis. For $j \ge mid$, the path goes right, into the old right child, so $\text{leaf}(v', j) = \text{leaf}(v, j)$. Lines L9, L11 and L12 only build new nodes and read fields of old ones, so no existing node changes. The count of new nodes is one per level of the path, and the path has at most $\lceil \lg(hi - lo) \rceil + 1$ nodes by the halving argument of Lemma 2. $\square$

Theorem. After any sequence of UPDATE calls on any existing versions, the invariant holds: $\text{GET}(\text{roots}[t], i) = A_t[i]$ for every version $t$ and every $i \in [0, n)$. GET takes $O(\log n)$ time, each UPDATE takes $O(\log n)$ time and adds at most $\lceil \lg n \rceil + 1$ nodes, and after $m$ versions the structure holds at most $2n - 1 + (m - 1)(\lceil \lg n \rceil + 1)$ nodes.

Proof. By induction on the number of updates. Version 0 satisfies the invariant by Lemma 1. Suppose it holds for versions $0, \ldots, m - 1$, and UPDATE$(t, i, x)$ creates version $m$, defined by $A_m[i] = x$ and $A_m[j] = A_t[j]$ for $j \ne i$. By Lemma 3, the new root $v'$ of line L13 satisfies $\text{val}(v', i) = x = A_m[i]$ and $\text{val}(v', j) = \text{val}(\text{roots}[t], j) = A_t[j] = A_m[j]$ for $j \ne i$. No existing node changed, so for every older version $s$, the leaves reached from $\text{roots}[s]$ hold the same values as before, and the invariant still holds for $s$. Lemma 2 then gives the claim about GET. The time and the node counts follow from Lemmas 1 to 3, since every line does $O(1)$ work besides the recursive calls. $\blacksquare$