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.
Chapter PDF
Similar content being viewed by others
References
Cheney, J.: Towards a general theory of names, binding and scope. In: MERLIN, pp. 33–40. ACM (2005)
Cirstea, H., Kirchner, C.: The rewriting calculus - part I. Log. J. IGPL 9(3), 339–375 (2001)
Clouston, R.: Equational Logic for Names and Binders. Ph.D. thesis, University of Cambridge (2009)
Clouston, R., Pitts, A.M.: Nominal equational logic. ENTCS 172, 223–257 (2007)
Day, B.: On closed categories of functors. Lecture Notes in Math. 137, 1–38 (1970)
Dowek, G., Gabbay, M.J.: From nominal sets binding to functions and λ-abstraction: connecting the logic of permutation models with the logic of functions, arXiv (2011)
Fiore, M., Hur, C.K.: Term equational systems and logics. In: MFPS. ENTCS, vol. 218, pp. 171–192 (2008)
Gabbay, M.J.: A Theory of Inductive Definitions with Alpha-Equivalence. Ph.D. thesis, Cambridge University (2001)
Gabbay, M.J.: FM-HOL, a higher-order theory of names. In: 35 Years of Automath (2002)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects Comput. 13, 341–363 (2002)
Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. BEATCS 62, 222–259 (1997)
Jay, B., Kesner, D.: Pure Pattern Calculus. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 100–114. Springer, Heidelberg (2006)
Jay, B., Kesner, D.: First-class patterns. J. Funct. Program. 19, 191–225 (2009)
Kelly, G.M.: Basic concepts of enriched category theory, LMS Lecture Note Series, vol. 64. Cambridge University Press (1982)
Menni, M.: About И-quantifiers. Appl. Categor. Struct. 11(5), 421–445 (2003)
Pitts, A.M.: Nominal Logic: A First Order Theory of Names and Binding. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol. 2215, pp. 219–242. Springer, Heidelberg (2001)
Pitts, A.M.: Nominal sets, the metamathematics of names (2011) (unpublished manuscript)
Pym, D.J.: The Semantics and Proof Theory of the Logic of Buunched Implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers (2002)
Schöpp, U.: Names and Binding in Type Theory. Ph.D. thesis, University of Edinburgh (2006)
Schöpp, U., Stark, I.: A Dependent Type Theory with Names and Binding. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 235–249. Springer, Heidelberg (2004)
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: Effective tool support for the working semanticist. J. Funct. Program. 20(1), 71–122 (2010)
Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programming with binders made simple. In: ICFP. SIGPLAN Notices, vol. 38, pp. 263–274 (2003)
Tzevelekos, N.: Nominal Game Semantics. Ph.D. thesis, University of Oxford (2008)
Urban, C., Kaliszyk, C.: General Bindings and Alpha-Equivalence in Nominal Isabelle. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 480–500. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clouston, R. (2013). Generalised Name Abstraction for Nominal Sets. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)