equal
deleted
inserted
replaced
48 side a connection with regular expressions. Unfortunately, automata are difficult |
48 side a connection with regular expressions. Unfortunately, automata are difficult |
49 to formalise in HOL-based theorem provers. The reason is that |
49 to formalise in HOL-based theorem provers. The reason is that |
50 they need to be represented as graphs, matrices or functions, none of which |
50 they need to be represented as graphs, matrices or functions, none of which |
51 are inductive datatypes. Also convenient operations for disjoint unions of |
51 are inductive datatypes. Also convenient operations for disjoint unions of |
52 graphs and functions are not easily formalisiable in HOL. In contrast, regular |
52 graphs and functions are not easily formalisiable in HOL. In contrast, regular |
53 expressions can be defined conveniently as datatype and a corresponding |
53 expressions can be defined conveniently as a datatype and a corresponding |
54 reasoning infrastructure comes for free. We show in this paper that a central |
54 reasoning infrastructure comes for free. We show in this paper that a central |
55 result from formal language theory---the Myhill-Nerode theorem---can be |
55 result from formal language theory---the Myhill-Nerode theorem---can be |
56 recreated using only regular expressions. |
56 recreated using only regular expressions. |
57 |
57 |
58 \end{abstract} |
58 \end{abstract} |
59 |
59 |
60 |
60 |
61 \input{session} |
61 \input{session} |
62 |
62 |
63 \mbox{}\\[-10mm] |
63 %%\mbox{}\\[-10mm] |
64 \bibliographystyle{plain} |
64 \bibliographystyle{plain} |
65 \bibliography{root} |
65 \bibliography{root} |
66 |
66 |
67 \end{document} |
67 \end{document} |
68 |
68 |