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