When developing a CFG, I find that one can be confused about whether the grammar is correct, i.e. whether it recognizes only the required strings and not other strings.

But this can be hard to see?

Are there techniques and tools for "proof-reading", whether the grammar is correct and succinct enough?

  • 2
    $\begingroup$ Let me recommend again to get familiar with the basics. Our reference material may be a good start. $\endgroup$ – Raphael Dec 29 '15 at 14:34

There is no general method for your problem. Indeed the problem whether a CFG accepts all strings is undecidable. However you can always try to find a formal proof.

Assume you want to prove that the grammar $G$ $$ S\to aSb \mid \varepsilon$$ generates the language $L= \{a^nb^n \mid n\ge0\}$. Then you have to show that (1) every string $a^kb^k\in L$ can be derived from $G$, and (2) every $w \in L(G)$ has the form $a^kb^k$.

Both statements are not difficult to prove. For example to show (1) you can argue as follows. If we apply the $S \to aSb$ rule $k$ times, then we get the string $a^kSb^k$. After substituting $S$ with $\varepsilon$ we obtain $a^kb^k$.

  • $\begingroup$ Right, but for more substantial languages and grammars, specially if the language is defined in less-than-formal terms, this is a formidable task. $\endgroup$ – vonbrand Dec 29 '15 at 14:03
  • 1
    $\begingroup$ Note that we have a reference question about this. Feel free to add an answer if you think the material lacks anything. (cc @vonbrand) $\endgroup$ – Raphael Dec 29 '15 at 14:35

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