A Classifying Topos for the Spectrum of Equivalences

TL;DR

The hierarchy, bi-Heyting structure, and Closure Theorem are proved constructively with no known process-algebraic proof.

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.

Figures (13)

• Figure 1: The geometric theory $\mathbb{T}_{\mathscr{M}}$ classifies the LTS structure; each topology $J_E$ localizes the classifying topos to the subtopos enforcing the corresponding equivalence. The middle topology $J_{\mathrm{sim}}$ is the first requiring Caramello's quotient-theory machinery; the 10 intermediate equivalences of the Energy--LT Bridge depend on it as well (§\ref{['sec:explicit-topologies']}).
• Figure 2: The self-loop $\mathscr{L}$ and two-cycle $\mathscr{C}$. The dashed lines show the relational bisimulation $R = \{(a,x),(a,y)\}$. No simulation $\mathscr{L} \to \mathscr{C}$ exists: $\mathscr{C}$ has no self-loops.
• Figure 3: The fork $\mathscr{F}$ and path $\mathscr{P}$ with mutual simulations. Dashed arrows: $f(a)=x$, $f(b)=f(c)=y$. Dotted arrows: $g(x)=a$, $g(y)=b$. The halting state $c$ (hatched) has no preimage under $g$.
• Figure 4: The hub-spokes $\mathscr{H}$ and two-cycle $\mathscr{C}$. Dashed arrows show the simulation $I \colon \mathscr{H} \to \mathscr{C}$ with $I(a)=x$, $I(b)=I(c)=y$; the reverse simulation is $K(x)=a$, $K(y)=b$. Non-injectivity $I(b)=I(c)$ collapses the branching that $\sigma_{\mathrm{det}}$ detects.
• Figure 5: The diamond graph $\mathscr{G}$ and confluence tree $\mathscr{T}$ with bisimulation $R = \{(a,a),(b,b),(c,c),(d,d_1),(d,d_2)\}$. The merge point $d$ in $\mathscr{G}$ splits into distinct sinks $d_1$, $d_2$ in $\mathscr{T}$; both have self-loops but share no common successor.

Theorems & Definitions (86)

• Definition 2.1: Bisimulation-invariant sequent
• Lemma 3.1: Soundness and Completeness
• proof
• Remark 3.2: Size of the theory
• Definition 3.3: Path equivalence
• Lemma 3.4: Lifting Lemma
• proof
• Definition 3.5: Relational bisimulation
• Definition 3.6: Functional bisimulation
• Remark 3.7: Functional vs. relational bisimulation