OmegaLanguage

Stream: CSLib

[Ching-Tsun Chou]

I started a PR cslib#92 on ωLanguage, which is the infinite-word analogue of Mathlib.Computability.Language. If anyone has a better idea for the definition of omegaPower, please let me know. One of my goals is to port the theorems in:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Languages/Basic.lean
some of which are pretty nasty to prove. I can definitely use some better ideas.

[Thomas Waring]

Is it true that L^ω = (L∗)↗ω? — that might not be easier to work with as a definition but it is at least cleaner (or seems so to me)

[Ching-Tsun Chou]

L^ω ⊆ (L∗)↗ω is certainly true, but I'm not too sure about the other direction. I'm working on an alternative definition of L^ω that uses an ωSequence version of flatten, in a manner analogous to how L∗ is defined in Mathlib.Computability.Language. We will see whether this makes the proofs easier

[Ching-Tsun Chou]

The PR cslib#92 for OmegaLanguage is now ready for review. The proofs of the harder results have been much improved relative to:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Languages/Basic.lean
We now have enough results about OmegaLanguage to start developing the theory of ω-automata.
CC: @Chris Henson , @Fabrizio Montesi

[Fabrizio Montesi]

That looks pretty good to me. I'd just like to point out this PR creates the Computability/Languages/ directory with this (containing Language and OmegaLanguage), which seems ok to me, in case anybody wants to comment on that.

[Chris Henson]

That did pass my notice, but I think it's fine? Maybe Languages.Languages is mildly confusing, but it's probably okay.

[Ching-Tsun Chou]

Actually the names of leaf files are in singular, not plural, forms. I expect Computability/Languages/ to get more files, such as OmegaRegularLanguage.lean.