TY - GEN
T1 - Generalised name abstraction for nominal sets
AU - Clouston, Ranald
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - adjoint functors
KW - name binding
KW - nominal sets
UR - http://www.scopus.com/inward/record.url?scp=84874420993&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-37075-5_28
DO - 10.1007/978-3-642-37075-5_28
M3 - Conference contribution
AN - SCOPUS:84874420993
SN - 9783642370748
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 434
EP - 449
BT - Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.
T2 - 16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
Y2 - 16 March 2013 through 24 March 2013
ER -