Proofs: LALR(1) parsing

The LALR(1) table is the LR(1) table merged by core, and its driver parses exactly L(G) full

This proof shows: correctness.

We use the pseudocode of the page. $G = (V, \Sigma, P, S)$ is augmented with production 0, $S' \to S$, where $S'$ occurs on no right side. We assume that every nonterminal derives some terminal string. Then $\mathrm{FIRST}(\gamma)$ is not empty for every $\gamma \ne \varepsilon$, and $\mathrm{FIRST}(\beta a) \ne \emptyset$ for every $\beta$ and every terminal or end marker $a$.

LR(1) facts we use. The canonical LR(1) collection has the start state $I_0 = \mathrm{CLOSURE}_1(\{[S' \to \bullet S, \$]\})$ and the transitions $\mathrm{GOTO}_1(J, X) = \mathrm{CLOSURE}_1(\{[A \to \alpha X \bullet \beta, b] : [A \to \alpha \bullet X \beta, b] \in J\})$. We use two standard results of Knuth (1965), also in Section 4.7 of the Dragon book.

• (K1) Validity. $[A \to \alpha \bullet \beta, a] \in \mathrm{GOTO}_1(I_0, \gamma)$ if and only if there is a rightmost derivation $S' \Rightarrow^*_{rm} \delta A a x \Rightarrow_{rm} \delta \alpha \beta a x$ with $\gamma = \delta \alpha$ (where $a x$ is read as $\$$ when $a = \$$).
• (K2) The canonical parser. If the canonical LR(1) table has no conflict, the LR(1) driver (lines L12 to L17 with the canonical table) accepts every $w \in L(G)$ and never meets an empty entry on it. It follows the rightmost derivation of $w$ backwards: for each right sentential form $\gamma y$ of that derivation, with $y \in \Sigma^*$ and the handle ending at the end of $\gamma$, there is a moment at which its stack spells $\gamma$ and the rest of the input is $y$.

The core of a set of LR(1) items is the set of its LR(0) items.

Lemma 1 (cores). For every set $K$ of LR(1) items, $\mathrm{core}(\mathrm{CLOSURE}_1(K)) = \mathrm{CLOSURE}_0(\mathrm{core}(K))$. Hence $\mathrm{core}(\mathrm{GOTO}_1(J, X)) = \mathrm{GOTO}_0(\mathrm{core}(J), X)$, and every canonical LR(1) state reachable from $I_0$ by $\gamma$ has as its core the closure of the LR(0) state reachable from state 0 by $\gamma$.

Proof. Both closures add $B \to \bullet \eta$ for the same items $A \to \alpha \bullet B \beta$; the LR(1) closure adds it with the lookaheads $\mathrm{FIRST}(\beta a)$, and this set is not empty by our assumption. So an induction on the number of closure steps shows that the two sides contain the same LR(0) items. The other two claims follow by induction on $|\gamma|$. $\square$

For an LR(0) state $q$ and an item $i$ in its closure, let $\mathrm{LA}^*(q, i) = \{a : [i, a] \in J$ for some canonical LR(1) state $J$ with $\mathrm{core}(J) = \mathrm{CLOSURE}_0(q)\}$. Write $C_q$ for the set CLOSURE1 of lines L5 and L8, computed from the final sets LA.

Lemma 2 (no extra lookaheads). At every moment, $\mathrm{LA}[q, i] \subseteq \mathrm{LA}^*(q, i)$ for every kernel item $i$ of $q$. Hence $[i, b] \in C_q$ implies $b \in \mathrm{LA}^*(q, i)$.

Proof. Line L2 is correct because $[S' \to \bullet S, \$] \in I_0$ and the only state with the kernel item $S' \to \bullet S$ is state 0. Suppose the claim holds before line L6 adds $b$ to $\mathrm{LA}[\mathrm{GOTO}(q, X), A \to \alpha X \bullet \beta]$ because of $[A \to \alpha \bullet X \beta, b] \in C$. The LR(1) closure has the property $\mathrm{CLOSURE}_1(K) = \bigcup_{k \in K} \mathrm{CLOSURE}_1(\{k\})$, because each closure step uses one item. Each item $[i, a]$ of line L5 lies in some canonical state $J$ with core $q$, by the hypothesis, and $J$ is closed, so $\mathrm{CLOSURE}_1(\{[i, a]\}) \subseteq J$. So $[A \to \alpha \bullet X \beta, b]$ lies in such a $J$. Then $[A \to \alpha X \bullet \beta, b] \in \mathrm{GOTO}_1(J, X)$, whose core is $\mathrm{GOTO}_0(q, X)$ by Lemma 1, so $b \in \mathrm{LA}^*(\mathrm{GOTO}(q, X), A \to \alpha X \bullet \beta)$. The second claim follows by the same argument for $C_q$. $\square$

Lemma 3 (no missing lookaheads). After line L7, every canonical LR(1) state $J$ with core $q$ satisfies $J \subseteq C_q$. Hence $\mathrm{LA}^*(q, i) = \{b : [i, b] \in C_q\}$.

Proof. By induction on the length of a shortest path from $I_0$ to $J$. The kernel of $I_0$ is $[S' \to \bullet S, \$]$, and $\$ \in \mathrm{LA}[0, S' \to \bullet S]$ by line L2; $\mathrm{CLOSURE}_1$ is monotone, so $I_0 \subseteq C_0$. Let $J = \mathrm{GOTO}_1(J', X)$ with $J' \subseteq C_{q'}$ by induction, where $q' = \mathrm{core}(J')$. Each kernel item of $J$ is $[A \to \alpha X \bullet \beta, b]$ with $[A \to \alpha \bullet X \beta, b] \in J' \subseteq C_{q'}$. When line L7 ends, a full pass has changed nothing, so the pass of line L6 for $q'$ found $b$ already in $\mathrm{LA}[\mathrm{GOTO}(q', X), A \to \alpha X \bullet \beta]$, and $\mathrm{GOTO}(q', X) = q$ by Lemma 1. So the kernel of $J$ is in the set given to CLOSURE1 for $q$, and by monotonicity $J \subseteq C_q$. The equality then follows from Lemma 2. $\square$

The loop of lines L3 to L7 ends, because each pass that does not end it adds at least one element to a set LA, and these sets are subsets of a finite set.

Corollary 4. For every state $q$ and terminal or end marker $a$, the entry $\mathrm{ACTION}[q, a]$ of lines L8 to L10 is the union of the entries $\mathrm{ACTION}_1[J, a]$ of the canonical LR(1) table over the states $J$ with core $q$, where a shift to $J''$ is read as a shift to $\mathrm{core}(J'')$. In particular, if the LALR table has no conflict, neither has the canonical table, and $G$ is LR(1).

Proof. The canonical table puts shift on $a$ in $J$ when an item with $\bullet a$ is in $J$, and reduce or accept on $a$ when a completed item with lookahead $a$ is in $J$. By Lemmas 2 and 3, $C_q$ is the union of these $J$, and lines L9 and L10 read the same items. Shift targets agree by Lemma 1. Two different actions in some $\mathrm{ACTION}_1[J, a]$ would appear in $\mathrm{ACTION}[q, a]$. $\square$

From now on, line L11 has passed, so every entry has at most one action, and by Corollary 4 the grammar is LR(1). LR(1) grammars are unambiguous (Knuth 1965).

Lemma 5 (soundness). At every moment of the driver, let the stack hold the states $q_0 q_1 \cdots q_m$, with symbols $X_1, \ldots, X_m$, where $X_k$ is the symbol on the transition into $q_k$. Then $q_0 = 0$, $q_k = \mathrm{GOTO}(q_{k-1}, X_k)$, and the value stack holds trees $T_1, \ldots, T_m$, where $T_k$ is a derivation tree with root $X_k$, and the leaves of $T_1, \ldots, T_m$ in order spell the consumed input $a_1 \cdots a_{i-1}$. If the driver returns a tree at line L16, it is a parse tree of $w$.

Proof. Line L12 makes the claim true. Line L14 pushes $\mathrm{GOTO}(q_m, a)$ with the leaf $a$. At line L15, the reduction by $A \to \beta$ is in $\mathrm{ACTION}[q_m, a]$ because the completed item $A \to \beta \bullet$ is in the closure of $q_m$. In the LR(0) automaton, an item $A \to \beta' \bullet \beta''$ in the closure of $\mathrm{GOTO}(q, X)$ with $\beta' \ne \varepsilon$ is a kernel item that came from $A \to \beta''' \bullet X \beta''$ in the closure of $q$ with $\beta' = \beta''' X$. So, going down the stack, the top $|\beta|$ symbols are $\beta$, and there are at least $|\beta|$ of them above $q_0$. The new tree has root $A$, its children are the popped trees in order, and it uses the production $A \to \beta$; the leaves keep their order. The new state is $\mathrm{GOTO}$ of the exposed state on $A$, which exists because the exposed state has $A \to \bullet \beta$ in its closure and so an item with $\bullet A$ in its closure.

At line L16 the closure of $q_m$ contains $S' \to S \bullet$ and the lookahead is $\$$, so all of $w$ is consumed. The item $S' \to S \bullet$ comes only from $S' \to \bullet S$, which is only in state 0, because $S'$ is on no right side. No transition enters state 0, because every non-start kernel item has its dot after position 0. So the stack is $0\, q_1$ with $X_1 = S$, and $T_1$ is a parse tree of $w$. $\square$

Lemma 6 (completeness). If $w \in L(G)$, the driver accepts $w$.

Proof. Run the canonical LR(1) driver on $w$ next to the LALR driver. We show by induction on the number of moves that, before each move, the LALR stack is $\mathrm{core}(J_0) \cdots \mathrm{core}(J_m)$ when the LR(1) stack is $J_0 \cdots J_m$, and both have read the same input. This holds at the start. By (K2) the LR(1) driver has an action $t$ in $\mathrm{ACTION}_1[J_m, a]$. By Corollary 4, $t$ (with shift targets mapped to their cores) is in $\mathrm{ACTION}[\mathrm{core}(J_m), a]$, which has no other action, so the LALR driver makes the same move. A shift pushes $\mathrm{core}(\mathrm{GOTO}_1(J_m, a)) = \mathrm{GOTO}(\mathrm{core}(J_m), a)$ by Lemma 1. A reduction pops the same number of states from both stacks and pushes $\mathrm{GOTO}_1(J_k, A)$ and $\mathrm{GOTO}(\mathrm{core}(J_k), A)$, which correspond by Lemma 1. By (K2) the LR(1) driver accepts, so the LALR driver accepts at the same move. $\square$

Lemma 7 (termination). The driver stops on every input.

Proof. There are at most $n + 1$ shifts, so it is enough to show that no run of reductions without a shift is infinite. Suppose that one is, with lookahead $a$ from time $t_0$ on. Each reduction pops the top $|\beta|$ entries and then pushes one; call the stack length after the pops the low point of the move. Let $b(t)$ be the least low point of the moves at or after $t$. It never decreases.

Claim T. Let $t \ge t_0$ and let $e$ be the top entry at time $t$. Within a bounded number of moves, the driver pops $e$. Let $q$ be its state. The driver makes a reduction at time $t$, so some completed item $[A \to \beta \bullet]$ in the closure of $q$ has $a \in \mathrm{LA}^*(q, A \to \beta \bullet)$ by Lemma 2: there is a canonical state $J$ with core $q$ that contains $[A \to \beta \bullet, a]$. Let $J$ be reached by $\gamma$. By (K1), $S' \Rightarrow^*_{rm} \delta A a x \Rightarrow_{rm} \gamma a x$. Each nonterminal derives a terminal string, so $\gamma a x$ derives a sentence $z = u a x'$ with $\gamma \Rightarrow^* u$, through a rightmost derivation in which $\gamma a x$ occurs. The canonical driver on $z$ follows this rightmost derivation backwards, so at some moment its stack spells $\gamma$ with top state $J$ and lookahead $a$. From that moment, compare it with the LALR driver from time $t$, restricted to the entries above $e$ and above $J$. As in Lemma 6, by (K2) and Corollary 4 the two drivers make the same moves, with the LALR states the cores of the LR(1) states, until one of them pops its base entry ($J$ or $e$), and then the other pops its base entry at the same move, or until the LR(1) driver shifts $a$, and then the LALR driver shifts $a$. The LR(1) driver accepts $z$ in finitely many moves, so one of these events happens within a bound $B(q, a)$ that does not depend on $t$. A shift is excluded, so $e$ is popped.

Case 1: $b(t)$ grows without bound. Let $k = b(t_0)$, and let $t_k$ be the last move at or after $t_0$ with low point $k$; it exists because some move has low point $k$ and $b(t) > k$ from some time on. Every later move has a low point above $k$, so the entry at position $k + 1$, which the move at $t_k$ pushed, is never popped. It is the top entry right after $t_k$, and this contradicts Claim T.

Case 2: $b(t) = M$ from some time $t_1$ on. The entries at positions $1, \ldots, M$ are never popped after $t_1$, and infinitely many moves have low point $M$ and push an entry at position $M + 1$. Each such entry has the symbol of the nonterminal it reduces to, so two of these moves, at times $t_2 < t_3$, push trees $T_2$ and $T_3$ with the same root $A$. The consumed input does not change, so the trees above position $M$ span the same input before and after. Trees are never destroyed: a popped tree becomes a child of the new tree. Between $t_2$ and $t_3$ no move has a low point below $M$, so $T_2$ stays inside some tree above position $M$, and the move at $t_3$ pops all of these trees into $T_3$. So $T_2$ is a subtree of $T_3$. $T_3 \ne T_2$, and both span the same input. So $A \Rightarrow^+ \mu A \nu$ with $\mu \nu \Rightarrow^* \varepsilon$. Since $A$ derives a terminal string and occurs in a sentential form (it is the root of a tree in a viable stack, by Lemma 5 and Lemma 1), repeating this derivation gives infinitely many parse trees for one sentence, so $G$ is ambiguous. This contradicts the remark after Corollary 4. $\square$

Theorem. If line L11 finds no conflict, LALR-PARSE returns a parse tree of $w$ if $w \in L(G)$ and "reject" otherwise. If it finds a conflict, $G$ has no conflict-free LALR(1) table and the parser reports this.

Proof. By Lemma 7 the driver stops, at line L16 or line L17. By Lemma 6 it stops at line L16 when $w \in L(G)$, and by Lemma 5 it stops at line L16 only when $w \in L(G)$, with a parse tree. The table of lines L1 to L10 is determined by $G$, so a conflict means that $G$ is not LALR(1). $\blacksquare$