Closure properties of DFAs (and regular expressions)

Stream: Is there code for X?

[Kin Yau James Wong]

Has anyone started working on closure properties of DFAs and regular expressions, i.e. closure under unions, star etc.? If not, perhaps I might start working on that.

[Shreyas Srinivas]

You could work on this using Dexter Kozen's book. It has a very neat presentation of all the proofs.

[Martin Dvořák]

FYI, I have an ongoing work on closure properties of higher levels in the Chomsky hierarchy.

[Kin Yau James Wong]

Martin Dvořák said:

FYI, I have an ongoing work on closure properties of higher levels in the Chomsky hierarchy.

Sounds great! I will mainly stick with DFAs and Regular expressions.

[Martin Dvořák]

I recommend proving that finite automata and regular expressions recognize the same languages. First, it is something we want to have. Second, some of the closure properties will immediately follow.

[Kin Yau James Wong]

I believe some others are already working on formalizing their equivalence though

[Stefan Hetzl]

Indeed. There are pull requests #15649, #15651, and 15654 on that topic.