Implementação do algoritmo de decisão para a equivalência de res.

Vivam! Este pdf serve como um documento que vos explique qual a minha ideia para implementar o algoritmo de decisão para as res. Na realidade, a ideia na sua essência não é minha. É sim a adaptação de um dos 4 métodos standard para a implementação de programas recursivos gerais na framework dos programas dotados de recursão estrutural, como é o caso do Coq. O método é o da construção de um iterador e está descrito na secção 15.3 do Coq'Art.

Ideia do método

A ideia desta técnica é seguir os seguintes três passos:

• determinar o funcional associado à função recursiva que se pretende implementar;
• demonstrar que a função recursiva termina, ou é uma função total. Para tal usa-se o apenas funcional definido no ponto anterior;
• construir a função alvo, usando os dois itens anteriores.

Escolhi esta tecnica porque me parece mais apropriada para codificar lemas que se referem a certos pontos do fluxo de execução do algoritmo de decisção. Um exemplo é a necessidade de provar que se um determinado valor pertence ao conjunto de expressões regulares S ainda por tratar, numa determinada iteração do algoritmo, então pentende ao histórico H na iteracção ou então numa iteração , o valor irá passar a constar do histórico H.

O truque desta técnica está em usar indução bem fundada para descrever de forma estruturalmente decrescente as várias iterações do algoritmo. Esta descrição é, na realidade, codificada como termos do predicado Acc, que representa a noção de acessibilidade numa cadeia finita decrescente de valores.

Agora vou passar a descrever os vários componentes que necessitei de codificar para que a implementação do algoritmo siga, o mais à risca possível, os passos da descrição feita no Coq'Art.

Funções úteis

O algoritmo para a decisão da equivalência de res. (trate-mo-lo a partir de agora com AREdec) resume-se ao seguinte comportamento (simplificado): primeiro, e dadas duas res, decorre uma pequena fase de inicialização de variáveis :

• inicializa um conjunto S com um par contendo as duas res. dadas como argumentos. Este conjunto irá conter ao longo da execução todos os pares que ainda não foram tratados.
• inicialização de um conjunto vazio H que ao longo das interções de AREdec irá acumular todos os pares já "tratatos". Uma vez que um determinado par é adicionado a H, caso volte a ser considerado em futuras iterações do algoritmo, é imediatamente ignorado e é considerado um novo valor de S. Esta restrição evita que AREdec entre em ciclo, pois não existe repetição de pares e também porque H tem um número finito de elementos.

De seguida, dá-se início ao seguinte ciclo, que termina em duas situações:

• o conjunto S fica vazio e portanto não existem mais pares a serem processados;
• é encontrado um par onde não existe partilha de linguagem constante.

Caso nenhum dos casos anteriores ocorra, um novo conjunto de res será produzido por derivação dos símbolos em , todo ele disjunto de H e apenas no caso de o par a ser considerado não exista já em H. Este processo repete-se o número de vezes suficiente até se registar a ocorrência de uma das condições de terminação, ocorrência esta que surge sempre num número finito (e limitado) de vezes.

De seguida vou apresentar as funções que vão permitir construir os vários pontos acima.

Partilha da linguagem constante

Por partilha de linguagem constante entre dois conjuntos de res. entende-se que ou ambos os conjuntos aceitam a linguagem vazia , ou nenhum dos conjuntos a aceita. Esta função é fundamental para encontrar contra-exemplos no cálculo da equivalência de duas res. Do resultado da função f_c_of_re_pair, definida abaixo, é possível construír uma proposição que exibe o facto de as res. dadas como argumento não serem equivalentes.

Adição condicional de novos pares

Já foi acima referido que novos pares que já tenham sido processador em iterações anteriores do algoritmo, i.e., elementos de H, não considerados. Esta restrição aplica-se quando se constroem os novos pares de derivadas com base no alfabeto . A geração das derivadas é implementada através de um fold da lista que representa , e cuja função a aplicar é a adição de novos elementos que não estejam já presentes no histórico.

