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 rstorder logic, the lambdacalculus, or process calculi. Nominal algebra has a semantics in nominal sets (sets with a nitelysupported permutation action); previous work 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 avour of implication; nominal sets have signicantly 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; it corresponds to closure under homomorphic images, subalgebras, products, and an atomsabstraction construction specic to nominalstyle semantics.  
International

Si 
JCR

Si 
Title

JOURNAL OF LOGIC AND COMPUTATION 
ISBN

0955792X 
Impact factor JCR

0,821 
Impact info


Volume



10.1093/logcom/exn055 
Journal number

0 
From page

1 
To page

28 
Month

ENERO 
Ranking
