3
views
0
recommends
+1 Recommend
0 collections
0
shares
• Record: found
• Abstract: found
• Article: found
Is Open Access

# On Nominal Syntax and Permutation Fixed Points

Preprint

Bookmark
There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

### 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. We provide a definition of $$\alpha$$-equivalence modulo equational theories that take 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.

### Most cited references10

• Record: found

### Nominal logic, a first order theory of names and binding

(2003)
Bookmark
• Record: found

### Nominal unification

(2004)
Bookmark
• Record: found

### Nominal rewriting

(2007)
Bookmark

### Author and article information

###### Journal
21 February 2019
###### Article
1902.08345