30 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |
32 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |
31 \institute{PLA University, China \and TU Munich, Germany} |
33 \institute{PLA University, China \and TU Munich, Germany} |
32 \maketitle |
34 \maketitle |
33 |
35 |
34 \begin{abstract} |
36 \begin{abstract} |
35 There are numerous textbooks on regular languages. Nearly all of them |
37 There are numerous textbooks on regular languages. Nearly all of them |
36 introduce the subject by describing finite automata and |
38 introduce the subject by describing finite automata and only mentioning on the |
37 only mentioning on the side a connection with regular expressions. |
39 side a connection with regular expressions. Unfortunately, automata are a |
38 Unfortunately, automata are a hassle for formalisations in HOL-based |
40 hassle for formalisations in HOL-based theorem provers. The reason is that |
39 theorem provers. The reason is that they need to be represented as graphs, |
41 they need to be represented as graphs, matrices or functions, none of which |
40 matrices or functions, none of which are inductive datatypes. Also |
42 are inductive datatypes. Also convenient operations for disjoint unions of |
41 operations, such as disjoint unions of graphs, are not easily formalisiable |
43 graphs and functions are not easily formalisiable in HOL. In contrast, regular |
42 in HOL. In contrast, regular expressions can be defined conveniently |
44 expressions can be defined conveniently as datatype and a corresponding |
43 as datatype and a corresponding reasoning infrastructure comes for |
45 reasoning infrastructure comes for free. We show in this paper that a central |
44 free. We show in this paper that a central result from formal |
46 result from formal language theory---the Myhill-Nerode theorem---can be |
45 language theory---the Myhill-Nerode theorem---can be recreated |
47 recreated using only regular expressions. |
46 using only regular expressions. |
48 |
47 \end{abstract} |
49 \end{abstract} |
48 |
50 |
49 |
51 |
50 \input{session} |
52 \input{session} |
51 |
53 |