From b59d893239054f3c709032d38b26fddade66ad75 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Wed, 27 May 2026 21:31:34 -0700 Subject: [PATCH] feat(LTS/LTSCat): labelled transition systems as coalgebras MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Cslib/Foundations/Semantics/LTS/LTSCat/Coalgebra.lean, which exhibits labelled transition systems with a fixed label set as coalgebras of the Set-endofunctor F_L X = Set (L × X) on Type u. LTS.Endo Label is the endofunctor F_L. LTS.Coalgebra Label is the category of F_L-coalgebras, defined as Endofunctor.Coalgebra (Endo Label), reusing Mathlib's existing notion. LTS.Coalgebra.toLTS extracts the LTS underlying a coalgebra, and LTS.Coalgebra.toLTSCat is the functor from Coalgebra Label to LTSCat sending a functional bisimulation to its underlying simulation. LTS.Coalgebra.toLTSCat is faithful. The theorem graph_isBisimulation shows that every coalgebra morphism is, as the graph of its underlying state map, a functional bisimulation between the underlying LTSs. The dual construction homOfGraphBisim lifts every functional bisimulation to a coalgebra morphism, and graphBisimEquiv packages both directions into a bijection between coalgebra morphisms V ⟶ W and state maps V.V → W.V whose graph is a functional bisimulation. This is not an equivalence of categories, as LTSCat is strictly larger (objects can carry different label sets, morphisms can rename labels, drop them to silent steps, and need only be one-way simulations); graphBisimEquiv exhibits LTS.Coalgebra Label as a non-full subcategory of LTSCat, namely the label-preserving functional bisimulations between same-label LTSs. Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean is made universe polymorphic for LTS.Morphism, LTS.Morphism.id, LTS.Morphism.comp, and the Category LTSCat instance, and @[ext] is added on LTS.Morphism. references.bib adds the Rutten2000 entry. Cslib.lean imports the new file. --- Cslib.lean | 1 + .../Semantics/LTS/LTSCat/Basic.lean | 10 +- .../Semantics/LTS/LTSCat/Coalgebra.lean | 193 ++++++++++++++++++ references.bib | 11 + 4 files changed, 211 insertions(+), 4 deletions(-) create mode 100644 Cslib/Foundations/Semantics/LTS/LTSCat/Coalgebra.lean diff --git a/Cslib.lean b/Cslib.lean index b504973c3..0f9c1e64c 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -78,6 +78,7 @@ public import Cslib.Foundations.Semantics.LTS.Divergence public import Cslib.Foundations.Semantics.LTS.Execution public import Cslib.Foundations.Semantics.LTS.HasTau public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic +public import Cslib.Foundations.Semantics.LTS.LTSCat.Coalgebra public import Cslib.Foundations.Semantics.LTS.Notation public import Cslib.Foundations.Semantics.LTS.OmegaExecution public import Cslib.Foundations.Semantics.LTS.Relation diff --git a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean index 9c40c3dcd..8c3afbe1c 100644 --- a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean @@ -53,7 +53,8 @@ A morphism between two labelled transition systems consists of (1) a function on states, (2) a partial function on labels, and a proof that (1) preserves each transition along (2). -/ -structure LTS.Morphism (lts₁ lts₂ : LTSCat) : Type where +@[ext] +structure LTS.Morphism (lts₁ lts₂ : LTSCat.{u, v}) : Type (max u v) where /-- Mapping of states of `lts₁` to states of `lts₂` -/ stateMap : lts₁.State → lts₂.State /-- Mapping of labels of `lts₁` to labels of `lts₂` -/ @@ -63,7 +64,7 @@ structure LTS.Morphism (lts₁ lts₂ : LTSCat) : Type where lts₁.lts.Tr s l s' → (withIdle lts₂.lts).Tr (stateMap s) (labelMap l) (stateMap s') /-- The identity LTS morphism. -/ -def LTS.Morphism.id (lts : LTSCat) : LTS.Morphism lts lts where +def LTS.Morphism.id (lts : LTSCat.{u, v}) : LTS.Morphism lts lts where stateMap := _root_.id labelMap := pure labelMap_tr _ _ _ := _root_.id @@ -72,7 +73,8 @@ def LTS.Morphism.id (lts : LTSCat) : LTS.Morphism lts lts where We use Kleisli composition to define this. -/ -def LTS.Morphism.comp {lts₁ lts₂ lts₃} (f : LTS.Morphism lts₁ lts₂) (g : LTS.Morphism lts₂ lts₃) : +def LTS.Morphism.comp {lts₁ lts₂ lts₃ : LTSCat.{u, v}} + (f : LTS.Morphism lts₁ lts₂) (g : LTS.Morphism lts₂ lts₃) : LTS.Morphism lts₁ lts₃ where stateMap := g.stateMap ∘ f.stateMap labelMap := f.labelMap >=> g.labelMap @@ -84,7 +86,7 @@ def LTS.Morphism.comp {lts₁ lts₂ lts₃} (f : LTS.Morphism lts₁ lts₂) (g cases hμ : μ l with grind /-- Finally, we prove that these form a category. -/ -instance : CategoryTheory.Category LTSCat where +instance : CategoryTheory.Category LTSCat.{u, v} where Hom := LTS.Morphism id := LTS.Morphism.id comp := LTS.Morphism.comp diff --git a/Cslib/Foundations/Semantics/LTS/LTSCat/Coalgebra.lean b/Cslib/Foundations/Semantics/LTS/LTSCat/Coalgebra.lean new file mode 100644 index 000000000..6bf07fac6 --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/LTSCat/Coalgebra.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2026 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Cslib.Foundations.Semantics.LTS.Bisimulation +public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic +public import Mathlib.CategoryTheory.Endofunctor.Algebra +public import Mathlib.CategoryTheory.Types.Basic +public import Mathlib.CategoryTheory.Functor.FullyFaithful + +/-! +# Labelled transition systems as coalgebras + +For a label set `L`, a labelled transition system on `X` is the same datum as a +coalgebra `α : X → Set (L × X)` for the `Set`-endofunctor `F_L X = Set (L × X)`. +This file defines `F_L` as an endofunctor of `Type u`, exhibits LTSs as +coalgebras via Mathlib's `CategoryTheory.Endofunctor.Coalgebra`, and proves +that Mathlib's coalgebra morphisms coincide with functional bisimulations on +the underlying LTSs. + +## Main definitions + +- `LTS.Endo`: the endofunctor `F_L X = Set (L × X)` on `Type u`. +- `LTS.Coalgebra.toLTSCat`: the forgetful functor from coalgebras of `F_L` to + `LTSCat` that maps a functional bisimulation to its underlying simulation. + +## Main results + +- `LTS.Coalgebra.instFaithful`: `toLTSCat` is faithful. +- `LTS.Coalgebra.graphBisimEquiv`: coalgebra morphisms `V ⟶ W` are in bijection + with the state maps `V.V → W.V` whose graph is a functional bisimulation + between the underlying LTSs. + +## References + +* [J. Rutten, *Universal coalgebra: a theory of systems*][Rutten2000] +* [G. Winskel and M. Nielsen, *Models for concurrency*][WinskelNielsen1995] +-/ + +@[expose] public section + +namespace Cslib + +universe u + +open CategoryTheory TypeCat Endofunctor + +namespace LTS + +/-- Action on morphisms of the LTS endofunctor: image of a set under +`(l, x) ↦ (l, f x)`. -/ +def Endo.mapFn (Label : Type u) {X Y : Type u} (f : X → Y) (S : Set (Label × X)) : + Set (Label × Y) := + {p | ∃ x : X, (p.1, x) ∈ S ∧ f x = p.2} + +namespace Endo + +variable {Label : Type u} {X Y Z : Type u} + +@[simp] lemma mem_mapFn (f : X → Y) (S : Set (Label × X)) (p : Label × Y) : + p ∈ mapFn Label f S ↔ ∃ x : X, (p.1, x) ∈ S ∧ f x = p.2 := Iff.rfl + +lemma mapFn_id : mapFn Label (_root_.id : X → X) = _root_.id := by + funext S + ext ⟨l, x⟩ + constructor + · rintro ⟨_, hw, rfl⟩ + exact hw + · exact fun hx => ⟨x, hx, rfl⟩ + +lemma mapFn_comp (f : X → Y) (g : Y → Z) : + mapFn Label (g ∘ f) = mapFn Label g ∘ mapFn Label f := by + funext S + ext ⟨l, z⟩ + constructor + · rintro ⟨x, hx, rfl⟩ + exact ⟨f x, ⟨x, hx, rfl⟩, rfl⟩ + · rintro ⟨y, ⟨x, hx, rfl⟩, rfl⟩ + exact ⟨x, hx, rfl⟩ + +end Endo + +/-- The `Set`-endofunctor `F_L X = Set (L × X)` on `Type u`. -/ +@[reducible] def Endo (Label : Type u) : Type u ⥤ Type u where + obj X := Set (Label × X) + map {_ _} f := ofHom (Endo.mapFn Label f) + map_id _ := by aesop + map_comp f g := by aesop + +/-- The category of LTS-coalgebras for a fixed label set, as Mathlib's +`Endofunctor.Coalgebra` applied to `Endo Label`. Morphisms are the strict +commuting-square coalgebra morphisms, which are precisely the functional +bisimulations on the underlying LTSs (see `Coalgebra.graph_isBisimulation` and +`Coalgebra.homOfGraphBisim`). -/ +abbrev Coalgebra (Label : Type u) : Type (u + 1) := Endofunctor.Coalgebra (Endo Label) + +namespace Coalgebra + +variable {Label : Type u} + +/-- The LTS underlying a coalgebra of `Endo Label`. -/ +abbrev toLTS (V : Coalgebra Label) : LTS V.V Label where + Tr s l s' := (l, s') ∈ (V.str : V.V → _) s + +@[simp] lemma toLTS_Tr (V : Coalgebra Label) (s : V.V) (l : Label) (s' : V.V) : + (toLTS V).Tr s l s' ↔ (l, s') ∈ (V.str : V.V → _) s := Iff.rfl + +variable (Label) in +/-- The forgetful functor `Coalgebra Label ⥤ LTSCat` mapping each functional +bisimulation to its underlying simulation. -/ +def toLTSCat : Coalgebra Label ⥤ LTSCat.{u, u} where + obj V := ({ State := V.V, Label := Label, lts := toLTS V } : LTSCat.{u, u}) + map {V W} f := + { stateMap := (f.f : V.V → W.V) + labelMap := pure + labelMap_tr := by + intro s s' l h + have hcomm := ConcreteCategory.congr_hom f.h s + simp_all only [types_comp_apply, Endo, ofHom_apply, withIdle, toLTS] + rw [← hcomm] + exact ⟨s', h, rfl⟩ } + map_id _ := rfl + map_comp _ _ := by + apply Morphism.ext + · rfl + · exact (fish_pure pure).symm + +/-- `toLTSCat` is faithful: a functional bisimulation is determined by its +underlying state map. -/ +instance : (toLTSCat Label).Faithful where + map_injective {_ _} _ _ h := by + apply Endofunctor.Coalgebra.Hom.ext + apply Hom.ext + apply Fun.ext + funext x + exact congrFun (congrArg Morphism.stateMap h) x + +/-- Mathlib's coalgebra morphisms are precisely the functional bisimulations of +the underlying LTSs. Forward direction: every coalgebra morphism, viewed as the +graph of its underlying state map, is an `LTS.IsBisimulation`. -/ +theorem graph_isBisimulation {V W : Coalgebra Label} (f : V ⟶ W) : + LTS.IsBisimulation (toLTS V) (toLTS W) (fun s t => (f.f : V.V → W.V) s = t) := by + intro s t hst l + have hcomm := ConcreteCategory.congr_hom f.h s + simp_all only [types_comp_apply, Endo, ofHom_apply] + constructor + · intro s' h + exact ⟨(f.f : V.V → W.V) s', hcomm ▸ ⟨s', h, rfl⟩, rfl⟩ + · intro t' h + obtain ⟨s', hs', rfl⟩ := hcomm ▸ h + exact ⟨s', hs', rfl⟩ + +/-- Backward direction: any function whose graph is an LTS bisimulation is the +underlying state map of a (unique) coalgebra morphism. -/ +def homOfGraphBisim {V W : Coalgebra Label} (f : V.V → W.V) + (h : LTS.IsBisimulation (toLTS V) (toLTS W) (fun s t => f s = t)) : V ⟶ W where + f := ofHom f + h := by + apply Hom.ext + apply Fun.ext + funext s + ext ⟨l, t'⟩ + simp only [Endo] + constructor + · rintro ⟨s', hs', rfl⟩ + obtain ⟨_, ht₂, rfl⟩ := (h rfl l).1 _ hs' + exact ht₂ + · intro ht' + obtain ⟨s', hs', rfl⟩ := (h rfl l).2 _ ht' + exact ⟨s', hs', rfl⟩ + +/-- Coalgebra morphisms `V ⟶ W` are in bijection with the state maps `V.V → W.V` whose graph is +a functional bisimulation between the underlying LTSs. -/ +def graphBisimEquiv {V W : Coalgebra Label} : + (V ⟶ W) ≃ + { f : V.V → W.V // + LTS.IsBisimulation (toLTS V) (toLTS W) (fun s t => f s = t) } where + toFun φ := ⟨φ.f, graph_isBisimulation φ⟩ + invFun p := homOfGraphBisim p.1 p.2 + left_inv φ := by + apply Endofunctor.Coalgebra.Hom.ext + rfl + right_inv _ := rfl + +end Coalgebra + +end LTS + +end Cslib diff --git a/references.bib b/references.bib index f0d122d17..95182f20b 100644 --- a/references.bib +++ b/references.bib @@ -358,6 +358,17 @@ @book{KearnsVazirani1994 address = {Cambridge, MA, USA} } +@article{Rutten2000, + author = {Rutten, J. J. M. M.}, + title = {Universal coalgebra: a theory of systems}, + journal = {Theoretical Computer Science}, + volume = {249}, + number = {1}, + pages = {3--80}, + year = {2000}, + doi = {10.1016/S0304-3975(00)00056-6} +} + @incollection{WinskelNielsen1995, author = {Winskel, Glynn and Nielsen, Mogens}, isbn = {9780198537809},