Desunificação nominal via restrições de ponto fixo
Autor(a)
Batista, Leonardo Melo
Orientador(a) Coorientador(a)
Nantes Sobrinho, Daniele
Data de aceite
2022-01-11
Data de disponibilizacao
2022-01-11
Data de publicacao
2022-01-11
Data de defesa submissao
2021-09-28
Citacao
BATISTA, Leonardo Melo. Desunificação Nominal via Restrições de Ponto Fixo. 2021. 110 f., il. Dissertação (Mestrado em Matemática)—Universidade de Brasília, Brasília, 2021.
Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2021.
Resumo Portugues
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.
Resumo Ingles
This work is about the Nominal Disunification Problem, that is, the problem of solving
equations and disequations between nominal terms, which are extensions of first-order
terms with constructors for variable abstraction and renaming. In the nominal syntax via
fixed points, variables that can be abstracted are represented by atoms, and equality
between two nominal terms $s$ and $t$ is given by alpha-equivalence, denoted by
$s\faleq t$, and consists of equality modulo renaming of abstracted atoms. In turn,
alpha-equivalence is defined using the fixed point relation, $\pi\fixp t$, where $\pi$ is a
permutation of atoms and $t$ is a nominal term, and implements the fact that $\pi\cdot
t$ (permutation $\pi$ applied on term $t$) is alpha-equivalent to $t$, symbolically
$\pi\cdot t\faleq t$. In recent works, this new approach has proven to be quite promising
for the treatment of equational theories in the nominal context. With the aim of
investigating nominal disunification problems modulo equational theories, in this work
we propose na extension of the method for solving the nominal disunification problems
using the fixed point approach: we reformulate the necessary concepts for the
specification of the problem; we prove the necessary syntactic properties; and finally,
we present the algorithm $\disunifyFP$: na algorithm (proven correct) to compute a
finite and complete representation of solutions for the nominal disunification problem.
Unidade academica
Instituto de Ciências Exatas (IE)
Departamento
Departamento de Matemática (IE MAT)
Programa de Pos-Graduacao
Programa de Pós-Graduação em Matemática
Agencia financiadora
Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) e Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES).
Idioma
por
Tipo de documento
Dissertação
Formato
application/pdf
Direitos de acesso
Acesso Aberto
Termo de licenca
A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br,www.ibict.br,http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.
