Nominal (universal) algebra: Equational logic with names and binding

M.J. Gabbay, A.H.J. Mathijssen

    Research output: Contribution to journalArticleAcademicpeer-review

    57 Citations (Scopus)

    Abstract

    In informal mathematical discourse (such as the text of a paper on theoretical computer science), we often reason about equalities involving binding of object-variables. We find ourselves writing assertions involving meta-variables and captureavoidance constraints on where object-variables can and cannot occur free. Formalizing such assertions is problematic because the standard logical frameworks cannot express capture-avoidance constraints directly. In this article, we make the case for extending the logic of equality with meta-variables and capture-avoidance constraints, to obtain ‘nominal algebra’. We use nominal techniques that allow for a direct formalization of meta-level assertions, while remaining close to informal practice. We investigate proof-theoretical properties, we provide a sound and complete semantics in nominal sets and we compare and contrast our design decisions with other possibilities leading to similar systems.
    Original languageEnglish
    Pages (from-to)1455-1508
    JournalJournal of Logic and Computation
    Volume19
    Issue number6
    DOIs
    Publication statusPublished - 2009

    Fingerprint

    Dive into the research topics of 'Nominal (universal) algebra: Equational logic with names and binding'. Together they form a unique fingerprint.

    Cite this