FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Fixed-Point Constraints for Nominal Equational Unification

Authors: Mauricio Ayala-Rincon, Maribel Fernandez and Daniele Nantes-Sobrinho

Paper Information

Title:Fixed-Point Constraints for Nominal Equational Unification
Authors:Mauricio Ayala-Rincon, Maribel Fernandez and Daniele Nantes-Sobrinho
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:alpha-equivalence, nominal terms, fixed point equations, equational theories, nominal unification
Abstract:

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. This notion of nominal unifier behaves better than the standard notion based on freshness contexts: nominal unification remains finitary in the presence of equational theories such as commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts.

Pages:16
Talk:Jul 12 11:00 (Session 74B: Unification)
Paper: