Proofs: Banker's queue

The banker's queue takes O(1) amortized time per operation, also under persistent use full

This proof shows: time.amortized.

We count one unit for each step of $O(1)$ work. The unshared cost of an operation is the work it does outside the forcing of suspensions: it is $O(1)$ for each of EMPTY, SNOC, HEAD, TAIL and CHECK, since line L9 only builds two suspensions. The shared cost is the work done when a suspension runs for the first time. Memoization means that each suspension runs at most once in the whole execution, whatever the number of versions that force it.

Costs of the suspensions. A rotation of a front $F$ of length $m$ and a rear $R$ of length $m + 1$ makes the stream $F ⧺ \text{REVERSE}(R)$. Its cells are suspensions made one by one: the cell of index $j < m$ does $O(1)$ own work (it forces cell $j$ of $F$, which is a suspension of an older stream with its own debits, and builds the next suspension of the concatenation). The cell of index $m$ forces the end of $F$, then runs REVERSE$(R)$, which does $m + 1$ steps, and returns its first cell. The cells after index $m$ were built by REVERSE and cost nothing more. We give each suspension debits equal to its own work, in units: the cell $j < m$ gets 1 debit and the cell $m$ gets $m + 2$ debits (one for its own step and $m + 1$ for REVERSE). All debits of a stream are attached to it when the rotation creates it, even to cells that are built later.

The accounting rule. Each operation may discharge some debits of the version it acts on. The record of discharged debits belongs to a version: the new version inherits the record of its argument and adds the debits that the operation discharges. The rule is that a suspension may be forced by an operation on a version $Q$ only when, in the record of $Q$, all debits of that suspension are discharged. The amortized cost of an operation is its unshared cost plus the number of debits it discharges.

Lemma 1 (the rule bounds the total). If the rule holds in an execution, the total actual cost of the execution is at most the sum of the amortized costs of its operations.

Proof. The total actual cost is the sum of the unshared costs plus, for each suspension $s$ that runs, its own work $c(s)$. Take a suspension $s$ that runs, and the operation that first forces it, on a version $Q$. By the rule, all $c(s)$ debits of $s$ are discharged in the record of $Q$. Each entry of that record was added by one operation in the history of $Q$, and that operation counted it in its amortized cost. Distinct suspensions have distinct debits, so these discharge events are distinct for distinct $s$. So $\sum_s c(s)$ is at most the total number of discharges, and the total actual cost is at most the sum of the amortized costs. The same debit may be discharged in several histories; that only makes the bound larger, not wrong. $\square$

The debit invariant. For a version with front $F$ of length $\ell_f$ and rear length $\ell_r$, let $d(j)$ be the number of debits on cell $j$ of $F$ that are not yet discharged in its record, and $D(i) = \sum_{j=0}^{i} d(j)$. The invariant is

Each operation discharges the earliest debits first: to discharge $k$ debits, take them from the cell of least index with a debit left, then the next one, and so on. If $k$ is more than the debits left, all of them are discharged. After discharging $k$ debits in this way, the new prefix sums are $D'(i) = \max(0, D(i) - k)$.

Lemma 2. SNOC discharges 1 debit, or 2 if it makes a rotation, and TAIL discharges 2 debits. Then (D) holds for every version.

Proof. EMPTY has no cells, so (D) holds. Assume (D) for the argument $Q$.

Snoc without a rotation. The front is the same and $\ell_r$ grows by 1, so the bound $\ell_f - \ell_r$ falls by 1 and $2i$ does not change. After the discharge of 1 debit, $D'(i) = \max(0, D(i) - 1)$. If $D(i) \ge 1$ then $D'(i) \le \min(2i, \ell_f - \ell_r) - 1 \le \min(2i, \ell_f - \ell_r - 1)$. If $D(i) = 0$ then $D'(i) = 0$, and $0 \le 2i$ and $0 \le \ell_f - (\ell_r + 1)$ because no rotation means $\ell_r + 1 \le \ell_f$.

