Document Open Access Logo

Separation and Renaming in Nominal Sets

Authors Joshua Moerman, Jurriaan Rot

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.31.pdf
  • Filesize: 0.5 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Nominal sets
  • Separated product
  • Adjunction
  • Automata
  • Coalgebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Cite As Get BibTex

Joshua Moerman and Jurriaan Rot. Separation and Renaming in Nominal Sets. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.31

Author Details

Joshua Moerman
  • RWTH Aachen University, Germany
Jurriaan Rot
  • University College London, United Kingdom and Radboud University, The Netherlands

Funding

This work was partially supported by the ERC AdG project 787914 FRAPPANT and a Marie Curie Fellowship (grant code 795119).

Acknowledgements

We would like to thank Jamie Gabbay, Gerco van Heerdt, Tom Hirschowitz, Bart Jacobs, and the anonymous reviewers for their useful comments.

References

  1. Michael Francis Atiyah and Ian G. MacDonald. Introduction to commutative algebra. Addison-Wesley-Longman, 1969. Google Scholar
  2. Mikołaj Bojańczyk. Slightly Infinite Sets. Draft May 22, 2019. URL: https://www.mimuw.edu.pl/~bojan/upload/main-9.pdf.
  3. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  4. Mikołaj Bojańczyk, Bartek Klin, Sławomir Lasota, and Szymon Toruńczyk. Turing Machines with Atoms. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 183-192. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.24.
  5. Ranald Clouston. Generalised Name Abstraction for Nominal Sets. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013. Proceedings, volume 7794 of Lecture Notes in Computer Science, pages 434-449. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37075-5_28.
  6. Gilles Dowek and Murdoch James Gabbay. PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. Theor. Comput. Sci., 451:38-69, 2012. URL: https://doi.org/10.1016/j.tcs.2012.06.007.
  7. Marcelo P. Fiore and Daniele Turi. Semantics of Name and Value Passing. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 93-104. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/LICS.2001.932486.
  8. Murdoch J. Gabbay. FM-HOL, a higher-order theory of names. Thirty Five years of Automath, Heriot-Watt University, Edinburgh, 2002. Google Scholar
  9. Murdoch J. Gabbay. Nominal Renaming Sets. Technical report, Heriot-Watt University, 2007. URL: https://www.gabbay.org/paper.html#nomrs-tr.
  10. Murdoch J. Gabbay and Martin Hofmann. Nominal Renaming Sets. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008. Proceedings, volume 5330 of Lecture Notes in Computer Science, pages 158-173. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_11.
  11. Murdoch J. Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax Involving Binders. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 214-224. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782617.
  12. Claudio Hermida and Bart Jacobs. Structural Induction and Coinduction in a Fibrational Setting. Inf. Comput., 145(2):107-152, 1998. URL: https://doi.org/10.1006/inco.1998.2725.
  13. Malte Isberner, Falk Howar, and Bernhard Steffen. Learning register automata: from languages to program structures. Machine Learning, 96(1-2):65-98, 2014. URL: https://doi.org/10.1007/s10994-013-5419-7.
  14. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  15. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859-879, 2015. URL: https://doi.org/10.1016/j.jcss.2014.12.005.
  16. Henning Kerstan, Barbara König, and Bram Westerbaan. Lifting Adjunctions to Coalgebras to (Re)Discover Automata Constructions. In Marcello M. Bonsangue, editor, Coalgebraic Methods in Computer Science - 12th IFIP WG 1.3 International Workshop, CMCS 2014, Colocated with ETAPS 2014, Grenoble, France, April 5-6, 2014, Revised Selected Papers, volume 8446 of Lecture Notes in Computer Science, pages 168-188. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44124-4_10.
  17. Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. Logical Methods in Computer Science, 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:10)2016.
  18. Alexander Kurz and Daniela Petrisan. On universal algebra over nominal sets. Mathematical Structures in Computer Science, 20(2):285-318, 2010. URL: https://doi.org/10.1017/S0960129509990399.
  19. Joshua Moerman and Jurriaan Rot. Separation and Renaming in Nominal Sets. CoRR, abs/1906.00763, 2019. Google Scholar
  20. Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski. Learning nominal automata. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 613-625. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3009879.
  21. Peter W. O'Hearn. On bunched typing. J. Funct. Program., 13(4):747-796, 2003. URL: https://doi.org/10.1017/S0956796802004495.
  22. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  23. Andrew M. Pitts. Nominal Presentation of Cubical Sets Models of Type Theory. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, 20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France, volume 39 of LIPIcs, pages 202-220. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.TYPES.2014.202.
  24. Andrew M. Pitts. Nominal techniques. SIGLOG News, 3(1):57-72, 2016. URL: https://doi.org/10.1145/2893582.2893594.
  25. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  26. Ulrich Schöpp. Names and binding in type theory. PhD thesis, University of Edinburgh, UK, 2006. URL: http://hdl.handle.net/1842/1203.
  27. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:9)2013.
  28. Harold Simmons. The topos of actions on a monoid. Unpublished manuscript, number 12N. URL: http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Rsets.pdf.
  29. Sam Staton. Name-passing process calculi: operational models and structural operational semantics. PhD thesis, University of Cambridge, Computer Laboratory, June 2007. URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-688.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact