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.
@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2018.7, author = {Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele}, title = {{Fixed-Point Constraints for Nominal Equational Unification}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {7:1--7:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.7}, URN = {urn:nbn:de:0030-drops-91777}, doi = {10.4230/LIPIcs.FSCD.2018.7}, annote = {Keywords: nominal terms, fixed-point equations, nominal unification, equational theories} }
Feedback for Dagstuhl Publishing