feat(Foundations/Automata): add Machine closed symmetric monoidal category

Cslib.lean

@@ -36,6 +36,7 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Foundations.Automata.Machine
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects

Cslib/Foundations/Automata/Machine.lean

@@ -0,0 +1,189 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.OmegaSequence.Init
+public import Mathlib.CategoryTheory.Monoidal.Braided.Basic
+public import Mathlib.CategoryTheory.Monoidal.Closed.Basic
+
+@[expose] public section
+
+/-! # Category of machines
+
+## References
+
+* [J. A. Goguen, *Minimal realization of machines in closed categories*][Goguen1972]
+
+-/
+
+namespace Cslib.Automata
+
+universe u
+
+/-- Category of machines with objects as types and morphisms as stream functions. -/
+def Machine := Type u
+
+namespace Machine
+
+variable {X Y Z : Machine.{u}}
+
+/-- Homomorphism as a stream function. -/
+def Hom (X Y : Machine.{u}) := ωSequence X → ωSequence Y
+
+def id (X : Machine.{u}) : ωSequence X → ωSequence X := fun x => x
+
+def comp (f : Hom X Y) (g : Hom Y Z) := g ∘ f
+
+open CategoryTheory
+
+instance : LargeCategory Machine where
+  Hom
+  id
+  comp
+
+def tensorObj (X Y : Machine.{u}) : Machine := X × Y
+
+def tensorHom
+    {X₁ Y₁ X₂ Y₂ : Machine.{u}}
+    (f : X₁ ⟶ Y₁)
+    (g : X₂ ⟶ Y₂)
+    (v : ωSequence (X₁ × X₂)) :
+    ωSequence (Y₁ × Y₂) :=
+  let x₁s := f (ωSequence.map (fun p => p.1) v)
+  let x₂s := g (ωSequence.map (fun p => p.2) v)
+  ωSequence.zip Prod.mk x₁s x₂s
+
+def whiskerLeft
+    (X : Machine.{u}) {Y₁ Y₂ : Machine.{u}} : (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂) :=
+  tensorHom (𝟙 X)
+
+def whiskerRight
+    {X₁ X₂ : Machine.{u}} (f : X₁ ⟶ X₂) (Y : Machine.{u}) : tensorObj X₁ Y ⟶ tensorObj X₂ Y :=
+  tensorHom f (𝟙 Y)
+
+def tensorUnit : Machine := PUnit
+
+section associators
+
+def associator_hom : ωSequence ((X × Y) × Z) → ωSequence (X × (Y × Z)) :=
+  ωSequence.map fun ((a, b), c) => (a, (b, c))
+
+def associator_inv : ωSequence (X × (Y × Z)) → ωSequence ((X × Y) × Z) :=
+  ωSequence.map fun (a, (b, c)) => ((a, b), c)
+
+theorem associator_hom_inv : associator_hom ≫ associator_inv = 𝟙 (tensorObj (tensorObj X Y) Z) :=
+  rfl
+
+theorem associator_inv_hom : associator_inv ≫ associator_hom = 𝟙 (tensorObj X (tensorObj Y Z)) :=
+  rfl
+
+def associator
+    (X Y Z : Machine.{u}) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) where
+  hom := associator_hom
+  inv := associator_inv
+  hom_inv_id := associator_hom_inv
+  inv_hom_id := associator_inv_hom
+
+end associators
+
+def leftUnitor_hom : ωSequence (PUnit × X) → ωSequence X := ωSequence.map Prod.snd
+
+def leftUnitor_inv : ωSequence X → ωSequence (PUnit × X) := ωSequence.map fun x => (PUnit.unit, x)
+
+theorem leftUnitor_hom_inv_id : leftUnitor_hom ≫ leftUnitor_inv = 𝟙 (tensorObj tensorUnit X) := rfl
+
+theorem leftUnitor_inv_hom_id : leftUnitor_inv ≫ leftUnitor_hom = 𝟙 X := rfl
+
+def leftUnitor (X : Machine.{u}) : tensorObj tensorUnit X ≅ X where
+  hom := leftUnitor_hom
+  inv := leftUnitor_inv
+  hom_inv_id := leftUnitor_hom_inv_id
+  inv_hom_id := leftUnitor_inv_hom_id
+
+def rightUnitor_hom : ωSequence (X × PUnit) → ωSequence X := ωSequence.map Prod.fst
+
+def rightUnitor_inv : ωSequence X → ωSequence (X × PUnit) := ωSequence.map fun x => (x, PUnit.unit)
+
+theorem rightUnitor_hom_inv_id : rightUnitor_hom ≫ rightUnitor_inv = 𝟙 (tensorObj X tensorUnit) :=
+  rfl
+
+theorem rightUnitor_inv_hom_id : rightUnitor_inv ≫ rightUnitor_hom = 𝟙 X := rfl
+
+def rightUnitor (X : Machine.{u}) : tensorObj X tensorUnit ≅ X where
+  hom := rightUnitor_hom
+  inv := rightUnitor_inv
+  hom_inv_id := rightUnitor_hom_inv_id
+  inv_hom_id := rightUnitor_inv_hom_id
+
+instance : MonoidalCategory Machine where
+  tensorObj
+  tensorHom
+  whiskerLeft
+  whiskerRight
+  tensorUnit
+  associator
+  leftUnitor
+  rightUnitor
+
+open MonoidalCategory
+
+def braiding_hom (X Y : Machine.{u}) : ωSequence (X × Y) → ωSequence (Y × X) :=
+  ωSequence.map Prod.swap
+
+theorem braiding_hom_inv_id (X Y : Machine.{u}) : braiding_hom X Y ≫ braiding_hom Y X = 𝟙 (X ⊗ Y) :=
+  rfl
+
+def braiding (X Y : Machine.{u}) : X ⊗ Y ≅ Y ⊗ X where
+  hom := braiding_hom X Y
+  inv := braiding_hom Y X
+  hom_inv_id := braiding_hom_inv_id X Y
+  inv_hom_id := braiding_hom_inv_id Y X
+
+instance : SymmetricCategory Machine where
+  braiding
+
+def rightAdj {X : Machine.{u}} : Machine ⥤ Machine where
+  obj Y := ωSequence X → Y
+  map f s := ⟨fun n xs => f ⟨fun m => s m xs⟩ n⟩
+
+def toFun (f : (tensorLeft X).obj A ⟶ Y) (a : ωSequence A) : ωSequence (ωSequence X → Y) :=
+  ⟨fun n xs => f (ωSequence.zip Prod.mk xs a) n⟩
+
+def invFun (g : Z ⟶ X.rightAdj.obj Y) (xas : ωSequence (X × Z)) : ωSequence Y :=
+  ⟨fun n => g (ωSequence.map Prod.snd xas) n (ωSequence.map Prod.fst xas)⟩
+
+theorem left_inv (f : (tensorLeft X).obj A ⟶ Y) : invFun (toFun f) = f := rfl
+
+theorem right_inv (g : A ⟶ X.rightAdj.obj Y) : toFun (invFun g) = g := rfl
+
+def inv : ((tensorLeft X).obj A ⟶ Y) ≃ (A ⟶ X.rightAdj.obj Y) where
+  toFun
+  invFun
+  left_inv
+  right_inv
+
+def adj_eq : (Y Z : Machine.{u}) → ((tensorLeft X).obj Y ⟶ Z) ≃ (Y ⟶ X.rightAdj.obj Z) :=
+  fun _ _ => inv
+
+open Adjunction
+
+def adj_hom_eq : CoreHomEquiv (tensorLeft X) X.rightAdj where
+  homEquiv := adj_eq
+
+def adj : tensorLeft X ⊣ X.rightAdj := mkOfHomEquiv adj_hom_eq
+
+@[implicit_reducible]
+def closed (X : Machine.{u}) : Closed X where
+  rightAdj
+  adj
+
+instance : MonoidalClosed Machine where
+  closed
+
+end Machine
+
+end Cslib.Automata

references.bib

@@ -107,6 +107,17 @@ @inbook{          Girard1995
   collection={London Mathematical Society Lecture Note Series}
 }
 
+@article{         Goguen1972,
+author = {J. A. Goguen},
+title = {{Minimal realization of machines in closed categories}},
+volume = {78},
+journal = {Bulletin of the American Mathematical Society},
+number = {5},
+publisher = {American Mathematical Society},
+pages = {777 -- 783},
+year = {1972},
+}
+
 @article{         Hennessy1985,
   author       = {Matthew Hennessy and
                   Robin Milner},