Proofs: Catenable deque

The catenable deque operations keep the invariant, compute the right sequences and run in the stated time full

This proof shows: correctness, termination, complexity.

We use the definitions of the page. For an element $x$ of level $k$, $\text{items}(x)$ is $\langle x \rangle$ if $k = 0$, and the concatenation of the items of its children otherwise. For a tuple $t$ of elements, $\text{items}(t)$ is the concatenation of the items of its elements. For a c-deque, $\text{seq}(\text{Shallow}(d)) = \text{items}(d)$ and $\text{seq}(\text{Deep}(f, m, r)) = \text{items}(f) \cdot \text{seq}(m) \cdot \text{items}(r)$. A valid c-deque of level $k$ is a c-deque of level $k$ that satisfies (C1) to (C3). Its depth is the number of Deep levels on its spine: 0 for Shallow, and $1 + \text{depth}(m)$ for $\text{Deep}(f, m, r)$. A valid c-deque is empty exactly when it is $\text{Shallow}()$, because a Deep one has at least 2 elements in its front.

No line of the pseudocode writes into a tuple or a node that exists before the call: every result is a new node whose parts are new or old. So every earlier version keeps its sequence, and it suffices to prove the claims about the results.

Lemma 1 (CONS). If $q$ is a valid c-deque of level $k$ and $x$ an element of level $k$, then CONS$(x, q)$ returns a valid c-deque of level $k$ with sequence $\text{items}(x) \cdot \text{seq}(q)$, after at most $\text{depth}(q) + 1$ calls of CONS.

Proof. By induction on $\text{depth}(q)$. Line L1 returns a Shallow tuple of at most 4 elements. Line L2 returns a Deep c-deque with a front of 2 and a rear of 3 elements and an empty middle, which is valid, and its sequence is $\text{items}(x, a) \cdot \text{items}(b, c, e)$, as required. Otherwise $q = \text{Deep}(f, m, r)$. If $|f| < 4$, line L4 makes a front of 3 or 4 elements. If $f = (a, b, c, e)$, the tuple $(b, c, e)$ is an element of level $k + 1$ by (C1), and $m$ is a valid c-deque of level $k + 1$ of depth $\text{depth}(q) - 1$. By the hypothesis, the call of line L6 returns a valid c-deque $m'$ of level $k + 1$ with $\text{seq}(m') = \text{items}(b, c, e) \cdot \text{seq}(m)$, after at most $\text{depth}(q)$ calls. The new front $(x, a)$ has 2 elements, and the sequence is $\text{items}(x, a) \cdot \text{items}(b, c, e) \cdot \text{seq}(m) \cdot \text{items}(r) = \text{items}(x) \cdot \text{seq}(q)$. $\square$

By symmetry, SNOC$(q, x)$ returns a valid c-deque with sequence $\text{seq}(q) \cdot \text{items}(x)$ after at most $\text{depth}(q) + 1$ calls.

Lemma 2 (HEAD and TAIL). If $q$ is a non-empty valid c-deque of level $k$, then HEAD$(q)$ is an element of level $k$, TAIL$(q)$ is a valid c-deque of level $k$, $\text{items}(\text{HEAD}(q)) \cdot \text{seq}(\text{TAIL}(q)) = \text{seq}(q)$, and TAIL makes at most $\text{depth}(q) + 1$ calls of TAIL.

Proof. By induction on $\text{depth}(q)$. HEAD returns the first element of $d$ or of $f$. Line L7 drops the first element of a non-empty Shallow tuple. Otherwise $q = \text{Deep}(f, m, r)$ and HEAD$(q)$ is the first element $a$ of $f$. If $|f| > 2$, line L9 leaves a front of 2 or 3 elements. Otherwise $f = (a, b)$ (line L10). If $m$ is not empty, the hypothesis applies to $m$, of smaller depth: $g = \text{HEAD}(m)$ is an element of level $k + 1$, a tuple of 2 or 3 elements of level $k$ by (C1), and TAIL$(m)$ is valid with $\text{items}(g) \cdot \text{seq}(\text{TAIL}(m)) = \text{seq}(m)$. The front $b \cdot g$ of line L11 has 3 or 4 elements, and the sequence of the result is $\text{items}(b) \cdot \text{items}(g) \cdot \text{seq}(\text{TAIL}(m)) \cdot \text{items}(r) = \text{items}(b) \cdot \text{seq}(m) \cdot \text{items}(r)$, which is $\text{seq}(q)$ without $\text{items}(a)$. If $m$ is empty, $\text{seq}(q) = \text{items}(a) \cdot \text{items}(b) \cdot \text{items}(r)$, and $s = b \cdot r$ has $1 + |r|$ elements, from 3 to 5. Line L13 returns it as a Shallow tuple if it has at most 4, and line L14 splits 5 elements into a front of 2 and a rear of 3. In both cases the sequence is $\text{items}(s)$. $\square$

By symmetry, LAST and INIT satisfy the mirror statement.

Lemma 3 (PUSH-FRONT and PUSH-BACK). If $d$ is a tuple of 2 to 4 elements of level $k$ and $m$ a valid c-deque of level $k + 1$, then PUSH-FRONT$(d, m)$ is a valid c-deque of level $k + 1$ with sequence $\text{items}(d) \cdot \text{seq}(m)$, and PUSH-BACK$(m, d)$ is one with sequence $\text{seq}(m) \cdot \text{items}(d)$. Each makes at most two calls of CONS or SNOC at the top, and the c-deques they apply to have depth at most $\text{depth}(m) + 1$.

