ideas for first contribution

Stream: CSLib

[Ira Fesefeldt]

I currently have a bit more time on hand and wanted to use that on contributing to nice projects. And I think CSLib could be such a nice project, but I'm a bit lost where I my contributions could be valuable.

I recently finished my phd on theoretical computer science in program verification, in case my expertise level is relevant. I thought the Algorithms folder still looks a bit empty, but I'm open for any ideas.

Any recommendations where/what I could contribute?

[Arjun Bhamra]

I wanted to join this discussion to also ask where contributions would be appreciated; this is my first foray into open source Lean. @Ira Fesefeldt, I was leaning towards adding more sorting algorithms to CSLib, like insertion sort, etc., as they are integral to the CS curriculum at most universities. Would that be appreciated, or are there other algorithms to focus on instead?

[Shreyas Srinivas]

The algorithms section is empty partly because Boole hasn’t landed yet and partly because we are still not fixed on the correct modelling of algorithms. There is the very lightweight cslib#165 which has been merged and there is (imo) the more systematic version that’s still WIP (cslib#201)

[Shreyas Srinivas]

The latter is mine and I will get to finishing jt soon modulo some other upcoming deadline constraints.

[Shreyas Srinivas]

I understand that there is a lot to do on the automata and logic side as well and it is in better shape.

[Arjun Bhamra]

Shreyas Srinivas said:

I understand that there is a lot to do on the automata and logic side as well and it is in better shape.

Are there any specific areas you could point me to, PRs/issues or otherwise? I'd love to help (assuming the barrier to entry isn't too high for me). Thanks for the heads-up w.r.t the Algorithms section.

[Chris Henson]

I can point to a couple of things I know of:

• Cslib.Foundations.Data.Relation has recently expanded a bit, but still likely missing pretty basic theorems. Exercises in Chapter 2 of the listed reference could be good for instance.
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_diamond is a complete but overly long proof that I would love for someone to clean up. In PLFA for instance they have a very nice proof (using what is sometimes called the Takahashi translation) that I had trouble getting to work with locally nameless syntax
• I would be happy to review any proofs of strong normalization for the existing locally nameless lambda calculi (there is currently untyped, STLC, and System F with subtyping). The locally nameless part can make things tricky and I'm going to in the hopefully near future encourage a different binding scheme for most of CSLib, but it would still be valuable to have these proofs.

[Arjun Bhamra]

Sounds good, I'll try taking a look at the Relation file and "Term Rewriting and All That" (great name for a book); thanks!

[Oliver Soeser]

I'd also be very interested in helping with Relation! Is there anything important to watch when contributing?

[Chris Henson]

One oddity is that to my knowledge there isn't an upstream definition of just the symmetric closure of a relation, so feel free to add this definition if you need it. You may find yourself wanting certain inductions that haven't been defined yet, these would be welcome contributions as well. If there's any questions about the right way to state a missing definition, please ask here and I'd be happy to discuss.

[Snir Broshi]

Chris Henson said:

One oddity is that to my knowledge there isn't an upstream definition of just the symmetric closure of a relation

docs#CompRel, but it should probably be renamed Relation.SymmGen and moved to Mathlib.Logic.Relation

[Ching-Tsun Chou]

I'm working on porting the results in my earlier automata theory project:
https://github.com/ctchou/AutomataTheory
into cslib. But there are still many interesting results in automata theory which are not in my plan. Here are some examples off the top of my head:

• Regular expressions as another characterization of regular languages.
• Brzozowski's algorithm (https://en.wikipedia.org/wiki/DFA_minimization#Brzozowski's_algorithm).
• The connection between Büchi automata and monadic second-order logic.

[Chris Henson]

Snir Broshi said:

docs#CompRel, but it should probably be renamed Relation.SymmGen and moved to Mathlib.Logic.Relation

Thanks for sharing this! I agree, and it appears this file is not imported anywhere at the moment, so probably an easy change.

[Kim Morrison]

This is not a small project, but I really really hope the CSLib instigates a good Float library for Lean. This seems like one of the highest impact possible projects, and of course there is an excellent model to follow from Rocq.

[Ira Fesefeldt]

I was already in the process of telling myself that I shouldn't try to work on/port a Float library :|

[Ching-Tsun Chou]

Kim Morrison said:

This is not a small project, but I really really hope the CSLib instigates a good Float library for Lean.

Any specific Rocq works do you have in mind?

[Dexin Zhang]

Ching-Tsun Chou said:

Any specific Rocq works do you have in mind?

I guess it's Flocq

[Arjun Bhamra]

Chris Henson said:

Snir Broshi said:

docs#CompRel, but it should probably be renamed Relation.SymmGen and moved to Mathlib.Logic.Relation

Thanks for sharing this! I agree, and it appears this file is not imported anywhere at the moment, so probably an easy change.

Just to clarify, we'd want to hold off on any formalization of symmetric closure within CSLib's Relation.leanuntil CompRel is moved? There are probably other theorems/exercises that don't require symmetric closure, will try to find those

[Chris Henson]

You can still use CompRel in the meantime.

[Thomas Waring]

Chris Henson said:

... proofs of strong normalization for the existing locally nameless lambda calculi