A função anterior devolve a função de adição de um novo elemento a um qualquer conjunto, considerando que não se encontra no histórico H. Essa função é depois utilizada na função genDrvs que produz novos pares de conjuntos de derivadas de res.

Pares possíveis

A prova da terminação do AREdec assenta no facto de o número de possíveis combinações de derivadas de um qualquer par de res é sempre finito e limitado pelo número de símbolos existentes em e . A totalidade dos pares possíveis de conjuntos de derivadas de um par e dados pelas seguintes duas funções:

Agora são apresentadas algumas das propriedades lógicas importantes que estão relacionadas com as produção de novos pares de derivadas. Essas propriedades são as seguintes:

• as derivadas de um par de conjuntos com um só elemento é sub-conjunto de todos os pares de derivadas por um símbolo

• para cada novo par de conjuntos de res. produzido por genDrvs é possível saber qual o símbolo que originou a derivada que corresponde a

• todos os novos pares produzidos a partir de um par da totalidade dos pares de derivadas são elementos deste último. Esta propriedade garante a finitude dos elementos que podem ser considerados ao longo de toda a execução de AREdec

Geração de novos pares a serem considerados

Usando a definição genDrvs introduzida na secção anterior, podemos agora finalizar a função que produz novos pares de derivadas que poderão a ser processados no futuro pelo algoritmo. Assim, a função genDrvsPairs devolve um valor parcial, dependendo do resultado da partilha da linguagem constante dos conjuntos de res. dados como argumento. Caso não partilhem a mesma linguagem constante, é devolvido o termo None que determina que um contra-exemplo foi encontrado. Caso contrário, é devolvida um termo que é o resultado da execução de genDrvs, isto é, um conjunto de pares de derivadas não presentes no histórico H.

O seguinte lema dá-nos a análise de casos possíveis para o reultado da execução de genDrvPairs, que no caso afirmativo também fornece uma prova de que os termos que constituem o resultado são um subconjunto da totalidade das derivadas. O termo que define o caso negativo não está ainda completo. Na versão final erá ser substituido por um tipo- que contém um certificado de que o facto do par que foi processado não partilhar a linguagem constante implica a não equivalência das respectivas res.

Agora implementamos uma função que descreve uma iteração do algoritmo. O resultado vai ser um triplo, cujos componentes são:

• um valor booleano parcial, estabelecendo se deve ou não existir uma nova iteração e, no caso de terminação, devolver o valor correspondente à avaliação da equivalência das res. dadas como argumentos;
• o conjunto actualiazado de para serem processados na próxima iteração do algoritmo ;
• o histórico dos pares já processados

O código é o seguinte:

Pares de res. certificados

Agora define-se a estrutura de dados a usar no algoritmo. Basicamente corresponde a um triplo , onde as variáveis , e definem, respectivamente, o indicador de uma nova iteração do algoritmo, ou a terminação do mesmo; o conjunto de pares que ainda podem vir a ser considerados pelo algoritmo antes de este terminar; o histórico de pares já processados pelo algoritmo. Juntamente com estas variáveis, o tiplo algT incluí provas da finitude e correcção dos pares considerados em cada iteração do algoritmo.

Como vimos anteriormente, existe uma fase de inicialização do algoritmo AREdec. Essa inicialização prende-se com a criação dos conjuntos Stack e History, o primeiro contendo o par formado pelas res. dadas como argumento ao algoritmo de decisão e o segundo sendo vazio.

Agora é a definição da execução de uma iteração do algoritmo. Esta função implica a construção de demonstrações que garantem a boa formação dos elementos que irão dar origem à veracidade ou não da equivalência das res. r1 e r2

Definição do funcional

Agora definimos o funcional que define a iteração do algoritmo um determinado número de vezes. O funcional termina pois está definido por indução estrutural no número natural que determina o número de iterações a executar.

Agora seguem-se alguns lemas que definem a especificação lógica da função alg_step.

Invariants of the constant language for pairs of re sets