CCT-UFCA/Ciência da Computação/Autômatos e Linguagens Formais/Corretude de GLCs

Veremos como fazer a última prova de corretude que veremos na cadeira, que será das Gramáticas Livres de Contexto.

Definições

Uma cadeia palíndroma x é uma cadeia que é igual a sua reversa, ou seja, x = x⁻¹;
Uma cadeia y é dita prefixo de uma cadeia x se a subcadeia formada pelos primeiros |y| símbolos de x é igual a y;
Uma cadeia y é dita sufixo de uma cadeia x se a subcadeia formada pelos últimos |y| símbolos de x é igual a y;
ε é prefixo e sufixo de qualquer cadeia;
Seja V uma variável de uma GLC. Denotamos o conjunto de todas as cadeias geradas pela variável V por L(V);
- Assim, se S é a variável inicial de uma GLC G, temos que L(S) é a linguagem de G, ou seja, L(S) = L(G);

Corretude de Gramáticas Livres-de-Contexto

Seja G uma GLC e L uma linguagem. Dizemos que G é correta em relação à L, se L = L(G). Quando L está clara pelo contexto, podemos dizer apenas que G é correta.

A importância de se provar a corretude de gramáticas livres-de-contexto reside principalmente na garantia da precisão e consistência das linguagens que elas descrevem. Algumas aplicações para GLCs que mostram essa importância são:

Validação de Linguagens: As gramáticas livres-de-contexto são usadas para definir formalmente linguagens, como linguagens de programação, protocolos de comunicação, formatos de dados, entre outros. Provar a sua corretude assegura que essas definições estejam livres de ambiguidades e que todos os elementos da linguagem sejam corretamente descritos pela gramática.
Interpretação e Compilação: As gramáticas livres-de-contexto são fundamentais para a interpretação e compilação de linguagens de programação. Provar sua corretude ajuda a garantir que o compilador ou interpretador interprete corretamente o código fonte conforme definido pela gramática.
Padrões e Normas: Em muitos casos, gramáticas definem padrões e normas de construção de uma linguagem de comunicação em um determinado contexto. Provar a corretude de gramáticas livres-de-contexto em relação a esses padrões é crucial para garantir a conformidade e a interoperabilidade entre diferentes sistemas e ferramentas.

Para provar que uma GLC G é correta em relação a uma linguagem L, é necessário provar que L = L(G). Para isso, precisamos provar que x ∈ L(G) se e somente se x ∈ L. A implicação x ∈ L(G) ⇒ x ∈ L é provada através da demonstração de um conjunto de implicações no formato x ∈ L(V) ⇒ P(x), onde V é uma variável da gramática e P é um predicado sobre a cadeia x. Devemos ter pelo menos uma implicação para cada variável da gramática e pelo menos uma da implicações é a x ∈ L(S) ⇒ x ∈ L, onde S é a variável inicial da gramática, a qual implicará diretamente no que queremos provar, ou seja, que x ∈ L(G) ⇒ x ∈ L.

Nós devemos provar essas implicações usando indução estrutural na gramática, algo possível pela natureza recorrente das gramáticas. Os casos base da indução estrutural são sempre os casos base das variáveis, ou seja, devemos provar que as implicações são verdadeiras para as cadeias geradas pela aplicação direta de uma regra de produção, ou seja, cadeias de terminais x para as quais existe uma regra de produção do tipo V → x.

Devemos fazer um passo indutivo para cada regra de produção do tipo V → x, onde x possui pelo menos uma variável. Para cada regra de produção desse tipo, vamos supor que as implicações são verdadeiras para às variáveis em x e, então, vamos provar que as implicações são verdadeiras para a V à esquerda da regra de produção. Com isso, a nossa prova por indução estrutural estará completa.

