Abstract | ||
---|---|---|
A formalisation of soundness of the notion of α-equivalence in nominal abstract syntax modulo associative (A) and associative-commutative (AC) equational theories is described. Initially, the notion of α-equivalence is specified based on a so called “weak” nominal relation as suggested by Urban in his nominal development in Isabelle/HOL. Then, it is formalised in Coq that this equality is indeed an equivalence relation. After that, general α-equivalence with A and AC function symbols is specified and formally proved to be an equivalence relation. As corollaries, the soundness α-equivalence modulo A and modulo AC is obtained. Finally, an algorithm for checking α-equivalence modulo A and AC is proposed. General α-equivalence problems are log-linearly solved while AC and the combination of A and AC α-equivalence problems have the same complexity as standard first-order approaches. This development is a first step towards verification of nominal matching, unification and narrowing algorithms modulo equational theories in general. |
Year | DOI | Venue |
---|---|---|
2017 | 10.1016/j.entcs.2017.04.003 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
Nominal logic,Alpha Equivalence,Equivalence modulo A and AC | HOL,Discrete mathematics,Equivalence relation,Associative property,Modulo,Unification,Equivalence (measure theory),Abstract syntax,Soundness,Mathematics | Journal |
Volume | ISSN | Citations |
332 | 1571-0661 | 0 |
PageRank | References | Authors |
0.34 | 7 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
M. Ayala-Rincón | 1 | 10 | 5.38 |
Washington de Carvalho Segundo | 2 | 0 | 1.69 |
Maribel Fernández | 3 | 0 | 3.72 |
Daniele Nantes Sobrinho | 4 | 2 | 3.08 |