How to Prove That a Formal Grammar Is Correct

A formal grammar is correct when it generates exactly the strings that it is intended to describe. The standard proof is therefore an equality proof: if $G$ is the grammar and $L$ is the target language, establish

$$L(G)=L.$$

The most reliable way to prove this equality is to prove both inclusions separately. This method applies to context-free grammars and, with suitable changes, to regular and unrestricted grammars as well.

What “correct” means

Let $G=(V,\Sigma,P,S)$ be a grammar, where $V$ is the set of variables, $\Sigma$ is the terminal alphabet, $P$ is the set of productions, and $S$ is the start symbol. The language generated by $G$ is

$$L(G)=\{w\in\Sigma^*: S\Rightarrow^* w\}.$$

Here, $S\Rightarrow^* w$ means that $w$ can be obtained from $S$ through zero or more production applications.

Suppose the intended language is $L$. There are two obligations:

1. Soundness: $L(G)\subseteq L$. The grammar does not generate invalid strings.
2. Completeness: $L\subseteq L(G)$. The grammar generates every valid string.

Together, these imply $L(G)=L$.

Correctness does not necessarily mean that the grammar is unambiguous. A grammar may generate exactly the right language but provide two or more parse trees for one string.

Proving soundness

To prove soundness, start with an arbitrary string $w$ such that $S\Rightarrow^*w$. You must show that $w$ satisfies the definition of the target language.

The proof usually follows one of these patterns:

• induction on the number of production applications;
• structural induction on the grammar’s recursive rules;
• an invariant that remains true for every sentential form.

The key is to examine every production that can contribute to a derivation. If each production preserves the desired property, then the final terminal string has that property too.

Proving completeness

To prove completeness, start with an arbitrary string $w\in L$. Use the description of $w$ to construct a derivation from $S$.

For recursively defined languages, induction on the size of the string is often natural. The induction step should explain which production corresponds to the structure of the string. For example, if every nonempty string in the target language has the form $axb$, use a production that adds $a$ at the left and $b$ at the right.

Worked example: the language $\{a^n b^n:n\geq 0\}$

Consider the grammar

$$S\to aSb\mid\varepsilon.$$

The intended language is

$$L=\{a^n b^n:n\geq 0\}.$$

This language contains

$$\varepsilon,\quad ab,\quad aabb,\quad aaabbb,\ldots$$

We will prove that the grammar is correct.

Soundness

We show that every string derived from $S$ has the form $a^n b^n$ for some $n\geq0$.

Use induction on the number of times the production $S\to aSb$ is used.

Base case: If it is used zero times, then the derivation is

$$S\Rightarrow\varepsilon.$$

This is $a^0b^0$, so the claim holds.

Inductive step: Assume a derivation using $k$ copies of $S\to aSb$ produces $a^k b^k$. A derivation using $k+1$ copies has the form

$$S\Rightarrow aSb\Rightarrow^* a(a^k b^k)b=a^{k+1}b^{k+1}.$$

Thus every generated string contains the same number of $a$ symbols and $b$ symbols, with all $a$ symbols before all $b$ symbols. Therefore,

$$L(G)\subseteq\{a^n b^n:n\geq0\}.$$

Completeness

Now take any string in the target language. It has the form $a^n b^n$ for some $n\geq0$.

If $n=0$, then

$$S\Rightarrow\varepsilon.$$

If $n>0$, apply $S\to aSb$ exactly $n$ times and then apply $S\to\varepsilon$:

$$S\Rightarrow aSb \Rightarrow aaSbb \Rightarrow\cdots \Rightarrow a^nSb^n \Rightarrow a^n b^n.$$

Therefore every string in the target language is generated by the grammar:

$$\{a^n b^n:n\geq0\}\subseteq L(G).$$

The two inclusions establish

$$L(G)=\{a^n b^n:n\geq0\}.$$

The grammar is correct for this language.

A useful proof template

For many grammar questions, the following structure is enough:

Claim. The grammar $G$ generates exactly the language $L$.

Soundness. Let $w\in L(G)$. Analyze a derivation $S\Rightarrow^*w$, usually by induction. Show that $w$ has the required form, so $w\in L$.

Completeness. Let $w\in L$. Use the structure or defining recurrence of $w$ to construct a derivation $S\Rightarrow^*w$. Hence $w\in L(G)$.

Conclusion. Since both inclusions hold, $L(G)=L$.

Avoid saying only that the grammar “looks like” the language. A few successful derivations demonstrate possibility, not correctness. They do not show that every valid string is generated or that invalid strings are excluded.

Correctness versus ambiguity

A grammar can be correct but ambiguous. For example, the grammar

$$E\to E+E\mid E\times E\mid (E)\mid x$$

can generate arithmetic expressions, but an expression such as $x+x\times x$ may have different parse trees corresponding to different groupings. Whether that is acceptable depends on the language specification.

If the grammar must be unambiguous, add a third proof obligation: show that every generated string has at most one parse tree, or at most one leftmost derivation. For arithmetic, this is usually handled by separating precedence levels, for example with distinct variables for expressions, terms, and factors.

Common mistakes

• Proving only soundness: Showing that generated strings are valid does not show that all valid strings can be generated.
• Proving only completeness: A grammar may generate every intended string and many unintended ones.
• Forgetting the empty string: If the target definition allows $n=0$, the proof must account for $\varepsilon$.
• Using examples as a proof: Listing derivations for several strings cannot replace an induction or general construction.
• Confusing language equality with unambiguity: Exact language generation and unique parsing are different properties.
• Ignoring the start symbol: Derivations must begin with the specified start symbol, not an arbitrary variable.

For a programming-language grammar, the same distinction remains useful: first prove that the syntax accepts every intended valid construct and rejects strings outside the syntactic language; then analyze semantic rules, such as type checking, separately.