King's College London

Research portal

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

Research output: Contribution to journalArticlepeer-review

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

Original languageEnglish
Pages (from-to)3-23
JournalTheoretical Computer Science
Early online date1 Mar 2019
Accepted/In press23 Feb 2019
E-pub ahead of print1 Mar 2019
Published16 Aug 2019


King's Authors


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.

Download statistics

No data available

View graph of relations

© 2020 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454