A Formalisation of the Myhill-Nerode Theorem using Regular Expressions only

Christian Urban

There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. 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. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. I will show that most parts of formal language theory, including the Myhill-Nerode Theorem, can be formalised using only regular expressions. The central notions in this work are derivatives and partial derivatives of regular expressions.