Tail without a rotation. The new front is $F$ without cell 0, so the new cell $i$ is the old cell $i + 1$, and $d(0) = 0$ by (D) at $i = 0$. The new prefix sums before the discharge are $E(i) = D(i + 1)$, and $D(i + 1) \le \min(2i + 2, \ell_f - \ell_r)$. The new bound is $\min(2i, (\ell_f - 1) - \ell_r)$, which is at least $\min(2i + 2, \ell_f - \ell_r) - 2$. After the discharge of 2 debits, if $E(i) \ge 2$ then $E(i) - 2$ is within the new bound; if $E(i) < 2$ then the new prefix sum is 0, and $0 \le \min(2i, \ell_f - 1 - \ell_r)$ because no rotation means $\ell_r \le \ell_f - 1$.

An operation with a rotation. A rotation happens when, after the update of the lengths, $\ell_r = \ell_f + 1$. For a snoc this means $\ell_r = \ell_f$ in $Q$; for a tail it means $\ell_r = \ell_f$ in $Q$ as well, since the tail lowers $\ell_f$ by 1. In both cases (D) for $Q$ gives $D(i) \le \ell_f - \ell_r = 0$ for every $i$, so every cell of the front of $Q$ is free of debits, and so is every cell of the shorter front after a tail. The new version has the new stream of length $2m + 1$, where $m$ is the length of the old front after the operation, and $\ell_r = 0$. Its only debits are those of the rotation: $D(i) = i + 1$ for $i < m$ and $D(i) = 2m + 2$ for $m \le i \le 2m$. After the discharge of 2 debits, $D'(i) = \max(0, i - 1) \le 2i$ for $i < m$, and $D'(i) \le 2m + 1 = \ell_f - \ell_r$ for all $i$. For $i \ge m$, $D'(i) = 2m \le 2i$. So (D) holds. (When $m = 0$ the stream has one cell with 2 debits, and both are discharged.)

HEAD does not change the version, so (D) still holds for it. $\square$

Lemma 3. The accounting rule holds.

Proof. HEAD and TAIL force only the first cell of the front of their argument. By (D) at $i = 0$, $D(0) \le 0$, so that cell has no debits left. Forcing cell 0 of a rotated stream forces cell 0 of its inner front $F$, which had no debits at the rotation (proof of Lemma 2), and the cell $m$ forces the end of $F$ and REVERSE, whose debits are on cell $m$ itself. A cell of index $j > 0$ of a stream is forced only when it has become cell 0 of the front of some version, after the $j$ tails that removed the cells before it; then (D) for that version applies to it. No other operation forces a suspension. $\square$

Theorem. Any sequence of $k$ operations on a banker's queue, applied to any versions in any order, takes $O(k)$ time in total. So each operation takes $O(1)$ amortized time, also under persistent use.

Proof. Each operation has $O(1)$ unshared cost and discharges at most 2 debits, so its amortized cost is $O(1)$. By Lemma 3 the accounting rule holds, and by Lemma 1 the total actual cost is at most the sum of the amortized costs, which is $O(k)$. $\blacksquare$

The banker's queue keeps its invariant and implements a persistent queue full

This proof shows: correctness.

We use the pseudocode of the page. A stream denotes the finite sequence of the items of its cells; forcing a suspension does not change what it denotes, only whether its value is stored. For a list $R$, $\text{rev}(R)$ is its reverse, and $\cdot$ is concatenation of sequences. For a queue $Q = (\ell_f, F, \ell_r, R)$ let

A tuple is valid if $\ell_f = |F|$, $\ell_r = |R|$ and $\ell_r \le \ell_f$.

Lemma 1 (CHECK). Let $(\ell_f, F, \ell_r, R)$ satisfy $\ell_f = |F|$, $\ell_r = |R|$ and $\ell_r \le \ell_f + 1$. Then CHECK returns a valid tuple $Q'$ with $\text{seq}(Q') = F \cdot \text{rev}(R)$.

