The Myhill-Nerode theorem, proved using regular expressions

Stream: maths

[Chris Wong]

Found this interesting paper. This might give us a way to formalize regular languages without depending on automata (and graphs).

https://nms.kcl.ac.uk/christian.urban/Publications/rexp.pdf

[Scott Morrison]

The two sentences

Unfortunately, automata are not so straightforward to
formalise in theorem provers. The reason is that natural representations for automata are
graphs, matrices or functions, none of which are inductive datatypes.

sounds very strange relative to mathlib! :-)

[Scott Morrison]

And a little bit later:

Systems such as Coq permit quantification over
types and thus can state such a definition. This has been recently exploited in an elegant and
short formalisation of the Myhill-Nerode theorem in Coq by Doczkal et al. (2013), but as
said this is not available to us working in Isabelle/HOL.

suggests that this approach is not going to be a natural one for Lean.

[Chris Wong]

Yeah, I can see how we're not constrained in the same way Isabelle/HOL folks are :P

What do you mean by it being unnatural?

[Chris Wong]

(I guess since Myhill-Nerode is so easy to prove in terms of automata, any other approach will feel unnatural in comparison? :shrug: )

[Scott Morrison]

No -- I just meant that they are essentially complaining about the lack of dependent types, and point out that it was straightforward to formalise in Coq, and presumably for this problem Coq and Lean will be pretty equivalent.

[Chris Wong]

Yeah, I found this repo soon afterward (along with a bunch of papers):

https://github.com/coq-community/reglang

I guess a Lean translation of this would be quite doable, but not very interesting (in terms of research value)

[Alex J. Best]

There seem to be quite a few different implementations in coq with different aims. The connection with decision procedures for presburger arithmetic (aka omega in lean) sounds really cool though to me.