A formalisation of nominal α-equivalence with A, C, and AC function symbols

Maurício Ayala-Rincón; Washington de Carvalho-Segundo; Maribel Fernández; Daniele Nantes-Sobrinho; Ana Cristina Rocha-Oliveira

doi:10.1016/j.tcs.2019.02.020

A formalisation of nominal α-equivalence with A, C, and AC function symbols

Maurício Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández, Daniele Nantes-Sobrinho, Ana Cristina Rocha-Oliveira

Universidade de Brasilia

Research output: Contribution to journal › Article › peer-review

12 Citations (Scopus)

165 Downloads (Pure)

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(n ² 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.

Original language	English
Pages (from-to)	3-23
Journal	Theoretical Computer Science
Volume	781
Early online date	1 Mar 2019
DOIs	https://doi.org/10.1016/j.tcs.2019.02.020
Publication status	Published - 16 Aug 2019

Keywords

Alpha equivalence
Equivalence modulo A, C and AC axioms
Nominal syntax

Access to Document

10.1016/j.tcs.2019.02.020

A formalisation of nominal_AYALA-RINCON_Accepted23Feb2019 Epub1Mar2019_GREEN AAMAccepted author manuscript, 1.42 MBLicence: CC BY-NC-ND

Cite this

@article{ddca7ec50d1842a98e4a285b1cc5534f,

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(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. ",

keywords = "Alpha equivalence, Equivalence modulo A, C and AC axioms, Nominal syntax",

author = "Maur{\'i}cio Ayala-Rinc{\'o}n and {de Carvalho-Segundo}, Washington and Maribel Fern{\'a}ndez and Daniele Nantes-Sobrinho and Rocha-Oliveira, {Ana Cristina}",

year = "2019",

month = aug,

day = "16",

doi = "10.1016/j.tcs.2019.02.020",

language = "English",

volume = "781",

pages = "3--23",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - A formalisation of nominal α-equivalence with A, C, and AC function symbols

AU - Ayala-Rincón, Maurício

AU - de Carvalho-Segundo, Washington

AU - Fernández, Maribel

AU - Nantes-Sobrinho, Daniele

AU - Rocha-Oliveira, Ana Cristina

PY - 2019/8/16

Y1 - 2019/8/16

N2 - 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.

AB - 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.

KW - Alpha equivalence

KW - Equivalence modulo A, C and AC axioms

KW - Nominal syntax

UR - http://www.scopus.com/inward/record.url?scp=85062263381&partnerID=8YFLogxK

UR - https://nms.kcl.ac.uk/maribel.fernandez/papers/fornaeACAC.pdf

U2 - 10.1016/j.tcs.2019.02.020

DO - 10.1016/j.tcs.2019.02.020

M3 - Article

SN - 0304-3975

VL - 781

SP - 3

EP - 23

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

A formalisation of nominal α-equivalence with A, C, and AC function symbols

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this