Document Open Access Logo

A Data Type of Intrinsically Plane Graphs in Agda

Authors Malin Altenmüller , Conor Titania Mc Bride

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.13.pdf
  • Filesize: 2.72 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Mathematics of computing → Graphs and surfaces
  • Theory of computation → Rewrite systems
Keywords
  • planar graph
  • spanning tree
  • dependent types
  • graph rewriting

Metrics

Abstract

This work develops a suitable data type for plane graph embeddings in Agda. Graphs are used as combinatorial representations for string diagrams, a graphical calculus for monoidal categories. Whenever a monoidal theory does not include any symmetry or braiding operations, it describes processes that are sensitive to their topology. To encode this information in the graphical language, we have to consider surface-embeddings of graphs. We study the simplest case, plane graphs, and present their implementation in Agda. We overcome issues like the cyclic nature of a graph by using one of its spanning trees as an underlying inductive structure. The graphs we implement are plane by construction and any operation on them is guaranteed to preserve this planarity. Additionally, we present a notion of focussing on a certain subgraph within a graph. This operation is crucial for the application of local rewrite rules which themselves are at the centre of diagrammatic reasoning in monoidal categories.

Cite As Get BibTex

Malin Altenmüller and Conor Titania Mc Bride. A Data Type of Intrinsically Plane Graphs in Agda. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 13:1-13:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.13

Author Details

Malin Altenmüller
  • University of Edinburgh, UK
Conor Titania Mc Bride
  • University of Strathclyde, Glasgow, UK
  • Quantinuum, Cambridge, UK

Funding

  • Altenmüller, Malin: funded by EPSRC grant number EP/X025551/1.

Acknowledgements

We would like to thank the anonymous reviewers for helpful suggestions.

Supplementary Materials

References

  1. Marie Albenque and Dominique Poulalhon. A generic method for bijections between blossoming trees and planar maps. Electron. J. Comb., 22:2, 2015. URL: https://doi.org/10.37236/3386.
  2. Malin Altenmüller. Combinatorial Presentations of String Diagrams for Non-Symmetric Monoidal Categories. PhD thesis, University of Strathclyde, 2025. URL: https://maltenmuller.github.io/thesis/thesis.pdf.
  3. Malin Altenmüller and Ross Duncan. A category of surface-embedded graphs. In Jade Master and Martha Lewis, editors, Proceedings Fifth International Conference on Applied Category Theory, ACT 2022, Glasgow, United Kingdom, 18-22 July 2022, volume 380, pages 41-62, 2022. URL: https://doi.org/10.4204/EPTCS.380.3.
  4. Olivier Bernardi. Bijective counting of tree-rooted maps and shuffles of parenthesis systems. Electronic Journal of Combinatorics, 14:R9, 2007. URL: https://doi.org/10.37236/928.
  5. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer-Verlag, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.
  6. Richard S Bird. On building cyclic and shared structures in haskell. Formal Aspects Comput., 24:609-621, 2012. URL: https://doi.org/10.1007/S00165-012-0243-6.
  7. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 710-719. ACM, 2016. URL: https://doi.org/10.1145/2933575.2935316.
  8. Bob Coecke and Ross Duncan. Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics, 13:43016, 2011. Google Scholar
  9. Lucas Dixon and Aleks Kissinger. Open-graphs and monoidal theories. Math. Struct. Comput. Sci., 23:308-359, 2013. URL: https://doi.org/10.1017/S0960129512000138.
  10. Ross Duncan. Types for quantum computing. PhD thesis, University of Oxford, UK, 2006. URL: http://ora.ox.ac.uk/objects/uuid:c2901ae8-9386-4dbf-879d-e37bbc2692bd.
  11. Jack R Edmonds. A combinatorial representation for oriented polyhedral surfaces. Notices of the American Mathematical Society, 7:646, 1960. Google Scholar
  12. Martin Erwig. Inductive graphs and functional graph algorithms. J. Funct. Program., 11:467-492, 2001. URL: https://doi.org/10.1017/S0956796801004075.
  13. Neil Ghani, Makoto Hamana, Tarmo Uustalu, and Varmo Vene. Representing cyclic structures as nested datatypes. In Proc. of 7th Symp. on Trends in Functional Programming, TFP, volume 2006, 2006. Google Scholar
  14. Georges Gonthier. Formal proof-the four-color theorem. Notices of the AMS, 55, 2008. Google Scholar
  15. Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Dongming Wang and Zeng Zhibin, editors, Computer Mathematics, 8th Asian Symposium, ASCM 2007, volume 5081, pages 21-22. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87827-8_3.
  16. Jonathan L Gross and Thomas W Tucker. Topological Graph Theory. Dover Publications, 2001. Original work published 1987 by Wiley-Interscience. Google Scholar
  17. Adam Gundry, Conor McBride, and James McKinna. Type inference in context. In Venanzio Capretta and James Chapman, editors, Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010, pages 43-54. ACM, 2010. URL: https://doi.org/10.1145/1863597.1863608.
  18. Makoto Hamana. Initial algebra semantics for cyclic sharing structures. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608, pages 127-141. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_11.
  19. Lothar Heffter. Über das problem der nachbargebiete. Mathematische Annalen, 38:477-508, 1891. Google Scholar
  20. Gérard Huet. The zipper. Journal of Functional Programming, 7:549-554, 1997. URL: https://doi.org/10.1017/S0956796897002864.
  21. David J King and John Launchbury. Lazy depth-first search and linear graph algorithms in haskell. Gla, 1993. Google Scholar
  22. Aleks Kissinger and Vladimir Zamdzhiev. Equational reasoning with context-free families of string diagrams. In Francesco Parisi-Presicce and Bernhard Westfechtel, editors, Graph Transformation - 8th International Conference, ICGT 2015, Held as Part of STAF 2015, L'Aquila, Italy, July 21-23, 2015. Proceedings, volume 9151, pages 138-154. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21145-9_9.
  23. Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Regular behaviours with names - on rational fixpoints of endofunctors on nominal sets. Appl. Categorical Struct., 24:663-701, 2016. URL: https://doi.org/10.1007/S10485-016-9457-8.
  24. Bojan Mohar and Carsten Thomassen. Graphs on Surfaces. Johns Hopkins University Press, 2001. URL: http://jhupbooks.press.jhu.edu/ecom/MasterServlet/GetItemDetailsHandler?iN=9780801866890&qty=1&source=2&viewMode=3&loggedIN=false&JavaScript=y.
  25. Andrey Mokhov. Algebraic graphs with class (functional pearl). In Iavor S Diatchki, editor, Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford, United Kingdom, September 7-8, 2017, pages 2-13. ACM, 2017. URL: https://doi.org/10.1145/3122955.3122956.
  26. Peter Selinger. A survey of graphical languages for monoidal categories, 2011. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  27. Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. Log. Methods Comput. Sci., 11, 2015. URL: https://doi.org/10.2168/LMCS-11(3:22)2015.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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