Nominal algebra and the HSP theorem

Research output: Contribution to journalArticle

21 Citations (Scopus)

Abstract

Nominal algebra is a logic of equality developed to reason algebraically in the presence of binding. In previous work, it has been shown how nominal algebra can be used to specify and reason algebraically about systems with binding, such as first-order logic, the ?-calculus or process calculi. Nominal algebra has a semantics in nominal sets (sets with a finitely supported permutation action); previous work proved soundness and completeness. The HSP theorem characterizes the class of models of an algebraic theory as a class closed under homomorphic images, subalgebras and products, and is a fundamental result of universal algebra. It is not obvious that nominal algebra should satisfy the HSP theorem: nominal algebra axioms are subject to so-called freshness conditions which give them some flavour of implication; nominal sets have significantly richer structure than the sets semantics traditionally used in universal algebra. The usual method of proof for the HSP theorem does not obviously transfer to the nominal algebra setting. In this article, we give the constructions which show that, after all, a 'nominal' version of the HSP theorem holds for nominal algebra; it corresponds to closure under homomorphic images, subalgebras, products and an atoms-abstraction construction specific to nominal-style semantics.

Original languageEnglish
Pages (from-to)341-367
Number of pages27
JournalJournal of Logic and Computation
Volume19
Issue number2
DOIs
Publication statusPublished - 2009

Keywords

  • Equational logic
  • HSP or Birkhoffs theorem
  • Nominal algebra
  • Nominal sets
  • Nominal terms
  • Universal algebra

Fingerprint Dive into the research topics of 'Nominal algebra and the HSP theorem'. Together they form a unique fingerprint.

  • Cite this