A Formalisation of Nominal a equivalence with A and AC Function Symbols
Abstract A formalisation of soundness of the notion of a equivalence in nominal abstract syntax modulo associative (A) and associative commutative (AC) equational theories is described. Initially, the notion of a 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 a equivalence with A and AC function symbols is specified and formally proved to be an equivalence relation. As corollaries, the soundness a equivalence modulo A and modulo AC is obtained. Finally, an algorithm for checking a equivalence modulo A and AC is proposed. General a equivalence problems are log linearly solved while AC and the combination of A and AC a 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.
LSFA