formalizing context free grammars and lr parsers

Stream: general

[Paige Thomas]

I'm starting to embark on a project to do this, and I'm just wondering if anyone might have any general advice or pointers to resources. So far I have found this and this, and am coding here for now.

[Yaël Dillies]

Did you ask @Martin Dvořák ?

[Paige Thomas]

No, why?

[Yaël Dillies]

Actually, are you at all aware of docs#ContextFreeGrammar ?

[Paige Thomas]

yeah, I think this will involve a lot more though.

[Yaël Dillies]

Sure, I'm just seeing your Lean file and thinking "The whole first few hundred lines are already in mathlib" :smile:

[Paige Thomas]

:)

[Rida Hamadani]

There is also #13514

[Martin Dvořák]

My main advice is that, if you want your work to be useful for the community, you should not be reïnventing Mathlib.
Instead, look at what Mathlib already has in this directory:
https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Computability
Create PRs with whatever is missing and you need for your work.

[Paige Thomas]

To be honest, the idea of contributing to Mathlib is pretty anxiety inducing. My workflow doesn't tend to lend itself to a stable API.

[Violeta Hernández]

Well, that's why the review process exists! We're glad to help suggest improvements.

[Riccardo Brasca]

Please don't be stressed about the review! Sometimes it takes time (just because we are all busy) but we are very happy to have new contributors. If you are unsure about anything, feel free to ask here!

[Damiano Testa]

Besides, a repository with some developed theory is useful to the community, even if it is not in mathlib!

[Ira Fesefeldt]

I felt that overcoming my anxiety this year contributing to mathlib was one of the best ideas to get better at lean, because I felt that the reviews were always very helpful, nice and productive.

[Yaël Dillies]

... and I liked your PRs!

[Martin Dvořák]

Kayla Thomas said:

To be honest, the idea of contributing to Mathlib is pretty anxiety inducing. My workflow doesn't tend to lend itself to a stable API.

Your repository will still be useful as a standalone project if it is compatible with Mathlib.
Less so if it competes against Mathlib (in the sense that you write your own definitions of DFA, CFG, etc and prove some results about them that are not proved for the DFA, CFG, etc in Mathlib).

[Shreyas Srinivas]

Counterpoint, don't focus on integrating things with Mathlib. Freely try things out, and see what works. You can leave the integration with mathlib for a later point. People will still be happy to help.

[Shreyas Srinivas]

(deleted)

[Paige Thomas]

Thank you all :) I'm kind of leaning towards @Shreyas Srinivas 's suggestion for now, in part because there is a large PhD thesis of HOL4 code on context free grammars that I want to try and translate closely from.

[Paige Thomas]

If anyone is interested, this is the HOL4 code: https://github.com/mn200/CFL-HOL
I'm starting with: https://github.com/mn200/CFL-HOL/blob/master/lib/grammarDefScript.sml

[Paige Thomas]

(deleted)