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

[matthunz]

Adds a new Foundations.Automata.Machine module following Minimal realization of machines in closed categories.

This new Machine category can act as a building block for automata in category theory (like digital circuits) by providing the foundational instances of a MonoidalClosed SymmetricCategory.

/-- Category of machines with objects as types and morphisms as stream functions. -/
def Machine := Type u

/-- Homomorphism as a stream function. -/
def Hom (X Y : Machine.{u}) := Stream' X → Stream' Y

[ctchou]

I don't know anything about monoidal category. But I noticed that this PR adds code to the namespace Cslib.Automata, which is currently used by (traditional) automata theory. I'm just wondering whether this new code would cause confusion.

[matthunz]

That makes sense 👍 I was trying to match what I saw here like CsLib.Logic being used in CsLib/Foundations/Logic and CsLib/Logics but I definitely wouldn't be opposed to moving things around, maybe it'd be better under something like CsLib.CategoryTheory.Automata so everything related to category theory is in one spot?

[chenson2018]

Maybe we'd try to make it match #391 and be in a subdirectory in Automata? I'd wait to move things around until after the PR is initially reviewed.

[ctchou]

BTW, I noticed that mathlib's Stream' is used in this PR. Although mathlib's Stream' looks like infinite sequences, it is actually not intended as infinite sequences; see this very long discussion:
#mathlib4 > Why is Stream' called Stream'?
If you really want infinite sequences, you should use cslib's ωSequence in Cslib/Foundations/Data/OmegaSequence.

[matthunz]

Huh alright I read through some of that discussion and I still don't totally understand the difference but I'll defer to your thinking.

Changed in 3c90e9f (which helped me catch that I actually had this under CsLib instead of Cslib 😅)

[ctchou]

I think the upshot is that if all you want is infinite sequences in the naive sense (namely, basically Nat → T for some type T), you should use ωSequence, which now also has more API than Stream'.

[matthunz]

Oh good to know 👍I didn't notice the extra API in ωSequence which I definitely think I can make use of in some other stuff