Proofs: Binary random-access list

The binary random-access list keeps its invariant and implements a persistent list full

This proof shows: correctness, termination.

We use the pseudocode and the invariant (B1) to (B3) of the page. For a leaf tree $t$, $\text{seq}(t)$ is the sequence of the items of its leaves from left to right, and $\text{size}(t) = |\text{seq}(t)|$. For a digit list $L = d_0, \ldots, d_{\ell-1}$, $\text{seq}(L)$ is the concatenation of $\text{seq}(t)$ over the One digits $d_k = \text{One } t$ in increasing order of $k$. We say that a digit list $L$ is valid from rank $j$ if each $d_k = \text{One } t$ of $L$ has $t$ complete of rank $j + k$, and its last digit, if any, is a One. A list is valid when it is valid from rank 0; this is (B1) and (B2), and (B3) is the definition of $\text{seq}(L)$.

The facts about trees that we use: if $t_1$ and $t_2$ are complete of rank $k$, then LINK$(t_1, t_2)$ is complete of rank $k + 1$ and has sequence $\text{seq}(t_1) \cdot \text{seq}(t_2)$; and a complete tree $\text{node}(w, t_1, t_2)$ of rank $k + 1 \ge 1$ has children complete of rank $k$, with $w = 2^{k+1}$ and $\text{seq} = \text{seq}(t_1) \cdot \text{seq}(t_2)$. Both follow from the definitions.

Lemma 1 (CONS-TREE). If $L$ is valid from rank $j$ and $t$ is complete of rank $j$, then CONS-TREE$(t, L)$ terminates and returns a list $L'$ that is valid from rank $j$ with $\text{seq}(L') = \text{seq}(t) \cdot \text{seq}(L)$.

