equal
deleted
inserted
replaced
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 that 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 defined as inductive datatype. Also |
39 or matrices, neither of which can be defined as inductive datatype. Also |
40 operations, such as disjoint unions 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 conveniently |
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. |
46 \end{abstract} |
46 \end{abstract} |