2026-10-16T07:51:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9177 2024-03-06T09:43:33Z ddc:004 open_access

Fixed-Point Constraints for Nominal Equational Unification Ayala-Rincón, Mauricio Fernández, Maribel Nantes-Sobrinho, Daniele nominal terms fixed-point equations nominal unification equational theories 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 fixed-point 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mauricio Ayala-Rincón and Maribel Fernández and Daniele Nantes-Sobrinho 2018 Is Part Of LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2018.7 urn:nbn:de:0030-drops-91777 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.7 eng https://creativecommons.org/licenses/by/3.0/legalcode