Generalized Name Abstraction for Nominal Sets

Abstract

The Gabbay-Pitts nominal sets model provides a framework for reasoning with names in abstract syntax. It has appealing semantics for name binding, via a functor mapping each nominal set to the 'atom-abstractions' of its elements. We wish to generalise this construction for applications where sets, lists, or other patterns of names are bound simultaneously. The atom-abstraction functor has left and right adjoint functors that can themselves be generalised, and their generalisations remain adjoints, but the atom-abstraction functor in the middle comes apart to leave us with two notions of generalised abstraction for nominal sets. We give new descriptions of both notions of abstraction that are simpler than those previously published. We discuss applications of the two notions, and give conditions for when they coincide.