eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-07-04
7:1
7:16
10.4230/LIPIcs.FSCD.2018.7
article
Fixed-Point Constraints for Nominal Equational Unification
Ayala-Rincón, Mauricio
1
Fernández, Maribel
2
Nantes-Sobrinho, Daniele
1
Departments of Mathematics and Computer Science, Universidade de Brasília, Brasília, Brazil
Department of Informatics, King’s College London, London, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol108-fscd2018/LIPIcs.FSCD.2018.7/LIPIcs.FSCD.2018.7.pdf
nominal terms
fixed-point equations
nominal unification
equational theories