Prova do algoritmo de Brzozowski para minimização do DFA?

O algoritmo de Brzozowki é amplamente citado. Várias perguntas aqui dão exemplos ou discutem sua complexidade. Mas não consegui encontrar uma prova de correção para o algoritmo. Como provamos que está correto? Qualquer prova acessível aos estudantes de ciências da computação seria muito bem-vinda.

A prova do resultado de Brzozowski é técnica, mas não muito complicada. De fato, temos apenas que considerar uma sequência de determinação de reversão, para obter o resultado mínimo que desejamos. (A primeira sequência de determinação de reversão leva a um FSA determinístico para a reversão do idioma original; a prova de minoria é para a segunda determinação de reversão.)

Primeiro, é preciso ter uma boa visão dos diferentes autômatos envolvidos. E nervos de aço.

A construção de Brzozowski. Seja um autômato determinístico para a linguagem . Assumimos que todos os estados de são alcançáveis ​​a partir do estado inicial .$A = (Q, \Sigma, \delta, q_0, F)$$L=L(A)$$Q$$q_0$

No primeiro passo, inverte-se o autômato: todas as arestas são invertidas e os estados inicial e final são trocados. Informalmente, obtemos o autômato .$\mathrm{rev}(A) = (Q, \Sigma, \delta^{-1}, F, q_0)$

Na segunda etapa, determina-se o autômato assim obtido, pela construção padrão, mas mantendo apenas estados alcançáveis. Obtemos . Os estados de são conjuntos de estados para : ; o estado inicial consiste nos estados iniciais de , que são estados finais em : ; os estados finais em são os estados que contêm um estado final para : sse .$A'= \mathrm{det}(\mathrm{rev}(A)) = (Q', \Sigma, \delta', q'_0, F')$$A'$$\mathrm{rev}(A)$$Q'\subseteq 2^Q$$\mathrm{rev}(A)$$Q$$q'_0 = F$$A'$$\mathrm{rev}(A)$$U\in F'$$q_0\in U$

A chave da prova é a seguinte relação importante entre os autômatos e .$A$$A'$

Observação básica: sse .$q\in \delta'(X,w^R)$$\delta(q,w) \in X$

Prova (apenas um lado). sse existe um estado em e um caminho de para em com a etiqueta . Mas isso significa que existe um caminho de para com o rótulo em ou ; assim . fim de prova.$q\in \delta'(X,w^R)$$p$$X$$p$$q$$\mathrm{rev}(A)$$w^R$$q$$p$$w$$A$$\delta(q,w) = p$$\delta(q,w) \in X$

Conforme anunciado, isso é usado para provar a propriedade essencial de que precisamos.

Propriedade: é mínimo (e determinístico para ).$A'$$L^R$

Prova. Sejam e dois estados em que não podem ser distinguidos. Isso significa que, para qualquer string , temos iff . Mostramos que agora e são iguais.$U$$V$$A'$$w^R$$\delta'(U,w^R) \in F'$$\delta'(V,w^R) \in F'$$U$$V$

Pela construção de , podemos reformular a indistinguibilidade como iff .$F'$$\delta'(U,w^R) \ni q_0$$\delta'(V,w^R) \ni q_0$

Aplique a observação de base, e nós temos sse .$\delta(q_0,w) \in U$$\delta(q_0,w) \in V$

A partir dessa igualdade, segue, como todos os estados em são assumidos como alcançáveis, portanto, para qualquer estado em ou há uma cadeia tal que . fim de prova.$U=V$$Q$$p$$U$$V$$w$$p = \delta(q_0,w)$

Mas mesmo depois de provar, o resultado ainda é uma mágica real!