Paper Info
Title
A formalisation of nominal -equivalence with A, C, and AC function symbols.
Abstract
This paper describes a formalisation in Coq of nominal syntax extended with associative (A), commutative (C) and associative-commutative (AC) operators. This formalisation is based on a natural notion of nominal α-equivalence, avoiding the use of an auxiliary weak α-relation used in previous formalisations of nominal AC equivalence. A general α-relation between terms with A, C and AC function symbols is specified and formally proved to be an equivalence relation. As corollaries, one obtains the soundness of α-equivalence modulo A, C and AC operators. General α-equivalence problems with A operators are log-linearly bounded in time while if there are also C operators they can be solved in O(n2log⁡n); nominal α-equivalence problems that also include AC operators can be solved with the same running time complexity as in standard first-order AC approaches.
Year
DOI
Venue
2019
10.1016/j.tcs.2019.02.020
Theoretical Computer Science
Keywords
DocType
Volume
Nominal syntax,Alpha equivalence,Equivalence modulo A, C and AC axioms
Journal
781
ISSN
Citations 
PageRank 
0304-3975
0
0.34
References 
Authors
0
5
Name
Order
Citations
PageRank
M. Ayala-Rincón1105.38
Washington de Carvalho Segundo201.69
Maribel Fernández303.72
Daniele Nantes Sobrinho423.08
Ana Cristina Rocha Oliveira592.43