| Autor: |
Ayala-Rincón, Mauricio, de Carvalho-Segundo, Washington, Fernández, Maribel, Nantes-Sobrinho, Daniele |
| Jazyk: |
angličtina |
| Rok vydání: |
2017 |
| Předmět: |
|
| Zdroj: |
Ayala-Rincón, M, de Carvalho-Segundo, W, Fernández, M & Nantes-Sobrinho, D 2017, ' A Formalisation of Nominal α-equivalence with A and AC Function Symbols : LSFA 2016-11th Workshop on Logical and Semantic Frameworks with Applications (LSFA) ', Electronic Notes in Theoretical Computer Science, vol. 332, pp. 21-38 . https://doi.org/10.1016/j.entcs.2017.04.003 |
| DOI: |
10.1016/j.entcs.2017.04.003 |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
