Document Open Access Logo

The Directed Van Kampen Theorem in Lean

Authors Henning Basold , Peter Bruin , Dominique Lawson

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.8.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Henning Basold
  • Leiden Institute of Advanced Computer Science, Leiden University, The Netherlands
Peter Bruin
  • Mathematisch Instituut, Leiden University, The Netherlands
Dominique Lawson
  • Student, Leiden University, The Netherlands

Funding

  • Bruin, Peter: Partially supported by the Dutch Research Council (NWO/OCW), as part of the Quantum Software Consortium programme (project number 024.003.037).

Cite AsGet BibTex

Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen Theorem in Lean. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.8

Abstract

Directed topology augments the concept of a topological space with a notion of directed paths. This leads to a category of directed spaces, in which the morphisms are continuous maps respecting directed paths. Directed topology thereby enables an accurate representation of computation paths in concurrent systems that usually cannot be reversed. Even though ideas from algebraic topology have analogues in directed topology, the directedness drastically changes how spaces can be characterised. For instance, while an important homotopy invariant of a topological space is its fundamental groupoid, for directed spaces this has to be replaced by the fundamental category because directed paths are not necessarily reversible. In this paper, we present a Lean 4 formalisation of directed spaces and of a Van Kampen theorem for them, which allows the fundamental category of a directed space to be computed in terms of the fundamental categories of subspaces. Part of this formalisation is also a significant theory of directed spaces, directed homotopy theory and path coverings, which can serve as basis for future formalisations of directed topology. The formalisation in Lean can also be used in computer-assisted reasoning about the behaviour of concurrent systems that have been represented as directed spaces.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Mathematics of computing → Algebraic topology
Keywords
  • Lean
  • Directed Topology
  • Van Kampen Theorem
  • Directed Homotopy Theory
  • Formalised Mathematics

Metrics

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

Related Versions

Supplementary Materials

References

  1. Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen theorem in Lean, 2023. Pre-print. URL: https://arxiv.org/abs/2312.06506.
  2. Ronald Brown. Elements of Modern Topology. McGraw-Hill, 1968. Google Scholar
  3. Ronald Brown. Topology and Groupoids. BookSurge Publishing, 2006. Google Scholar
  4. Ronald Brown, Philip J. Higgins, and Rafael Sivera. Nonabelian Algebraic Topology: Filtered spaces, crossed complexes, cubical homotopy groupoids. European Mathematical Society, 2011. URL: https://doi.org/10.4171/083.
  5. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Lecture Notes in Computer Science, pages 378-388. Springer, Springer International Publishing, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  6. Jérémy Dubut. Directed Homotopy and Homology Theories for Geometric Models of True Concurrency. PhD thesis, Université Paris-Saclay, 2017. URL: https://tel.archives-ouvertes.fr/tel-01590515.
  7. Lisbeth Fajstrup. Dicovering Spaces. Homology, Homotopy and Applications, 5(2):1-17, 2003. URL: https://doi.org/10.4310/HHA.2003.v5.n2.a1.
  8. Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raußen. Directed Algebraic Topology and Concurrency. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-15398-8.
  9. Lisbeth Fajstrup, Eric Goubault, and Martin Raußen. Detecting Deadlocks in Concurrent Systems. In CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, pages 332-347, 1998. URL: https://doi.org/10.1007/BFb0055632.
  10. Lisbeth Fajstrup, Martin Raußen, and Eric Goubault. Algebraic topology and concurrency. Theoretical Computer Science, 357(1):241-278, 2006. Clifford Lectures and the Mathematical Foundations of Programming Semantics. URL: https://doi.org/10.1016/j.tcs.2006.03.022.
  11. Philippe Gaucher. Six Model Categories for Directed Homotopy. Categories and General Algebraic Structures with Applications, 15(1):145-181, 2021. URL: https://doi.org/10.52547/cgasa.15.1.145.
  12. Marco Grandis. Directed homotopy theory, I. The fundamental category. Cahiers de topologie et géométrie différentielle catégoriques, 44(4):281-316, 2003. URL: http://archive.numdam.org/item/CTGDC_2003__44_4_281_0/.
  13. Marco Grandis. Directed Algebraic Topology: Models of Non-Reversible Worlds. New Mathematical Monographs. Cambridge University Press, 2009. URL: https://doi.org/10.1017/CBO9780511657474.
  14. Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen theorem in homotopy type theory. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl Publishing, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.22.
  15. Sanjeevi Krishnan. A Convenient Category of Locally Preordered Spaces. Applied Categorical Structures, 17(5):445-466, 2009. URL: https://doi.org/10.1007/s10485-008-9140-9.
  16. Dominique Lawson. GitHub - Dominique-Lawson/Directed-Topology-Lean-4. Software, version 1.1., swhId: https://archive.softwareheritage.org/swh:1:dir:479a73373a2bf508149f7d1b889b42304fe78a9e;origin=https://github.com/Dominique-Lawson/Directed-Topology-Lean-4;visit=swh:1:snp:a7554a8cd1b293b90366ad72928c60031a03f19c;anchor=swh:1:rev:009529606c66d37ef93b4b81b8587f71ce4d2c56 (visited on 2024-07-08). URL: https://github.com/Dominique-Lawson/Directed-Topology-Lean-4/tree/v1.1.
  17. Tom Leinster. Basic Category Theory. Cambridge University Press, 2014. URL: https://doi.org/10.1017/cbo9781107360068.
  18. The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New Orleans, LA, 2020. ACM. URL: https://doi.org/10.1145/3372885.3373824.
  19. James R. Munkres. Topology, a first course. Prentice-Hall, 1975. Google Scholar
  20. Vaughan R. Pratt. Modeling Concurrency with Geometry. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL), pages 311-322, 1991. URL: https://doi.org/10.1145/99583.99625.
  21. Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. Homotopy type theory in Lean. In Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings 8, pages 479-495. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_30.
  22. Rob J. van Glabbeek. On the expressiveness of higher dimensional automata. Theoretical Computer Science, 356(3):265-290, 2006. URL: https://doi.org/10.1016/j.tcs.2006.02.012.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact