Jak udowodnić, że gramatyka jest jednoznaczna?

Mój problem polega na tym, jak mogę udowodnić, że gramatyka jest jednoznaczna? Mam następującą gramatykę:

i uczynię to jednoznaczną gramatyką, myślę, że jest poprawne:

• $S → S_1 ∣ S_2$

• $S_1 → \mbox{if } expression \mbox{ then } S ∣ \mbox{if } expression \mbox{ then } S_2 \mbox{ else } S_1$

• $S_2 → \mbox{if } expression \mbox{ then } S_2 \mbox{ else } S_2 ∣ statement$

Wiem, że jednoznaczna gramatyka ma jedno drzewo analizy dla każdego terminu.

Nie ma (co najmniej) jednym ze sposobów wykazania jednoznaczność gramatyki dla języka L . Składa się z dwóch kroków:$G = (N,T,\delta,S)$$L$

1. Wykazać .$L \subseteq \mathcal{L}(G)$
2. Wykazać .$[z^n]S_G(z) = |L_n|$

Pierwszy krok jest całkiem jasny: pokaż, że gramatyka generuje (przynajmniej) słowa, które chcesz, to jest poprawność.

Drugi krok pokazuje, że ma tyle drzew składni dla słów o długości n, jak L ma słowa o długości n - z 1. oznacza to jednoznaczność. Wykorzystuje funkcję struktury G, która sięga do Chomsky'ego i Schützenbergera [1], mianowicie$G$$n$$L$$n$$G$

$\qquad \displaystyle S_G(z) = \sum_{n=0}^\infty t_nz^n$

z liczba drzew składniowych G ma dla słów o długości n . Oczywiście trzeba mieć | L n | aby to zadziałało.$t_n = [z^n]S_G(z)$$G$$n$$|L_n|$

Zaletą jest to, że jest (zwykle) łatwy do uzyskania dla języków bezkontekstowych, chociaż znalezienie zamkniętego formularza dla t n może być trudne. Przekształć G w układ równań funkcji z jedną zmienną na nieterminal:$S_G$$t_n$$G$

$\qquad \displaystyle \left[ A(z) = \sum\limits_{(A, a_0 \dots a_k) \in \delta} \ \prod\limits_{i=0}^{k} \ \tau(a_i)\ : A \in N \right] \text{ with } \tau(a) = \begin{cases} a(z) &, a \in N \\ z &, a \in T \\ \end{cases}.$

Może to wyglądać zniechęcająco, ale tak naprawdę jest to tylko syntaktyczna transformacja, co stanie się jasne w przykładzie. Chodzi o to, że wygenerowane symbole końcowe są liczone w wykładnik i dlatego, że układ ma taką samą postać co G , Z, n zachodzi tak często, w sumie, jak N zaciski mogą być generowane przez G . Szczegóły w Kuich [2].$z$$G$$z^n$$n$$G$

Rozwiązanie tego układu równań (algebra komputerowa!) Daje ; teraz „tylko” trzeba pociągnąć za współczynnik (w zamkniętej, ogólnej formie). TCS Ściągawka i komputer algebra często może zrobić.$S(z) = S_G(z)$

Przykład

Rozważ prostą gramatykę z regułami$G$

.$\qquad \displaystyle S \to aSa \mid bSb \mid \varepsilon$

Oczywiste jest, że (krok 1, dowód przez indukcję). Są 2 $\mathcal{L}(G) = \{ww^R \mid w \in \{a,b\}^*\}$ palindromy o długościn,jeżelinjest parzyste, wprzeciwnym razie0.$2^{\frac{n}{2}}$$n$$n$$0$

Ustawienie układu równań daje

$\qquad \displaystyle S(z) = 2z^2S(z) + 1$

którego rozwiązaniem jest

.$\qquad \displaystyle S_G(z) = \frac{1}{1-2z^2}$

Współczynniki pokrywają się z liczbą palindromów, więc G jest jednoznaczne.$S_G$ $G$

1. Algebraiczna teoria języków bezkontekstowych Chomsky'ego, Schützenberger (1963)
2. O entropii języków bezkontekstowych autorstwa Kuicha (1970)

This is a good question, but some Googling would have told you that there is no general method for deciding ambiguity, so you need to make your question more specific.

For some grammars, a proof by induction (over word length) is possible.

Consider for example a grammar $G$ over $\Sigma = \{a,b\}$ given by the following rules:

$\qquad \displaystyle S \to aSa \mid bSb \mid \varepsilon$

All words of length $\leq 1$ in $L(G)$ -- there's only $\varepsilon$ -- have only one left-derivation.

Assume that all words of length $\leq n$ for some $n \in \mathbb{N}$ have only one left-derivation.

Now consider arbitrary $w = w_1 w' w_n \in L(G) \cap \Sigma^n$ for some $n > 0$. Clearly, $w_1 \in \Sigma$. If $w_1 = a$, we know that the first rule in every left-derivation has to be $S \to aSa$; if $w_1 = b$, it has to be $S \to bSb$. This covers all cases. By induction hypothesis, we know that there is exactly one left-derivation for $w'$. In combination, we conclude that there is exactly one left-derivation for $w$ as well.

This becomes harder if

• there are multiple non-terminals,
• the grammar is not linear, and/or
• the grammar is left-recursive.

It may help to strengthen the claim to all sentential forms (if the grammar has no unproductive non-terminals) and "root" non-terminals.

I think the conversion to Greibach normal form maintains (un)ambiguity, to applying this step first may take care of left-recursion nicely.

The key is to identify one feature of every word that fixes (at least) one derivation step. The rest follows inductively.

Basically, it's a child generation problem. Start with the first expression, and generate it's children .... Keep doing it recursively (DFS), and after quite a few iterations, see if you can generate the same expanded expression from two different children. If you are able to do that, it's ambiguous. There is no way to determine the running time of this algorithm though. Assume it's safe, after maybe generating 30 levels of children :) (Of course it could bomb on the 31st)