Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0055

TitleNominal Algebra and the HSP Theorem
AuthorsMurdoch J. Gabbay, Aad Mathijssen
AbstractNominal 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 first-order logic, the lambda-calculus, or process calculi. Nominal algebra has a semantics in nominal sets (sets with a finitely-supported 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 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 paper we give the constructions which show that, after all, a ‘nominal’ version of the HSP theorem holds for nominal algebra.
GroupDependable Systems Group


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 © Copyright Heriot-Watt University, Disclaimer