37 recognised by a finite deterministic automaton. This approach has many |
38 recognised by a finite deterministic automaton. This approach has many |
38 benefits. Among them is that it is easy to convince oneself from the fact that |
39 benefits. Among them is that it is easy to convince oneself from the fact that |
39 regular languages are closed under complementation: one just has to exchange |
40 regular languages are closed under complementation: one just has to exchange |
40 the accepting and non-accepting states in the corresponding automaton to |
41 the accepting and non-accepting states in the corresponding automaton to |
41 obtain an automaton for the complement language. The problem, however, lies with |
42 obtain an automaton for the complement language. The problem, however, lies with |
42 formalising such reasoning in a theorem prover, in our case |
43 formalising such reasoning in a HOL-based theorem prover, in our case |
43 Isabelle/HOL. Automata need to be represented as graphs or matrices, neither |
44 Isabelle/HOL. Automata consist of states and transitions. They need to be represented |
|
45 as graphs or matrices, neither |
44 of which can be defined as inductive datatype.\footnote{In some works |
46 of which can be defined as inductive datatype.\footnote{In some works |
45 functions are used to represent state transitions, but also they are not |
47 functions are used to represent state transitions, but also they are not |
46 inductive datatypes.} This means we have to build our own reasoning |
48 inductive datatypes.} This means we have to build our own reasoning |
47 infrastructure for them, as neither Isabelle/HOL nor HOL4 nor HOLlight support |
49 infrastructure for them, as neither Isabelle/HOL nor HOL4 nor HOLlight support |
48 them with libraries. |
50 them with libraries. |
49 |
51 |
50 Even worse, reasoning about graphs and matrices can be a real hassle in HOL-based |
52 Even worse, reasoning about graphs and matrices can be a real hassle in HOL-based |
51 theorem provers. Consider for example the operation of sequencing |
53 theorem provers. Consider for example the operation of sequencing |
52 two automata, say $A_1$ and $A_2$, by connecting the |
54 two automata, say $A_1$ and $A_2$, by connecting the |
53 accepting states of one atomaton to the |
55 accepting states of $A_1$ to the initial state of $A_2$: |
54 initial state of the other: |
|
55 |
56 |
56 |
57 |
57 \begin{center} |
58 \begin{center} |
58 \begin{tabular}{ccc} |
59 \begin{tabular}{ccc} |
59 \begin{tikzpicture}[scale=0.8] |
60 \begin{tikzpicture}[scale=0.8] |
107 |
108 |
108 \end{tabular} |
109 \end{tabular} |
109 \end{center} |
110 \end{center} |
110 |
111 |
111 \noindent |
112 \noindent |
112 On ``paper'' we can build the corresponding graph using the disjoint union of |
113 On ``paper'' we can define the corresponding graph in terms of the disjoint |
113 the state nodes and add |
114 union of the state nodes. Unfortunately in HOL, the definition for disjoint |
114 two more nodes for the new initial state and the new accepting |
|
115 state. Unfortunately in HOL, the definition for disjoint |
|
116 union, namely |
115 union, namely |
117 |
116 |
118 \begin{center} |
117 \begin{center} |
119 @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"} |
118 @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"} |
120 \end{center} |
119 \end{center} |
121 |
120 |
122 \noindent |
121 \noindent |
123 changes the type---the disjoint union is not a set, but a set of pairs. |
122 changes the type---the disjoint union is not a set, but a set of pairs. |
124 Using this definition for disjoint unions means we do not have a single type for automata |
123 Using this definition for disjoint unions means we do not have a single type for automata |
125 and hence will not be able to state properties about \emph{all} |
124 and hence will not be able to state properties about \emph{all} |
126 automata, since there is no type quantification available in HOL. A working |
125 automata, since there is no type quantification available in HOL. An |
127 alternative is to give every state node an identity, for example a natural |
126 alternative, which provides us with a single type for automata, is to give every |
|
127 state node an identity, for example a natural |
128 number, and then be careful renaming these identities apart whenever |
128 number, and then be careful renaming these identities apart whenever |
129 connecting two automata. This results in very clunky proofs |
129 connecting two automata. This results in clunky proofs |
130 establishing that properties are invariant under renaming. Similarly, |
130 establishing that properties are invariant under renaming. Similarly, |
131 combining two automata represented as matrices results in very adhoc |
131 connecting two automata represented as matrices results in very adhoc |
132 constructions, which are not pleasant to reason about. |
132 constructions, which are not pleasant to reason about. |
133 |
133 |
134 Because of these problems to do with representing automata, there seems |
134 Because of these problems to do with representing automata, there seems |
135 to be no substantial formalisation of automata theory and regular languages |
135 to be no substantial formalisation of automata theory and regular languages |
136 carried out in a HOL-based theorem prover. We are only aware of the |
136 carried out in a HOL-based theorem prover. We are only aware of the |
137 large formalisation of the automata theory in Nuprl \cite{Constable00} and |
137 large formalisation of the automata theory in Nuprl \cite{Constable00} and |
138 some smaller in Coq \cite{Filliatre97}. |
138 some smaller formalisations in Coq, for example \cite{Filliatre97}. |
139 |
139 |
140 In this paper, we will not attempt to formalise automata theory, but take a completely |
140 In this paper, we will not attempt to formalise automata theory, but take a completely |
141 different approach to regular languages. Instead of defining a regular language as one |
141 different approach to regular languages. Instead of defining a regular language as one |
142 where there exists an automaton that recognises all strings of the language, we define |
142 where there exists an automaton that recognises all strings of the language, we define |
143 a regular language as |
143 a regular language as: |
144 |
144 |
145 \begin{definition}[A Regular Language] |
145 \begin{definition}[A Regular Language] |
146 A language @{text A} is regular, provided there is a regular expression that matches all |
146 A language @{text A} is regular, provided there is a regular expression that matches all |
147 strings of @{text "A"}. |
147 strings of @{text "A"}. |
148 \end{definition} |
148 \end{definition} |
149 |
149 |
150 \noindent |
150 \noindent |
151 The reason is that regular expressions, unlike graphs and matrices, can |
151 The reason is that regular expressions, unlike graphs and matrices, can |
152 be easily defined as inductive datatype. Therefore a corresponding reasoning |
152 be easily defined as inductive datatype. Therefore a corresponding reasoning |
153 infrastructure comes in Isabelle for free. The purpose of this paper is to |
153 infrastructure comes for free. This has recently been used for formalising regular |
|
154 expression matching in HOL4 \cite{OwensSlind08}. The purpose of this paper is to |
154 show that a central result about regular languages, the Myhill-Nerode theorem, |
155 show that a central result about regular languages, the Myhill-Nerode theorem, |
155 can be recreated by only using regular expressions. A corollary of this |
156 can be recreated by only using regular expressions. This theorem give a necessary |
156 theorem will be the usual closure properties, including complementation, |
157 and sufficient condition for when a language is regular. As a corollary of this |
157 of regular languages. |
158 theorem we can easily establish the usual closure properties, including |
158 |
159 complementation, for regular languages.\smallskip |
159 |
160 |
160 \noindent |
161 \noindent |
161 {\bf Contributions:} A proof of the Myhill-Nerode Theorem based on regular expressions. The |
162 {\bf Contributions:} To our knowledge, our proof of the Myhill-Nerode theorem is the |
162 finiteness part of this theorem is proved using tagging-functions (which to our knowledge |
163 first that is based on regular expressions, only. We prove the part of this theorem |
163 are novel in this context). |
164 stating that a regular expression has only finitely many partitions using certain |
164 |
165 tagging-functions. Again to our best knowledge, these tagging functions have |
|
166 not been used before to establish the Myhill-Nerode theorem. |
165 *} |
167 *} |
166 |
168 |
167 section {* Preliminaries *} |
169 section {* Preliminaries *} |
168 |
170 |
169 text {* |
171 text {* |
170 Strings in Isabelle/HOL are lists of characters and the |
172 Strings in Isabelle/HOL are lists of characters with the \emph{empty string} |
171 \emph{empty string} is the empty list, written @{term "[]"}. \emph{Languages} are sets of |
173 being represented by the empty list, written @{term "[]"}. \emph{Languages} |
172 strings. The language containing all strings is written in Isabelle/HOL as @{term "UNIV::string set"}. |
174 are sets of strings. The language containing all strings is written in |
173 The notation for the quotient of a language @{text A} according to a relation @{term REL} is |
175 Isabelle/HOL as @{term "UNIV::string set"}. The notation for the quotient |
174 @{term "A // REL"}. The concatenation of two languages is written @{term "A ;; B"}; a language |
176 of a language @{text A} according to a relation @{term REL} is @{term "A // |
175 raised tow the power $n$ is written @{term "A \<up> n"}. Both concepts are defined as |
177 REL"}. The concatenation of two languages is written @{term "A ;; B"}; a |
|
178 language raised to the power $n$ is written @{term "A \<up> n"}. Both concepts |
|
179 are defined as |
176 |
180 |
177 \begin{center} |
181 \begin{center} |
178 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]} |
182 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]} |
179 \hspace{7mm} |
183 \hspace{7mm} |
180 @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]} |
184 @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]} |
233 From @{text "(*)"} it follows then that |
224 From @{text "(*)"} it follows then that |
234 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn |
225 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn |
235 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this |
226 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this |
236 is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed |
227 is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed |
237 \end{proof} |
228 \end{proof} |
|
229 |
|
230 \noindent |
|
231 Regular expressions are defined as the following inductive datatype |
|
232 |
|
233 \begin{center} |
|
234 @{text r} @{text "::="} |
|
235 @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
236 @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
237 @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
238 @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
239 @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
240 @{term "STAR r"} |
|
241 \end{center} |
|
242 |
|
243 \noindent |
|
244 The language matched by a regular expression is defined as usual: |
|
245 |
|
246 \begin{center} |
|
247 \begin{tabular}{c@ {\hspace{10mm}}c} |
|
248 \begin{tabular}{rcl} |
|
249 @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\ |
|
250 @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\ |
|
251 @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\ |
|
252 \end{tabular} |
|
253 & |
|
254 \begin{tabular}{rcl} |
|
255 @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & |
|
256 @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ |
|
257 @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & |
|
258 @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ |
|
259 @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} & |
|
260 @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\ |
|
261 \end{tabular} |
|
262 \end{tabular} |
|
263 \end{center} |
238 *} |
264 *} |
239 |
265 |
240 section {* Finite Partitions Imply Regularity of a Language *} |
266 section {* Finite Partitions Imply Regularity of a Language *} |
241 |
267 |
242 text {* |
268 text {* |