TY - JOUR
T1 - On nominal syntax and permutation fixed points
AU - Ayala-Rincón, Mauricio
AU - Fernández, Maribel
AU - Nantes-Sobrinho, Daniele
PY - 2020/1/1
Y1 - 2020/1/1
N2 - 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 α-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 this is not the case when unifiers are expressed using freshness contexts. We provide a definition of α-equivalence modulo equational theories that takes into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.
AB - 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 α-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 this is not the case when unifiers are expressed using freshness contexts. We provide a definition of α-equivalence modulo equational theories that takes into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.
KW - Alpha-conversion
KW - Equational theories
KW - Nominal syntax
KW - Unification
UR - http://www.scopus.com/inward/record.url?scp=85082132437&partnerID=8YFLogxK
U2 - 10.23638/LMCS-16(1:19)2020
DO - 10.23638/LMCS-16(1:19)2020
M3 - Article
AN - SCOPUS:85082132437
SN - 1860-5974
VL - 16
SP - 19:1-19:36
JO - Logical methods in computer science
JF - Logical methods in computer science
IS - 1
ER -