Do you have any thoughts about how (or if, I suppose) we should go about formalising logical relations / reducibility candidates? It would be nice if some of those arguments could be generalised across different calculi & different results, but I don't really see how one would go about that

[Chris Henson]

Thomas Waring said:

Chris Henson said:

... proofs of strong normalization for the existing locally nameless lambda calculi

Do you have any thoughts about how (or if, I suppose) we should go about formalising logical relations / reducibility candidates? It would be nice if some of those arguments could be generalised across different calculi & different results, but I don't really see how one would go about that

I'm not sure either. As I've mentioned before, I have plans for adapting work from Isabelle and Rocq for unifying binding across CSLib, essentially metaprograms that give you an inductive definition and tactics. The work that is maybe the closest analogy to that for logical relations is Beluga (see these slides too) and contextual types, but I'm not as comfortable with what this would look like in Lean. I'm very open to experimentation that builds on this literature if that's something you're interested in, it's just a bit more unfamiliar to me personally and possibly somewhat uncharted territory.

[Ira Fesefeldt]

Ching-Tsun Chou said:

I'm working on porting the results in my earlier automata theory project:
https://github.com/ctchou/AutomataTheory
into cslib. But there are still many interesting results in automata theory which are not in my plan. Here are some examples off the top of my head:

• Regular expressions as another characterization of regular languages.
• Brzozowski's algorithm (https://en.wikipedia.org/wiki/DFA_minimization#Brzozowski's_algorithm).
• The connection between Büchi automata and monadic second-order logic.

As far as I can tell, there is already quite some work done on the characterization of regular languages as regular expressions in mathlib (regular expressions themselves are there defined already, the thompson construction exists twice as pr). Is the general plan to move such results to Cslib or...?

[Chris Henson]

The idea of moving things from Mathlib to CSLib, contingent on agreement from both groups of maintainers, has been discussed but there is no active effort to do so yet. Especially considering CSLib is a very new project in comparison to Mathlib, there is no rush to do so until everyone feels comfortable that this makes sense in the long term. As we are downstream of Mathlib, we can easily extend existing Mathlib modules in CSLib. We have done so in a few cases, including upstreaming back to Mathlib when appropriate. In other cases we have some definitions that diverge slightly, but have proofs of equivalence.

[Ching-Tsun Chou]

Yes, the definition of regular expressions exists in mathlib. But the closures of regular languages under boolean operations appeared in mathlib only a month ago and the PRs for the closures under concatenation and Kleene star are still open. You can't prove the equivalence between regular expressions and regular languages without those results. After my PRs cslib#239 and cslib#241 are closed, those result will exist in cslib.

Also, the automata infrastructure in cslib strives to treat automata on finite words and automata on infinite words in as uniform a fashion as possible. There is nothing about automata on infinite words in mathlib.

[Kat Zhuchko]

Hi all :smiling_face: Since the discussion came up, I’m also curious about the future of regular expressions in CSLib.

Mathlib’s definition of regexes currently does not have complement and intersection (I'm asking because I’ve formalized algorithms for these operations before). If I wanted to build on the existing Mathlib definitions, what would be the recommended way to integrate these new constructors into CSLib?

I’m also interested in a more general symbolic setting, where single characters are replaced by predicates. Again, is it preferable to keep the standard definition and work on a parallel version, or is there room for a discussion about generalising the definition to symbolic alphabets (which subsumes the classical one). I’d love to hear what the maintainers consider the cleanest approach for such generalisations.

[Chris Henson]

Hey Kat, nice to hear from you! :) I'm not so familiar with this material so sorry in advance if I misunderstand anything, but I can answer your questions from the maintainer perspective

If I wanted to build on the existing Mathlib definitions, what would be the recommended way to integrate these new constructors into CSLib?

For areas where definitions exists in Mathlib and we're happy to continue using those definitions in CSLib, we welcome PRs that extend currently existing Mathlib namespaces. As an example, there is Cslib.Foundations.Data.Relation with some additional definitions about relations that have more of a CS flavor.

Again, is it preferable to keep the standard definition and work on a parallel version, or is there room for a discussion about generalising the definition ...

This is a bit of a judgement call. As an example for automata, we use some different definitions from Mathlib because they extend some CSLib-specific definitions. Some places we have theorems relating to the Mathlib equivalent, like Cslib.Computability.Languages.RegularLanguage.

So in short, we try our best to avoid unnecessary duplication of Mathlib, but we are in general welcoming of PRs that define something with more generality than Mathlib. It sounds like this your situation, so I think we'd welcome the more general extension to symbolic alphabets, ideally with a proof connecting it to any existing Mathlib work. Does that answer your questions?

[Shreyas Srinivas]

I second Chris’s idea fwiw. Mathlib is a great library to depend on, but CSlib should not chain itself to Mathlib’s design decisions. If Mathlib likes our definitions then they can discuss with us about upstreaming it. There are two other factors to consider :

1. Making up steaming PRs is quite a bit of extra non-lean work.
2. CSLib should ideally be self contained for CS concepts, not just a patch on what is missing in mathlib. That will make CSLib a mess with bits and pieces here, and bits and pieces in mathlib.

[Kat Zhuchko]

Thanks a lot for the helpful reply. I will think about more about how to best structure it and come back when I have something reasonably settled for a potential PR!