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

Antes de entramos mais em detalhes sobre o conteúdo, vamos definir primeiro algumas observações.

Definições, notações e propriedades

Seja M = (Q, Σ, δ, q₀, F) um AFD. Para qualquer cadeia x em Σ, ˆδ(q, x) denota o estado que M estará ao ler a cadeia x supondo que ele está atualmente no estado q;
Se a premissa A é falsa, a implicação A ⇒ B é verdadeira, não importando qual seja a conclusão B;
O resto da divisão de um natural qualquer por um natural y é sempre um natural maior ou igual a 0 e menor ou igual a y − 1;
Se x deixa resto r quando dividido por y, temos que x + 1 deixa resto r + 1 quando dividido por y se r < y − 1, ou deixa resto 0 quando dividido por y se r = y − 1.

Corretude de AFDs

Seja M um autômato finito e L uma linguagem. Dizemos que M é correto em relação à L, se L = L(M), ou seja, se M reconhece L. Quando L está clara pelo contexto, podemos dizer apenas que M é correto. Compreender como provar a corretude de um autômato finito é crucial para o cientista da computação por várias razões como:

Verificação de funcionalidade: Provar a corretude de um autômato finito garante que ele realiza com precisão a tarefa para a qual foi projetado. Isso é essencial em aplicações onde a contabilidade e a precisão são críticas, como em compiladores, design de protocolos de rede e sistemas de controle automatizados;
Detecção de erros e depuração: Uma prova formal de corretude pode ajudar a identificar e corrigir erros no design do autômato. Ao verificar sistematicamente cada aspecto da operação do autômato, os desenvolvedores podem garantir que todos os estados e transições possíveis sejam tratados corretamente;
Otimização: Compreender a prova de correção também pode levar a oportunidades de otimização. Uma vez que a correção é estabelecida, pode-se explorar maneiras de tornar o autômato mais eficiente sem comprometer sua funcionalidade; e
Fundamentos teóricos: Autômatos finitos são modelos fundamentais na ciência da computação teórica. Provar sua correção ajuda a reforçar o entendimento teórico desses modelos e suas aplicações. Esse conhecimento é fundamental para estudar modelos e linguagens computacionais mais complexos como a Máquina de Turing.

Para provar que um autômato M é correto em relação a uma linguagem L, é necessário provar que L = L(M), ou seja, é necessário provar que x ∈ L(M) se e somente se x ∈ L. A prova de corretude de AFDs normalmente são menos complexas do que a de AFNs. Nesta nota de aula, serão trabalhados apenas a corretude de AFDs e, portanto, daqui em diante, todos os autômatos finitos são AFDs.

Mais especificamente, para provar a corretude de um AFD, é preciso que se saiba a função que cada um dos seus estados desempenha na aceitação de uma cadeia. Em outras palavras, para provar a corretude de um AFD M = (Q, Σ, δ, q₀, F), é fundamental que seja estabelecido, quando necessário, que propriedades uma cadeia x deve ter para que ˆδ(q₀, x) = q para cada q ∈ Q. Cada propriedade normalmente (mas não obrigatoriamente sempre) tem a forma " ˆδ(q₀, x) = q ⇒ x tem uma propriedade P".

Uma vez estabelecida as implicações acima, a técnica de indução estrutural na cadeia x, ou indução finita no tamanho da cadeia x, deve ser usada para prová-las. O caso base consiste na cadeia ε. Nesse caso, temos que provar que cada implicação " ˆδ(q0, x) = q ⇒ x tem uma propriedade P" é verdadeira para x = ε. Assim, no caso base, as implicações são sempre verdadeiras por conta da hipótese falsa, exceto para o estado inicial. No passo indutivo, considerando uma cadeia x arbitrária de tamanho maior do que zero, deve-se supor a hipótese indutiva, ou seja, deve-se supor que todas as implicações são verdadeiras para qualquer cadeia de tamanho menor do que x (se a prova for por indução no tamanho de x), ou para a cadeia w, onde x = wa e a é o último símbolo de x (se a prova for por indução estrutural).

Provadas as propriedades, elas podem então serem utilizadas para provar a corretude do autômato. Para isso, são provadas a implicações x ∈ L(M) ⇒ x ∈ L e a implicação x ∉ L(M) ⇒ x ∉ L. A prova da implicação x ∈ L(M) ⇒ x ∈ L é feita normalmente de forma direta, iniciando com x ∈ L(M). Disto temos que, após ler a cadeia x, o autômato deve estar em um estado de aceitação. Podemos então usar as implicações provadas para os estados de aceitação para obter propriedades sobre x e, usando tais propriedades, concluir que x ∈ L.

