Proofs: Shift-reduce parsing

The shift-reduce driver builds a reverse rightmost derivation, and the exact decision procedure parses every grammar full

This proof shows: correctness, termination.

We use the pseudocode SHIFT-REDUCE of the page and the notation of the context-free grammar page. The input is $w = a_1 \cdots a_n$. A configuration is the stack, a sequence of trees $t_1, \ldots, t_m$ with roots $X_1, \ldots, X_m$, together with pos. A legal move is a shift (if $pos \le n$) or a reduction by a production $A \to \beta$ whose right side $\beta$ is the sequence of the top $|\beta|$ roots. The augmented grammar adds a new start symbol $S'$ and the production $S' \to S$.

Claim 1: whatever DECIDE does, an accepted tree is right

Invariant. After every move, (i) the leaves of $t_1, \ldots, t_m$, left to right, are $a_1 \cdots a_{pos-1}$; (ii) each $t_i$ is a parse tree with root $X_i$; (iii) if $p_1, \ldots, p_r$ are the productions of the reductions so far, then applying $p_r, p_{r-1}, \ldots, p_1$ to $X_1 \cdots X_m\, a_{pos} \cdots a_n$, each to the rightmost nonterminal, gives a rightmost derivation $X_1 \cdots X_m\, a_{pos} \cdots a_n \Rightarrow^*_{rm} w$.

Proof. At the start the stack is empty, pos is 1, and the derivation of $w$ from $w$ has no step. A shift appends the leaf $a_{pos}$ and increases pos, which changes neither the string $X_1 \cdots X_m\, a_{pos} \cdots a_n$ nor the derivation. A reduction by $A \to \beta$ replaces the top trees, whose roots spell $\beta$, by a node $A$ over them, which keeps (i) and (ii). The string becomes $\alpha A\, a_{pos} \cdots a_n$, where $\alpha$ is the rest of the stack, and $\alpha A\, a_{pos} \cdots a_n \Rightarrow \alpha \beta\, a_{pos} \cdots a_n$ rewrites $A$, which is the rightmost nonterminal because everything after it is terminal. So this step, followed by the old derivation, is a rightmost derivation, which is (iii). $\square$

When the driver accepts, the stack is the single tree with root $S$ and pos is $n + 1$, so by (i) and (ii) it is a parse tree of $w$, and by (iii) the reductions read backwards are a rightmost derivation $S \Rightarrow^*_{rm} w$.

Goodness and item chains

A configuration is good if some sequence of legal moves leads from it to the stack $S$ with pos $= n + 1$. Legal moves depend only on the roots, so goodness depends only on $X_1 \cdots X_m$ and pos.

Lemma 2. The configuration with roots $\gamma = X_1 \cdots X_m$ at position pos is good if and only if there are productions $S' \to \beta_1 A_2 \delta_1$, $A_2 \to \beta_2 A_3 \delta_2$, ..., $A_{k-1} \to \beta_{k-1} A_k \delta_{k-1}$ and $A_k \to \beta_k \delta_k$ of the augmented grammar such that $\gamma = \beta_1 \beta_2 \cdots \beta_k$ and $\delta_k \delta_{k-1} \cdots \delta_1 \Rightarrow^* a_{pos} \cdots a_n$.

Proof. (Only if.) Take a sequence of moves that ends in acceptance, and let $T$ be the final tree, with a root $S'$ added above $S$. The current trees $t_1, \ldots, t_m$ are subtrees of $T$, because later moves only put new nodes above them; call them old, and call the nodes made by later reductions new. A new node is pushed on top of the stack, to the right of every old tree still there, so in the order of children, old trees always come before new nodes that contain no old tree. Hence the children of a new node are: some old trees, then at most one new node that contains old trees, then new nodes and future leaves that contain no old tree. Start at the root $S'$ and walk down: at a new node with production $A_j \to \beta_j A_{j+1} \delta_j$, $\beta_j$ are the roots of its old children, $A_{j+1}$ is the child that contains old trees, and $\delta_j$ are the rest; stop at the first node that has no child containing old trees, with production $A_k \to \beta_k \delta_k$. The $\beta$'s are all the old trees, in order, so their concatenation is $\gamma$. The trees of the $\delta$'s cover the leaves $a_{pos} \cdots a_n$, from the deepest node up, so $\delta_k \cdots \delta_1 \Rightarrow^* a_{pos} \cdots a_n$. (If the stack is already $S$ at $pos = n + 1$, take $k = 1$, $\beta_1 = S$, $\delta_1 = \varepsilon$.)

