Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Directed Van Kampen Theorem in Lean

Henning Basold, Peter Bruin, Dominique Lawson

TL;DR

The work addresses computing the directed homotopy type of spaces used to model concurrent systems by proving a directed Van Kampen theorem within Lean. It develops a formal framework for directed spaces $(X, P_X)$, directed maps, and directed homotopies, then constructs the fundamental category $\overrightarrow\Pi(X)$ and the fundamental monoid $\overrightarrow\pi(X,x)$, culminating in a constructive pushout result that enables modular reasoning about subsystems. The Lean formalization demonstrates both the feasibility and benefits of computer-assisted proofs in directed topology, including a counterexample showing limitations when generalizing to monoids. This has practical significance for compositional verification of concurrent systems and lays groundwork for further integration with Brown-style groupoid approaches and other directed-topological results.

Abstract

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.

The Directed Van Kampen Theorem in Lean

TL;DR

The work addresses computing the directed homotopy type of spaces used to model concurrent systems by proving a directed Van Kampen theorem within Lean. It develops a formal framework for directed spaces , directed maps, and directed homotopies, then constructs the fundamental category and the fundamental monoid , culminating in a constructive pushout result that enables modular reasoning about subsystems. The Lean formalization demonstrates both the feasibility and benefits of computer-assisted proofs in directed topology, including a counterexample showing limitations when generalizing to monoids. This has practical significance for compositional verification of concurrent systems and lays groundwork for further integration with Brown-style groupoid approaches and other directed-topological results.

Abstract

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.
Paper Structure (17 sections, 6 theorems, 30 equations, 1 figure)

This paper contains 17 sections, 6 theorems, 30 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Contributions
  3. Overview
  4. Directed Spaces
  5. Directed Spaces
  6. Directed Maps
  7. Directed Homotopies
  8. Homotopies
  9. Path Homotopies
  10. Fundamental Structures
  11. The Fundamental Category
  12. The Fundamental Monoid
  13. The Van Kampen Theorem
  14. The Van Kampen Theorem
  15. Formalization
  16. ...and 2 more sections

Key Result

Lemma 2.13

Let $X \in \textbf{dTop}$ be a directed space and $X_1$ and $X_2$ two open subspaces such that $X = X_1 \cup X_2$. Take $X_0 = X_1 \cap X_2$ as the intersection of $X_1$ and $X_2$. Let $i_k : X_0 \to X_k$ and $j_k : X_k \to X$, with $k \in \{1, 2 \}$ be the inclusion maps. We then get a pushout squa

Figures (1)

  • Figure 1: Possible execution paths of two programs A and B under three conditions: a) sequential (left), b) simultaneous (middle) and c) simultaneous with obstacles (right).

Theorems & Definitions (39)

  • Definition 2.1: Directed space
  • Example 2.2: Directed unit interval
  • Example 2.3: Directed unit circle
  • Example 2.4: Maximal directed space
  • Example 2.5: Minimal directed space
  • Example 2.6: Product of directed spaces
  • Example 2.7: Induced directed space
  • Definition 2.8
  • Definition 2.9
  • Definition 2.10
  • ...and 29 more