A Formalisation of Nominal α -equivalence with A and AC Function Symbols | Zendy

Maurício Ayala-Rincón | Zendy; Washington Luís Ribeiro de Carvalho Segundo | Zendy; Maribel Fernández | Zendy; Daniele Nantes-Sobrinho | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Formalisation of Nominal α -equivalence with A and AC Function Symbols

Author(s) -

Maurício Ayala-Rincón,

Washington Luís Ribeiro de Carvalho Segundo,

Maribel Fernández,

Daniele Nantes-Sobrinho

Publication year - 2017

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2017.04.003

Subject(s) - modulo , soundness , mathematics , equivalence (formal languages) , associative property , equivalence relation , logical equivalence , commutative property , unification , discrete mathematics , pure mathematics , algebra over a field , computer science , programming language

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research