Regular languages: the review queue

Stream: mathlib4

[Maja Kądziołka]

As detailed in #24205, there's currently quite a mess of many PRs in the regular languages area of Computability, with some of the PRs overlapping each other. As @Yury G. Kudryashov suggests, it would be good to discuss how to resolve this.

The main goal these all center around is the equivalence between regular expressions and finite automata, as well as the related area of constructing automata corresponding to various operators on languages.

Here's a list of PRs that somehow overlap one another:

• a series of PRs by @Tom Kranz , that proves equivalence between REs and NFAs, avoiding the epsilon-NFA step:
  • #15649 (GNFAs, going NFA -> GNFA -> RE)
  • #15651 (NFA union, concatenation, Kleene's star, i.e. majority of the RE -> NFA direction)
  • #15654 (the punchline: RE <-> NFA)
• a PR by @Anthony DeRossi which does RE -> epsilon-NFA conversion #20648
• a PR by @Rudy Peterson which implements NFA union, intersection and reversal #22361, which overlaps:
  • #15651 by @Tom Kranz, mentioned above, which also includes NFA union
  • #21573 by @Chris Wong, which does NFA reversal (notably this PR already got approved, but has merge conflicts)
  • #20238 by @Mehmet Emre , which does DFA complement and intersection

One key issue is the question: do we want to have e.g. intersection on both DFAs and NFAs? They show the same underlying facts about the class of regular languages, but they could have utility should one desire to put bounds on the number of states of an automaton...

I'd be interested to hear your ideas on how to resolve this going forward!

[Yury G. Kudryashov]

I think that it makes sense to have operations on different types of automata, even if they have equal power in terms of languages. It would be nice if the authors of the competing PRs

• review each other's PRs;
• resolve differences in design choices, if any; feel free to tag me here with questions;
• reach the state where PRs are compatible with each other;
• tag me here with the list of relevant PRs in the order they should be reviewed. I'll try to find time to review them quickly.

[Maja Kądziołka]

Okay. Then another issue is whether we want both the direct RE -> NFA and the RE -> eps-NFA constructions.

[Shreyas Srinivas]

I think there is a reasonable conceptual distinction between the different constructions. Technically what one is proving is “given any RE, applying <insert method name> transformation, one gets an equivalent automaton”

[Shreyas Srinivas]

The equivalence claim can be separately expressed as “there exists a transformation such that for any RE …”

[Yury G. Kudryashov]

Having different constructions that lead to the same statement about languages is fine with me, as long as the constructions reference each other in their docs and explain the differences there.

[Yury G. Kudryashov]

E.g., one can use them to transform specific regular expressions to automata.

[Chris Wong]

Regarding NFA reversal.

• I'm unfortunately really busy lately so don't have time to have a close look – it would be great if someone else could help with the merge conflict.
• From a cursory look at Rudy's approach, I prefer my one. The key differences are (a) the individual parts of the reversed NFA are defined separately, and (b) using Exists + Mem instead of Disjoint, and I don't consider those changes to be an improvement.