Proofs: Graph-structured stack

The graph-structured stack represents a splice-closed set of stacks, and POP returns exactly the paths it must full

This proof shows: correctness.

Setting. The graph $G$ has nodes, each with a key $(s, j)$ and a level $\mathrm{level}(v) = j$, and directed edges $v \to x$ with labels. The root is the node of $(q_0, 0)$. A path from $v$ is a sequence of nodes $v = y_0, y_1, \ldots, y_d$ with an edge $y_{i-1} \to y_i$ for each $i$. Nodes and edges may repeat. A stack of $G$ is a path from some node to the root, written in reverse, from the root up; $\mathrm{Paths}(G)$ is the set of these. For two sequences, juxtaposition means concatenation. We consider a GSS that starts with the root alone, and that is changed only by PUSH. The abstract set $\mathcal{S}$ starts as $\{(\mathrm{root})\}$. The call $\mathrm{PUSH}(s, j, x)$, with $v$ the node of $(s, j)$, replaces $\mathcal{S}$ by $\mathcal{S}'$, the least set of sequences that (a) contains $\mathcal{S}$, (b) contains $\sigma v$ for every $\sigma \in \mathcal{S}'$ whose last cell is $x$, and (c) is closed under splicing: if $\sigma_1 c \sigma_2$ and $\tau_1 c \tau_2$ are in $\mathcal{S}'$, so is $\tau_1 c \sigma_2$.

Invariants. (I1) no two nodes have the same key; (I2) $\mathrm{level}(x) \le \mathrm{level}(v)$ for every edge $v \to x$; (I3) every node has a path to the root; (I4) $\mathrm{Paths}(G) = \mathcal{S}$.

Lemma 1. $\mathrm{Paths}(G)$ is closed under splicing for every graph $G$.

Proof. Let $\sigma_1 c \sigma_2$ and $\tau_1 c \tau_2$ be stacks of $G$. Read from the top down, $\tau_1 c$ in reverse is a path from $c$ to the root, and $c \sigma_2$ in reverse is a path from the top of $\sigma_2$ (or from $c$) to $c$. Joining them at $c$ gives a path to the root, which read from the root up is $\tau_1 c \sigma_2$. $\square$

Lemma 2. The invariants hold initially and after each call of PUSH.

Proof. Initially $G$ has only the root and no edges, so (I1), (I2) and (I3) hold, and $\mathrm{Paths}(G) = \{(\mathrm{root})\} = \mathcal{S}$.

Consider $\mathrm{PUSH}(s, j, x)$ on a graph $G$ that satisfies the invariants, and let $G'$ be the graph after it. Line L1 ensures $\mathrm{level}(x) \le j$, and otherwise the call fails and changes nothing. NODE (lines L5 and L6) returns the node with key $(s, j)$ if there is one, and makes one only if there is none, so (I1) holds. ADD-EDGE (lines L7 and L8) adds at most the edge $v \to x$, with $\mathrm{level}(x) \le j = \mathrm{level}(v)$, so (I2) holds. After the call, $v$ has the edge to $x$, and $x$ has a path to the root in $G$ by (I3), so $v$ has one in $G'$; the other nodes keep their paths, so (I3) holds.

For (I4), if the edge $v \to x$ was already in $G$, then $G' = G$ as a graph, so $\mathrm{Paths}(G') = \mathrm{Paths}(G) = \mathcal{S}$. This set already satisfies (a), and (c) by Lemma 1, and (b) because every stack $\sigma$ of $G$ ending at $x$ extends by the edge $v \to x$ to the stack $\sigma v$. So $\mathcal{S}' = \mathcal{S}$, as $\mathcal{S}'$ is the least such set. Now let the edge be new.

($\mathcal{S}' \subseteq \mathrm{Paths}(G')$.) $\mathrm{Paths}(G')$ contains $\mathrm{Paths}(G) = \mathcal{S}$, because $G'$ has all the edges of $G$. It satisfies (b), because a stack $\sigma$ of $G'$ that ends at $x$ extends by the edge $v \to x$. It satisfies (c) by Lemma 1. Since $\mathcal{S}'$ is the least set with (a), (b) and (c), $\mathcal{S}' \subseteq \mathrm{Paths}(G')$.

