33 \begin{abstract} |
33 \begin{abstract} |
34 There are numerous textbooks on regular languages. Nearly all of them |
34 There are numerous textbooks on regular languages. Nearly all of them |
35 introduce the subject by describing finite automata and |
35 introduce the subject by describing finite automata and |
36 only mentioning on the side a connection with regular expressions. |
36 only mentioning on the side a connection with regular expressions. |
37 Unfortunately, automata are a hassle for formalisations in HOL-based |
37 Unfortunately, automata are a hassle for formalisations in HOL-based |
38 theorem provers. The reason is they need to be represented as graphs |
38 theorem provers. The reason is that they need to be represented as graphs |
39 or matrices, neither of which can be easily defined as datatype. Also |
39 or matrices, neither of which can be defined as inductive datatype. Also |
40 operations, such as disjoint union of graphs, are not easily formalisiable |
40 operations, such as disjoint unions of graphs, are not easily formalisiable |
41 in HOL. In contrast, regular expressions can be defined easily |
41 in HOL. In contrast, regular expressions can be defined easily |
42 as datatype and a corresponding reasoning infrastructure comes for |
42 as datatype and a corresponding reasoning infrastructure comes for |
43 free. We show in this paper that a central result from formal |
43 free. We show in this paper that a central result from formal |
44 language theory---the Myhill-Nerode theorem---can be recreated |
44 language theory---the Myhill-Nerode theorem---can be recreated |
45 using only regular expressions. |
45 using only regular expressions. |