Desunificação nominal via restrições de ponto fixo

Abstract

Esta dissertação trata do Problema de Desunificação Nominal, isto é, do problema em resolver equações e desequações entre termos nominais, que são uma extensão de termos de primeira ordem com construtores para abstração de variáveis e renomeamento. Na sintaxe nominal via ponto fixo, as variáveis que podem ser abstraídas são representadas por átomos, e a igualdade entre dois termos nominais $s$ e $t$ é dada pela alfa-equivalência, denotada por $s \faleq t$, que consiste na igualdade módulo renomeamento de átomos abstraídos. Por sua vez, a alfa-equivalência é definida usando a relação de ponto fixo $\pi\fixp t$, onde $\pi$ é uma permutação e $t$ um termo nominal, implementando o fato de que $\pi\cdot t$ (a permutação $\pi$ aplicada no termo $t$) é alfa-equivalente a $t$, simbolicamente $\pi\cdot t\faleq t$. Em trabalhos recentes, esta nova abordagem mostrou-se bastante promissora para o tratamento de teorias equacionais no contexto nominal. Com o objetivo de investigar em trabalhos futuros os problemas de desunificação nominal módulo teorias equacionais, neste trabalho propomos uma extensão do método para resolução do problema de desunificação nominal utilizando a abordagem de ponto fixo: reformulamos os conceitos necessários para especificação do problema; provamos propriedades sintáticas; e finalmente, apresentamos o algoritmo $\disunifyFP$: um algoritmo (provado correto) para computar uma representação finita e completa de soluções para o problema de desunificação nominal.