Proofs: LL parse table

BUILD fills each cell with exactly the productions whose PREDICT set contains the token full

This proof shows: correctness.

Statement. Let $G = (V, \Sigma, R, S)$ be a grammar in which every nonterminal is reachable from $S$. When BUILD$(G)$ stops, the computed sets equal $\mathrm{Null}$, $\mathrm{FIRST}(A)$ and $\mathrm{FOLLOW}(A)$ as defined on the page, for each $A \in V$, and each cell satisfies invariant (T): $M[A, a]$ holds exactly the productions $A \to \alpha$ with $a \in \mathrm{PREDICT}(A \to \alpha)$. LOOKUP$(M, A, a)$ returns error exactly when no production of $A$ has $a$ in its PREDICT set, and the unique such production when there is one. Without the reachability hypothesis, $\mathrm{Null}$ and FIRST are still exact, and the computed $\mathrm{FOLLOW}(A)$ contains the true one.

Setup. We treat $\$$ as an extra terminal and work with sentential forms of $S\$$. For a string $\gamma$ over $V \cup \Sigma \cup \{\$\}$, $\mathrm{FIRST}(\gamma) = \{ a : \gamma \Rightarrow^* a \rho \}$. We use the splitting lemma of the derivation page in its general form, whose proof is the same: if $Y_1 \cdots Y_k \Rightarrow^m \gamma$, then $\gamma = \gamma_1 \cdots \gamma_k$ with $Y_i \Rightarrow^{m_i} \gamma_i$ and $\sum m_i = m$. A consequence: $a \in \mathrm{FIRST}(Y_1 \cdots Y_k)$ if and only if there is an $i$ with $Y_1 \cdots Y_{i-1} \Rightarrow^* \varepsilon$ and $a \in \mathrm{FIRST}(Y_i)$, since the first terminal of $\gamma$ lies in the first nonempty piece $\gamma_i$. The computation of $\mathrm{Null}$ is proved correct on the nullable symbol page. We write $F(\cdot)$ and $Fo(\cdot)$ for the sets that the loops compute.

Step 1: termination. Each loop of SETS repeats a pass only when the pass added an element to some set. The sets are subsets of the finite sets $V$, $V \times \Sigma$ and $V \times (\Sigma \cup \{\$\})$, and elements are never removed. So each loop makes at most $|V|(|\Sigma| + 1) + 1$ passes, and BUILD stops.

Step 2: FIRST is sound. Claim: if $a$ is added to $F(A)$, then $a \in \mathrm{FIRST}(A)$. Induction on the order of the additions. The rule of lines L3 and L4 adds $a$ when $A \to X_1 \cdots X_k$, $X_1 \cdots X_{i-1}$ is nullable, and $a \in F(X_i)$, where $F(a) = \{a\}$ for a terminal. If $X_i$ is a nonterminal, $a$ was added to $F(X_i)$ earlier, so $X_i \Rightarrow^* a \rho$ by the induction hypothesis. In both cases $A \Rightarrow X_1 \cdots X_k \Rightarrow^* X_i \cdots X_k \Rightarrow^* a \rho X_{i+1} \cdots X_k$.

Step 3: FIRST is complete. Claim: if $A \Rightarrow^m a \rho$, then $a \in F(A)$ when the loop stops. Strong induction on $m \ge 1$. The first step is $A \Rightarrow X_1 \cdots X_k$, and $X_1 \cdots X_k \Rightarrow^{m-1} a \rho$. By the splitting lemma there is an $i$ with $X_1 \cdots X_{i-1} \Rightarrow^* \varepsilon$ and $X_i \Rightarrow^{m_i} a \rho'$ with $m_i \le m - 1$. If $X_i$ is the terminal $a$, the rule adds $a$ to $F(A)$. Otherwise $a \in F(X_i)$ by the induction hypothesis, and the last pass of the loop changed nothing, so the rule for $A \to X_1 \cdots X_k$ and this $i$ found $a$ already in $F(A)$. With Step 2, $F(A) = \mathrm{FIRST}(A)$, and then the formula of the page gives $\mathrm{FIRST}(\alpha)$ for each string $\alpha$ by the consequence of the splitting lemma.

