← All papers
The Directed Van Kampen Theorem in Lean
cs.LO
Dec 11, 2023 · v1
TL;DR
Formalizes directed spaces and a directed Van Kampen theorem in Lean for concurrency reasoning.
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. 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 of the homotopy type of subspaces. By representing concurrent systems as directed spaces, it allows 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.
Problem
Directed topology extends topological spaces with directedness to faithfully represent computation with direction, but the directed Van Kampen theorem (which computes homotopy types of composed spaces from local subspace information) had not been formalized in a proof assistant.
Approach
The authors formalize directed spaces and the directed Van Kampen theorem in Lean. By representing concurrent systems as directed spaces, the theorem allows deduction of properties of a composed system from those of subsystems.
Results
A Lean formalization of directed spaces and the directed Van Kampen theorem is produced, enabling computer-assisted reasoning about the behavior of concurrent systems.