Observatorio de I+D+i UPM

Memorias de investigación
Research Publications in journals:
Nominal Algebra and the HSP Theorem
Year:2008
Research Areas
  • Programming language
Information
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 rst-order logic, the lambda-calculus, or process calculi. Nominal algebra has a semantics in nominal sets (sets with a nitely-supported 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 so-called freshness conditions which give them some avour of implication; nominal sets have signi cantly 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 atoms-abstraction construction speci c to nominal-style semantics.
International
Si
JCR
Si
Title
JOURNAL OF LOGIC AND COMPUTATION
ISBN
0955-792X
Impact factor JCR
0,821
Impact info
Volume
10.1093/logcom/exn055
Journal number
0
From page
1
To page
28
Month
ENERO
Ranking
Participants
  • Autor: Murdoch Gabbay (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2020 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)