Prove/find context free grammar is unambiguous for the language $L$

I am trying to find a grammar and prove that it is unambiguous for the language $$L$$, where $$L = \{ w \in \{a,b\}^+; |w|_a = |w|_b \}$$ Essentially: word $$w$$ contains at least one $$a$$ and $$b$$; where the number of $$a$$ is equal to the number of $$b$$.

What I tried: I am currently working with a grammar that has the following rules: (updated based on Tonita's suggestion) \begin{align} S &\to AS \mid BS \mid A \mid B\\ A &\to aXb\\ B &\to bYa \\ X &\to AX \mid \varepsilon\\ Y &\to BY \mid \varepsilon \end{align} I believe that this CFG does indeed produce all words of the language $$L$$; since it won't produce an empty word, will always produce a word containing an equal amount of a's and b's, and covers all of their possible permutations. Now I wanted to ask how would I go on proving that this grammar is unambiguous; or whether my grammar satisfies the provided language at all!

Currently, I am trying to work out a way to prove that all the words can only have exactly one derivation tree, pretty lost here, would appreciate any concepts/hints/solutions/advice.

• You forgot a rule for $S$ stopping the recursion: for now, every $S$ unfolding produces $S$ again. Apr 20 at 17:26
• Please modify the question, not the comment. Apr 20 at 18:14
• Thanks! Have updated it! Apr 20 at 18:25

Your updated grammar is SLR(1) which can be seen there, thus unambiguous, but constructing SLR-parsing tables is not an elegant way to prove things. If you use the following grammar form (which is almost equivalent to yours but distinguishes the first derivation to produce non-empty words), then the proof is much simpler: this grammar is LL(1), and it is not hard to construct the parsing table.

$$\begin{array}{l} S \rightarrow A S_1\;|\;B S_1\\ S_1 \rightarrow A S_1\;|\;B S_1\;|\;\varepsilon\\ A \rightarrow a X b \\ X \rightarrow A X\;|\;\varepsilon\\ B \rightarrow b Y a \\ Y \rightarrow B Y\;|\;\varepsilon \end{array}$$ The LL(1)-property guarantees that your grammar is unambiguous as well. Still, this method is again rather technical than elegant and involves the grammar change.

But you can notice that the nonterminals $$X$$ and $$Y$$ produce languages of balanced brackets if we use the mappings $$a\rightarrow ($$, $$b\rightarrow )$$ (for $$X$$) and $$a\rightarrow )$$, $$b\rightarrow ($$ (for $$Y$$). This leads to a reasoning that I like the most.

First, we can easily prove that no prefix of $$(w)$$, where $$w$$ is a balanced bracket sequence, is a balanced bracket sequence. Do it yourself.

Then it is easy to see that the rule $$S\rightarrow A$$ can be applied only to words having structure $$a w b$$, where $$w$$ is balanced w.r.t. $$(a,b)$$; but these words cannot be parsed by rule $$S\rightarrow A S$$, because that forces a balanced-bracket-prefix to exist. Thus, there is the only possibility to split the word to the part parsed by $$A$$ and the remainder parsed by $$S$$: since the prefix of the form $$a w' b$$ (where $$w'$$ is balanced w.r.t. $$(a,b)$$) is unique.

The same reasoning works for parsing the $$(b,a)$$-balanced parts.

Hope that helps!