dfa and regular expressions

Stream: general

[Frederick Pu]

Hi, I'm currently taking theory of computation in university and we're go over the proof that the set of all languages accepted by regular expressions are the set of all regular languages.

I was wondering if I could get a PR for formalizing this equivalence.

[Yaël Dillies]

Hey! I believe this was already formalised, although I don't quite remember where... :thinking:

[Yaël Dillies]

Regardless, you should feel free to work on this. Just be aware that you might be duplicating work, if that matters to you

[Frederick Pu]

image.png

[Frederick Pu]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/RegularExpressions.html#RegularExpression

[Yaël Dillies]

This specific TODO was addressed. Let me find the PR

[Yaël Dillies]

#12648 and around

[Frederick Pu]

so where could i find this on mathlib?

[Yaël Dillies]

Looks like it wasn't merged. I would suggest you try to work with the authors @Tom Kranz and @Russell Emerine to get the PRs in mathlib

[Kim Morrison]

#12648 is not the PR to look at: it was obsoleted by a series of smaller PRs.

[Kim Morrison]

• feat(Data/FinEnum): Option instance and Type recursor #15647
• feat(Computability): introduce Generalised NFA as bridge to Regular Expression #15649
• feat(Computability/NFA): operations for Thompson's construction #15651
• feat(Computability): language-preserving maps between NFA and RE #15654

[Kim Morrison]

Those PRs do indeed appear to be stuck at awaiting-author.

[Frederick Pu]

how does that work? are they in draft or smth

[Kim Morrison]

The awaiting-author label means that a reviewer has asked questions, or requested changes, and the author needs to respond, and then remove the awaiting-author label themselves, so the PR returns to visibility on the #queue.

[Kim Morrison]

Fairly often, however, PRs end up stuck in that state, and it doesn't hurt for an interested party to politely ping them about it. :-)

[Frederick Pu]

why are they proving nfa is equivalent to regular expression? wouldnt it be easier to do dfa <-> regular expression? and then nfa <-> dfa?

[Tom Kranz]

I didn't know I had to remove the label myself; thank you for the explanation! Y'all are catching me at a good time, since I've got a bit of breathing room right now to look over the merge requests and see what (if anything) hasn't been adressed.