Step 4: FOLLOW is complete. Claim: if $S\$ \Rightarrow^m \beta A \gamma$, then $\mathrm{FIRST}(\gamma) \subseteq Fo(A)$. Since $a \in \mathrm{FOLLOW}(A)$ means $S \$ \Rightarrow^* \beta A a \gamma'$, and $a \in \mathrm{FIRST}(a\gamma')$, this gives $\mathrm{FOLLOW}(A) \subseteq Fo(A)$. Induction on $m$.

• $m = 0$: the form is $S\$$, so $A = S$ and $\gamma = \$$, and line L6 puts $\$$ in $Fo(S)$.

• $m \ge 1$: the last step rewrites $C \to \eta$ in $\delta_1 C \delta_2$, giving $\delta_1 \eta \delta_2 = \beta A \gamma$, and $S\$ \Rightarrow^{m-1} \delta_1 C \delta_2$. Three cases for the position of this occurrence of $A$.

  • In $\delta_2$: $\delta_2 = \rho A \gamma$, and the same occurrence has the right context $\gamma$ in $\delta_1 C \delta_2$. The induction hypothesis applies.
  • In $\delta_1$: $\delta_1 = \beta A \rho$ and $\gamma = \rho \eta \delta_2$. In the earlier form the right context is $\rho C \delta_2$, and $\rho C \delta_2 \Rightarrow \rho \eta \delta_2$, so $\mathrm{FIRST}(\gamma) \subseteq \mathrm{FIRST}(\rho C \delta_2) \subseteq Fo(A)$ by the induction hypothesis.
  • In $\eta$: $\eta = \eta_1 A \eta_2$ and $\gamma = \eta_2 \delta_2$. Let $a \in \mathrm{FIRST}(\eta_2 \delta_2)$. By the splitting lemma, either $a \in \mathrm{FIRST}(\eta_2)$, and lines L7 and L8 put $a$ in $Fo(A)$ for the production $C \to \eta_1 A \eta_2$; or $\eta_2$ is nullable and $a \in \mathrm{FIRST}(\delta_2)$. In the second case $a \in Fo(C)$ by the induction hypothesis for the occurrence of $C$ in $\delta_1 C \delta_2$, and line L8 adds $Fo(C)$ to $Fo(A)$ because $\eta_2$ is nullable.

  In each case the last pass of the loop changed nothing, so the element is in $Fo(A)$ when the loop stops.

Step 5: FOLLOW is sound when every nonterminal is reachable. Claim: each element added to $Fo(A)$ is in $\mathrm{FOLLOW}(A)$. Induction on the order of the additions. Line L6 adds $\$$ to $Fo(S)$, and $S\$$ itself shows $\$ \in \mathrm{FOLLOW}(S)$. Line L8 uses a production $B \to \alpha A \beta$. Since $B$ is reachable, $S \$ \Rightarrow^* \rho B \tau$ for some $\rho, \tau$. If $a \in \mathrm{FIRST}(\beta)$, then $S\$ \Rightarrow^* \rho \alpha A \beta \tau \Rightarrow^* \rho \alpha A a \rho' \tau$. If $\beta$ is nullable and $b$ was added earlier to $Fo(B)$, then $b \in \mathrm{FOLLOW}(B)$ by the induction hypothesis, so $S\$ \Rightarrow^* \rho' B b \tau'$, and $\rho' B b \tau' \Rightarrow \rho' \alpha A \beta b \tau' \Rightarrow^* \rho' \alpha A b \tau'$. In both cases the token is in $\mathrm{FOLLOW}(A)$. (Without reachability this step fails: a production of an unreachable $B$ can add tokens to $Fo(A)$. Step 4 does not use reachability.)

Step 6: the cells. Lines L3 to L6 add $p = A \to \alpha$ to $M[A, a]$ exactly when $a \in \mathrm{FIRST}(\alpha)$, or $\alpha$ is nullable and $a \in \mathrm{FOLLOW}(A)$; by Steps 2 to 5 these are the true sets. That is the definition of $a \in \mathrm{PREDICT}(p)$, and no other line adds to a cell. So (T) holds. LOOKUP reads the cell at line L7 and returns error when it is empty (line L8), reports the conflict when it has two or more productions (line L9), and returns its only production otherwise (line L10).

So BUILD fills every cell as (T) says, and LOOKUP returns its content. $\blacksquare$