Grammars are inherently recursive objects, so the answer seems obvious: by induction. That said, the specifics are often tricky to get right. In the sequel I will describe a technique that allows to reduce many a grammar-correctness proof to mechanical steps, provided some creative preprocessing is done.
$\newcommand{\lang}[1]{\mathcal{L}(#1)}
\newcommand{\sent}[1]{\vartheta(#1)}
\newcommand{\derive}{\mathbin{\Rightarrow}}
\newcommand{\derivestar}{\mathbin{\Rightarrow^*}}
\newcommand{\nats}{\mathbb{N}}$
The basic idea is to not restrict oneself to words of grammar and language; it is hard to grasp the structure of the grammar in this way. Instead, we will argue about the set of sentences the grammar can create. Furthermore, we will split one daunting proof goal into many small goals that are more tractable.
Let $G=(N,T,\delta,S)$ a formal grammar with non-terminals $N$, terminals $T$, rules $\delta$ and starting symbol $S \in N$. We
denote by $\sent{G}$ the set of sentences that can be derived from $S$ given $\delta$, that is $\alpha \in \sent{G} \iff S \derivestar \alpha$. The language generated by $G$ is $\lang{G} = \sent{G} \cap T^*$. Suppose we want to show that $L = \lang{G}$ for some $L \subseteq T^*$.
The ansatz
Here is how we go about that. We define $M_1, \dots, M_k \subseteq (N \cup T)^*$ so that
- $\displaystyle \sent{G} = \bigcup_{i=1}^k M_i$ and
- $\displaystyle T^* \cap \bigcup_{i=1}^k M_i = L$.
While 2. is usually clear by definition of the $M_i$, 1. requires some serious work. The two items together clearly imply $\lang{G} = L$ as desired.
For ease of notation, let's denote $M = \bigcup_{i=1}^k M_i$.
The rocky road
There are two major steps to performing such a proof.
How to find (good) $M_i$?
One strategy is to investigate phases the grammar works through. Not every grammar is amenable to this idea; in general,
this is a creative step. It helps if we can define the grammar ourselves; with some experience, we will be able to define
grammars more tractable with this approach.
How to prove 1.?
As with any set equality, there are two directions.
- $\sent{G} \subseteq M$: (structural) induction over the productions of $G$.
- $M \subseteq \sent{G}$: Usually one induction by $M_i$, starting from the one that contains $S$.
This is as specific as it gets; the details depend on the grammar and language at hand.
Example
Consider the language
$\qquad \displaystyle L = \{ a^n b^n c^m \mid n,m \in \nats \}$
and the grammar $G = (\{S,A\}, \{a,b,c\}, \delta, S)$ with $\delta$ given by
$\qquad \begin{align}
S &\to Sc \mid A \\
A &\to aAb \mid \varepsilon
\end{align}$
for which we want to show that $L = \lang{G}$. What are the phases this grammar works through? Well, first it generates $c^m$ and then $a^n b^n$. This immediately informs our choice of $M_i$, namely
$\qquad \begin{align}
M_0 &= \{Sc^m \mid m \in \nats \} \;, \\
M_1 &= \{ a^n A b^n c^m \mid m,n \in \nats \} \;, \\
M_2 &= \{ a^n b^n c^m \mid m,n \in \nats \} \;. \\
\end{align}$
As $M_2 = L$ and $M_0 \cap T^* = M_1 \cap T^* = \emptyset$, item 2. is already taken care of. Towards 1., we split the proof in two parts as announced.
$\mathbf{\sent{G} \subseteq M}$
We perform structural induction along the rules of $G$.
I.A.: Since $S = Sc^0 \in M_0$ we anchor successfully.
I.H.: Assume for some set of sentences $X \subseteq \sent{G}$ that we also know $X \subseteq M$.
I.S.: Let $\alpha \in X \subseteq \sent{G} \cap M$ arbitrary. We have to show that whatever form $\alpha$ has and whatever rule is applied next, we don't leave $M$. We do this by complete case distinction. By induction hypothesis, we know that (exactly) one of the following cases applies:
- $w \in M_0$, that is $w = Sc^m$ for some $m \in \nats$.
Two rules can be applied, both of which derive a sentence in $M$:
- $Sc^m \derive Sc^{m+1} \in M_0$ and
- $Sc^m \derive Ac^m = a^0Ab^0c^m \in M_1$.
- $w \in M_1$, i.e. $w = a^nAb^nc^m$ for some $m,n \in \nats$:
- $w \derive a^{n+1}Ab^{n+1}c^m \in M_1$ and
- $w \derive a^nb^nc^m \in M_2$.
- $w \in M_3$: since $w \in T^*$, no further derivations are possible.
Since we have successfully covered all cases, the induction is complete.
$\mathbf{\sent{G} \supseteq M}$
We perform one (simple) proof per $M_i$. Note how we chain the proofs so "later" $M_i$ can anchor using the "earlier" $M_i$.
- $M_1$: We perform an induction over $m$, anchoring in $Sc^0 = S$ and using $S \to Sc$ in the step.
- $M_2$: We fix $m$ to an arbitrary value and induce over $n$. We anchor in $Ac^m$, using that $S \derivestar Sc^m \derive Ac^m$ by the former proof. The step progresses via $A \to aAb$.
- $M_3$: For arbitrary $m,n \in \nats$ we use the former proof for $S \derivestar a^nAb^nc^m \derive a^nb^nc^m$.
This concludes the second direction of the proof of 1., and we are done.
We can see that we heavily exploit that the grammar is linear. For non-linear grammars, we need $M_i$ with more than one variable parameter (in the proof(s)), which can become ugly. If we have control over the grammar, this teaches us to keep it simple. Consider as deterring example this grammar which is equivalent to $G$:
$\qquad \begin{align}
S &\to aAbC \mid \varepsilon \\
A &\to aAb \mid \varepsilon \\
C &\to cC \mid \varepsilon
\end{align}$
Exercise
Give a grammar for
$\qquad L = \{ b^k a^l (bc)^m a^n b^o \mid k,l,m,n,o \in \nats, k \neq o, 2l = n, m \geq 2 \}$
and prove its correctness.
If you have trouble, a grammar:
Consider $G = (\{S,B_r,B_l,A,C\}, \{a,b,c\}, \delta, S)$ with productions
$\quad \begin{align} S &\to bSb \mid B_l \mid B_r \\ B_l &\to bB_l \mid bA \\ B_r &\to B_r b \mid Ab \\ A &\to aAaa \mid C \\ C &\to bcC \mid bcbc \end{align}$
and $M_i$:
$\quad\begin{align} M_0 &= \{ b^i S b^i \mid i \in \nats \} \\ M_1 &= \{ b^i B_l b^o \mid o \in \nats, i \geq o \} \\ M_2 &= \{ b^k B_r b^i \mid k \in \nats, i \geq k \} \\ M_3 &= \{ b^k a^i A a^{2i} b^o \mid k,o,i \in \nats, k \neq o \} \\ M_4 &= \{ b^k a^l (bc)^i C a^{2l} b^o \mid k,o,l,i \in \nats, k \neq o \} \\ M_5 &= L \end{align}$
What about non-linear grammars?
The characterising feature of the class of context-free languages is the Dyck language: essentially, every context-free language can be expressed as the intersection of a Dyck language and a regular language. Unfortunately, the Dyck language is not linear, that is we can give no grammar that is inherently suited to this approach.
We can, of course, still define $M_i$ and do the proof, but it's bound to be more arduous with nested inductions and what not.
There is one general way I know of that can help to some extent. We change the ansatz to showing that we generate at least all
required words, and that we generate the right amount of words (per length). Formally, we show that
- $\displaystyle \sent{G} \supseteq L$ and
- $\displaystyle |\lang{G} \cap T^n| = |L \cap T^n|$ for all $n \in \nats$.
This way, we can restrict ourselves to the "easy" direction from the original ansatz and exploit structure in the language, ignoring overcomplicated features the grammar may have. Of course, there is no free lunch: we get the all new task of counting the words $G$ generates for each $n \in \nats$. Lucky for us, this is often tractable; see here and here for details¹. You can find some examples in my bachelor thesis.
For ambiguous and non-context-free grammars, I'm afraid we are back to ansatz one and thinking caps.
- When using that particular method for counting, we get as a bonus that the grammar is unambiguous. In turn, this also means that the technique has to fail for ambiguous grammars as we can never prove 2.
