A formalisation of nominal α-equivalence with A, C, and AC function symbols
| Autor: | Daniele Nantes-Sobrinho, Maribel Fernández, Washington de Carvalho-Segundo, Ana Cristina Rocha-Oliveira, Mauricio Ayala-Rincón |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Soundness
Discrete mathematics Equivalence modulo A C and AC axioms General Computer Science Unification Modulo 0102 computer and information sciences 02 engineering and technology 01 natural sciences Theoretical Computer Science Nominal syntax 010201 computation theory & mathematics Bounded function 0202 electrical engineering electronic engineering information engineering Equivalence relation 020201 artificial intelligence & image processing Alpha equivalence Equivalence (formal languages) Commutative property Associative property Mathematics |
| Zdroj: | Ayala-Rincón, M, de Carvalho-Segundo, W, Fernández, M, Nantes-Sobrinho, D & Rocha-Oliveira, A C 2019, ' A formalisation of nominal α-equivalence with A, C, and AC function symbols ', Theoretical Computer Science, vol. 781, pp. 3-23 . https://doi.org/10.1016/j.tcs.2019.02.020 |
| ISSN: | 0304-3975 |
| Popis: | 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(n 2 log 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. 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: |
|
Full Text from ScienceDirect