A implicação x ∉ L(M) ⇒ x ∉ L também é normalmente provada de forma direta, iniciando com x ∉ L(M). Disto, temos então que, após ler a cadeia x, o autômato deve estar em um estado que não é de aceitação. Analisando cada possível estado que o AFD pode ter parado, podemos então novamente usar as implicações para os estados que não são de aceitação para obter propriedades para x e, usando tais propriedades, concluir que x ∉ L.

Exemplo

Considere a linguagem L = {0 n | n ≥ 0} sob o alfabeto Σ = {0, 1}. A seguir, temos um AFD M que reconhece L:

Primeiramente, vamos provar as seguinte propriedades usando indução estrutural:

(1) ˆδ(q₁, x) = q₁ ⇒ x = 0ⁿ para algum n ≥ 0;

(2) ˆδ(q₁, x) = q₂ ⇒ x contém um símbolo 1.

Caso base (x = ε): Temos que ˆδ(q₁, ε) = q₁ e, de fato, x = ε = 0⁰ . Com isso, a implicação (1) está provada. Adicionalmente, temos que ˆδ(q₁, ε) ≠ q₂. Logo, como sua premissa é falsa, a implicação (2) está provada.

Passo Indutivo: Seja x = wa, onde w é uma cadeia no alfabeto Σ e a ∈ Σ é um símbolo do alfabeto. Suponha que as implicações (1) e (2) são válidas para w. Vamos provar que também são válidas para x.

Vamos provar (1) para x. Suponha que ˆδ(q₁, x) = q₁. Nesse caso, note que a = 0, ou seja, x = w0, pois não há transição com o símbolo 1 chegando ao estado q₁. Como ˆδ(q₁, x) = q₁ e x = w0, temos que ˆδ(q₁, w0) = q₁, ou seja, partindo de q₁, a última transição após ler x é uma transição com o símbolo 0 chegando em q₁. No entanto, a única transição com o símbolo 0 que chega em q₁ parte do próprio estado q₁. Assim, podemos inferir que o autômato estava no estado q₁ antes de pegar a transição com o símbolo 0 para chegar novamente no estado q₁, ou seja, ˆδ(q₁, w) = q₁. Pela nossa hipótese indutiva, aplicando (1) à w, temos que w = 0^k para algum k ≥ 0. Como x = w0, temos que x = 0^k+1. Logo, x = 0ⁿ para algum n ≥ 0. Com isso, concluímos a prova da implicação (1) para x.

Agora, vamos provar (2) para x. Suponha que ˆδ(q₁, x) = q₂. Se a = 1, temos que x = w₁ e, portanto, x contém um símbolo 1 (o seu último símbolo), provando diretamente a implicação (1) sem necessidade de argumentação adicional. Por outro lado, se a = 0, temos que x = w0. Como ˆδ(q₁, x) = q₂ e x = w0, temos que ˆδ(q₁, w0) = q₂, ou seja, partindo de q₁, a última transição após ler x é uma transição com o símbolo 0 chegando em q₂. No entanto, a única transição com o símbolo 0 que chega em q₂ parte do próprio estado q₂. Assim, podemos inferir que o autômato estava no estado q₂ antes de usar a transição com o símbolo 0 para chegar novamente no estado q₂, ou seja, ˆδ(q₁, w) = q₂. Pela nossa hipótese indutiva, aplicando a implicação (2) à w, temos que w possui um símbolo 1 e, consequentemente, x também possui um símbolo 1, pois x = w0. Com isso, concluímos a prova da implicação (2) para x.

Provadas as implicações (1) e (2), agora vamos provar que L(M) = L. Para provar essa igualdade, basta provarmos que x ∈ L(M) se e somente se x ∈ L. Se x ∈ L(M), então ˆδ(q₁, x) = q₁, visto que q₁ é o único estado de aceitação de M. Então, pela implicação (1), temos que x = 0ⁿ para algum n ≥ 0. Portanto, x ∈ L. Por outro lado, se x ∉ L(M), ˆδ(q₁, x) = q₂, visto que esse é o único estado de M que não é de aceitação. Assim, pela implicação (2), temos que x contém um símbolo 1. Portanto, temos que x ∉ L, visto que L não possui nenhuma cadeia que contém o símbolo 1.