Blog
About

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

      , ,

      Read this article at

      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.

          Related collections

          Most cited references 10

          • Record: found
          • Abstract: not found
          • Article: not found

          Nominal logic, a first order theory of names and binding

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Nominal unification

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Nominal rewriting

                Bookmark

                Author and article information

                Journal
                21 February 2019
                Article
                1902.08345

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                Custom metadata
                33 pages, 3rd International Conference for Formal Structures for Computation and Deduction
                cs.LO

                Theoretical computer science

                Comments

                Comment on this article