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

Similarmente à corretude dos Autômatos Finitos, veremos formas de provar a corretude de Expressões Regulares para observarmos o funcionamento deles mais atentamente.

Definições

Sejam A e B dois conjuntos. É verdade que, se x ∈ A e A ⊆ B, então x ∈ B;
Sejam R e S são expressões regulares. Temos que é verdade que (R)* = (R)*(R)*; que L(S) ⊆ L(R) =⇒ L((S)*) ⊆ L((R)*); e ainda que L((R)*) ⊆ L((S ∪ R)*).

Corretude de ERs

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

Compreender como provar a corretude de uma expressão regular é bastante importante dada as suas várias aplicações. Alguns exemplos de aplicação para expressões regulares são:

Validação de Formatos: Verificação de formatos de e-mail, números de telefone, endereços IP, códigos postais, senhas etc.;
Pesquisa e Substituição: Encontrar e substituir trechos específicos de texto em documentos ou na localização de padrões complexos em arquivos de log ou dados textuais;
Extração de Dados: Extração de partes específicas de texto de documentos ou páginas web (web scraping), e coletamento de informações estruturadas a partir de dados não estruturados; e
Linguagem de Programação e Compiladores: Na análise léxica em compiladores define tokens em código-fonte, e highlighting de sintaxe em editores de texto e IDEs.

Para provar que uma expressão regular R é correta em relação a uma linguagem L, é necessário provar que L = L(R). Para isso, podemos, ou calcular a linguagem L(R) a partir da própria expressão R e averiguar se temos diretamente que L(R) = L, ou provar que x ∈ L(R) se e somente se x ∈ L.

Quando for necessário provar que x ∈ L(R) se e somente se x ∈ L, a prova da implicação x ∈ L(R) ⇒ x ∈ L normalmente é feita de forma direta, provando propriedades sobre as subexpressões de R. As propriedades são sempre da forma x ∈ L(R') ⇒ P(x), onde R' é uma subexpressão de R e P é uma predicado que denota uma propriedade sobre a cadeia x. A ideia é provar propriedades sobre as expressões menores e usá-las para provar propriedades sobre expressões maiores até que se tenha o suficiente para provar a implicação x ∈ L(R) ⇒ x ∈ L, que é a ida em si e é a última propriedade a ser provada.

Finalmente, a prova da implicação x ∈ L ⇒ x ∈ L(R) normalmente é feita por indução finita no tamanho de x, mas pode ser feita também em outro aspecto numérico de x, como o número de símbolos em x de determinado tipo. Primeiramente, precisa-se provar o caso base, ou seja, x = ε. Depois, no passo indutivo, para um natural k arbitrário maior do que as cadeias no caso base, assume-se que a implicação vale para todas as cadeias de tamanho menor do que k para então provar que a implicação vale para todas as cadeias de tamanho k.

Exemplos

Exemplo 1: Considere a linguagem L = {0ⁿ1^m| n, m ≥ 1} sob o alfabeto Σ = {0,1}. Uma ER que representa L é a R = 0⁺1⁺.Temos que:

Assim, temos diretamente que L(R) = L e, portanto, provar a equivalência x ∈ L(R) ⇔ x ∈ L não é necessário.

Exemplo 2: Considere a linguagem L = {w | w possui um número par de símbolos 0} sob o alfabeto Σ = {0,1}. Uma ER que representa L é a R = (1 ∪ 01*0)*. Note que L(R) ○ L(R) = L(R).

Provando a Ida ( x ∈ L(R) ⇒ x ∈ L ): Se x ∈ L(R), temos que x = w₁w₂ _... w_k, onde cada w_i ∈ L(1 ∪ 01*0). Como toda string em L(1) ou L(01*0) possui um número par de símbolos 0 (a string em L(1) com zero símbolos 0 e as strings em L(01*0) sempre com exatamente dois símbolos 0), então cada w_i tem um número par de símbolos 0. Como o número de símbolos 0 em x é igual a soma dos símbolos 0 de todas as substrings w_i e cada w_i tem um número par de símbolos 0, então x tem um número par de símbolos 0.

Provando a Volta ( x ∈ L ⇒ x ∈ L(R)): Vamos provar por indução em |x| que, x ∈ L ⇒ x ∈ L(R). Se |x| = 0, x = ε. De fato, ε ∈ L e ε ∈ L(R). Logo, a implicação é válida para x = ε.

Seja k um inteiro arbitrário maior do que zero. Suponha que, para toda string x com no máximo k − 1, x ∈ L(R). Vamos provar que, para toda string x com k símbolos, x ∈ L(R). Se x ∉ L, a implicação x ∈ L ⇒ x ∈ L(R) é verdadeira por conta da premissa falsa. Então, suponha que x ∈ L. Se x = 1^k , então claramente x ∈ L(R), visto que L(1*) ⊆ L(R).

Seja então x ∈ L uma string de tamanho k que contém pelo menos um símbolo 0. Como x ∈ L, então x tem pelo menos dois símbolos 0. Seja i a posição do penúltimo símbolo 0. Definimos a cadeia z como sendo o sufixo de x a partir da posição i e a cadeia y o prefixo até a posição i − 1 de forma que x = yz. Note que y pode ser a cadeia vazia, bastando para isso que x = z. Por essa definição, temos que z possui apenas dois símbolos 0 e inicia com um deles, ou seja, z ∈ L(01*01*) ⊆ L(1 ∪ 01*0)* = L(R).

Temos que y tem um número par de símbolos 0, pois x tem um número par de símbolos 0 e z possui dois zeros. Logo, y ∈ L. Adicionalmente, podemos afirmar que |y| < |x| visto que z não é a cadeia vazia. Portanto, usando a hipótese indutiva, podemos afirmar que y ∈ L(R). Como x = yz e y, z ∈ L(R), então x ∈ L(R) ○ L(R) = L(R).