($\mathrm{Paths}(G') \subseteq \mathcal{S}'$.) Let $\pi$ be a stack of $G'$, and let $k$ be the number of times it uses the new edge, as a step from $x$ up to $v$. We show $\pi \in \mathcal{S}'$ by induction on $k$. If $k = 0$, $\pi$ is a stack of $G$, so $\pi \in \mathcal{S} \subseteq \mathcal{S}'$. If $k > 0$, split $\pi$ at its last use of the new edge: $\pi = \alpha v \beta$, where $\alpha$ ends at $x$ and $\beta$, the part above this occurrence of $v$, does not use the new edge. The stack $\alpha$ uses the new edge $k - 1$ times, so $\alpha \in \mathcal{S}'$ by induction, and $\alpha v \in \mathcal{S}'$ by (b). If $\beta$ is empty, we are done. Otherwise the first node of $\beta$ has an edge to $v$ in $G$, because $\beta$ does not use the new edge, so $v$ is a node of $G$, and by (I3) for $G$ it has a path to the root in $G$. Let $\rho$ be this stack, which ends at $v$. Then $\rho \beta$ is a stack of $G$: below $v$ it follows $\rho$, and above $v$ it follows $\beta$, which uses only edges of $G$. So $\rho \beta \in \mathcal{S} \subseteq \mathcal{S}'$. Splicing $\rho \beta$ and $\alpha v$ at the cell $v$ by (c) gives $\alpha v \beta = \pi \in \mathcal{S}'$. $\square$

Lemma 3 (POP). $\mathrm{POP}(u, m, e)$ terminates and returns, once for each path $u = y_0, y_1, \ldots, y_m$ of $m$ edges from $u$ that contains the edge $e$ as a step (or for each such path, if $e$ is none), the pair of its end node $y_m$ and its labels in the order $\ell(y_{m-1} \to y_m), \ldots, \ell(y_0 \to y_1)$, bottom first.

Proof. Call an entry $(y, d, \mathit{used}, \mathit{labels})$ of $T$ the representative of a path $y_0, \ldots, y_d$ from $u$ when $y = y_d$, $\mathit{labels}$ lists the labels of its edges from the top down, and $\mathit{used}$ is true exactly when $e$ is none or the path contains $e$. Line L9 puts on $T$ the representative of the path of length 0. Line L14 replaces the representative of a path $P$ of length $d < m$ by the representatives of all extensions of $P$ by one edge, one for each out-edge of $y_d$: the new flag is true exactly when $P$ used $e$ or the new edge is $e$. Each entry is removed once at line L11. So, ignoring line L13, the entries that pass through $T$ are the representatives of the paths from $u$ of length at most $m$, each once, since two different paths differ at a first step and the two extensions there are different entries. The number of these paths is finite, since every node has finitely many out-edges, so the loop ends.

Line L13 discards the representative of a path $P$ only if $P$ has not used $e = y_0' \to x_0'$ and $\mathrm{level}(y_d) < \mathrm{level}(y_0')$. Every extension of $P$ moves from $y_d$ along edges, which by (I2) never increase the level, so all nodes after $y_d$ have level less than $\mathrm{level}(y_0')$. None of them is $y_0'$, so no extension takes the step $e$, and no extension of length $m$ would be returned. When $e$ is none, the floor is 0 and no level is below it, so line L13 discards nothing. Hence the entries with $d = m$ that reach line L12 include the representatives of all paths of length $m$ that use $e$ (or of all paths of length $m$), and line L12 returns exactly those with the flag true, each with its labels reversed into bottom-first order. $\square$

Theorem. In a GSS changed only by PUSH, after every operation the stacks of the graph are exactly the abstract set $\mathcal{S}$. $\mathrm{POP}(u, m, e)$ returns, for each stack of $\mathcal{S}$ with top $u$ and at least $m + 1$ cells that takes the step $e$ in its top $m$ steps (or for each such stack, if $e$ is none), the cell that becomes the top when its top $m$ cells are removed, together with the labels of the removed steps; it returns each such pair once for each different top segment of $m$ steps.

Proof. The first part is Lemma 2 (I4); POP and tops do not change the graph. For the second part, the top $m$ steps of a stack of $\mathcal{S}$ with top $u$ are, read from the top down, a path of $m$ edges from $u$. Conversely, by (I3) every path of $m$ edges from $u$ to a node $y$ extends below $y$ to a stack of $\mathcal{S}$. So the top segments of $m$ steps of the stacks with top $u$ are exactly the paths of $m$ edges from $u$, and Lemma 3 gives the result. $\blacksquare$