A Classifying Topos for the Spectrum of Equivalences

TL;DR

This paper develops a topos-theoretic framework to classify and analyze the spectrum of behavioral equivalences in process algebra, unifying various notions through geometric theories and Grothendieck topologies.

Contribution

It introduces a geometric theory-based hierarchy of process equivalences, extending to all 13 known types, with a constructive proof and formalization in Lean 4.

Findings

Hierarchical classification of process equivalences via topos theory.

Constructive proofs of the hierarchy and closure properties.

Formalization of the spectrum in Lean 4/Mathlib.

Abstract

What makes two computational systems equivalent? Topos theory answers with classifying toposes: a system's semantic content is encoded in the geometric theory it classifies, and two presentations are equivalent when their classifying toposes coincide. Process algebra answers with the linear time-branching time spectrum of van Glabbeek: a hierarchy of behavioral equivalences from trace equivalence to bisimilarity, each determined by which observations can distinguish processes. We show these are aspects of a single structure in which behavioral abstraction is localization. Each labeled transition system receives a geometric theory $\mathbb{T}_M$ whose classifying topos $\mathcal{E}[\mathbb{T}_M]$ determines its provable geometric sequents. Mutual simulation is strictly coarser than bisimulation, strictly coarser than topos equivalence; diamond-only Hennessy-Milner logic characterizes the bisimulation-invariant fragment of geometric logic -- a geometric van Benthem theorem. Grothendieck topologies yield $J_{\mathrm{bisim}} \subsetneq J_{\mathrm{sim}} \subsetneq J_{\mathrm{trace}}$, constructive for trace and bisimulation; a counterexample shows the observation-class approach inadequate for simulation, motivating Caramello's duality. Energy-topology extends this to all 13 named equivalences. Lattice closure yields 30 elements including 17 unnamed hybrids absent because the energy-game framework computes but does not close. $L_{30}$ is indecomposable with $S \to F = \mathrm{IF}$; a Geometric Closure Theorem computes presheaf Heyting implications at a single free extension. The hierarchy, bi-Heyting structure, and Closure Theorem are proved constructively with no known process-algebraic proof. The spectrum is a finite sub-poset of an infinite coframe whose operations (meets, implications, subtractions) yield structure inaccessible from process algebra. Formalized in Lean 4/Mathlib.