Desunificação Nominal via Ponto Fixo

Resumo


Este é um trabalho em andamento sobre a resolução de equações e diferenças entre termos nominais, chamado de problema de desunificação nominal. Ao invés de usarmos as técnicas nominais padrões que envolvem restrições de freshness (i.e., expressões da forma a#t que significa "o átomo a não ocorre livre em t'') para implementar alpha-equivalência, seguiremos uma abordagem alternativa que envolve equações de ponto fixo, i.e., equações da forma pi.t=_\alpha t, onde t é um termo nominal e pi uma permutação. Essa abordagem será conveniente a futuras extensões do problema envolvendo teorias equacionais.
Palavras-chave: desunificação nominal, ponto fixo, técnicas nominais

Referências

Ayala-Rincón, M., de Carvalho Segundo, W., Fernández, M., and Nantes-Sobrinho, D.(2017). On solving nominal fixpoint equations. In Front. of Combining Systems - 11th Int. Symp., FroCoS 2017, Proc., volume 10483 of LNCS, pages 209–226. Springer.

Ayala-Rincón, M., Fernández, M., and Nantes-Sobrinho, D. (2020a). On nominal syntax and permutation fixed points. Log. Methods Comput. Sci., 16(1).

Ayala-Rincón, M., Fernández, M., Nantes-Sobrinho, D., and Vale, D. (2020b). On solving nominal disunification constraints. In Proc. of the 14th Work. on Logical and Semantic Frameworks with Applications, LSFA 2019, volume 348 of ENTCS, pages 3–22.

Buntine, W. L. and Bürckert, H. (1994). On solving equations and disequations. J. ACM, 41(4):591–629.

Comon, H. and Lescanne, P. (1989). Equational problems and disunification. J. Symb. Comput., 7(3/4):371–425.

Fernández, M. and Gabbay, M. (2007). Nominal rewriting. Inf. Comput., 205(6):917–965.

Gabbay, M. and Pitts, A. M. (2002). A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341–363.

Pitts, A. M. (2013). Nominal Sets: Names and Symmetry in Computer Science. CUP.

Urban, C., Pitts, A. M., and Gabbay, M. (2004). Nominal unification. Theor. Comput. Sci., 323(1-3):473–497.
Publicado
18/07/2021
Como Citar

Selecione um Formato
BATISTA, Leonardo; NANTES-SOBRINHO, Daniele . Desunificação Nominal via Ponto Fixo. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 2. , 2021, Evento Online. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2021 . p. 9-16. ISSN 2763-8731. DOI: https://doi.org/10.5753/wbl.2021.15773.