
Technical Report HWMACSTR0055
Title  Nominal Algebra and the HSP Theorem 

Authors  Murdoch J. Gabbay, Aad Mathijssen 

Date  20071105 

Abstract  Nominal algebra is a logic of equality developed to reason algebraically
in the presence of binding. In previous work the authors have shown
how nominal algebra can be used to specify and reason algebraically about systems with binding, such as firstorder logic, the lambdacalculus, or process calculi.
Nominal algebra has a semantics in nominal sets (sets with a finitelysupported
permutation action) and in previous work the authors proved soundness and
completeness.
The HSP theorem characterises 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 socalled 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 paper we give the constructions which show that, after all, a ‘nominal’ version of the HSP theorem holds for nominal algebra. 

Group  Dependable Systems Group 

Notes  

Download  