Proof. If $\ell_r \le \ell_f$, line L8 returns the same tuple, which is then valid, and the sequence is the same. Otherwise $\ell_r = \ell_f + 1$, and line L9 returns $(\ell_f + \ell_r, F ⧺ \text{REVERSE}(R), 0, \langle\rangle)$. The lazy concatenation $F ⧺ G$ denotes $F \cdot G$ (by induction on $|F|$: if $F$ is empty its value is the value of $G$, and otherwise its first cell holds the first item of $F$ and its rest is the concatenation of the rest of $F$ with $G$). REVERSE$(R)$ denotes $\text{rev}(R)$. So the new front denotes $F \cdot \text{rev}(R)$, its length is $|F| + |R| = \ell_f + \ell_r$, the new rear is empty with length 0, and $0 \le \ell_f + \ell_r$. The tuple is valid, and its sequence is $F \cdot \text{rev}(R) \cdot \text{rev}(\langle\rangle) = F \cdot \text{rev}(R)$. $\square$

Lemma 2 (operations). Let $Q$ be valid with $\text{seq}(Q) = \langle x_1, \ldots, x_n \rangle$.

1. EMPTY returns a valid tuple with sequence $\langle\rangle$.
2. SNOC$(Q, x)$ returns a valid tuple with sequence $\langle x_1, \ldots, x_n, x \rangle$.
3. If $n = 0$, HEAD and TAIL report an error. If $n \ge 1$, HEAD$(Q)$ returns $x_1$, and TAIL$(Q)$ returns a valid tuple with sequence $\langle x_2, \ldots, x_n \rangle$.

Proof. (1) Line L1 returns $(0, \langle\rangle, 0, \langle\rangle)$, which is valid with the empty sequence.

(2) Line L3 calls CHECK on $(\ell_f, F, \ell_r + 1, \text{cons}(x, R))$. Here $|\text{cons}(x, R)| = \ell_r + 1$ and $\ell_r + 1 \le \ell_f + 1$, so Lemma 1 applies, and the result is valid with sequence $F \cdot \text{rev}(\text{cons}(x, R)) = F \cdot \text{rev}(R) \cdot \langle x \rangle = \langle x_1, \ldots, x_n, x \rangle$.

(3) Since $Q$ is valid, $n = \ell_f + \ell_r \le 2\ell_f$, so $\ell_f = 0$ if and only if $n = 0$. If $n = 0$, lines L4 and L6 report the error. If $n \ge 1$, then $\ell_f \ge 1$, so $F$ is non-empty and its first item is the first item of $F \cdot \text{rev}(R)$, which is $x_1$; line L5 returns it. In line L7 the rest $F'$ of $F$ has $|F'| = \ell_f - 1$ and $F = \langle x_1 \rangle \cdot F'$. The arguments of CHECK satisfy $\ell_r \le \ell_f = (\ell_f - 1) + 1$, so by Lemma 1 the result is valid with sequence $F' \cdot \text{rev}(R) = \langle x_2, \ldots, x_n \rangle$. $\square$

Lemma 3 (no old version changes). No operation changes the sequence of a tuple that existed before it.

Proof. The operations create new tuples, new list cells (line L3) and new suspensions (line L9). They never assign to a field of an existing tuple, cell or suspension. The only change to existing objects is the memoization of a forced suspension, which stores the value that the suspension denotes and so does not change the sequence of any stream. $\square$

Theorem. Every version that a program builds from EMPTY by SNOC and TAIL, applied to any earlier versions in any order, is valid, and HEAD, TAIL and SNOC act on each version as the persistent queue type specifies.

Proof. By induction on the number of operations performed. EMPTY gives a valid version by Lemma 2(1). Each later operation takes as argument a version that was valid when it was made, and by Lemma 3 it still has the same fields and sequence, so it is still valid. Lemma 2(2) and 2(3) then give the result of the operation and the validity of the new version. $\blacksquare$