Mauricio Ayala-Rincón ; Maribel Fernández ; Daniele Nantes-Sobrinho - On Nominal Syntax and Permutation Fixed Points

lmcs:5209 - Logical Methods in Computer Science, February 17, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:19)2020
On Nominal Syntax and Permutation Fixed PointsArticle

Authors: Mauricio Ayala-Rincón ORCID; Maribel Fernández ORCID; Daniele Nantes-Sobrinho

    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.


    Volume: Volume 16, Issue 1
    Published on: February 17, 2020
    Accepted on: November 6, 2019
    Submitted on: February 25, 2019
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Consultation statistics

    This page has been seen 1234 times.
    This article's PDF has been downloaded 339 times.