equal
deleted
inserted
replaced
55 they need to be represented as graphs, matrices or functions, none of which |
55 they need to be represented as graphs, matrices or functions, none of which |
56 are inductive datatypes. Also convenient operations for disjoint unions of |
56 are inductive datatypes. Also convenient operations for disjoint unions of |
57 graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular |
57 graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular |
58 expressions can be defined conveniently as a datatype and a corresponding |
58 expressions can be defined conveniently as a datatype and a corresponding |
59 reasoning infrastructure comes for free. We show in this paper that a central |
59 reasoning infrastructure comes for free. We show in this paper that a central |
60 result from formal language theory---the Myhill-Nerode theorem---can be |
60 result from formal language theory---the Myhill-Nerode Theorem---can be |
61 recreated using only regular expressions. From this theorem many closure |
61 recreated using only regular expressions. From this theorem many closure |
62 properties of regular languages follow. |
62 properties of regular languages follow. |
63 \end{abstract} |
63 \end{abstract} |
64 \maketitle |
64 \maketitle |
65 |
65 |