From 53b325cff6628d02bb52fef3870f4a2b6f60a139 Mon Sep 17 00:00:00 2001 From: Matt Hunzinger Date: Tue, 7 Apr 2026 22:24:54 -0400 Subject: [PATCH 1/5] feat: Machine --- Cslib/Foundations/Automata/Machine.lean | 197 ++++++++++++++++++++++++ references.bib | 11 ++ 2 files changed, 208 insertions(+) create mode 100644 Cslib/Foundations/Automata/Machine.lean diff --git a/Cslib/Foundations/Automata/Machine.lean b/Cslib/Foundations/Automata/Machine.lean new file mode 100644 index 000000000..019dc9c33 --- /dev/null +++ b/Cslib/Foundations/Automata/Machine.lean @@ -0,0 +1,197 @@ +/- +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 Mathlib.CategoryTheory.Monoidal.Braided.Basic +public import Mathlib.CategoryTheory.Monoidal.Closed.Basic +public import Mathlib.Data.Stream.Init + +@[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 causal 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}) := Stream' X → Stream' Y + +def id (X : Machine.{u}) : Stream' X → Stream' 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} + (f : X₁ ⟶ Y₁) + (g : X₂ ⟶ Y₂) + (v : Stream' (X₁ × X₂)) : + Stream' (Y₁ × Y₂) := + let x₁s := f (Stream'.map (fun p => p.1) v) + let x₂s := g (Stream'.map (fun p => p.2) v) + Stream'.zip Prod.mk x₁s x₂s + +def whiskerLeft + (X : Machine.{u}) + {Y₁ Y₂ : Machine} : + (Y₁ ⟶ Y₂) → + (tensorObj X Y₁ ⟶ tensorObj X Y₂) := + tensorHom (𝟙 X) + +def whiskerRight + {X₁ X₂ : Machine} + (f : X₁ ⟶ X₂) + (Y : Machine.{u}) : tensorObj X₁ Y ⟶ tensorObj X₂ Y := + tensorHom f (𝟙 Y) + +def tensorUnit : Machine := PUnit + +section associators + +def associator_hom : Stream' ((X × Y) × Z) → Stream' (X × (Y × Z)) := + Stream'.map fun ((a, b), c) => (a, (b, c)) + +def associator_inv : Stream' (X × (Y × Z)) → Stream' ((X × Y) × Z) := + Stream'.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 : Stream' (PUnit × X) → Stream' X := Stream'.map Prod.snd + +def leftUnitor_inv : Stream' X → Stream' (PUnit × X) := + Stream'.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 : Stream' (X × PUnit) → Stream' X := Stream'.map Prod.fst + +def rightUnitor_inv : Stream' X → Stream' (X × PUnit) := Stream'.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}) : Stream' (X × Y) → Stream' (Y × X) := Stream'.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 := + { 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} : Machine ⥤ Machine where + obj Y := Stream' X → Y + map f s n xs := f (fun m => s m xs) n + +def toFun (f : (tensorLeft X).obj A ⟶ Y) (a : Stream' A) (n : ℕ) (xs : Stream' X) : Y := + f (Stream'.zip Prod.mk xs a) n + +def invFun (g : Z ⟶ X.rightAdj.obj Y) (xas : Stream' (X × Z)) (n : ℕ) : Y := + g (Stream'.map Prod.snd xas) n (Stream'.map Prod.fst xas) + +theorem left_inv (f : (tensorLeft X).obj A ⟶ Y) : invFun (toFun f) = f := by + funext xas n + congr 1 + +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 diff --git a/references.bib b/references.bib index 2cccb928f..15b4f7801 100644 --- a/references.bib +++ b/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}, From 2b5d9fce17bb1ef93062c1cf5e2e4288a58dfa9f Mon Sep 17 00:00:00 2001 From: Matt Hunzinger Date: Wed, 8 Apr 2026 12:56:51 -0400 Subject: [PATCH 2/5] refactor: formatting --- Cslib/Foundations/Automata/Machine.lean | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/Cslib/Foundations/Automata/Machine.lean b/Cslib/Foundations/Automata/Machine.lean index 019dc9c33..50f78470f 100644 --- a/Cslib/Foundations/Automata/Machine.lean +++ b/Cslib/Foundations/Automata/Machine.lean @@ -58,16 +58,11 @@ def tensorHom Stream'.zip Prod.mk x₁s x₂s def whiskerLeft - (X : Machine.{u}) - {Y₁ Y₂ : Machine} : - (Y₁ ⟶ Y₂) → - (tensorObj X Y₁ ⟶ tensorObj X Y₂) := + (X : Machine.{u}) {Y₁ Y₂ : Machine} : (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂) := tensorHom (𝟙 X) def whiskerRight - {X₁ X₂ : Machine} - (f : X₁ ⟶ X₂) - (Y : Machine.{u}) : tensorObj X₁ Y ⟶ tensorObj X₂ Y := + {X₁ X₂ : Machine} (f : X₁ ⟶ X₂) (Y : Machine.{u}) : tensorObj X₁ Y ⟶ tensorObj X₂ Y := tensorHom f (𝟙 Y) def tensorUnit : Machine := PUnit @@ -97,11 +92,9 @@ end associators def leftUnitor_hom : Stream' (PUnit × X) → Stream' X := Stream'.map Prod.snd -def leftUnitor_inv : Stream' X → Stream' (PUnit × X) := - Stream'.map fun x => (PUnit.unit, x) +def leftUnitor_inv : Stream' X → Stream' (PUnit × X) := Stream'.map fun x => (PUnit.unit, x) -theorem leftUnitor_hom_inv_id : - leftUnitor_hom ≫ leftUnitor_inv = 𝟙 (tensorObj tensorUnit X) := rfl +theorem leftUnitor_hom_inv_id : leftUnitor_hom ≫ leftUnitor_inv = 𝟙 (tensorObj tensorUnit X) := rfl theorem leftUnitor_inv_hom_id : leftUnitor_inv ≫ leftUnitor_hom = 𝟙 X := rfl @@ -143,11 +136,11 @@ def braiding_hom (X Y : Machine.{u}) : Stream' (X × Y) → Stream' (Y × X) := 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 := - { 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 } +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 From 5f0f906a4d3dc5ae3c96f1674f2f30a1ae837df0 Mon Sep 17 00:00:00 2001 From: Matt Hunzinger Date: Wed, 8 Apr 2026 13:11:14 -0400 Subject: [PATCH 3/5] refactor: simplify and specify universe levels --- Cslib/Foundations/Automata/Machine.lean | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/Cslib/Foundations/Automata/Machine.lean b/Cslib/Foundations/Automata/Machine.lean index 50f78470f..7e1eab5b0 100644 --- a/Cslib/Foundations/Automata/Machine.lean +++ b/Cslib/Foundations/Automata/Machine.lean @@ -48,7 +48,7 @@ instance : LargeCategory Machine where def tensorObj (X Y : Machine.{u}) : Machine := X × Y def tensorHom - {X₁ Y₁ X₂ Y₂ : Machine} + {X₁ Y₁ X₂ Y₂ : Machine.{u}} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (v : Stream' (X₁ × X₂)) : @@ -58,11 +58,11 @@ def tensorHom Stream'.zip Prod.mk x₁s x₂s def whiskerLeft - (X : Machine.{u}) {Y₁ Y₂ : Machine} : (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂) := + (X : Machine.{u}) {Y₁ Y₂ : Machine.{u}} : (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂) := tensorHom (𝟙 X) def whiskerRight - {X₁ X₂ : Machine} (f : X₁ ⟶ X₂) (Y : Machine.{u}) : tensorObj X₁ Y ⟶ tensorObj X₂ Y := + {X₁ X₂ : Machine.{u}} (f : X₁ ⟶ X₂) (Y : Machine.{u}) : tensorObj X₁ Y ⟶ tensorObj X₂ Y := tensorHom f (𝟙 Y) def tensorUnit : Machine := PUnit @@ -108,8 +108,8 @@ def rightUnitor_hom : Stream' (X × PUnit) → Stream' X := Stream'.map Prod.fst def rightUnitor_inv : Stream' X → Stream' (X × PUnit) := Stream'.map fun x => (x, PUnit.unit) -theorem rightUnitor_hom_inv_id : - rightUnitor_hom ≫ rightUnitor_inv = 𝟙 (tensorObj X tensorUnit) := rfl +theorem rightUnitor_hom_inv_id : rightUnitor_hom ≫ rightUnitor_inv = 𝟙 (tensorObj X tensorUnit) := + rfl theorem rightUnitor_inv_hom_id : rightUnitor_inv ≫ rightUnitor_hom = 𝟙 X := rfl @@ -145,7 +145,7 @@ def braiding (X Y : Machine.{u}) : X ⊗ Y ≅ Y ⊗ X where instance : SymmetricCategory Machine where braiding -def rightAdj {X : Machine} : Machine ⥤ Machine where +def rightAdj {X : Machine.{u}} : Machine ⥤ Machine where obj Y := Stream' X → Y map f s n xs := f (fun m => s m xs) n @@ -155,9 +155,7 @@ def toFun (f : (tensorLeft X).obj A ⟶ Y) (a : Stream' A) (n : ℕ) (xs : Strea def invFun (g : Z ⟶ X.rightAdj.obj Y) (xas : Stream' (X × Z)) (n : ℕ) : Y := g (Stream'.map Prod.snd xas) n (Stream'.map Prod.fst xas) -theorem left_inv (f : (tensorLeft X).obj A ⟶ Y) : invFun (toFun f) = f := by - funext xas n - congr 1 +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 From a380b2d35137f03b17e46b91a326819df81c95de Mon Sep 17 00:00:00 2001 From: Matt Hunzinger Date: Wed, 8 Apr 2026 20:59:14 -0400 Subject: [PATCH 4/5] fix: add import in main Cslib module --- Cslib.lean | 1 + Cslib/Foundations/Automata/Machine.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Cslib.lean b/Cslib.lean index 3e5977af2..3fcb3c7b1 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Foundations/Automata/Machine.lean b/Cslib/Foundations/Automata/Machine.lean index 7e1eab5b0..86643522a 100644 --- a/Cslib/Foundations/Automata/Machine.lean +++ b/Cslib/Foundations/Automata/Machine.lean @@ -24,7 +24,7 @@ namespace CsLib.Automata universe u -/-- Category of machines with objects as types and morphisms as causal stream functions. -/ +/-- Category of machines with objects as types and morphisms as stream functions. -/ def Machine := Type u namespace Machine From 3c90e9f453450532f6d939a054a4317def546f69 Mon Sep 17 00:00:00 2001 From: Matt Hunzinger Date: Thu, 9 Apr 2026 21:23:45 -0400 Subject: [PATCH 5/5] =?UTF-8?q?refactor:=20change=20from=20Stream'=20to=20?= =?UTF-8?q?=CF=89Sequence?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cslib/Foundations/Automata/Machine.lean | 51 +++++++++++++------------ 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/Cslib/Foundations/Automata/Machine.lean b/Cslib/Foundations/Automata/Machine.lean index 86643522a..565180a8d 100644 --- a/Cslib/Foundations/Automata/Machine.lean +++ b/Cslib/Foundations/Automata/Machine.lean @@ -6,9 +6,9 @@ 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 -public import Mathlib.Data.Stream.Init @[expose] public section @@ -20,7 +20,7 @@ public import Mathlib.Data.Stream.Init -/ -namespace CsLib.Automata +namespace Cslib.Automata universe u @@ -32,9 +32,9 @@ namespace Machine variable {X Y Z : Machine.{u}} /-- Homomorphism as a stream function. -/ -def Hom (X Y : Machine.{u}) := Stream' X → Stream' Y +def Hom (X Y : Machine.{u}) := ωSequence X → ωSequence Y -def id (X : Machine.{u}) : Stream' X → Stream' X := fun x => x +def id (X : Machine.{u}) : ωSequence X → ωSequence X := fun x => x def comp (f : Hom X Y) (g : Hom Y Z) := g ∘ f @@ -51,11 +51,11 @@ def tensorHom {X₁ Y₁ X₂ Y₂ : Machine.{u}} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) - (v : Stream' (X₁ × X₂)) : - Stream' (Y₁ × Y₂) := - let x₁s := f (Stream'.map (fun p => p.1) v) - let x₂s := g (Stream'.map (fun p => p.2) v) - Stream'.zip Prod.mk x₁s x₂s + (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₂) := @@ -69,11 +69,11 @@ def tensorUnit : Machine := PUnit section associators -def associator_hom : Stream' ((X × Y) × Z) → Stream' (X × (Y × Z)) := - Stream'.map fun ((a, b), c) => (a, (b, c)) +def associator_hom : ωSequence ((X × Y) × Z) → ωSequence (X × (Y × Z)) := + ωSequence.map fun ((a, b), c) => (a, (b, c)) -def associator_inv : Stream' (X × (Y × Z)) → Stream' ((X × Y) × Z) := - Stream'.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 @@ -90,9 +90,9 @@ def associator end associators -def leftUnitor_hom : Stream' (PUnit × X) → Stream' X := Stream'.map Prod.snd +def leftUnitor_hom : ωSequence (PUnit × X) → ωSequence X := ωSequence.map Prod.snd -def leftUnitor_inv : Stream' X → Stream' (PUnit × X) := Stream'.map fun x => (PUnit.unit, x) +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 @@ -104,9 +104,9 @@ def leftUnitor (X : Machine.{u}) : tensorObj tensorUnit X ≅ X where hom_inv_id := leftUnitor_hom_inv_id inv_hom_id := leftUnitor_inv_hom_id -def rightUnitor_hom : Stream' (X × PUnit) → Stream' X := Stream'.map Prod.fst +def rightUnitor_hom : ωSequence (X × PUnit) → ωSequence X := ωSequence.map Prod.fst -def rightUnitor_inv : Stream' X → Stream' (X × PUnit) := Stream'.map fun x => (x, PUnit.unit) +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 @@ -131,7 +131,8 @@ instance : MonoidalCategory Machine where open MonoidalCategory -def braiding_hom (X Y : Machine.{u}) : Stream' (X × Y) → Stream' (Y × X) := Stream'.map Prod.swap +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 @@ -146,14 +147,14 @@ instance : SymmetricCategory Machine where braiding def rightAdj {X : Machine.{u}} : Machine ⥤ Machine where - obj Y := Stream' X → Y - map f s n xs := f (fun m => s m xs) n + 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 : Stream' A) (n : ℕ) (xs : Stream' X) : Y := - f (Stream'.zip Prod.mk xs a) 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 : Stream' (X × Z)) (n : ℕ) : Y := - g (Stream'.map Prod.snd xas) n (Stream'.map Prod.fst xas) +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 @@ -185,4 +186,4 @@ instance : MonoidalClosed Machine where end Machine -end CsLib.Automata +end Cslib.Automata