Skip navigation
Use este identificador para citar ou linkar para este item: http://repositorio.unb.br/handle/10482/34780
Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
EVENTO_FixedPointConstraints.pdf686,28 kBAdobe PDFVisualizar/Abrir
Título: Fixed-point constraints for nominal equational unification
Autor(es): Ayala-Rincón, Mauricio
Fernández, Maribel
Nantes Sobrinho, Daniele
Assunto: Termos nominais
Equações de ponto fixo
Unificação nominal
Teoria de equações
Data de publicação: 2018
Editora: Daugstuhl research Online Publishing Server
Referência: AYALA-RINCÓN, Mauricio; FERNÁNDEZ, Maribel; NANTES SOBRINHO, Daniele. Fixed-point constraints for nominal equational unification. In: INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION, 3., 2018, Dagstuhl - Germany. Proceedings [...]. Dagstuhl - Germany: Daugstuhl research Online Publishing Server, 2018. DOI: 10.4230/LIPIcs.FSCD.2018.7. Disponível em: http://drops.dagstuhl.de/opus/volltexte/2018/9177/. Acesso em: 11 jun. 2019.
Abstract: We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new alpha-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixedpoint constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts.
Unidade Acadêmica: Instituto de Ciências Exatas (IE)
Departamento de Matemática (IE MAT)
Licença: © Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho; licensed under Creative Commons License CC-BY.
DOI: 10.4230/LIPIcs.FSCD.2018.7
Aparece nas coleções:Trabalhos apresentados em evento

Mostrar registro completo do item Visualizar estatísticas



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.