Proof. If $|d| \le 3$, $d$ is itself an element of level $k + 1$, and line L15 is Lemma 1. If $d = (d_1, d_2, d_3, d_4)$, the pairs $(d_1, d_2)$ and $(d_3, d_4)$ are elements of level $k + 1$, and two uses of Lemma 1 give the sequence $\text{items}(d_1, d_2) \cdot \text{items}(d_3, d_4) \cdot \text{seq}(m)$. A CONS adds at most one Deep level, since only line L2 turns a Shallow c-deque into a Deep one, at the bottom of the spine. PUSH-BACK is symmetric. $\square$

Lemma 4 (FROM-TUPLE). For a tuple $s$ of at most 8 elements of level $k$, FROM-TUPLE$(s)$ is a valid c-deque of level $k$ with sequence $\text{items}(s)$.

Proof. If $|s| \le 4$, it is a Shallow tuple. If $5 \le |s| \le 8$, the front has $\lfloor |s|/2 \rfloor$ and the rear $\lceil |s|/2 \rceil$ elements, both between 2 and 4, and the middle is empty. $\square$

Lemma 5 (CAT). If $q_1$ and $q_2$ are valid c-deques of level $k$, then CAT$(q_1, q_2)$ returns a valid c-deque of level $k$ with sequence $\text{seq}(q_1) \cdot \text{seq}(q_2)$.

Proof. By induction on $|\text{seq}(q_1)|$, the number of items in $q_1$. Line L17: $|d_1| + |d_2| \le 8$, so Lemma 4 applies. Lines L18 to L20: $q_2 = \text{Deep}(f_2, m_2, r_2)$. If $|d| = 0$, the result is $q_2$; if $|d| = 1$, it is CONS of the one element onto $q_2$, by Lemma 1. If $2 \le |d| \le 4$, $d$ is a valid front, and by Lemma 3 PUSH-FRONT$(f_2, m_2)$ is a valid c-deque of level $k + 1$ with sequence $\text{items}(f_2) \cdot \text{seq}(m_2)$. The sequence of the result is $\text{items}(d) \cdot \text{items}(f_2) \cdot \text{seq}(m_2) \cdot \text{items}(r_2) = \text{seq}(q_1) \cdot \text{seq}(q_2)$. Lines L21 to L23 are symmetric. Line L24: both are Deep. By Lemma 3, $p_1 = \text{PUSH-BACK}(m_1, r_1)$ and $p_2 = \text{PUSH-FRONT}(f_2, m_2)$ are valid of level $k + 1$, with sequences $\text{seq}(m_1) \cdot \text{items}(r_1)$ and $\text{items}(f_2) \cdot \text{seq}(m_2)$. The c-deque $p_1$ holds the items of $q_1$ except those of $f_1$, and $f_1$ is not empty, so $|\text{seq}(p_1)| < |\text{seq}(q_1)|$, and the hypothesis applies to CAT$(p_1, p_2)$. The result has sequence $\text{items}(f_1) \cdot \text{seq}(m_1) \cdot \text{items}(r_1) \cdot \text{items}(f_2) \cdot \text{seq}(m_2) \cdot \text{items}(r_2)$, which is $\text{seq}(q_1) \cdot \text{seq}(q_2)$. $\square$

The induction also proves that every call terminates: each recursive call of CONS and TAIL is on a c-deque of smaller depth, and each recursive call of CAT is on a first argument with fewer items.

Lemma 6 (depth). A valid c-deque of level 0 with $n \ge 1$ items has depth at most $\lg n - 1$ when it is Deep. More generally, if a valid c-deque of level $k$ with $N$ items is Deep, then $N \ge 2^{k+2}$.

Proof. An element of level $j$ holds at least $2^j$ items, by induction on $j$ with (C1). A Deep c-deque of level $k$ has at least 4 elements of level $k$ in its front and rear, so $N \ge 4 \cdot 2^k$. If a c-deque of level 0 has depth $D \ge 1$, the c-deque at the bottom of its spine of Deep levels is Deep of level $D - 1$ and holds at most $n$ items, so $n \ge 2^{D+1}$. $\square$

Theorem. On valid c-deques with at most $n$ items, CONS, SNOC, TAIL and INIT take $O(\log n)$ time in the worst case, HEAD and LAST $O(1)$, and CAT$(q_1, q_2)$ takes $O\big((1 + \log \min(n_1, n_2)) \cdot (1 + \log(n_1 + n_2))\big)$, where $n_1$ and $n_2$ are the sizes of $q_1$ and $q_2$. Each operation builds $O(1)$ new nodes and tuples of $O(1)$ size per unit of time, so the space of $m$ operations is $O(n_0 + \text{their total time})$.

Proof. Every line except the recursive calls does $O(1)$ work, because tuples have at most 8 elements. By Lemmas 1 and 2, CONS and TAIL make at most $\text{depth}(q) + 1$ calls, which is $O(\log n)$ by Lemma 6. In CAT, consider the call at nesting level $k$ that reaches line L24. Its arguments are valid of level $k$ and hold at most $n_1$ and $n_2$ items, since every recursive argument holds a subset of the items of the argument above it. Both are Deep, so by Lemma 6 $\min(n_1, n_2) \ge 2^{k+2}$, and there are at most $1 + \lg \min(n_1, n_2)$ levels of recursion. Each level does at most four calls of CONS or SNOC, inside PUSH-BACK and PUSH-FRONT, or in lines L19 and L22, on c-deques of at most $n_1 + n_2$ items, each $O(\log(n_1 + n_2))$ by Lemmas 1 and 6. $\blacksquare$