Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.7
URN: urn:nbn:de:0030-drops-91777
URL: https://drops.dagstuhl.de/opus/volltexte/2018/9177/
Ayala-Rincón, Mauricio ; Fernández, Maribel ; Nantes-Sobrinho, Daniele
Fixed-Point Constraints for Nominal Equational Unification
| pdf-format: |
|
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 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.
BibTeX - Entry
@InProceedings{ayalarincn_et_al:LIPIcs:2018:9177,
author = {Mauricio Ayala-Rinc{\'o}n and Maribel Fern{\'a}ndez and Daniele Nantes-Sobrinho},
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 = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9177},
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}
}
| Keywords: | nominal terms, fixed-point equations, nominal unification, equational theories | |
| Seminar: | 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) | |
| Issue date: | 2018 | |
| Date of publication: | 04.07.2018 |