(If.) Split $a_{pos} \cdots a_n$ into parts derived by the symbols of $\delta_k, \ldots, \delta_1$ and choose a parse tree for each part. Build $T$ from the bottom: a node $A_k$ over the old trees of $\beta_k$ and the trees of $\delta_k$, then a node $A_{k-1}$ over the old trees of $\beta_{k-1}$, the node $A_k$ and the trees of $\delta_{k-1}$, and so on up to $S'$. Then $T$ is a parse tree of $w$ that contains $t_1, \ldots, t_m$, and its new nodes are the nodes on the chain and the nodes of the $\delta$ trees. Do the moves of the postorder of the new nodes and future leaves: shift each future leaf when it comes, and reduce each new node when it comes. By induction along the postorder, when a node comes, all its children are finished and are the top entries of the stack in order, since everything later in the postorder is to their right. So each move is legal, and the last one makes the node $S$ over everything, at pos $n + 1$. $\square$

The implementation tests the condition of Lemma 2 by running the items of the chains over $\gamma$. It keeps pairs (item $[A \to \beta \cdot \delta]$, $e$), where $e$ is the position where the continuations of the ancestors, $\delta_{j-1} \cdots \delta_1$, must start to derive $a_e \cdots a_n$. Reading a symbol $X$ moves the dot over $X$; at an item $[A \to \beta \cdot B \delta]$ with end $e$, the pairs $([B \to \cdot \eta], e')$ are added for every $e'$ with $\delta \Rightarrow^* a_{e'} \cdots a_{e-1}$. The configuration is good when some pair $([A \to \beta \cdot \delta], e)$ after $\gamma$ has $\delta \Rightarrow^* a_{pos} \cdots a_{e-1}$. The relation $\Rightarrow^*$ on substrings is computed once by a least fixpoint.

Claim 2: the exact procedure accepts exactly $L(G)$ and stops

Lemma 3. From a good configuration that is not an acceptance, the procedure returns a legal move to a good configuration, and the number of moves before the next shift or acceptance is finite.

Proof. Fix an accepting continuation $c_0, c_1, \ldots$ from the current configuration $c_0$. Every $c_i$ is good. Let $c_j$ be the configuration just before its first shift, or its final acceptance; the moves $c_0 \to \cdots \to c_j$ are good reductions, and $c_j$ is a target: shifting from it is good, or it is the acceptance. If $c_0$ is a target the procedure shifts or accepts. Otherwise the breadth-first search over good reductions from $c_0$ explores level by level, each stack has at most $|P|$ reductions, and a target lies at depth at most $j$; so the search stops, and returns the first move of a shortest path to a target, which leads to a good configuration. Let $d(c)$ be the length of a shortest path of good reductions from $c$ to a target. The move goes along a shortest path, so $d$ decreases by one at each reduction. When $d = 0$ the procedure shifts or accepts. $\square$

Theorem. With the exact procedure, the driver accepts if and only if $w \in L(G)$, and it always stops.

Proof. The start configuration, empty stack at pos 1, is good exactly when $w \in L(G)$: by Lemma 2 with $\gamma = \varepsilon$, the condition reads $S \Rightarrow^* w$. If it is not good, the procedure reports an error at once. If it is good, by Lemma 3 every move keeps the configuration good, there are at most $n$ shifts, and between two shifts there are finitely many reductions, so the run reaches the acceptance; by Claim 1 the returned tree is a parse tree of $w$. $\square$