Move automata theory in mathlib to CSLib?

Stream: mathlib4

[Fabrizio Montesi]

Is there interest in moving automata theory from mathlib to cslib perhaps? Reviewing efforts currently span over the two libs (#mathlib4 > Regular languages: the review queue ), and it would certainly be good to unify the APIs (some of the convenient APIs we use in CSLib to define automata are out of scope for mathlib).

We really try to avoid duplicating results in CSLib, but sometimes this requires developing boilerplate. That's ok per se, but sometimes it's not so straightforward to tell people when they should just go for a CSLib 'native' API approach or instead direct them to go through a mathlib compat layer to reuse results in mathlib somehow... it also depends on how much proof automation can help with the compat theorems.

(In fact, one could even make an argument for moving all of computability to CSLib, but for now I'd like to have a more focused discussion.)

[Chris Henson]

A relevant thread from a couple of months ago that expressed some concerns with moving things from Mathlib to CSLib: #mathlib4 > Is there a plan to offload Mathlib.Computability to Cslib?

I would guess that some of these concerns are still held. I think (as a CSLib maintainer, but a single opinion) that there is merit to the idea that some areas of Mathlib might have been in CSLib to begin with if it existed earlier. At the same time however, I am open to the idea but not in a rush to move anything. While I have personally made a large effort to make CSLib adhere to the standards that Mathlib uses, there is a differential that comes with experience. As the person who is often maintaining the nightly testing and Mathlib compatibility, I am very willing to take a longer timeline on this to ensure that we are all comfortable with what it would mean to move anything to CSLib.

[Fabrizio Montesi]

Thanks for your availability. We should definitely take our time in doing it, if we do it.

That thread contains some good points.
In general, if the relevant people are comfortable contributing to cslib, then moving computability things to cslib sounds reasonable to me. Computability is a vast topic, with results and APIs that clearly don't fall into mathlib's current reviewing interests. It'd be good to put it in one place.

[Snir Broshi]

Fabrizio Montesi said:

if the relevant people are comfortable contributing to cslib

Should we tag them? (I'm not sure what's the etiquette)

[Snir Broshi]

and by "them" I'm thinking of everyone involved in #31247

[Fabrizio Montesi]

Sure, thanks. I was unsure as to whom to reach out to.

[Fabrizio Montesi]

Btw, that's an example of parallel APIs in the making: https://leanprover.github.io/cslib/docs/Cslib/Computability/Automata/DA/Prod.html

Some operations can be generally stated for (F)LTSs, which are out of mathlib's scope, so CSLib is destined to have some parallel work on discrete/probabilistic/etc. automata.

[Ching-Tsun Chou]

I think, as a matter of courtesy, everyone in the following thread should be notified of this discussion:
#mathlib4 > Regular languages: the review queue

[Snir Broshi]

@Rudy Peterson @Yaël Dillies

[Yaël Dillies]

I see this move as a good idea. I'm happy to review computability theory, but I am not particularly qualified to do so

[Bolton Bailey]

How do we feel about moving other components of Computability/ to CSLib, such as the development of Turing Machines and Polynomial time computation? After adding P vs NP to formal-conjectures, I have been thinking of doing a larger Turing-machine based development of complexity classes in CSLib#192, but I think it would be a bit awkward if the definitions and higher-level lemmas about them straddle the libraries.

[Bolton Bailey]

Oh, sorry, I see now that you mentioned you wanted this discussion to be more focused, perhaps I will share my thoughts in the other thread linked above.

[Rudy Peterson]

I would be interested in adding libraries for weighted language theory, which may be a better fit for CSLib: #mathlib4 > Weighted Formal Languages

[Ching-Tsun Chou]

Are there some good references on weighted formal langauges?

[Yury G. Kudryashov]

Does CSLib depend on Mathlib? Some parts of the automata theory can be very useful in dynamics (but we aren't there yet).

[Ching-Tsun Chou]

Yes, very much so

[Chris Henson]

Yury G. Kudryashov said:

Does CSLib depend on Mathlib? Some parts of the automata theory can be very useful in dynamics (but we aren't there yet).

Yes, we do.

[Mario Carneiro]

I don't see why this requires moving anything anywhere. You can PR things to mathlib to make the automata theory that exists more consistent with the cslib design

[Fabrizio Montesi]

Won't it always require boilerplate? How will I make things like NFA use the defs and results about LTS from cslib? (Which is what we do in cslib.)

[Mario Carneiro]

the boilerplate only happens if you have two equivalent but unequal definitions. You should avoid that by upstreaming and downstreaming things until they are using the same definitions

[Rudy Peterson]

Ching-Tsun Chou said:

Are there some good references on weighted formal langauges?

The main resource I've based my work on is: https://drive.google.com/file/d/1wXv-e5tL6WxwK7vzBuVSDySYjkuoGW7f/view
This book is associated with this course: https://rycolab.io/classes/aflt-s24/

This textbook also seems good: https://link.springer.com/book/10.1007/978-3-642-01492-5

[Eric Wieser]

Mario Carneiro said:

You should avoid that by upstreaming and downstreaming things until they are using the same definitions

To elaborate, I think this is generally a reasonably good worflow:

• Look at the mathlib definition, and conclude that it might not quite work for your use-case
• Try a new definition downstream, duplicating some API, and investigate whether the new definition actually ends up more convenient.
• Once the new definition is stable (for instance, I think CSLib has redefined NFA a few times), consider upstreaming the design by merging it into the mathlib version

[Fabrizio Montesi]

So far I can see five opinions for, a few neutrals, and one opinion against. More opinions are always welcome. There's also been some discussion about computability at large, but that's less pressing and imo we can discuss that later, case by case.

I'd like to get a better idea of what a good process would be (if we decided to go ahead). Rough draft:

1. We declare the intention to move and create a dedicated topic.
2. PRs to add the content of automata theory from mathlib are submitted to the cslib repo. These PRs refactor defs to align with cslib's design (types go under the Cslib namespace, theorems from other parts of cslib are reused when it makes sense, etc.).
3. When we're all happy with the code in cslib, automata theory files are deprecated in mathlib with a pointer to cslib.

[Mario Carneiro]

If the types moved to mathlib, they would not be under the Cslib namespace, of course. You could alias them to the Cslib namespace but I don't see why you would Oh, you mean for moving from mathlib to cslib

[Mario Carneiro]

Note that steps 1 and 2 can be done in cslib without step 3. That corresponds to Eric's first two bullets

[Fabrizio Montesi]

Yes, that's by design. :⁠-⁠)

[Mario Carneiro]

which is to say, you can start with that and delay deciding whether mathlib will defer to cslib or vice versa once you have your better design (i.e. step 1 can come after step 2)

[Fabrizio Montesi]

I can probably live with that, but let me take a round of internal discussion.