24
+ − 1 (*<*)
+ − 2 theory Paper
39
+ − 3 imports "../Myhill" "LaTeXsugar"
24
+ − 4 begin
39
+ − 5
+ − 6 declare [[show_question_marks = false]]
+ − 7
54
+ − 8 consts
+ − 9 REL :: "(string \<times> string) \<Rightarrow> bool"
66
+ − 10 UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
54
+ − 11
70
+ − 12 abbreviation
+ − 13 "EClass x R \<equiv> R `` {x}"
54
+ − 14
39
+ − 15 notation (latex output)
50
+ − 16 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
75
+ − 17 str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
50
+ − 18 Seq (infixr "\<cdot>" 100) and
+ − 19 Star ("_\<^bsup>\<star>\<^esup>") and
+ − 20 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
58
+ − 21 Suc ("_+1" [100] 100) and
54
+ − 22 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
66
+ − 23 REL ("\<approx>") and
67
+ − 24 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
82
+ − 25 L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
75
+ − 26 Lam ("\<lambda>'(_')" [100] 100) and
+ − 27 Trn ("_, _" [100, 100] 100) and
71
+ − 28 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
88
+ − 29 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
+ − 30 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999)
24
+ − 31 (*>*)
+ − 32
70
+ − 33
24
+ − 34 section {* Introduction *}
+ − 35
+ − 36 text {*
58
+ − 37 Regular languages are an important and well-understood subject in Computer
60
+ − 38 Science, with many beautiful theorems and many useful algorithms. There is a
66
+ − 39 wide range of textbooks on this subject, many of which are aimed at students
+ − 40 and contain very detailed ``pencil-and-paper'' proofs
60
+ − 41 (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
+ − 42 formalising these theorems and by verifying formally the algorithms.
59
+ − 43
66
+ − 44 There is however a problem: the typical approach to regular languages is to
+ − 45 introduce finite automata and then define everything in terms of them. For
+ − 46 example, a regular language is normally defined as one whose strings are
+ − 47 recognised by a finite deterministic automaton. This approach has many
71
+ − 48 benefits. Among them is the fact that it is easy to convince oneself that
66
+ − 49 regular languages are closed under complementation: one just has to exchange
+ − 50 the accepting and non-accepting states in the corresponding automaton to
+ − 51 obtain an automaton for the complement language. The problem, however, lies with
67
+ − 52 formalising such reasoning in a HOL-based theorem prover, in our case
70
+ − 53 Isabelle/HOL. Automata are build up from states and transitions that
82
+ − 54 need to be represented as graphs, matrices or functions, none
+ − 55 of which can be defined as inductive datatype.
66
+ − 56
82
+ − 57 In case of graphs and matrices, this means we have to build our own
+ − 58 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+ − 59 HOLlight support them with libraries. Even worse, reasoning about graphs and
+ − 60 matrices can be a real hassle in HOL-based theorem provers. Consider for
+ − 61 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
+ − 62 connecting the accepting states of $A_1$ to the initial state of $A_2$:
60
+ − 63
+ − 64 \begin{center}
66
+ − 65 \begin{tabular}{ccc}
+ − 66 \begin{tikzpicture}[scale=0.8]
+ − 67 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 68
+ − 69 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 70 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 71
+ − 72 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 73 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 74
+ − 75 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 76 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 77
+ − 78 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 79 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 80 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 81
+ − 82 \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 83 \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 84 \end{tikzpicture}
+ − 85
+ − 86 &
+ − 87
+ − 88 \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+ − 89
+ − 90 &
+ − 91
+ − 92 \begin{tikzpicture}[scale=0.8]
+ − 93 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 94
+ − 95 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 96 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 97
+ − 98 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 99 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 100
+ − 101 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 102 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 103
+ − 104 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 105 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 106 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 107
+ − 108 \draw (C) to [very thick, bend left=45] (B);
+ − 109 \draw (D) to [very thick, bend right=45] (B);
+ − 110
+ − 111 \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 112 \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 113 \end{tikzpicture}
+ − 114
+ − 115 \end{tabular}
60
+ − 116 \end{center}
+ − 117
+ − 118 \noindent
67
+ − 119 On ``paper'' we can define the corresponding graph in terms of the disjoint
88
+ − 120 union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
66
+ − 121 union, namely
82
+ − 122 %
+ − 123 \begin{equation}\label{disjointunion}
66
+ − 124 @{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}"}
82
+ − 125 \end{equation}
60
+ − 126
61
+ − 127 \noindent
66
+ − 128 changes the type---the disjoint union is not a set, but a set of pairs.
+ − 129 Using this definition for disjoint unions means we do not have a single type for automata
+ − 130 and hence will not be able to state properties about \emph{all}
67
+ − 131 automata, since there is no type quantification available in HOL. An
+ − 132 alternative, which provides us with a single type for automata, is to give every
+ − 133 state node an identity, for example a natural
70
+ − 134 number, and then be careful to rename these identities apart whenever
67
+ − 135 connecting two automata. This results in clunky proofs
66
+ − 136 establishing that properties are invariant under renaming. Similarly,
67
+ − 137 connecting two automata represented as matrices results in very adhoc
66
+ − 138 constructions, which are not pleasant to reason about.
+ − 139
82
+ − 140 Functions are much better supported in Isabelle/HOL, but they still lead to similar
88
+ − 141 problems as with graphs. Composing, for example, two non-deterministic automata in parallel
+ − 142 poses again the problem of how to implement disjoint unions. Nipkow \cite{Nipkow98}
+ − 143 dismisses the option of using identities, because it leads to ``messy proofs''. He
82
+ − 144 opts for a variant of \eqref{disjointunion}, but writes
+ − 145
+ − 146 \begin{quote}
+ − 147 \it ``If the reader finds the above treatment in terms of bit lists revoltingly
+ − 148 concrete, I cannot disagree.''
+ − 149 \end{quote}
+ − 150
+ − 151 \noindent
+ − 152 Moreover, it is not so clear how to conveniently impose a finiteness condition
+ − 153 upon functions in order to represent \emph{finite} automata. The best is
+ − 154 probably to resort to more advanced reasoning frameworks, such as \emph{locales}.
+ − 155
66
+ − 156 Because of these problems to do with representing automata, there seems
+ − 157 to be no substantial formalisation of automata theory and regular languages
82
+ − 158 carried out in a HOL-based theorem prover. Nipkow establishes in
+ − 159 \cite{Nipkow98} the link between regular expressions and automata in
+ − 160 the context of lexing. The only larger formalisations of automata theory
+ − 161 are carried out in Nuprl \cite{Constable00} and in Coq (for example
+ − 162 \cite{Filliatre97}).
58
+ − 163
82
+ − 164 In this paper, we will not attempt to formalise automata theory in
+ − 165 Isabelle/HOL, but take a completely different approach to regular
+ − 166 languages. Instead of defining a regular language as one where there exists
+ − 167 an automaton that recognises all strings of the language, we define a
+ − 168 regular language as:
54
+ − 169
82
+ − 170 \begin{definition}
77
+ − 171 A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
54
+ − 172 strings of @{text "A"}.
+ − 173 \end{definition}
+ − 174
+ − 175 \noindent
88
+ − 176 The reason is that regular expressions, unlike graphs, matrices and functons, can
71
+ − 177 be easily defined as inductive datatype. Consequently a corresponding reasoning
+ − 178 infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
+ − 179 of regular expression matching based on derivatives \cite{OwensSlind08}. The purpose of this paper is to
+ − 180 show that a central result about regular languages---the Myhill-Nerode theorem---can
+ − 181 be recreated by only using regular expressions. This theorem gives necessary
+ − 182 and sufficient conditions for when a language is regular. As a corollary of this
67
+ − 183 theorem we can easily establish the usual closure properties, including
+ − 184 complementation, for regular languages.\smallskip
61
+ − 185
+ − 186 \noindent
88
+ − 187 {\bf Contributions:}
+ − 188 There is an extensive literature on regular languages.
+ − 189 To our knowledge, our proof of the Myhill-Nerode theorem is the
67
+ − 190 first that is based on regular expressions, only. We prove the part of this theorem
+ − 191 stating that a regular expression has only finitely many partitions using certain
+ − 192 tagging-functions. Again to our best knowledge, these tagging functions have
+ − 193 not been used before to establish the Myhill-Nerode theorem.
24
+ − 194 *}
+ − 195
50
+ − 196 section {* Preliminaries *}
+ − 197
+ − 198 text {*
67
+ − 199 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
+ − 200 being represented by the empty list, written @{term "[]"}. \emph{Languages}
+ − 201 are sets of strings. The language containing all strings is written in
71
+ − 202 Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
+ − 203 is written @{term "A ;; B"} and a language raised to the power $n$ is written
+ − 204 @{term "A \<up> n"}. Their definitions are
54
+ − 205
+ − 206 \begin{center}
58
+ − 207 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+ − 208 \hspace{7mm}
+ − 209 @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+ − 210 \hspace{7mm}
+ − 211 @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
54
+ − 212 \end{center}
+ − 213
+ − 214 \noindent
58
+ − 215 where @{text "@"} is the usual list-append operation. The Kleene-star of a language @{text A}
71
+ − 216 is defined as the union over all powers, namely @{thm Star_def}. In the paper
88
+ − 217 we will make use of the following properties of these constructions.
58
+ − 218
71
+ − 219 \begin{proposition}\label{langprops}\mbox{}\\
+ − 220 \begin{tabular}{@ {}ll@ {\hspace{10mm}}ll}
+ − 221 (i) & @{thm star_cases} & (ii) & @{thm[mode=IfThen] pow_length}\\
+ − 222 (iii) & @{thm seq_Union_left} &
+ − 223 \end{tabular}
+ − 224 \end{proposition}
+ − 225
+ − 226 \noindent
88
+ − 227 We omit the proofs, but invite the reader to consult
71
+ − 228 our formalisation.\footnote{Available at ???}
+ − 229
+ − 230
+ − 231 The notation for the quotient of a language @{text A} according to an
88
+ − 232 equivalence relation @{term REL} is in Isabelle/HOL @{term "A // REL"}. We will write
71
+ − 233 @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
+ − 234 as @{text "{y | y \<approx> x}"}.
+ − 235
+ − 236
51
+ − 237 Central to our proof will be the solution of equational systems
77
+ − 238 involving sets of languages. For this we will use Arden's lemma \cite{Brzozowski64}
71
+ − 239 which solves equations of the form @{term "X = A ;; X \<union> B"} provided
+ − 240 @{term "[] \<notin> A"}. However we will need the following ``reverse''
50
+ − 241 version of Arden's lemma.
+ − 242
75
+ − 243 \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
86
+ − 244 If @{thm (prem 1) arden} then
+ − 245 @{thm (lhs) arden} has the unique solution
+ − 246 @{thm (rhs) arden}.
50
+ − 247 \end{lemma}
+ − 248
+ − 249 \begin{proof}
86
+ − 250 For the right-to-left direction we assume @{thm (rhs) arden} and show
+ − 251 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
71
+ − 252 we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
50
+ − 253 which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both
+ − 254 sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
51
+ − 255 is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction.
50
+ − 256
86
+ − 257 For the other direction we assume @{thm (lhs) arden}. By a simple induction
51
+ − 258 on @{text n}, we can establish the property
50
+ − 259
+ − 260 \begin{center}
86
+ − 261 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
50
+ − 262 \end{center}
+ − 263
+ − 264 \noindent
+ − 265 Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
71
+ − 266 all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
+ − 267 of @{text "\<star>"}.
51
+ − 268 For the inclusion in the other direction we assume a string @{text s}
86
+ − 269 with length @{text k} is element in @{text X}. Since @{thm (prem 1) arden}
75
+ − 270 we know by Prop.~\ref{langprops}@{text "(ii)"} that
71
+ − 271 @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
51
+ − 272 (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer).
53
+ − 273 From @{text "(*)"} it follows then that
50
+ − 274 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
75
+ − 275 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
71
+ − 276 this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
50
+ − 277 \end{proof}
67
+ − 278
+ − 279 \noindent
88
+ − 280 Regular expressions are defined as the inductive datatype
67
+ − 281
+ − 282 \begin{center}
+ − 283 @{text r} @{text "::="}
+ − 284 @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 285 @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 286 @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 287 @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 288 @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 289 @{term "STAR r"}
+ − 290 \end{center}
+ − 291
+ − 292 \noindent
88
+ − 293 and the language matched by a regular expression is defined as
67
+ − 294
+ − 295 \begin{center}
+ − 296 \begin{tabular}{c@ {\hspace{10mm}}c}
+ − 297 \begin{tabular}{rcl}
+ − 298 @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
+ − 299 @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
+ − 300 @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
+ − 301 \end{tabular}
+ − 302 &
+ − 303 \begin{tabular}{rcl}
+ − 304 @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 305 @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 306 @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 307 @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 308 @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+ − 309 @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+ − 310 \end{tabular}
+ − 311 \end{tabular}
+ − 312 \end{center}
70
+ − 313
88
+ − 314 \noindent
+ − 315 Given a set or regular expressions @{text rs}, we will need the operation of generating
+ − 316 a regular expressions that matches all languages of @{text rs}. We only need the existence
+ − 317 of such an regular expressions therefore we use Isabelle's @{const "fold_graph"} and Hilbert's
+ − 318 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"} which, roughly speaking, folds @{const ALT} over the
+ − 319 set @{text rs} with @{const NULL} for the empty set. We can prove that for finite sets @{text rs}
82
+ − 320
88
+ − 321 \begin{center}
+ − 322 @{thm (lhs) folds_alt_simp}@{text "= \<Union> (\<calL> ` rs)"}
+ − 323 \end{center}
+ − 324
+ − 325 \noindent
+ − 326 holds. (whereby @{text "\<calL> ` rs"} stands for the
+ − 327 image of the set @{text rs} under function @{text "\<calL>"}).
+ − 328
82
+ − 329
50
+ − 330 *}
39
+ − 331
54
+ − 332 section {* Finite Partitions Imply Regularity of a Language *}
+ − 333
+ − 334 text {*
77
+ − 335 The key definition in the Myhill-Nerode theorem is the
75
+ − 336 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
+ − 337 strings are related, provided there is no distinguishing extension in this
+ − 338 language. This can be defined as:
+ − 339
70
+ − 340 \begin{definition}[Myhill-Nerode Relation]\mbox{}\\
75
+ − 341 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
70
+ − 342 \end{definition}
+ − 343
71
+ − 344 \noindent
75
+ − 345 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+ − 346 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
+ − 347 equivalence classes. One direction of the Myhill-Nerode theorem establishes
+ − 348 that if there are finitely many equivalence classes, then the language is
77
+ − 349 regular. In our setting we therefore have to show:
75
+ − 350
+ − 351 \begin{theorem}\label{myhillnerodeone}
+ − 352 @{thm[mode=IfThen] hard_direction}
+ − 353 \end{theorem}
71
+ − 354
75
+ − 355 \noindent
+ − 356 To prove this theorem, we define the set @{term "finals A"} as those equivalence
+ − 357 classes that contain strings of @{text A}, namely
+ − 358 %
71
+ − 359 \begin{equation}
70
+ − 360 @{thm finals_def}
71
+ − 361 \end{equation}
+ − 362
+ − 363 \noindent
77
+ − 364 It is straightforward to show that @{thm lang_is_union_of_finals} and
79
+ − 365 @{thm finals_in_partitions} hold.
75
+ − 366 Therefore if we know that there exists a regular expression for every
+ − 367 equivalence class in @{term "finals A"} (which by assumption must be
77
+ − 368 a finite set), then we can combine these regular expressions with @{const ALT}
75
+ − 369 and obtain a regular expression that matches every string in @{text A}.
70
+ − 370
75
+ − 371
77
+ − 372 We prove Thm.~\ref{myhillnerodeone} by giving a method that can calculate a
79
+ − 373 regular expression for \emph{every} equivalence class, not just the ones
77
+ − 374 in @{term "finals A"}. We
75
+ − 375 first define a notion of \emph{transition} between equivalence classes
+ − 376 %
71
+ − 377 \begin{equation}
+ − 378 @{thm transition_def}
+ − 379 \end{equation}
70
+ − 380
71
+ − 381 \noindent
75
+ − 382 which means that if we concatenate all strings matching the regular expression @{text r}
+ − 383 to the end of all strings in the equivalence class @{text Y}, we obtain a subset of
77
+ − 384 @{text X}. Note that we do not define an automaton here, we merely relate two sets
+ − 385 (w.r.t.~a regular expression).
75
+ − 386
+ − 387 Next we build an equational system that
+ − 388 contains an equation for each equivalence class. Suppose we have
+ − 389 the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+ − 390 contains the empty string @{text "[]"} (since equivalence classes are disjoint).
77
+ − 391 Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
75
+ − 392
+ − 393 \begin{center}
+ − 394 \begin{tabular}{rcl}
+ − 395 @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
+ − 396 @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+ − 397 & $\vdots$ \\
+ − 398 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+ − 399 \end{tabular}
+ − 400 \end{center}
70
+ − 401
75
+ − 402 \noindent
82
+ − 403 where the pairs @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions
+ − 404 @{term "Y\<^isub>i\<^isub>j \<Turnstile>(CHAR c\<^isub>i\<^isub>j)\<Rightarrow> X\<^isub>i"}. The term @{text "\<lambda>(EMPTY)"} acts as a marker for the equivalence
75
+ − 405 class containing @{text "[]"}. (Note that we mark, roughly speaking, the
+ − 406 single ``initial'' state in the equational system, which is different from
77
+ − 407 the method by Brzozowski \cite{Brzozowski64}, since for his purposes he needs to mark
+ − 408 the ``terminal'' states.) Overloading the function @{text L} for the two kinds of terms in the
75
+ − 409 equational system as follows
+ − 410
+ − 411 \begin{center}
86
+ − 412 @{thm L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+ − 413 @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
75
+ − 414 \end{center}
+ − 415
+ − 416 \noindent
+ − 417 we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+ − 418 %
+ − 419 \begin{equation}\label{inv1}
83
+ − 420 @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
75
+ − 421 \end{equation}
+ − 422
+ − 423 \noindent
+ − 424 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ − 425 %
+ − 426 \begin{equation}\label{inv2}
83
+ − 427 @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
75
+ − 428 \end{equation}
+ − 429
+ − 430 \noindent
77
+ − 431 The reason for adding the @{text \<lambda>}-marker to our equational system is
+ − 432 to obtain this equation, which only holds in this form since none of
+ − 433 the other terms contain the empty string.
+ − 434
+ − 435
+ − 436 Our proof of Thm.~\ref{myhillnerodeone}
75
+ − 437 will be by transforming the equational system into a \emph{solved form}
+ − 438 maintaining the invariants \eqref{inv1} and \eqref{inv2}. From the solved
+ − 439 form we will be able to read off the regular expressions using our
+ − 440 variant of Arden's Lemma (Lem.~\ref{arden}).
+ − 441
54
+ − 442 *}
+ − 443
+ − 444 section {* Regular Expressions Generate Finitely Many Partitions *}
39
+ − 445
+ − 446 text {*
+ − 447
54
+ − 448 \begin{theorem}
39
+ − 449 Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.
54
+ − 450 \end{theorem}
39
+ − 451
+ − 452 \begin{proof}
+ − 453 By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
50
+ − 454 and @{const CHAR} are straightforward, because we can easily establish
39
+ − 455
+ − 456 \begin{center}
+ − 457 \begin{tabular}{l}
+ − 458 @{thm quot_null_eq}\\
+ − 459 @{thm quot_empty_subset}\\
+ − 460 @{thm quot_char_subset}
+ − 461 \end{tabular}
+ − 462 \end{center}
+ − 463
+ − 464 \end{proof}
+ − 465 *}
+ − 466
+ − 467
54
+ − 468 section {* Conclusion and Related Work *}
+ − 469
24
+ − 470 (*<*)
+ − 471 end
+ − 472 (*>*)