Formal language theory

Stream: general

[Henrik Böving]

Rather out of curiosity: Does there exist work in Lean about formal language theory? So stuff like grammars, automata, turing machines etc. I've looked around a bit on the Internet but didn't really find anything but I'm guessing if there is something I missed out on people here will know about it.

[Ruben Van de Velde]

There's https://leanprover-community.github.io/mathlib_docs/computability/turing_machine.html for TMs

[Bryan Gin-ge Chen]

There are also DFA, NFA and language files in the computability directory (you should be able to navigate to them from the link above using the menu on the left).

[Yaël Dillies]

Yeah @Fox Thomson has done a bunch of this. He's currently on an internship doing Isabelle, but might be worth reaching out!

[Fox Thomson]

I've been working on regular languages and finite automata but unfortunately haven't had time for it recently. We have all the definitions and a proof of the pumping lemma but there's still work to be done. The next big milestone is showing DFA's and regular languages are the same thing.

[Henrik Böving]

Yeah I saw those TODOs in the regexp file, I would definitely be interested in working at that or maybe Pushdown Automata which are still missing as far as I can see but I wouldn't consider my Lean good enough (yet) to work on something like that.