Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

Specifying formal languages by giving formal grammars is a frequent task: we need grammars not only to describe languages, but also to parse them, or even do proper science. In all cases, it is important that the grammar at hand is correct, that is generates exactly the desired words.

We can often argue on a high-level why the grammar is an adequate representation of the desired language, omitting a formal proof. But what if we are in doubt or need a formal proof for some reason? What are techniques we can apply?

This is supposed to become a reference question. Therefore, please take care to give general, didactically presented answers that are illustrated by at least one example but nonetheless cover many situations. Thanks!

share|improve this question

1 Answer 1

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

  1. $\displaystyle \sent{G} = \bigcup_{i=1}^k M_i$ and
  2. $\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.


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}$


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

  1. $\displaystyle \sent{G} \supseteq L$ and
  2. $\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.

  1. 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.
share|improve this answer
I think there is a typo in the example(induction) $a^{n+1}Ab^{n+1}c^m \in M_2$ should be $a^{n+1}Ab^{n+1}c^m \in M_1$. –  Renato Sanhueza Jun 12 at 19:31
@RenatoSanhueza Right, thanks. –  Raphael Jun 13 at 8:32

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.