De forma similar, a implicação x ∈ L ⇒ x ∈ L(G) é provada através da demonstração de um conjunto de implicações no formato x ∈ P(x) ⇒ L(V), onde V é uma variável da gramática e P é um predicado sobre a cadeia x. Essas implicações normalmente são as voltas das implicações usadas na prova da implicação x ∈ L(G) ⇒ x ∈ L. Devemos ter pelo menos uma implicação para cada variável da gramática e pelo menos uma da implicações é a x ∈ L ⇒ x ∈ L(S), onde S é a variável inicial da gramática, a qual implicará diretamente no que queremos provar, ou seja, que x ∈ L ⇒ x ∈ L(G).

Nós devemos provar essas implicações usando indução finita no tamanho de x. Os casos base da indução finita são quando x tem tamanho menor ou igual a um inteiro da sua escolha. Algumas vezes, apenas o caso base para x de tamanho zero (x = ε) é suficiente, mas outras vezes, é necessário acrescentar mais casos base. Deve-se então provar todas as implicações, onde algumas delas serão verdade por conta da hipótese falsa. Quando a hipótese é verdadeira, devemos provar também a conclusão.

No passo indutivo, vamos supor que todas as implicações são verdadeiras para todas as cadeias x de tamanho menor do que um valor k arbitrário que é maior do que o tamanho do maior caso base. Devemos então provar que as implicações são verdadeiras para todas as cadeias x de tamanho k.

Exemplos

Considere a linguagem L = {w | w é palíndroma} sob o alfabeto Σ = {0,1}. Uma GLC G que gera L é a seguinte:

S → 0S0 | 1S1 | 0 | 1 | ε

Para provar a corretude da GLC acima, precisamos provar que x ∈ L(G) ⇔ x ∈ L.

Provando a Ida ( x ∈ L(G) ⇒ x ∈ L ): Para isso, provaremos por indução estrutural que x ∈ L(S) ⇒ x ∈ L. Os casos base da variável S são S → ε | 0 | 1. Nos três casos, x = 0, x = 1 e x = ε, temos que, de fato, x ∈ L visto que as três cadeias são palíndromas.

Agora, vamos ao passo indutivo. Considere então a regra S → 0S0. Suponha que toda cadeia gerada pela variável S à direita da produção é palíndroma. Vamos provar que toda variável gerada pela variável S à esquerda da produção também é palíndroma. Seja x uma cadeia gerada pela variável S à esquerda da produção. Logo, x = 0y0 onde y é uma cadeia gerada pela variável S à direita da produção. Pela hipótese indutiva, temos que y é palíndroma. Logo a cadeia x = 0y0 também é palíndroma, ou seja, x ∈ L. De forma análoga, podemos provar o mesmo para a regra S → 1S1. Com isso, por indução estrutural, concluímos que toda cadeia gerada pela variável S é palíndroma, ou seja, x ∈ L(G) ⇒ x ∈ L.

Provando a Volta ( x ∈ L ⇒ x ∈ L(G) ): Vamos provar por indução finita no tamanho de x que x ∈ L ⇒ x ∈ L(S). Para x de tamanho zero ou 1, ou seja, para x = ε, ou x = 0, ou x = 1, temos que x é gerado por S com as regras de produção S → ε | 0 | 1 respectivamente. Seja k ≥ 2 um natural arbitrário e suponha que a implicação é verdadeira para todas as cadeias de tamanho menor do que k. Vamos provar que a implicação também é válida para todas as cadeias palíndromas de tamanho k. Seja x uma cadeia de tamanho k. Se x não satisfaz a premissa da implicação, ou seja, se x não é palíndroma, então a implicação é verdadeira. Suponha então que x é uma cadeia palíndroma.

Como k ≥ 2, temos que, ou x = 0y0, ou x = 1y1 onde y é uma cadeia palíndroma (possivelmente vazia). Em ambos os casos, como o tamanho de y é menor do que o tamanho de x e y é uma cadeia palíndroma, podemos invocar a hipótese indutiva para concluir que y é uma cadeia gerada por S. Logo, para que S gere x, podemos usar as regras de produção S → 0S0 | 1S1, caso x = 0y0 ou x = 1y1 respectivamente, fazendo a variável S à direita da regra gerar y. Concluímos portanto, por indução finita, que x ∈ L ⇒ x ∈ L(G).