|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Ayberk Tosun (Zeroth Research). All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Ayberk Tosun |
| 5 | +-/ |
| 6 | + |
| 7 | +module |
| 8 | + |
| 9 | +public import Mathlib.CategoryTheory.Category.Basic |
| 10 | +public import Cslib.Foundations.Semantics.LTS.Basic |
| 11 | +public import Mathlib.Control.Basic |
| 12 | + |
| 13 | +@[expose] public section |
| 14 | + |
| 15 | +namespace Cslib |
| 16 | + |
| 17 | +variable {State Label : Type*} |
| 18 | + |
| 19 | +/-! # Category of Labelled Transition Systems |
| 20 | +
|
| 21 | +This file contains the definition of the category of labelled transition systems |
| 22 | +as defined in Winskel and Nielsen's handbook chapter [WinskelNielsen1995]. |
| 23 | +
|
| 24 | +## References |
| 25 | +
|
| 26 | +* [N. Winskel and M. Nielsen, *Models for concurrency*][WinskelNielsen1995] |
| 27 | +-/ |
| 28 | + |
| 29 | +/-- |
| 30 | +We first define what is denoted Tran* in [WinskelNielsen1995]: the extension of |
| 31 | +a transition relation with idle transitions. |
| 32 | +-/ |
| 33 | +def LTS.withIdle (lts : LTS State Label) : LTS State (Option Label) := |
| 34 | + ⟨fun s l s' => l.elim (s = s') (lts.Tr s · s')⟩ |
| 35 | + |
| 36 | +/-! ## LTSs and LTS morphisms form a category -/ |
| 37 | + |
| 38 | +/-- |
| 39 | +The definition of labelled transition system (with the type of states and the |
| 40 | +type of labels as part of the structure). |
| 41 | +-/ |
| 42 | +@[nolint checkUnivs] |
| 43 | +structure LTSCat : Type (max u v + 1) where |
| 44 | + /-- Type of states of an LTS -/ |
| 45 | + State : Type u |
| 46 | + /-- Type of labels of an LTS -/ |
| 47 | + Label : Type v |
| 48 | + /-- Transition relation of an LTS -/ |
| 49 | + lts : LTS State Label |
| 50 | + |
| 51 | +/-- |
| 52 | +A morphism between two labelled transition systems consists of (1) a function on |
| 53 | +states, (2) a partial function on labels, and a proof that (1) preserves each |
| 54 | +transition along (2). |
| 55 | +-/ |
| 56 | +structure LTS.Morphism (lts₁ lts₂ : LTSCat) : Type where |
| 57 | + /-- Mapping of states of `lts₁` to states of `lts₂` -/ |
| 58 | + stateMap : lts₁.State → lts₂.State |
| 59 | + /-- Mapping of labels of `lts₁` to labels of `lts₂` -/ |
| 60 | + labelMap : lts₁.Label → Option lts₂.Label |
| 61 | + /-- Stipulation that `stateMap` preserve transitions -/ |
| 62 | + labelMap_tr (s s' : lts₁.State) (l : lts₁.Label) : |
| 63 | + lts₁.lts.Tr s l s' → (withIdle lts₂.lts).Tr (stateMap s) (labelMap l) (stateMap s') |
| 64 | + |
| 65 | +/-- The identity LTS morphism. -/ |
| 66 | +def LTS.Morphism.id (lts : LTSCat) : LTS.Morphism lts lts where |
| 67 | + stateMap := _root_.id |
| 68 | + labelMap := pure |
| 69 | + labelMap_tr _ _ _ := _root_.id |
| 70 | + |
| 71 | +/-- Composition of LTS morphisms. |
| 72 | +
|
| 73 | +We use Kleisli composition to define this. |
| 74 | +-/ |
| 75 | +def LTS.Morphism.comp {lts₁ lts₂ lts₃} (f : LTS.Morphism lts₁ lts₂) (g : LTS.Morphism lts₂ lts₃) : |
| 76 | + LTS.Morphism lts₁ lts₃ where |
| 77 | + stateMap := g.stateMap ∘ f.stateMap |
| 78 | + labelMap := f.labelMap >=> g.labelMap |
| 79 | + labelMap_tr s s' l h := by |
| 80 | + obtain ⟨f, μ, p⟩ := f |
| 81 | + obtain ⟨g, ν, q⟩ := g |
| 82 | + simp only [LTS.withIdle] at p q |
| 83 | + change ((μ l).bind ν).elim (g (f s) = g (f s')) _ |
| 84 | + cases hμ : μ l with grind |
| 85 | + |
| 86 | +/-- Finally, we prove that these form a category. -/ |
| 87 | +instance : CategoryTheory.Category LTSCat where |
| 88 | + Hom := LTS.Morphism |
| 89 | + id := LTS.Morphism.id |
| 90 | + comp := LTS.Morphism.comp |
| 91 | + comp_id _ := by |
| 92 | + simp only [LTS.Morphism.comp, LTS.Morphism.id] |
| 93 | + congr 1 |
| 94 | + rw [fish_pure] |
| 95 | + assoc _ _ _ := by |
| 96 | + simp only [LTS.Morphism.comp] |
| 97 | + congr 1 |
| 98 | + rw [fish_assoc] |
| 99 | + |
| 100 | +end Cslib |
0 commit comments