feat(LTS): labeled transition systems as coalgebras#603
Open
tannerduve wants to merge 1 commit into
Open
Conversation
tannerduve
force-pushed
the
feat-lts-coalgebra
branch
3 times, most recently
from
f1ea11b to
80106c2
Compare
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.
tannerduve
force-pushed
the
feat-lts-coalgebra
branch
from
80106c2 to
b59d893
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds
Cslib/Foundations/Semantics/LTS/LTSCat/Coalgebra.lean, which defines labelled transition systems with a fixed label setLas coalgebras of the endofunctorF_L X = Set (L × X)onType u.LTS.Endo Labelis the endofunctorF_L : Type u ⥤ Type u.LTS.Coalgebra Labelis the category ofF_L-coalgebras, defined asEndofunctor.Coalgebra (Endo Label), using Mathlib'sCoalgebra.LTS.Coalgebra.toLTSCatis a faithful functor from the coalgebra category toLTSCat.The main result of this file is that coalgebra morphisms coincide with functional bisimulations. More precisely, we have an equivalence
graphBisimEquiv, stating that morphismsV ⟶ Ware in bijection with the state mapsV.V → W.Vwhose graph is a functional bisimulation between the underlying LTSsThis construction does not give an equivalence between categories, as
LTSCatis strictly larger. Its objects can have different label sets and its morphisms can rename labels vialabelMap, drop them to silent steps, and need only be one-way simulations, while coalgebra morphisms fix the label set.