A Name Abstraction Functor for Named Sets

AbstractThe problem of defining fully abstract operational models of name passing calculi has been given some elegant solutions, such as coalgebras over presheaf categories or over nominal sets. These formalisms fail to model garbage collection of unused names, hence they do not have nice properties with respects to finite state algorithms. The category of named sets, on the other hand, was designed for the purpose of supporting efficient algorithms to handle the semantics of name passing calculi. However the theory was developed in a rather ad-hoc fashion (e.g. the existence of a final coalgebra was only proved in the finite case). In this work we introduce a name abstraction functor for named sets and show that it provides a simple and effective notion of garbage collection of unused names. Along the way, we survey a number of needed results on the category of permutation algebras, an algebra-theoretic definition of nominal sets. In particular we give a formalization of the adjunction between abstraction and concretion, an example illustrating a nominal syntax alike handling of De Bruijn indexes, and an explicit functor to model the early semantics of the π-calculus in nominal sets