Proof. By induction on the length of $L$. If $L$ is empty (line L2), $L' = \langle \text{One } t \rangle$, valid from rank $j$, with sequence $\text{seq}(t)$. If $d_0 = \text{Zero}$ (line L3), $L'$ replaces it by One $t$, of rank $j$; the other digits and the last digit are unchanged (the last digit is not $d_0$, since a valid list does not end in Zero), and the new first tree comes before all others, so $\text{seq}(L') = \text{seq}(t) \cdot \text{seq}(L)$. If $d_0 = \text{One } u$ (lines L4 and L5), $u$ has rank $j$, so LINK$(t, u)$ is complete of rank $j + 1$ with sequence $\text{seq}(t) \cdot \text{seq}(u)$. The rest of $L$ is valid from rank $j + 1$ (it is empty or ends in a One) and is shorter, so by the hypothesis the recursive call returns $L''$ valid from rank $j + 1$ with $\text{seq}(L'') = \text{seq}(t) \cdot \text{seq}(u) \cdot \text{seq}(\text{rest}(L))$. Then $L' = \text{Zero} :: L''$ is valid from rank $j$, since $L''$ is non-empty and ends in a One, and $\text{seq}(L') = \text{seq}(L'') = \text{seq}(t) \cdot \text{seq}(L)$. $\square$

Lemma 2 (UNCONS-TREE). If $L$ is non-empty and valid from rank $j$, then UNCONS-TREE$(L)$ terminates and returns $(t, L')$ where $t$ is complete of rank $j$, $L'$ is valid from rank $j$, and $\text{seq}(t) \cdot \text{seq}(L') = \text{seq}(L)$.

Proof. By induction on the length of $L$. If $L = \langle \text{One } t \rangle$ (line L7), $t$ has rank $j$ and $L' = \langle\rangle$. If $d_0 = \text{One } t$ and $L$ has more digits (line L8), then $L' = \text{Zero} :: \text{rest}(L)$, whose last digit is the last digit of $L$, a One; so $L'$ is valid from rank $j$, and $\text{seq}(t) \cdot \text{seq}(L') = \text{seq}(L)$. If $d_0 = \text{Zero}$ (line L9), then $\text{rest}(L)$ is non-empty, because a valid list does not end in Zero, and it is valid from rank $j + 1$. By the hypothesis, the call returns a tree $u$ complete of rank $j + 1 \ge 1$, so $u = \text{node}(w, t_1, t_2)$ with $t_1$ and $t_2$ complete of rank $j$, and a list $L''$ valid from rank $j + 1$ with $\text{seq}(u) \cdot \text{seq}(L'') = \text{seq}(\text{rest}(L)) = \text{seq}(L)$. Line L10 returns $t_1$ and $L' = \text{One } t_2 :: L''$, which is valid from rank $j$ (if $L''$ is empty its last digit is One $t_2$), and $\text{seq}(t_1) \cdot \text{seq}(L') = \text{seq}(t_1) \cdot \text{seq}(t_2) \cdot \text{seq}(L'') = \text{seq}(L)$. $\square$

Lemma 3 (CONS, HEAD, TAIL). Let $L$ be valid with $\text{seq}(L) = \langle x_0, \ldots, x_{n-1} \rangle$. CONS$(x, L)$ is valid with sequence $\langle x, x_0, \ldots, x_{n-1} \rangle$. If $n \ge 1$, HEAD$(L) = x_0$ and TAIL$(L)$ is valid with sequence $\langle x_1, \ldots, x_{n-1} \rangle$. If $n = 0$, both report an error.

Proof. A leaf is complete of rank 0, so Lemma 1 with $j = 0$ gives the claim for CONS. A valid list is empty exactly when $n = 0$, since every One digit holds at least one item; then line L6 reports the error. Otherwise, by Lemma 2 with $j = 0$, UNCONS-TREE returns a tree of rank 0, which is a leaf $\text{leaf}(y)$, and a valid $L'$ with $\langle y \rangle \cdot \text{seq}(L') = \text{seq}(L)$. So $y = x_0$ and $\text{seq}(L') = \langle x_1, \ldots, x_{n-1} \rangle$. $\square$

Lemma 4 (LOOKUP). If $L$ is valid with $\text{seq}(L) = \langle x_0, \ldots, x_{n-1} \rangle$, then LOOKUP$(i, L)$ returns $x_i$ for $0 \le i < n$ and reports an error for $i \ge n$.

Proof. Let the One digits of $L$ hold the trees $u_1, u_2, \ldots, u_r$ in digit order, and let $s_q = \sum_{p < q} \text{size}(u_p)$. The loop of line L13 keeps this invariant: before the digits of $u_q$ are examined, the variable $i$ equals $i_0 - s_q$, where $i_0$ is the input index, and $i_0 \ge s_q$. It holds at the start ($s_1 = 0$). Zero digits change nothing. At the digit of $u_q$, if $i < \text{size}(u_q)$, then $s_q \le i_0 < s_{q+1}$, so $x_{i_0}$ is the item of index $i$ in $\text{seq}(u_q)$, and the descent starts. Otherwise line L19 subtracts $\text{size}(u_q)$, which gives $i_0 - s_{q+1}$ with $i_0 \ge s_{q+1}$, and the invariant holds for $u_{q+1}$. If the loop ends, $i_0 \ge s_{r+1} = n$, and line L20 reports the error correctly.

The descent of lines L16 to L18 keeps the invariant "the wanted item is the item of index $i$ in $\text{seq}(t)$, and $0 \le i < \text{size}(t)$". At a node $\text{node}(w, t_1, t_2)$ with $\text{size}(t_1) = w/2$, the item of index $i$ is in $t_1$ at index $i$ if $i < w/2$, and in $t_2$ at index $i - w/2$ otherwise, which is line L17. Each step goes one level down, so the loop stops after at most the rank of the tree, at a leaf with $i = 0$, whose item is the wanted one. $\square$

Lemma 5 (UPDATE). If $L$ is valid with $\text{seq}(L) = \langle x_0, \ldots, x_{n-1} \rangle$ and $0 \le i < n$, then UPDATE$(i, y, L)$ returns a valid list whose sequence is that of $L$ with $x_i$ replaced by $y$.

Proof. UPDATE-TREE$(i, y, t)$, for $t$ complete and $0 \le i < \text{size}(t)$, returns a tree of the same shape with the item of index $i$ replaced by $y$: by induction on the rank, a leaf has $i = 0$ (line L25), and at a node the same case split as in Lemma 4 sends the change to the correct child and keeps the other child and $w$ (lines L27 and L28). UPDATE then follows the same walk over the digits as LOOKUP, with the same invariant on $i$, and rebuilds the digit cells before the changed tree with the same digits (lines L21 and L24) and the changed tree in the same place (line L23). Ranks, the last digit and the order of the trees do not change, so the result is valid, and its sequence differs only at position $i$. The precondition $i < n$ means that line L23 is reached before the list ends. $\square$

Persistence. No line assigns to a field of an existing digit cell or tree node: lines L2, L3, L5, L7, L8, L10, L21, L23, L24, L27 and L28 build new cells and nodes, and share old ones only as children. So every list built earlier keeps its digits, trees and sequence.

Theorem. Every list built from the empty list by CONS, TAIL and UPDATE, applied to any earlier versions, is valid, and each operation returns the result that the persistent list type specifies. Each operation terminates.

Proof. The empty list is valid. By persistence, an earlier version is still valid when it is used again. Lemmas 3, 4 and 5 give the results and the validity of the new versions. Termination: CONS-TREE and UNCONS-TREE recurse on a shorter digit list, the loops of LOOKUP run over a finite digit list and down a finite tree, and UPDATE and UPDATE-TREE recurse on a shorter digit list or a lower rank. $\blacksquare$