Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2312.06506 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909613419397120 |
|---|---|
| author | Basold, Henning Bruin, Peter Lawson, Dominique |
| author_facet | Basold, Henning Bruin, Peter Lawson, Dominique |
| contents | Directed topology is an area of mathematics with applications in concurrency. It extends the concept of a topological space by adding a notion of directedness, which restricts how paths can evolve through a space and enables thereby a faithful representation of computation with their direction. In this paper, we present a Lean formalisation of directed spaces and a Van Kampen theorem for them. This theorem allows the calculation of the homotopy type of a space by combining local knowledge the homotopy type of subspaces. With this theorem, the reasoning about spaces can be reduced to subspaces and, by representing concurrent systems as directed spaces, we can reduce the deduction of properties of a composed system to that of subsystems. The formalisation in Lean can serve to support computer-assisted reasoning about the behaviour of concurrent systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_06506 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | The Directed Van Kampen Theorem in Lean Basold, Henning Bruin, Peter Lawson, Dominique Logic in Computer Science 03B35 F.4.1; F.1.2 Directed topology is an area of mathematics with applications in concurrency. It extends the concept of a topological space by adding a notion of directedness, which restricts how paths can evolve through a space and enables thereby a faithful representation of computation with their direction. In this paper, we present a Lean formalisation of directed spaces and a Van Kampen theorem for them. This theorem allows the calculation of the homotopy type of a space by combining local knowledge the homotopy type of subspaces. With this theorem, the reasoning about spaces can be reduced to subspaces and, by representing concurrent systems as directed spaces, we can reduce the deduction of properties of a composed system to that of subsystems. The formalisation in Lean can serve to support computer-assisted reasoning about the behaviour of concurrent systems. |
| title | The Directed Van Kampen Theorem in Lean |
| topic | Logic in Computer Science 03B35 F.4.1; F.1.2 |
| url | https://arxiv.org/abs/2312.06506 |