24
+ − 1 (*<*)
+ − 2 theory Paper
233
+ − 3 imports "../Closures2" "../Attic/Prefix_subtract"
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
92
+ − 15 abbreviation
162
+ − 16 "Append_rexp2 r_itm r \<equiv> Append_rexp r r_itm"
92
+ − 17
+ − 18
172
+ − 19 abbreviation
+ − 20 "pow" (infixl "\<up>" 100)
+ − 21 where
+ − 22 "A \<up> n \<equiv> A ^^ n"
+ − 23
+ − 24 syntax (latex output)
+ − 25 "_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})")
+ − 26 "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _ | _})")
+ − 27 translations
+ − 28 "_Collect p P" <= "{p. P}"
+ − 29 "_Collect p P" <= "{p|xs. P}"
+ − 30 "_CollectIn p A P" <= "{p : A. P}"
+ − 31
242
+ − 32 syntax (latex output)
+ − 33 "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" [0, 0, 10] 10)
+ − 34
173
+ − 35 abbreviation "ZERO \<equiv> Zero"
+ − 36 abbreviation "ONE \<equiv> One"
+ − 37 abbreviation "ATOM \<equiv> Atom"
+ − 38 abbreviation "PLUS \<equiv> Plus"
+ − 39 abbreviation "TIMES \<equiv> Times"
187
+ − 40 abbreviation "TIMESS \<equiv> Timess"
172
+ − 41 abbreviation "STAR \<equiv> Star"
239
+ − 42 abbreviation "ALLS \<equiv> Star Allreg"
172
+ − 43
203
+ − 44 definition
+ − 45 Delta :: "'a lang \<Rightarrow> 'a lang"
+ − 46 where
+ − 47 "Delta A = (if [] \<in> A then {[]} else {})"
172
+ − 48
39
+ − 49 notation (latex output)
181
+ − 50 str_eq ("\<approx>\<^bsub>_\<^esub>") and
+ − 51 str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and
172
+ − 52 conc (infixr "\<cdot>" 100) and
193
+ − 53 star ("_\<^bsup>\<star>\<^esup>" [101] 200) and
50
+ − 54 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
58
+ − 55 Suc ("_+1" [100] 100) and
54
+ − 56 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
66
+ − 57 REL ("\<approx>") and
67
+ − 58 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
186
+ − 59 lang ("\<^raw:\ensuremath{\cal{L}}>" 101) and
172
+ − 60 lang ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
174
+ − 61 lang_trm ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
75
+ − 62 Lam ("\<lambda>'(_')" [100] 100) and
89
+ − 63 Trn ("'(_, _')" [100, 100] 100) and
71
+ − 64 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
88
+ − 65 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
92
+ − 66 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
162
+ − 67 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+ − 68 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
172
+ − 69
233
+ − 70 uminus ("\<^raw:\ensuremath{\overline{\isa{>_\<^raw:}}}>" [100] 100) and
183
+ − 71 tag_Plus ("+tag _ _" [100, 100] 100) and
+ − 72 tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and
184
+ − 73 tag_Times ("\<times>tag _ _" [100, 100] 100) and
+ − 74 tag_Times ("\<times>tag _ _ _" [100, 100, 100] 100) and
+ − 75 tag_Star ("\<star>tag _" [100] 100) and
+ − 76 tag_Star ("\<star>tag _ _" [100, 100] 100) and
193
+ − 77 tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>" [100] 100) and
174
+ − 78 Delta ("\<Delta>'(_')") and
180
+ − 79 nullable ("\<delta>'(_')") and
186
+ − 80 Cons ("_ :: _" [100, 100] 100) and
+ − 81 Rev ("Rev _" [1000] 100) and
203
+ − 82 Deriv ("Der _ _" [1000, 1000] 100) and
+ − 83 Derivs ("Ders") and
186
+ − 84 ONE ("ONE" 999) and
193
+ − 85 ZERO ("ZERO" 999) and
203
+ − 86 pderivs_lang ("pdersl") and
193
+ − 87 UNIV1 ("UNIV\<^isup>+") and
203
+ − 88 Deriv_lang ("Dersl") and
217
+ − 89 Derivss ("Derss") and
203
+ − 90 deriv ("der") and
+ − 91 derivs ("ders") and
+ − 92 pderiv ("pder") and
+ − 93 pderivs ("pders") and
233
+ − 94 pderivs_set ("pderss") and
240
+ − 95 SUBSEQ ("Sub") and
+ − 96 SUPSEQ ("Sup") and
239
+ − 97 UP ("'(_')\<up>") and
+ − 98 ALLS ("ALL")
203
+ − 99
+ − 100
+ − 101 lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
+ − 102
+ − 103 definition
+ − 104 Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+ − 105 where
+ − 106 "Der c A \<equiv> {s. [c] @ s \<in> A}"
+ − 107
+ − 108 definition
+ − 109 Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+ − 110 where
+ − 111 "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+ − 112
167
+ − 113
119
+ − 114 lemma meta_eq_app:
+ − 115 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+ − 116 by auto
+ − 117
181
+ − 118 lemma str_eq_def':
+ − 119 shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)"
+ − 120 unfolding str_eq_def by simp
+ − 121
172
+ − 122 lemma conc_def':
+ − 123 "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
+ − 124 unfolding conc_def by simp
+ − 125
+ − 126 lemma conc_Union_left:
+ − 127 shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))"
+ − 128 unfolding conc_def by auto
+ − 129
+ − 130 lemma test:
+ − 131 assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
+ − 132 shows "X = \<Union> (lang_trm ` rhs)"
+ − 133 using assms l_eq_r_in_eqs by (simp)
+ − 134
233
+ − 135 abbreviation
+ − 136 notprec ("_ \<^raw:\mbox{$\not\preceq$}>_")
+ − 137 where
+ − 138 "notprec x y \<equiv> \<not>(x \<preceq> y)"
+ − 139
+ − 140 abbreviation
+ − 141 minimal_syn ("min\<^bsub>_\<^esub> _")
+ − 142 where
+ − 143 "minimal_syn A x \<equiv> minimal x A"
+ − 144
172
+ − 145
167
+ − 146 (* THEOREMS *)
+ − 147
+ − 148 notation (Rule output)
+ − 149 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ − 150
+ − 151 syntax (Rule output)
+ − 152 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 153 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+ − 154
+ − 155 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ − 156 ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+ − 157
+ − 158 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ − 159
+ − 160 notation (Axiom output)
+ − 161 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+ − 162
+ − 163 notation (IfThen output)
+ − 164 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 165 syntax (IfThen output)
+ − 166 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 167 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 168 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ − 169 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ − 170
+ − 171 notation (IfThenNoBox output)
+ − 172 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 173 syntax (IfThenNoBox output)
+ − 174 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 175 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 176 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ − 177 "_asm" :: "prop \<Rightarrow> asms" ("_")
+ − 178
203
+ − 179 lemma pow_length:
+ − 180 assumes a: "[] \<notin> A"
+ − 181 and b: "s \<in> A \<up> Suc n"
+ − 182 shows "n < length s"
+ − 183 using b
+ − 184 proof (induct n arbitrary: s)
+ − 185 case 0
+ − 186 have "s \<in> A \<up> Suc 0" by fact
+ − 187 with a have "s \<noteq> []" by auto
+ − 188 then show "0 < length s" by auto
+ − 189 next
+ − 190 case (Suc n)
+ − 191 have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
+ − 192 have "s \<in> A \<up> Suc (Suc n)" by fact
+ − 193 then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
+ − 194 by (auto simp add: Seq_def)
+ − 195 from ih ** have "n < length s2" by simp
+ − 196 moreover have "0 < length s1" using * a by auto
+ − 197 ultimately show "Suc n < length s" unfolding eq
+ − 198 by (simp only: length_append)
+ − 199 qed
167
+ − 200
233
+ − 201
+ − 202
+ − 203
24
+ − 204 (*>*)
+ − 205
70
+ − 206
24
+ − 207 section {* Introduction *}
+ − 208
+ − 209 text {*
167
+ − 210 \noindent
58
+ − 211 Regular languages are an important and well-understood subject in Computer
60
+ − 212 Science, with many beautiful theorems and many useful algorithms. There is a
66
+ − 213 wide range of textbooks on this subject, many of which are aimed at students
175
+ − 214 and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97,
+ − 215 HopcroftUllman69}). It seems natural to exercise theorem provers by
187
+ − 216 formalising the theorems and by verifying formally the algorithms.
+ − 217
+ − 218 A popular choice for a theorem prover would be one based on Higher-Order
+ − 219 Logic (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
201
+ − 220 presented in this paper we will use the Isabelle/HOL. HOL is a predicate calculus
175
+ − 221 that allows quantification over predicate variables. Its type system is
187
+ − 222 based on Church's Simple Theory of Types \cite{Church40}. Although many
+ − 223 mathematical concepts can be conveniently expressed in HOL, there are some
233
+ − 224 limitations that hurt badly when attempting a simple-minded formalisation
193
+ − 225 of regular languages in it.
+ − 226
201
+ − 227 The typical approach (for example \cite{HopcroftUllman69,Kozen97}) to
+ − 228 regular languages is to introduce finite deterministic automata and then
+ − 229 define everything in terms of them. For example, a regular language is
+ − 230 normally defined as:
59
+ − 231
175
+ − 232 \begin{dfntn}\label{baddef}
+ − 233 A language @{text A} is \emph{regular}, provided there is a
+ − 234 finite deterministic automaton that recognises all strings of @{text "A"}.
+ − 235 \end{dfntn}
+ − 236
+ − 237 \noindent
+ − 238 This approach has many benefits. Among them is the fact that it is easy to
+ − 239 convince oneself that regular languages are closed under complementation:
+ − 240 one just has to exchange the accepting and non-accepting states in the
+ − 241 corresponding automaton to obtain an automaton for the complement language.
+ − 242 The problem, however, lies with formalising such reasoning in a HOL-based
+ − 243 theorem prover. Automata are built up from states and transitions that need
+ − 244 to be represented as graphs, matrices or functions, none of which can be
+ − 245 defined as an inductive datatype.
66
+ − 246
82
+ − 247 In case of graphs and matrices, this means we have to build our own
+ − 248 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+ − 249 HOLlight support them with libraries. Even worse, reasoning about graphs and
172
+ − 250 matrices can be a real hassle in HOL-based theorem provers, because
+ − 251 we have to be able to combine automata. Consider for
82
+ − 252 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
167
+ − 253 connecting the accepting states of $A_1$ to the initial state of $A_2$:
172
+ − 254
60
+ − 255 \begin{center}
66
+ − 256 \begin{tabular}{ccc}
181
+ − 257 \begin{tikzpicture}[scale=1]
66
+ − 258 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 259
+ − 260 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 261 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 262
+ − 263 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 264 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 265
+ − 266 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 267 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 268
+ − 269 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 270 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 271 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 272
181
+ − 273 \draw (-0.6,0.0) node {\small$A_1$};
+ − 274 \draw ( 0.6,0.0) node {\small$A_2$};
66
+ − 275 \end{tikzpicture}
+ − 276
+ − 277 &
+ − 278
193
+ − 279 \raisebox{2.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
66
+ − 280
+ − 281 &
+ − 282
181
+ − 283 \begin{tikzpicture}[scale=1]
66
+ − 284 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 285
+ − 286 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 287 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 288
+ − 289 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 290 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 291
+ − 292 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 293 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 294
+ − 295 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 296 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 297 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 298
+ − 299 \draw (C) to [very thick, bend left=45] (B);
+ − 300 \draw (D) to [very thick, bend right=45] (B);
+ − 301
181
+ − 302 \draw (-0.6,0.0) node {\small$A_1$};
+ − 303 \draw ( 0.6,0.0) node {\small$A_2$};
66
+ − 304 \end{tikzpicture}
+ − 305
+ − 306 \end{tabular}
60
+ − 307 \end{center}
+ − 308
+ − 309 \noindent
178
+ − 310 On `paper' we can define the corresponding
172
+ − 311 graph in terms of the disjoint
88
+ − 312 union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
66
+ − 313 union, namely
82
+ − 314 %
+ − 315 \begin{equation}\label{disjointunion}
172
+ − 316 @{text "A\<^isub>1 \<uplus> A\<^isub>2 \<equiv> {(1, x) | x \<in> A\<^isub>1} \<union> {(2, y) | y \<in> A\<^isub>2}"}
82
+ − 317 \end{equation}
60
+ − 318
61
+ − 319 \noindent
173
+ − 320 changes the type---the disjoint union is not a set, but a set of
+ − 321 pairs. Using this definition for disjoint union means we do not have a
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 322 single type for the states of automata. As a result we will not be able to
248
+ − 323 define a regular language as one for which there exists
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 324 an automaton that recognises all its strings (Definition~\ref{baddef}). This
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 325 is because we cannot make a definition in HOL that is only polymorphic in
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 326 the state type, but not in the predicate for regularity; and there is no
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 327 type quantification available in HOL (unlike in Coq, for
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 328 example).\footnote{Slind already pointed out this problem in an email to the
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 329 HOL4 mailing list on 21st April 2005.}
196
+ − 330
198
+ − 331 An alternative, which provides us with a single type for states of automata,
+ − 332 is to give every state node an identity, for example a natural number, and
+ − 333 then be careful to rename these identities apart whenever connecting two
+ − 334 automata. This results in clunky proofs establishing that properties are
+ − 335 invariant under renaming. Similarly, connecting two automata represented as
+ − 336 matrices results in very adhoc constructions, which are not pleasant to
+ − 337 reason about.
66
+ − 338
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 339 Functions are much better supported in Isabelle/HOL, but they still lead to
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 340 similar problems as with graphs. Composing, for example, two
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 341 non-deterministic automata in parallel requires also the formalisation of
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 342 disjoint unions. Nipkow \cite{Nipkow98} dismisses for this the option of
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 343 using identities, because it leads according to him to ``messy
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 344 proofs''. Since he does not need to define what regular languages are,
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 345 Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 346 writes\smallskip
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 347
82
+ − 348
+ − 349 \begin{quote}
93
+ − 350 \it%
+ − 351 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
101
+ − 352 `` & All lemmas appear obvious given a picture of the composition of automata\ldots
+ − 353 Yet their proofs require a painful amount of detail.''
+ − 354 \end{tabular}
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 355 \end{quote}\smallskip
101
+ − 356
+ − 357 \noindent
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 358 and\smallskip
101
+ − 359
+ − 360 \begin{quote}
+ − 361 \it%
+ − 362 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
93
+ − 363 `` & If the reader finds the above treatment in terms of bit lists revoltingly
101
+ − 364 concrete, I cannot disagree. A more abstract approach is clearly desirable.''
93
+ − 365 \end{tabular}
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 366 \end{quote}\smallskip
101
+ − 367
+ − 368
82
+ − 369 \noindent
172
+ − 370 Moreover, it is not so clear how to conveniently impose a finiteness
+ − 371 condition upon functions in order to represent \emph{finite} automata. The
+ − 372 best is probably to resort to more advanced reasoning frameworks, such as
+ − 373 \emph{locales} or \emph{type classes}, which are \emph{not} available in all
+ − 374 HOL-based theorem provers.
82
+ − 375
172
+ − 376 Because of these problems to do with representing automata, there seems to
+ − 377 be no substantial formalisation of automata theory and regular languages
+ − 378 carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
+ − 379 the link between regular expressions and automata in the context of
+ − 380 lexing. Berghofer and Reiter \cite{BerghoferReiter09} formalise automata
+ − 381 working over bit strings in the context of Presburger arithmetic. The only
+ − 382 larger formalisations of automata theory are carried out in Nuprl
218
+ − 383 \cite{Constable00} and in Coq, e.g.~\cite{Filliatre97,Almeidaetal10}.
162
+ − 384
245
+ − 385 Also, one might consider automata as just convenient `vehicles' for
233
+ − 386 establishing properties about regular languages. However, paper proofs
+ − 387 about automata often involve subtle side-conditions which are easily
+ − 388 overlooked, but which make formal reasoning rather painful. For example
248
+ − 389 Kozen's proof of the Myhill-Nerode Theorem requires that automata do not
233
+ − 390 have inaccessible states \cite{Kozen97}. Another subtle side-condition is
+ − 391 completeness of automata, that is automata need to have total transition
+ − 392 functions and at most one `sink' state from which there is no connection to
+ − 393 a final state (Brzozowski mentions this side-condition in the context of
+ − 394 state complexity of automata \cite{Brzozowski10}). Such side-conditions mean
+ − 395 that if we define a regular language as one for which there exists \emph{a}
+ − 396 finite automaton that recognises all its strings (see
+ − 397 Definition~\ref{baddef}), then we need a lemma which ensures that another
+ − 398 equivalent one can be found satisfying the side-condition, and also need to
+ − 399 make sure our operations on automata preserve them. Unfortunately, such
245
+ − 400 `little' and `obvious' lemmas make formalisations of automata theory
+ − 401 hair-pulling experiences.
175
+ − 402
82
+ − 403 In this paper, we will not attempt to formalise automata theory in
173
+ − 404 Isabelle/HOL nor will we attempt to formalise automata proofs from the
172
+ − 405 literature, but take a different approach to regular languages than is
+ − 406 usually taken. Instead of defining a regular language as one where there
178
+ − 407 exists an automaton that recognises all its strings, we define a
82
+ − 408 regular language as:
54
+ − 409
186
+ − 410 \begin{dfntn}\label{regular}
+ − 411 A language @{text A} is \emph{regular}, provided there is a regular expression
+ − 412 that matches all strings of @{text "A"}.
167
+ − 413 \end{dfntn}
54
+ − 414
+ − 415 \noindent
258
+ − 416 And then `forget' automata completely.
172
+ − 417 The reason is that regular expressions, unlike graphs, matrices and
175
+ − 418 functions, can be easily defined as an inductive datatype. A reasoning
247
+ − 419 infrastructure (like induction and recursion) comes for free in
175
+ − 420 HOL. Moreover, no side-conditions will be needed for regular expressions,
178
+ − 421 like we need for automata. This convenience of regular expressions has
175
+ − 422 recently been exploited in HOL4 with a formalisation of regular expression
+ − 423 matching based on derivatives \cite{OwensSlind08} and with an equivalence
+ − 424 checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}. The
+ − 425 main purpose of this paper is to show that a central result about regular
248
+ − 426 languages---the Myhill-Nerode Theorem---can be recreated by only using
175
+ − 427 regular expressions. This theorem gives necessary and sufficient conditions
+ − 428 for when a language is regular. As a corollary of this theorem we can easily
+ − 429 establish the usual closure properties, including complementation, for
249
+ − 430 regular languages. We use the Continuation Lemma \cite{Rosenberg06},
248
+ − 431 which is also a corollary of the Myhill-Nerode Theorem, for establishing
245
+ − 432 the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip
61
+ − 433
174
+ − 434 \noindent
175
+ − 435 {\bf Contributions:} There is an extensive literature on regular languages.
248
+ − 436 To our best knowledge, our proof of the Myhill-Nerode Theorem is the first
175
+ − 437 that is based on regular expressions, only. The part of this theorem stating
+ − 438 that finitely many partitions imply regularity of the language is proved by
181
+ − 439 an argument about solving equational systems. This argument appears to be
175
+ − 440 folklore. For the other part, we give two proofs: one direct proof using
+ − 441 certain tagging-functions, and another indirect proof using Antimirov's
+ − 442 partial derivatives \cite{Antimirov95}. Again to our best knowledge, the
245
+ − 443 tagging-functions have not been used before for establishing the Myhill-Nerode
248
+ − 444 Theorem. Derivatives of regular expressions have been used recently quite
190
+ − 445 widely in the literature; partial derivatives, in contrast, attract much
187
+ − 446 less attention. However, partial derivatives are more suitable in the
248
+ − 447 context of the Myhill-Nerode Theorem, since it is easier to establish
190
+ − 448 formally their finiteness result. We are not aware of any proof that uses
248
+ − 449 either of them for proving the Myhill-Nerode Theorem.
24
+ − 450 *}
+ − 451
50
+ − 452 section {* Preliminaries *}
+ − 453
+ − 454 text {*
172
+ − 455 \noindent
67
+ − 456 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
177
+ − 457 being represented by the empty list, written @{term "[]"}. We assume there
+ − 458 are only finitely many different characters. \emph{Languages} are sets of
+ − 459 strings. The language containing all strings is written in Isabelle/HOL as
+ − 460 @{term "UNIV::string set"}. The concatenation of two languages is written
+ − 461 @{term "A \<cdot> B"} and a language raised to the power @{text n} is written
93
+ − 462 @{term "A \<up> n"}. They are defined as usual
54
+ − 463
+ − 464 \begin{center}
177
+ − 465 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 466 @{thm (lhs) conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}
+ − 467 & @{text "\<equiv>"} & @{thm (rhs) conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}\\
+ − 468
+ − 469 @{thm (lhs) lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}
+ − 470 & @{text "\<equiv>"} & @{thm (rhs) lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}\\
+ − 471
+ − 472 @{thm (lhs) lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+ − 473 & @{text "\<equiv>"} & @{thm (rhs) lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+ − 474 \end{tabular}
54
+ − 475 \end{center}
+ − 476
+ − 477 \noindent
113
+ − 478 where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
172
+ − 479 is defined as the union over all powers, namely @{thm star_def}. In the paper
88
+ − 480 we will make use of the following properties of these constructions.
58
+ − 481
167
+ − 482 \begin{prpstn}\label{langprops}\mbox{}\\
187
+ − 483 \begin{tabular}{@ {}lp{10cm}}
180
+ − 484 (i) & @{thm star_unfold_left} \\
92
+ − 485 (ii) & @{thm[mode=IfThen] pow_length}\\
172
+ − 486 (iii) & @{thm conc_Union_left} \\
187
+ − 487 (iv) & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then
+ − 488 there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"}
+ − 489 and @{term "x\<^isub>p \<noteq> []"} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
71
+ − 490 \end{tabular}
167
+ − 491 \end{prpstn}
71
+ − 492
+ − 493 \noindent
100
+ − 494 In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
156
+ − 495 string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
190
+ − 496 the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.
+ − 497 Property @{text "(iv)"} states that a non-empty string in @{term "A\<star>"} can
+ − 498 always be split up into a non-empty prefix belonging to @{text "A"} and the
+ − 499 rest being in @{term "A\<star>"}. We omit
100
+ − 500 the proofs for these properties, but invite the reader to consult our
218
+ − 501 formalisation.\footnote{Available in the Archive of Formal Proofs at
259
+ − 502 \url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}
218
+ − 503 \cite{myhillnerodeafp11}.}
71
+ − 504
181
+ − 505 The notation in Isabelle/HOL for the quotient of a language @{text A}
+ − 506 according to an equivalence relation @{term REL} is @{term "A // REL"}. We
+ − 507 will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as
+ − 508 \mbox{@{text "{y | y \<approx> x}"}}, and have @{text "x \<approx> y"} if and only if @{text
+ − 509 "\<lbrakk>x\<rbrakk>\<^isub>\<approx> = \<lbrakk>y\<rbrakk>\<^isub>\<approx>"}.
71
+ − 510
+ − 511
51
+ − 512 Central to our proof will be the solution of equational systems
176
+ − 513 involving equivalence classes of languages. For this we will use Arden's Lemma
198
+ − 514 (see for example \cite[Page 100]{Sakarovitch09}),
167
+ − 515 which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
201
+ − 516 @{term "[] \<notin> A"}. However we will need the following `reversed'
+ − 517 version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to
167
+ − 518 \mbox{@{term "X \<cdot> A"}}).
50
+ − 519
201
+ − 520 \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
203
+ − 521 If @{thm (prem 1) reversed_Arden} then
+ − 522 @{thm (lhs) reversed_Arden} if and only if
+ − 523 @{thm (rhs) reversed_Arden}.
167
+ − 524 \end{lmm}
50
+ − 525
+ − 526 \begin{proof}
203
+ − 527 For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+ − 528 that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"}
181
+ − 529 we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
+ − 530 which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
+ − 531 sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
201
+ − 532 is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation
+ − 533 completes this direction.
50
+ − 534
203
+ − 535 For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
51
+ − 536 on @{text n}, we can establish the property
50
+ − 537
+ − 538 \begin{center}
203
+ − 539 @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
50
+ − 540 \end{center}
+ − 541
+ − 542 \noindent
167
+ − 543 Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
+ − 544 all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
71
+ − 545 of @{text "\<star>"}.
51
+ − 546 For the inclusion in the other direction we assume a string @{text s}
203
+ − 547 with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
198
+ − 548 we know by Property~\ref{langprops}@{text "(ii)"} that
167
+ − 549 @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
+ − 550 (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
53
+ − 551 From @{text "(*)"} it follows then that
203
+ − 552 @{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
198
+ − 553 implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"}
174
+ − 554 this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
50
+ − 555 \end{proof}
67
+ − 556
+ − 557 \noindent
88
+ − 558 Regular expressions are defined as the inductive datatype
67
+ − 559
+ − 560 \begin{center}
176
+ − 561 \begin{tabular}{rcl}
+ − 562 @{text r} & @{text "::="} & @{term ZERO}\\
177
+ − 563 & @{text"|"} & @{term One}\\
+ − 564 & @{text"|"} & @{term "Atom c"}\\
+ − 565 & @{text"|"} & @{term "Times r r"}\\
+ − 566 & @{text"|"} & @{term "Plus r r"}\\
+ − 567 & @{text"|"} & @{term "Star r"}
176
+ − 568 \end{tabular}
67
+ − 569 \end{center}
+ − 570
+ − 571 \noindent
88
+ − 572 and the language matched by a regular expression is defined as
67
+ − 573
+ − 574 \begin{center}
176
+ − 575 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
172
+ − 576 @{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
+ − 577 @{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\
+ − 578 @{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\
+ − 579 @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 580 @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+ − 581 @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 582 @{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+ − 583 @{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+ − 584 @{thm (rhs) lang.simps(6)[where r="r"]}\\
67
+ − 585 \end{tabular}
+ − 586 \end{center}
70
+ − 587
100
+ − 588 Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
132
+ − 589 a regular expression that matches the union of all languages of @{text rs}. We only need to know the
+ − 590 existence
92
+ − 591 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
173
+ − 592 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const PLUS} over the
+ − 593 set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}
110
+ − 594 %
+ − 595 \begin{equation}\label{uplus}
203
+ − 596 \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}}
110
+ − 597 \end{equation}
88
+ − 598
+ − 599 \noindent
90
+ − 600 holds, whereby @{text "\<calL> ` rs"} stands for the
190
+ − 601 image of the set @{text rs} under function @{text "\<calL>"} defined as
+ − 602
+ − 603 \begin{center}
+ − 604 @{term "lang ` rs \<equiv> {lang r | r. r \<in> rs}"}
+ − 605 \end{center}
+ − 606
+ − 607 \noindent
+ − 608 In what follows we shall use this convenient short-hand notation for images of sets
+ − 609 also with other functions.
50
+ − 610 *}
39
+ − 611
132
+ − 612
133
+ − 613 section {* The Myhill-Nerode Theorem, First Part *}
54
+ − 614
+ − 615 text {*
177
+ − 616 \noindent
248
+ − 617 The key definition in the Myhill-Nerode Theorem is the
+ − 618 \emph{Myhill-Nerode Relation}, which states that w.r.t.~a language two
75
+ − 619 strings are related, provided there is no distinguishing extension in this
154
+ − 620 language. This can be defined as a tertiary relation.
75
+ − 621
174
+ − 622 \begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel}
+ − 623 Given a language @{text A}, two strings @{text x} and
123
+ − 624 @{text y} are Myhill-Nerode related provided
117
+ − 625 \begin{center}
181
+ − 626 @{thm str_eq_def'}
117
+ − 627 \end{center}
167
+ − 628 \end{dfntn}
70
+ − 629
71
+ − 630 \noindent
75
+ − 631 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+ − 632 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
108
+ − 633 equivalence classes. To illustrate this quotient construction, let us give a simple
101
+ − 634 example: consider the regular language containing just
92
+ − 635 the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
101
+ − 636 into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
90
+ − 637 as follows
+ − 638
+ − 639 \begin{center}
176
+ − 640 \begin{tabular}{l}
+ − 641 @{text "X\<^isub>1 = {[]}"}\\
+ − 642 @{text "X\<^isub>2 = {[c]}"}\\
90
+ − 643 @{text "X\<^isub>3 = UNIV - {[], [c]}"}
176
+ − 644 \end{tabular}
90
+ − 645 \end{center}
+ − 646
248
+ − 647 One direction of the Myhill-Nerode Theorem establishes
93
+ − 648 that if there are finitely many equivalence classes, like in the example above, then
+ − 649 the language is regular. In our setting we therefore have to show:
75
+ − 650
167
+ − 651 \begin{thrm}\label{myhillnerodeone}
96
+ − 652 @{thm[mode=IfThen] Myhill_Nerode1}
167
+ − 653 \end{thrm}
71
+ − 654
75
+ − 655 \noindent
90
+ − 656 To prove this theorem, we first define the set @{term "finals A"} as those equivalence
100
+ − 657 classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
75
+ − 658 %
71
+ − 659 \begin{equation}
70
+ − 660 @{thm finals_def}
71
+ − 661 \end{equation}
+ − 662
+ − 663 \noindent
132
+ − 664 In our running example, @{text "X\<^isub>2"} is the only
+ − 665 equivalence class in @{term "finals {[c]}"}.
174
+ − 666 It is straightforward to show that in general
+ − 667
177
+ − 668 \begin{equation}\label{finalprops}
174
+ − 669 @{thm lang_is_union_of_finals}\hspace{15mm}
+ − 670 @{thm finals_in_partitions}
177
+ − 671 \end{equation}
174
+ − 672
+ − 673 \noindent
+ − 674 hold.
75
+ − 675 Therefore if we know that there exists a regular expression for every
100
+ − 676 equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
93
+ − 677 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
98
+ − 678 that matches every string in @{text A}.
70
+ − 679
75
+ − 680
198
+ − 681 Our proof of Theorem~\ref{myhillnerodeone} relies on a method that can calculate a
79
+ − 682 regular expression for \emph{every} equivalence class, not just the ones
77
+ − 683 in @{term "finals A"}. We
93
+ − 684 first define the notion of \emph{one-character-transition} between
+ − 685 two equivalence classes
75
+ − 686 %
71
+ − 687 \begin{equation}
+ − 688 @{thm transition_def}
+ − 689 \end{equation}
70
+ − 690
71
+ − 691 \noindent
92
+ − 692 which means that if we concatenate the character @{text c} to the end of all
+ − 693 strings in the equivalence class @{text Y}, we obtain a subset of
77
+ − 694 @{text X}. Note that we do not define an automaton here, we merely relate two sets
110
+ − 695 (with the help of a character). In our concrete example we have
178
+ − 696 @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<^isub>i\<Rightarrow> X\<^isub>3"} with @{text "d\<^isub>i"} being any
+ − 697 other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>c\<^isub>j\<Rightarrow> X\<^isub>3"} for any
194
+ − 698 character @{text "c\<^isub>j"}.
75
+ − 699
156
+ − 700 Next we construct an \emph{initial equational system} that
+ − 701 contains an equation for each equivalence class. We first give
+ − 702 an informal description of this construction. Suppose we have
75
+ − 703 the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+ − 704 contains the empty string @{text "[]"} (since equivalence classes are disjoint).
77
+ − 705 Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
75
+ − 706
+ − 707 \begin{center}
+ − 708 \begin{tabular}{rcl}
173
+ − 709 @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, ATOM c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, ATOM c\<^isub>1\<^isub>p) + \<lambda>(ONE)"} \\
+ − 710 @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, ATOM c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, ATOM c\<^isub>2\<^isub>o)"} \\
75
+ − 711 & $\vdots$ \\
173
+ − 712 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, ATOM c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, ATOM c\<^isub>n\<^isub>q)"}\\
75
+ − 713 \end{tabular}
+ − 714 \end{center}
70
+ − 715
75
+ − 716 \noindent
173
+ − 717 where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"}
100
+ − 718 stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
159
+ − 719 X\<^isub>i"}.
+ − 720 %The intuition behind the equational system is that every
+ − 721 %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+ − 722 %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
+ − 723 %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
+ − 724 %predecessor states to @{text X\<^isub>i}.
+ − 725 There can only be
173
+ − 726 finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} in a right-hand side
156
+ − 727 since by assumption there are only finitely many
159
+ − 728 equivalence classes and only finitely many characters.
173
+ − 729 The term @{text "\<lambda>(ONE)"} in the first equation acts as a marker for the initial state, that
159
+ − 730 is the equivalence class
233
+ − 731 containing the empty string @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
115
+ − 732 single `initial' state in the equational system, which is different from
100
+ − 733 the method by Brzozowski \cite{Brzozowski64}, where he marks the
115
+ − 734 `terminal' states. We are forced to set up the equational system in our
248
+ − 735 way, because the Myhill-Nerode Relation determines the `direction' of the
123
+ − 736 transitions---the successor `state' of an equivalence class @{text Y} can
+ − 737 be reached by adding a character to the end of @{text Y}. This is also the
201
+ − 738 reason why we have to use our reversed version of Arden's Lemma.}
177
+ − 739 In our running example we have the initial equational system
+ − 740
+ − 741 \begin{equation}\label{exmpcs}
+ − 742 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 743 @{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
+ − 744 @{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM c)"}\\
+ − 745 @{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>1, ATOM d\<^isub>1) + \<dots> + (X\<^isub>1, ATOM d\<^isub>n)"}\\
184
+ − 746 & & \mbox{}\hspace{10mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}
177
+ − 747 \end{tabular}}
+ − 748 \end{equation}
+ − 749
+ − 750 \noindent
+ − 751 where @{text "d\<^isub>1\<dots>d\<^isub>n"} is the sequence of all characters
181
+ − 752 but not containing @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
178
+ − 753 characters.
177
+ − 754
100
+ − 755 Overloading the function @{text \<calL>} for the two kinds of terms in the
92
+ − 756 equational system, we have
75
+ − 757
+ − 758 \begin{center}
92
+ − 759 @{text "\<calL>(Y, r) \<equiv>"} %
172
+ − 760 @{thm (rhs) lang_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+ − 761 @{thm lang_trm.simps(1)[where r="r", THEN eq_reflection]}
75
+ − 762 \end{center}
+ − 763
+ − 764 \noindent
100
+ − 765 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
75
+ − 766 %
+ − 767 \begin{equation}\label{inv1}
173
+ − 768 @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, ATOM c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, ATOM c\<^isub>i\<^isub>q)"}.
75
+ − 769 \end{equation}
+ − 770
+ − 771 \noindent
+ − 772 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ − 773 %
+ − 774 \begin{equation}\label{inv2}
173
+ − 775 @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, ATOM c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, ATOM c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(ONE))"}.
75
+ − 776 \end{equation}
+ − 777
+ − 778 \noindent
160
+ − 779 holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is
103
+ − 780 to obtain this equation: it only holds with the marker, since none of
108
+ − 781 the other terms contain the empty string. The point of the initial equational system is
+ − 782 that solving it means we will be able to extract a regular expression for every equivalence class.
100
+ − 783
101
+ − 784 Our representation for the equations in Isabelle/HOL are pairs,
108
+ − 785 where the first component is an equivalence class (a set of strings)
+ − 786 and the second component
101
+ − 787 is a set of terms. Given a set of equivalence
100
+ − 788 classes @{text CS}, our initial equational system @{term "Init CS"} is thus
101
+ − 789 formally defined as
104
+ − 790 %
+ − 791 \begin{equation}\label{initcs}
+ − 792 \mbox{\begin{tabular}{rcl}
100
+ − 793 @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
+ − 794 @{text "if"}~@{term "[] \<in> X"}\\
173
+ − 795 & & @{text "then"}~@{term "{Trn Y (ATOM c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam ONE}"}\\
+ − 796 & & @{text "else"}~@{term "{Trn Y (ATOM c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
100
+ − 797 @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def}
104
+ − 798 \end{tabular}}
+ − 799 \end{equation}
100
+ − 800
+ − 801
+ − 802
+ − 803 \noindent
+ − 804 Because we use sets of terms
101
+ − 805 for representing the right-hand sides of equations, we can
100
+ − 806 prove \eqref{inv1} and \eqref{inv2} more concisely as
93
+ − 807 %
167
+ − 808 \begin{lmm}\label{inv}
100
+ − 809 If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
167
+ − 810 \end{lmm}
77
+ − 811
93
+ − 812 \noindent
198
+ − 813 Our proof of Theorem~\ref{myhillnerodeone} will proceed by transforming the
100
+ − 814 initial equational system into one in \emph{solved form} maintaining the invariant
198
+ − 815 in Lemma~\ref{inv}. From the solved form we will be able to read
89
+ − 816 off the regular expressions.
+ − 817
100
+ − 818 In order to transform an equational system into solved form, we have two
89
+ − 819 operations: one that takes an equation of the form @{text "X = rhs"} and removes
110
+ − 820 any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's
92
+ − 821 Lemma. The other operation takes an equation @{text "X = rhs"}
89
+ − 822 and substitutes @{text X} throughout the rest of the equational system
110
+ − 823 adjusting the remaining regular expressions appropriately. To define this adjustment
108
+ − 824 we define the \emph{append-operation} taking a term and a regular expression as argument
89
+ − 825
+ − 826 \begin{center}
177
+ − 827 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ − 828 @{thm (lhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ − 829 & @{text "\<equiv>"} &
+ − 830 @{thm (rhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\\
+ − 831 @{thm (lhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ − 832 & @{text "\<equiv>"} &
+ − 833 @{thm (rhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ − 834 \end{tabular}
89
+ − 835 \end{center}
+ − 836
92
+ − 837 \noindent
108
+ − 838 We lift this operation to entire right-hand sides of equations, written as
162
+ − 839 @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
101
+ − 840 the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
110
+ − 841 %
+ − 842 \begin{equation}\label{arden_def}
+ − 843 \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
94
+ − 844 @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 845 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
177
+ − 846 & & @{text "r' ="} & @{term "Star (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+ − 847 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "Append_rexp_rhs rhs' r'"}}\\
110
+ − 848 \end{tabular}}
+ − 849 \end{equation}
93
+ − 850
+ − 851 \noindent
101
+ − 852 In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
110
+ − 853 then we calculate the combined regular expressions for all @{text r} coming
177
+ − 854 from the deleted @{text "(X, r)"}, and take the @{const Star} of it;
178
+ − 855 finally we append this regular expression to @{text rhs'}. If we apply this
+ − 856 operation to the right-hand side of @{text "X\<^isub>3"} in \eqref{exmpcs}, we obtain
+ − 857 the equation:
+ − 858
+ − 859 \begin{center}
+ − 860 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 861 @{term "X\<^isub>3"} & @{text "="} &
184
+ − 862 @{text "(X\<^isub>1, TIMES (ATOM d\<^isub>1) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m})) + \<dots> "}\\
178
+ − 863 & & \mbox{}\hspace{13mm}
184
+ − 864 @{text "\<dots> + (X\<^isub>1, TIMES (ATOM d\<^isub>n) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}))"}
178
+ − 865 \end{tabular}
+ − 866 \end{center}
+ − 867
+ − 868
+ − 869 \noindent
201
+ − 870 That means we eliminated the recursive occurrence of @{text "X\<^isub>3"} on the
178
+ − 871 right-hand side. Note we used the abbreviation
184
+ − 872 @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}"}
178
+ − 873 to stand for a regular expression that matches with every character. In
183
+ − 874 our algorithm we are only interested in the existence of such a regular expression
+ − 875 and do not specify it any further.
178
+ − 876
+ − 877 It can be easily seen that the @{text "Arden"}-operation mimics Arden's
+ − 878 Lemma on the level of equations. To ensure the non-emptiness condition of
+ − 879 Arden's Lemma we say that a right-hand side is @{text ardenable} provided
110
+ − 880
+ − 881 \begin{center}
+ − 882 @{thm ardenable_def}
+ − 883 \end{center}
+ − 884
+ − 885 \noindent
156
+ − 886 This allows us to prove a version of Arden's Lemma on the level of equations.
110
+ − 887
167
+ − 888 \begin{lmm}\label{ardenable}
113
+ − 889 Given an equation @{text "X = rhs"}.
110
+ − 890 If @{text "X = \<Union>\<calL> ` rhs"},
179
+ − 891 @{thm (prem 2) Arden_preserves_soundness}, and
+ − 892 @{thm (prem 3) Arden_preserves_soundness}, then
135
+ − 893 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
167
+ − 894 \end{lmm}
110
+ − 895
+ − 896 \noindent
156
+ − 897 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
194
+ − 898 but we can still ensure that it holds throughout our algorithm of transforming equations
156
+ − 899 into solved form. The \emph{substitution-operation} takes an equation
95
+ − 900 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
94
+ − 901
+ − 902 \begin{center}
95
+ − 903 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ − 904 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 905 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 906 & & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
177
+ − 907 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> Append_rexp_rhs xrhs r'"}}\\
95
+ − 908 \end{tabular}
94
+ − 909 \end{center}
95
+ − 910
+ − 911 \noindent
134
+ − 912 We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
95
+ − 913 the regular expression corresponding to the deleted terms; finally we append this
+ − 914 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+ − 915 the substitution operation we will arrange it so that @{text "xrhs"} does not contain
178
+ − 916 any occurrence of @{text X}. For example substituting the first equation in
+ − 917 \eqref{exmpcs} into the right-hand side of the second, thus eliminating the equivalence
+ − 918 class @{text "X\<^isub>1"}, gives us the equation
+ − 919
+ − 920 \begin{equation}\label{exmpresult}
+ − 921 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 922 @{term "X\<^isub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM c))"}\\
+ − 923 \end{tabular}}
+ − 924 \end{equation}
96
+ − 925
134
+ − 926 With these two operations in place, we can define the operation that removes one equation
100
+ − 927 from an equational systems @{text ES}. The operation @{const Subst_all}
96
+ − 928 substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES};
100
+ − 929 @{const Remove} then completely removes such an equation from @{text ES} by substituting
110
+ − 930 it to the rest of the equational system, but first eliminating all recursive occurrences
96
+ − 931 of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+ − 932
+ − 933 \begin{center}
+ − 934 \begin{tabular}{rcl}
+ − 935 @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+ − 936 @{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+ − 937 \end{tabular}
+ − 938 \end{center}
100
+ − 939
+ − 940 \noindent
110
+ − 941 Finally, we can define how an equational system should be solved. For this
107
+ − 942 we will need to iterate the process of eliminating equations until only one equation
154
+ − 943 will be left in the system. However, we do not just want to have any equation
107
+ − 944 as being the last one, but the one involving the equivalence class for
+ − 945 which we want to calculate the regular
108
+ − 946 expression. Let us suppose this equivalence class is @{text X}.
107
+ − 947 Since @{text X} is the one to be solved, in every iteration step we have to pick an
108
+ − 948 equation to be eliminated that is different from @{text X}. In this way
+ − 949 @{text X} is kept to the final step. The choice is implemented using Hilbert's choice
107
+ − 950 operator, written @{text SOME} in the definition below.
100
+ − 951
+ − 952 \begin{center}
+ − 953 \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+ − 954 @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
+ − 955 & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+ − 956 & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\
+ − 957 \end{tabular}
+ − 958 \end{center}
+ − 959
+ − 960 \noindent
110
+ − 961 The last definition we need applies @{term Iter} over and over until a condition
159
+ − 962 @{text Cond} is \emph{not} satisfied anymore. This condition states that there
110
+ − 963 are more than one equation left in the equational system @{text ES}. To solve
+ − 964 an equational system we use Isabelle/HOL's @{text while}-operator as follows:
101
+ − 965
100
+ − 966 \begin{center}
+ − 967 @{thm Solve_def}
+ − 968 \end{center}
+ − 969
101
+ − 970 \noindent
198
+ − 971 We are not concerned here with the definition of this operator (see
+ − 972 Berghofer and Nipkow \cite{BerghoferNipkow00} for example), but note that we
+ − 973 eliminate in each @{const Iter}-step a single equation, and therefore have a
+ − 974 well-founded termination order by taking the cardinality of the equational
+ − 975 system @{text ES}. This enables us to prove properties about our definition
+ − 976 of @{const Solve} when we `call' it with the equivalence class @{text X} and
+ − 977 the initial equational system @{term "Init (UNIV // \<approx>A)"} from
108
+ − 978 \eqref{initcs} using the principle:
198
+ − 979
110
+ − 980 \begin{equation}\label{whileprinciple}
+ − 981 \mbox{\begin{tabular}{l}
103
+ − 982 @{term "invariant (Init (UNIV // \<approx>A))"} \\
+ − 983 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+ − 984 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+ − 985 @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+ − 986 \hline
+ − 987 \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
110
+ − 988 \end{tabular}}
+ − 989 \end{equation}
103
+ − 990
+ − 991 \noindent
104
+ − 992 This principle states that given an invariant (which we will specify below)
+ − 993 we can prove a property
+ − 994 @{text "P"} involving @{const Solve}. For this we have to discharge the following
+ − 995 proof obligations: first the
113
+ − 996 initial equational system satisfies the invariant; second the iteration
154
+ − 997 step @{text "Iter"} preserves the invariant as long as the condition @{term Cond} holds;
113
+ − 998 third @{text "Iter"} decreases the termination order, and fourth that
104
+ − 999 once the condition does not hold anymore then the property @{text P} must hold.
103
+ − 1000
104
+ − 1001 The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
108
+ − 1002 returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
104
+ − 1003 that this equational system still satisfies the invariant. In order to get
+ − 1004 the proof through, the invariant is composed of the following six properties:
103
+ − 1005
+ − 1006 \begin{center}
104
+ − 1007 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+ − 1008 @{text "invariant ES"} & @{text "\<equiv>"} &
103
+ − 1009 @{term "finite ES"} & @{text "(finiteness)"}\\
+ − 1010 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
104
+ − 1011 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
162
+ − 1012 & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
104
+ − 1013 & & & @{text "(distinctness)"}\\
110
+ − 1014 & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
162
+ − 1015 & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
103
+ − 1016 \end{tabular}
+ − 1017 \end{center}
+ − 1018
104
+ − 1019 \noindent
+ − 1020 The first two ensure that the equational system is always finite (number of equations
160
+ − 1021 and number of terms in each equation); the third makes sure the `meaning' of the
108
+ − 1022 equations is preserved under our transformations. The other properties are a bit more
+ − 1023 technical, but are needed to get our proof through. Distinctness states that every
154
+ − 1024 equation in the system is distinct. @{text Ardenable} ensures that we can always
156
+ − 1025 apply the @{text Arden} operation.
108
+ − 1026 The last property states that every @{text rhs} can only contain equivalence classes
+ − 1027 for which there is an equation. Therefore @{text lhss} is just the set containing
+ − 1028 the first components of an equational system,
+ − 1029 while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
123
+ − 1030 form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
110
+ − 1031 and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
108
+ − 1032
104
+ − 1033
110
+ − 1034 It is straightforward to prove that the initial equational system satisfies the
105
+ − 1035 invariant.
+ − 1036
167
+ − 1037 \begin{lmm}\label{invzero}
104
+ − 1038 @{thm[mode=IfThen] Init_ES_satisfies_invariant}
167
+ − 1039 \end{lmm}
104
+ − 1040
105
+ − 1041 \begin{proof}
+ − 1042 Finiteness is given by the assumption and the way how we set up the
198
+ − 1043 initial equational system. Soundness is proved in Lemma~\ref{inv}. Distinctness
154
+ − 1044 follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
113
+ − 1045 property also follows from the setup of the initial equational system, as does
174
+ − 1046 validity.
105
+ − 1047 \end{proof}
+ − 1048
113
+ − 1049 \noindent
+ − 1050 Next we show that @{text Iter} preserves the invariant.
+ − 1051
167
+ − 1052 \begin{lmm}\label{iterone}
104
+ − 1053 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
167
+ − 1054 \end{lmm}
104
+ − 1055
107
+ − 1056 \begin{proof}
156
+ − 1057 The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
110
+ − 1058 and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
+ − 1059 preserves the invariant.
+ − 1060 We prove this as follows:
+ − 1061
+ − 1062 \begin{center}
177
+ − 1063 \begin{tabular}{@ {}l@ {}}
+ − 1064 @{text "\<forall> ES."}\\ \mbox{}\hspace{5mm}@{thm (prem 1) Subst_all_satisfies_invariant} implies
110
+ − 1065 @{thm (concl) Subst_all_satisfies_invariant}
177
+ − 1066 \end{tabular}
110
+ − 1067 \end{center}
+ − 1068
+ − 1069 \noindent
156
+ − 1070 Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations
116
+ − 1071 keep the equational system finite. These operations also preserve soundness
198
+ − 1072 and distinctness (we proved soundness for @{const Arden} in Lemma~\ref{ardenable}).
154
+ − 1073 The property @{text ardenable} is clearly preserved because the append-operation
110
+ − 1074 cannot make a regular expression to match the empty string. Validity is
+ − 1075 given because @{const Arden} removes an equivalence class from @{text yrhs}
+ − 1076 and then @{const Subst_all} removes @{text Y} from the equational system.
132
+ − 1077 Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
110
+ − 1078 which matches with our proof-obligation of @{const "Subst_all"}. Since
132
+ − 1079 \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption
174
+ − 1080 to complete the proof.
107
+ − 1081 \end{proof}
+ − 1082
113
+ − 1083 \noindent
+ − 1084 We also need the fact that @{text Iter} decreases the termination measure.
+ − 1085
167
+ − 1086 \begin{lmm}\label{itertwo}
104
+ − 1087 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
167
+ − 1088 \end{lmm}
104
+ − 1089
105
+ − 1090 \begin{proof}
+ − 1091 By assumption we know that @{text "ES"} is finite and has more than one element.
+ − 1092 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
110
+ − 1093 @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
105
+ − 1094 that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+ − 1095 removes the equation @{text "Y = yrhs"} from the system, and therefore
174
+ − 1096 the cardinality of @{const Iter} strictly decreases.
105
+ − 1097 \end{proof}
+ − 1098
113
+ − 1099 \noindent
134
+ − 1100 This brings us to our property we want to establish for @{text Solve}.
113
+ − 1101
+ − 1102
167
+ − 1103 \begin{lmm}
104
+ − 1104 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+ − 1105 a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+ − 1106 and @{term "invariant {(X, rhs)}"}.
167
+ − 1107 \end{lmm}
104
+ − 1108
107
+ − 1109 \begin{proof}
110
+ − 1110 In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
198
+ − 1111 stronger invariant since Lemma~\ref{iterone} and \ref{itertwo} have the precondition
110
+ − 1112 that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ − 1113 in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
113
+ − 1114 Therefore our invariant cannot be just @{term "invariant ES"}, but must be
110
+ − 1115 @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
198
+ − 1116 @{thm (prem 2) Solve} and Lemma~\ref{invzero}, the more general invariant holds for
110
+ − 1117 the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
198
+ − 1118 Premise 2 is given by Lemma~\ref{iterone} and the fact that @{const Iter} might
110
+ − 1119 modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
198
+ − 1120 Premise 3 of~\eqref{whileprinciple} is by Lemma~\ref{itertwo}. Now in premise 4
110
+ − 1121 we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ − 1122 and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
113
+ − 1123 does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
110
+ − 1124 with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
123
+ − 1125 of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
110
+ − 1126 for which the invariant holds. This allows us to conclude that
113
+ − 1127 @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
174
+ − 1128 as needed.
107
+ − 1129 \end{proof}
+ − 1130
106
+ − 1131 \noindent
+ − 1132 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+ − 1133 there exists a regular expression.
+ − 1134
167
+ − 1135 \begin{lmm}\label{every_eqcl_has_reg}
105
+ − 1136 @{thm[mode=IfThen] every_eqcl_has_reg}
167
+ − 1137 \end{lmm}
105
+ − 1138
+ − 1139 \begin{proof}
138
+ − 1140 By the preceding lemma, we know that there exists a @{text "rhs"} such
105
+ − 1141 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+ − 1142 and that the invariant holds for this equation. That means we
+ − 1143 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
109
+ − 1144 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
198
+ − 1145 invariant and Lemma~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
156
+ − 1146 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
106
+ − 1147 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
113
+ − 1148 This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
176
+ − 1149 So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = lang (\<Uplus>rs)"}.
174
+ − 1150 With this we can conclude the proof.
105
+ − 1151 \end{proof}
+ − 1152
106
+ − 1153 \noindent
198
+ − 1154 Lemma~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
248
+ − 1155 of the Myhill-Nerode Theorem.
105
+ − 1156
198
+ − 1157 \begin{proof}[Proof of Theorem~\ref{myhillnerodeone}]
+ − 1158 By Lemma~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
105
+ − 1159 every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
110
+ − 1160 a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
123
+ − 1161 in @{term "finals A"} there exists a regular expression. Moreover by assumption
106
+ − 1162 we know that @{term "finals A"} must be finite, and therefore there must be a finite
105
+ − 1163 set of regular expressions @{text "rs"} such that
176
+ − 1164 @{term "\<Union>(finals A) = lang (\<Uplus>rs)"}.
105
+ − 1165 Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
174
+ − 1166 as the regular expression that is needed in the theorem.
105
+ − 1167 \end{proof}
233
+ − 1168
+ − 1169 \noindent
245
+ − 1170 Note that our algorithm for solving equational systems provides also a method for
+ − 1171 calculating a regular expression for the complement of a regular language:
+ − 1172 if we combine all regular
233
+ − 1173 expressions corresponding to equivalence classes not in @{term "finals A"},
245
+ − 1174 then we obtain a regular expression for the complement language @{term "- A"}.
+ − 1175 This is similar to the usual construction of a `complement automaton'.
54
+ − 1176 *}
+ − 1177
100
+ − 1178
+ − 1179
+ − 1180
+ − 1181 section {* Myhill-Nerode, Second Part *}
39
+ − 1182
+ − 1183 text {*
173
+ − 1184 \noindent
181
+ − 1185 In this section we will give a proof for establishing the second
248
+ − 1186 part of the Myhill-Nerode Theorem. It can be formulated in our setting as follows:
39
+ − 1187
193
+ − 1188 \begin{thrm}\label{myhillnerodetwo}
135
+ − 1189 Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
167
+ − 1190 \end{thrm}
39
+ − 1191
116
+ − 1192 \noindent
181
+ − 1193 The proof will be by induction on the structure of @{text r}. It turns out
116
+ − 1194 the base cases are straightforward.
+ − 1195
+ − 1196
+ − 1197 \begin{proof}[Base Cases]
173
+ − 1198 The cases for @{const ZERO}, @{const ONE} and @{const ATOM} are routine, because
149
+ − 1199 we can easily establish that
39
+ − 1200
114
+ − 1201 \begin{center}
+ − 1202 \begin{tabular}{l}
172
+ − 1203 @{thm quot_zero_eq}\\
+ − 1204 @{thm quot_one_subset}\\
+ − 1205 @{thm quot_atom_subset}
114
+ − 1206 \end{tabular}
+ − 1207 \end{center}
+ − 1208
116
+ − 1209 \noindent
174
+ − 1210 hold, which shows that @{term "UNIV // \<approx>(lang r)"} must be finite.
114
+ − 1211 \end{proof}
109
+ − 1212
116
+ − 1213 \noindent
183
+ − 1214 Much more interesting, however, are the inductive cases. They seem hard to be solved
117
+ − 1215 directly. The reader is invited to try.
+ − 1216
181
+ − 1217 In order to see how our proof proceeds consider the following suggestive picture
+ − 1218 taken from Constable et al \cite{Constable00}:
180
+ − 1219
181
+ − 1220 \begin{equation}\label{pics}
+ − 1221 \mbox{\begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
180
+ − 1222 \begin{tikzpicture}[scale=1]
+ − 1223 %Circle
+ − 1224 \draw[thick] (0,0) circle (1.1);
+ − 1225 \end{tikzpicture}
+ − 1226 &
+ − 1227 \begin{tikzpicture}[scale=1]
+ − 1228 %Circle
+ − 1229 \draw[thick] (0,0) circle (1.1);
+ − 1230 %Main rays
+ − 1231 \foreach \a in {0, 90,...,359}
+ − 1232 \draw[very thick] (0, 0) -- (\a:1.1);
+ − 1233 \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}
+ − 1234 \draw (\a: 0.65) node {$a_\l$};
+ − 1235 \end{tikzpicture}
+ − 1236 &
+ − 1237 \begin{tikzpicture}[scale=1]
+ − 1238 %Circle
+ − 1239 \draw[thick] (0,0) circle (1.1);
+ − 1240 %Main rays
+ − 1241 \foreach \a in {0, 45,...,359}
+ − 1242 \draw[very thick] (0, 0) -- (\a:1.1);
+ − 1243 \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
+ − 1244 \draw (\a: 0.77) node {$a_{\l}$};
+ − 1245 \end{tikzpicture}\\
+ − 1246 @{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"}
181
+ − 1247 \end{tabular}}
+ − 1248 \end{equation}
179
+ − 1249
181
+ − 1250 \noindent
190
+ − 1251 The relation @{term "\<approx>(lang r)"} partitions the set of all strings, @{term UNIV}, into some
183
+ − 1252 equivalence classes. To show that there are only finitely many of them, it
+ − 1253 suffices to show in each induction step that another relation, say @{text
184
+ − 1254 R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}.
+ − 1255
+ − 1256 \begin{dfntn}
245
+ − 1257 A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"}
184
+ − 1258 provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
+ − 1259 \end{dfntn}
+ − 1260
+ − 1261 \noindent
248
+ − 1262 For constructing @{text R}, we will rely on some \emph{tagging-functions}
198
+ − 1263 defined over strings. Given the inductive hypothesis, it will be easy to
+ − 1264 prove that the \emph{range} of these tagging-functions is finite. The range
+ − 1265 of a function @{text f} is defined as
183
+ − 1266
174
+ − 1267 \begin{center}
+ − 1268 @{text "range f \<equiv> f ` UNIV"}
+ − 1269 \end{center}
+ − 1270
+ − 1271 \noindent
181
+ − 1272 that means we take the image of @{text f} w.r.t.~all elements in the
+ − 1273 domain. With this we will be able to infer that the tagging-functions, seen
187
+ − 1274 as relations, give rise to finitely many equivalence classes.
+ − 1275 Finally we will show that the tagging-relations are more refined than
181
+ − 1276 @{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
+ − 1277 also be finite. We formally define the notion of a \emph{tagging-relation}
+ − 1278 as follows.
+ − 1279
117
+ − 1280
167
+ − 1281 \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
119
+ − 1282 and @{text y} are \emph{tag-related} provided
117
+ − 1283 \begin{center}
174
+ − 1284 @{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
117
+ − 1285 \end{center}
167
+ − 1286 \end{dfntn}
117
+ − 1287
145
+ − 1288
123
+ − 1289 In order to establish finiteness of a set @{text A}, we shall use the following powerful
118
+ − 1290 principle from Isabelle/HOL's library.
+ − 1291 %
+ − 1292 \begin{equation}\label{finiteimageD}
+ − 1293 @{thm[mode=IfThen] finite_imageD}
+ − 1294 \end{equation}
+ − 1295
+ − 1296 \noindent
123
+ − 1297 It states that if an image of a set under an injective function @{text f} (injective over this set)
131
+ − 1298 is finite, then the set @{text A} itself must be finite. We can use it to establish the following
118
+ − 1299 two lemmas.
+ − 1300
167
+ − 1301 \begin{lmm}\label{finone}
117
+ − 1302 @{thm[mode=IfThen] finite_eq_tag_rel}
167
+ − 1303 \end{lmm}
117
+ − 1304
+ − 1305 \begin{proof}
119
+ − 1306 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
123
+ − 1307 @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
201
+ − 1308 finite by assumption. Now @{term "f ` (UNIV // =tag=)"} is a subset of @{text "range f"},
119
+ − 1309 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+ − 1310 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
198
+ − 1311 From the assumptions we obtain \mbox{@{text "x \<in> X"}} and @{text "y \<in> Y"} with
123
+ − 1312 @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
+ − 1313 turn means that the equivalence classes @{text X}
198
+ − 1314 and @{text Y} must be equal. Therefore \eqref{finiteimageD} allows us to conclude
+ − 1315 with @{thm (concl) finite_eq_tag_rel}.
117
+ − 1316 \end{proof}
+ − 1317
167
+ − 1318 \begin{lmm}\label{fintwo}
123
+ − 1319 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
118
+ − 1320 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+ − 1321 If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+ − 1322 then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
167
+ − 1323 \end{lmm}
117
+ − 1324
+ − 1325 \begin{proof}
123
+ − 1326 We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
118
+ − 1327 be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
135
+ − 1328 @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
174
+ − 1329 which must be finite by assumption. What remains to be shown is that @{text f} is injective
118
+ − 1330 on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
+ − 1331 classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+ − 1332 @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+ − 1333 @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
135
+ − 1334 We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}.
+ − 1335 From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
123
+ − 1336 and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+ − 1337 such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
118
+ − 1338 are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
174
+ − 1339 they must also be @{text "R\<^isub>2"}-related, as we need to show.
117
+ − 1340 \end{proof}
+ − 1341
+ − 1342 \noindent
198
+ − 1343 Chaining Lemma~\ref{finone} and \ref{fintwo} together, means in order to show
181
+ − 1344 that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
174
+ − 1345 range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
183
+ − 1346 Let us attempt the @{const PLUS}-case first. We take as tagging-function
+ − 1347
119
+ − 1348 \begin{center}
181
+ − 1349 @{thm tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
119
+ − 1350 \end{center}
117
+ − 1351
119
+ − 1352 \noindent
183
+ − 1353 where @{text "A"} and @{text "B"} are some arbitrary languages. The reason for this choice
184
+ − 1354 is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}.
+ − 1355 This amounts to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
+ − 1356 @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will
187
+ − 1357 provide us with just the right assumptions in order to get the proof through.
183
+ − 1358
+ − 1359 \begin{proof}[@{const "PLUS"}-Case]
+ − 1360 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite
+ − 1361 (UNIV // \<approx>B)"} then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"}
+ − 1362 holds. The range of @{term "tag_Plus A B"} is a subset of this product
+ − 1363 set---so finite. For the refinement proof-obligation, we know that @{term
+ − 1364 "(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
184
+ − 1365 clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"}, as we needed to
183
+ − 1366 show. Finally we can discharge this case by setting @{text A} to @{term
+ − 1367 "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
119
+ − 1368 \end{proof}
+ − 1369
184
+ − 1370 \noindent
+ − 1371 The @{const TIMES}-case is slightly more complicated. We first prove the
187
+ − 1372 following lemma, which will aid the proof about refinement.
184
+ − 1373
+ − 1374 \begin{lmm}\label{refinement}
+ − 1375 The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\<approx>A"}, provided for
190
+ − 1376 all strings @{text x}, @{text y} and @{text z} we have that \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}}
184
+ − 1377 and @{term "x @ z \<in> A"} imply @{text "y @ z \<in> A"}.
+ − 1378 \end{lmm}
+ − 1379
109
+ − 1380
121
+ − 1381 \noindent
187
+ − 1382 We therefore can analyse how the strings @{text "x @ z"} are in the language
+ − 1383 @{text A} and then construct an appropriate tagging-function to infer that
190
+ − 1384 @{term "y @ z"} are also in @{text A}. For this we will use the notion of
+ − 1385 the set of all possible \emph{partitions} of a string:
182
+ − 1386
184
+ − 1387 \begin{equation}
+ − 1388 @{thm Partitions_def}
+ − 1389 \end{equation}
+ − 1390
187
+ − 1391 \noindent
+ − 1392 If we know that @{text "(x\<^isub>p, x\<^isub>s) \<in> Partitions x"}, we will
+ − 1393 refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x},
190
+ − 1394 and respectively to @{text "x\<^isub>s"} as the \emph{suffix}.
187
+ − 1395
+ − 1396
198
+ − 1397 Now assuming @{term "x @ z \<in> A \<cdot> B"}, there are only two possible ways of how to `split'
167
+ − 1398 this string to be in @{term "A \<cdot> B"}:
132
+ − 1399 %
125
+ − 1400 \begin{center}
181
+ − 1401 \begin{tabular}{c}
184
+ − 1402 \scalebox{1}{
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1403 \begin{tikzpicture}[fill=gray!20]
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1404 \node[draw,minimum height=3.8ex, fill] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1405 \node[draw,minimum height=3.8ex, right=-0.03em of x, fill] (za) { $\hspace{0.6em}@{text "z\<^isub>p"}\hspace{0.6em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1406 \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zza) { $\hspace{2.6em}@{text "z\<^isub>s"}\hspace{2.6em}$ };
184
+ − 1407
+ − 1408 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1409 (x.north west) -- ($(za.north west)+(0em,0em)$)
+ − 1410 node[midway, above=0.5em]{@{text x}};
+ − 1411
+ − 1412 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1413 ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+ − 1414 node[midway, above=0.5em]{@{text z}};
+ − 1415
+ − 1416 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1417 ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+ − 1418 node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
+ − 1419
+ − 1420 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1421 ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+ − 1422 node[midway, below=0.5em]{@{text "x @ z\<^isub>p \<in> A"}};
+ − 1423
+ − 1424 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1425 ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+ − 1426 node[midway, below=0.5em]{@{text "z\<^isub>s \<in> B"}};
+ − 1427 \end{tikzpicture}}
+ − 1428 \\[2mm]
+ − 1429 \scalebox{1}{
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1430 \begin{tikzpicture}[fill=gray!20]
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1431 \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{3em}@{text "x\<^isub>p"}\hspace{3em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1432 \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.2em}@{text "x\<^isub>s"}\hspace{0.2em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1433 \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
125
+ − 1434
+ − 1435 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1436 (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
128
+ − 1437 node[midway, above=0.5em]{@{text x}};
125
+ − 1438
+ − 1439 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1440 (z.north west) -- ($(z.north east)+(0em,0em)$)
128
+ − 1441 node[midway, above=0.5em]{@{text z}};
125
+ − 1442
+ − 1443 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1444 ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
167
+ − 1445 node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
125
+ − 1446
+ − 1447 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1448 ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
184
+ − 1449 node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> B"}};
125
+ − 1450
+ − 1451 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1452 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
184
+ − 1453 node[midway, below=0.5em]{@{term "x\<^isub>p \<in> A"}};
125
+ − 1454 \end{tikzpicture}}
159
+ − 1455 \end{tabular}
125
+ − 1456 \end{center}
132
+ − 1457 %
125
+ − 1458 \noindent
184
+ − 1459 Either @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}
+ − 1460 (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B}
+ − 1461 (second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case
+ − 1462 we will only go through if we know that @{term "x \<approx>A y"} holds @{text "(*)"}. Because then
+ − 1463 we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.
187
+ − 1464 In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is one possible partition
+ − 1465 of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the
185
+ − 1466 corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related'
184
+ − 1467 to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
187
+ − 1468 This will solve the second case.
185
+ − 1469 Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the
187
+ − 1470 tagging-function in the @{const Times}-case as:
184
+ − 1471
121
+ − 1472 \begin{center}
184
+ − 1473 @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~
185
+ − 1474 @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
121
+ − 1475 \end{center}
125
+ − 1476
+ − 1477 \noindent
198
+ − 1478 Note that we have to make the assumption for all suffixes @{text "x\<^isub>s"}, since we do
187
+ − 1479 not know anything about how the string @{term x} is partitioned.
+ − 1480 With this definition in place, let us prove the @{const "Times"}-case.
184
+ − 1481
125
+ − 1482
173
+ − 1483 \begin{proof}[@{const TIMES}-Case]
127
+ − 1484 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ − 1485 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
181
+ − 1486 @{term "tag_Times A B"} is a subset of this product set, and therefore finite.
187
+ − 1487 For the refinement of @{term "\<approx>(A \<cdot> B)"} and @{text "\<^raw:$\threesim$>\<^bsub>\<times>tag A B\<^esub>"},
+ − 1488 we have by Lemma \ref{refinement}
184
+ − 1489
127
+ − 1490 \begin{center}
184
+ − 1491 @{term "tag_Times A B x = tag_Times A B y"}
127
+ − 1492 \end{center}
184
+ − 1493
127
+ − 1494 \noindent
187
+ − 1495 and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot>
+ − 1496 B"}. As shown in the pictures above, there are two cases to be
+ − 1497 considered. First, there exists a @{text "z\<^isub>p"} and @{text
+ − 1498 "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s
+ − 1499 \<in> B"}. By the assumption about @{term "tag_Times A B"} we have @{term "\<approx>A
+ − 1500 `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Hence by the Myhill-Nerode
248
+ − 1501 Relation @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"},
187
+ − 1502 we can conclude in this case with @{term "y @ z \<in> A \<cdot> B"} (recall @{text
+ − 1503 "z\<^isub>p @ z\<^isub>s = z"}).
184
+ − 1504
185
+ − 1505 Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with
184
+ − 1506 @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
+ − 1507
127
+ − 1508 \begin{center}
185
+ − 1509 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
127
+ − 1510 \end{center}
184
+ − 1511
127
+ − 1512 \noindent
181
+ − 1513 and by the assumption about @{term "tag_Times A B"} also
184
+ − 1514
127
+ − 1515 \begin{center}
185
+ − 1516 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^isub>p \<in> A \<and> (y\<^isub>p, y\<^isub>s) \<in> Partitions y}"}
127
+ − 1517 \end{center}
128
+ − 1518
+ − 1519 \noindent
185
+ − 1520 This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
+ − 1521 such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
248
+ − 1522 {y\<^isub>s}"}. Unfolding the Myhill-Nerode Relation and together with the
187
+ − 1523 facts that @{text "x\<^isub>p \<in> A"} and \mbox{@{text "x\<^isub>s @ z \<in> B"}}, we
185
+ − 1524 obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
184
+ − 1525 this case. We again can complete the @{const TIMES}-case by setting @{text
+ − 1526 A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
+ − 1527 \end{proof}
+ − 1528
+ − 1529 \noindent
+ − 1530 The case for @{const Star} is similar to @{const TIMES}, but poses a few
187
+ − 1531 extra challenges. To deal with them, we define first the notion of a \emph{string
184
+ − 1532 prefix} and a \emph{strict string prefix}:
+ − 1533
128
+ − 1534 \begin{center}
184
+ − 1535 \begin{tabular}{l}
+ − 1536 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\
+ − 1537 @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+ − 1538 \end{tabular}
+ − 1539 \end{center}
+ − 1540
187
+ − 1541 When analysing the case of @{text "x @ z"} being an element in @{term "A\<star>"}
184
+ − 1542 and @{text x} is not the empty string, we have the following picture:
+ − 1543
+ − 1544 \begin{center}
+ − 1545 \scalebox{1}{
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1546 \begin{tikzpicture}[fill=gray!20]
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1547 \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{4em}@{text "x\<^bsub>pmax\<^esub>"}\hspace{4em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1548 \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.5em}@{text "x\<^bsub>s\<^esub>"}\hspace{0.5em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1549 \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1550 \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
128
+ − 1551
+ − 1552 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1553 (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ − 1554 node[midway, above=0.5em]{@{text x}};
+ − 1555
+ − 1556 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1557 (za.north west) -- ($(zb.north east)+(0em,0em)$)
+ − 1558 node[midway, above=0.5em]{@{text z}};
+ − 1559
+ − 1560 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1561 ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+ − 1562 node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
+ − 1563
+ − 1564 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1565 ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
185
+ − 1566 node[midway, below=0.5em]{@{term "x\<^isub>s @ z\<^isub>a \<in> A"}};
128
+ − 1567
+ − 1568 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1569 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
185
+ − 1570 node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"}};
128
+ − 1571
+ − 1572 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1573 ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
136
+ − 1574 node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
128
+ − 1575
+ − 1576 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1577 ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
184
+ − 1578 node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> A\<star>"}};
128
+ − 1579 \end{tikzpicture}}
+ − 1580 \end{center}
132
+ − 1581 %
128
+ − 1582 \noindent
184
+ − 1583 We can find a strict prefix @{text "x\<^isub>p"} of @{text x} such that @{term "x\<^isub>p \<in> A\<star>"},
+ − 1584 @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string
187
+ − 1585 @{text "[]"} would do (recall @{term "x \<noteq> []"}).
135
+ − 1586 There are potentially many such prefixes, but there can only be finitely many of them (the
128
+ − 1587 string @{text x} is finite). Let us therefore choose the longest one and call it
184
+ − 1588 @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
198
+ − 1589 know it is in @{term "A\<star>"} and cannot be the empty string. By Property~\ref{langprops}@{text "(iv)"},
185
+ − 1590 we can separate
187
+ − 1591 this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<noteq> []"}, @{text "a \<in> A"}
184
+ − 1592 and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
+ − 1593 otherwise @{text "x\<^bsub>pmax\<^esub>"} is not the longest prefix. That means @{text a}
128
+ − 1594 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
184
+ − 1595 @{text "z\<^isub>b"}. For this we know that @{text "x\<^isub>s @ z\<^isub>a \<in> A"} and
135
+ − 1596 @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
128
+ − 1597 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
184
+ − 1598 `border' of @{text x} and @{text z}. This string is @{text "x\<^isub>s @ z\<^isub>a"}.
+ − 1599
135
+ − 1600 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
128
+ − 1601 the following tagging-function:
132
+ − 1602 %
121
+ − 1603 \begin{center}
185
+ − 1604 @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~
+ − 1605 @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>s, x\<^isub>p) \<in> Partitions x}"}
121
+ − 1606 \end{center}
128
+ − 1607
177
+ − 1608 \begin{proof}[@{const Star}-Case]
130
+ − 1609 If @{term "finite (UNIV // \<approx>A)"}
+ − 1610 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
181
+ − 1611 @{term "tag_Star A"} is a subset of this set, and therefore finite.
185
+ − 1612 Again we have to show under the assumption @{term "x"}~@{term "=(tag_Star A)="}~@{term y}
+ − 1613 that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}.
+ − 1614
130
+ − 1615 We first need to consider the case that @{text x} is the empty string.
187
+ − 1616 From the assumption about strict prefixes in @{text "\<^raw:$\threesim$>\<^bsub>\<star>tag A\<^esub>"}, we
+ − 1617 can infer @{text y} is the empty string and
+ − 1618 then clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
134
+ − 1619 string, we can divide the string @{text "x @ z"} as shown in the picture
185
+ − 1620 above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"},
+ − 1621 we have
+ − 1622
130
+ − 1623 \begin{center}
185
+ − 1624 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^isub>s) \<in> Partitions x}"}
130
+ − 1625 \end{center}
185
+ − 1626
130
+ − 1627 \noindent
+ − 1628 which by assumption is equal to
185
+ − 1629
130
+ − 1630 \begin{center}
185
+ − 1631 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^isup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^isub>s) \<in> Partitions y}"}
130
+ − 1632 \end{center}
185
+ − 1633
130
+ − 1634 \noindent
190
+ − 1635 From this we know there exist a partition @{text "y\<^isub>p"} and @{text
185
+ − 1636 "y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
248
+ − 1637 y\<^isub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
185
+ − 1638 "y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
+ − 1639 Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
190
+ − 1640 A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set
187
+ − 1641 @{text "A"} to @{term "lang r"} and thus complete the proof.
121
+ − 1642 \end{proof}
39
+ − 1643 *}
+ − 1644
194
+ − 1645 section {* Second Part proved using Partial Derivatives\label{derivatives} *}
162
+ − 1646
+ − 1647 text {*
173
+ − 1648 \noindent
+ − 1649 As we have seen in the previous section, in order to establish
248
+ − 1650 the second direction of the Myhill-Nerode Theorem, it is sufficient to find
174
+ − 1651 a more refined relation than @{term "\<approx>(lang r)"} for which we can
+ − 1652 show that there are only finitely many equivalence classes. So far we
193
+ − 1653 showed this directly by induction on @{text "r"} using tagging-functions.
+ − 1654 However, there is also an indirect method to come up with such a refined
197
+ − 1655 relation by using derivatives of regular expressions~\cite{Brzozowski64}.
187
+ − 1656
193
+ − 1657 Assume the following two definitions for the \emph{left-quotient} of a language,
203
+ − 1658 which we write as @{term "Deriv c A"} and @{term "Derivs s A"} where @{text c}
193
+ − 1659 is a character and @{text s} a string, respectively:
174
+ − 1660
+ − 1661 \begin{center}
+ − 1662 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
+ − 1663 @{thm (lhs) Der_def} & @{text "\<equiv>"} & @{thm (rhs) Der_def}\\
+ − 1664 @{thm (lhs) Ders_def} & @{text "\<equiv>"} & @{thm (rhs) Ders_def}\\
+ − 1665 \end{tabular}
+ − 1666 \end{center}
+ − 1667
+ − 1668 \noindent
193
+ − 1669 In order to aid readability, we shall make use of the following abbreviation
187
+ − 1670
+ − 1671 \begin{center}
203
+ − 1672 @{abbrev "Derivss s As"}
187
+ − 1673 \end{center}
+ − 1674
+ − 1675 \noindent
190
+ − 1676 where we apply the left-quotient to a set of languages and then combine the results.
248
+ − 1677 Clearly we have the following equivalence between the Myhill-Nerode Relation
193
+ − 1678 (Definition~\ref{myhillneroderel}) and left-quotients
174
+ − 1679
+ − 1680 \begin{equation}\label{mhders}
203
+ − 1681 @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Derivs x A = Derivs y A"}
174
+ − 1682 \end{equation}
+ − 1683
+ − 1684 \noindent
193
+ − 1685 It is also straightforward to establish the following properties of left-quotients
174
+ − 1686
186
+ − 1687 \begin{equation}
+ − 1688 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
203
+ − 1689 @{thm (lhs) Deriv_simps(1)} & $=$ & @{thm (rhs) Deriv_simps(1)}\\
+ − 1690 @{thm (lhs) Deriv_simps(2)} & $=$ & @{thm (rhs) Deriv_simps(2)}\\
+ − 1691 @{thm (lhs) Deriv_simps(3)} & $=$ & @{thm (rhs) Deriv_simps(3)}\\
+ − 1692 @{thm (lhs) Deriv_simps(4)} & $=$ & @{thm (rhs) Deriv_simps(4)}\\
174
+ − 1693 @{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
203
+ − 1694 @{thm (lhs) Deriv_star} & $=$ & @{thm (rhs) Deriv_star}\\
+ − 1695 @{thm (lhs) Derivs_simps(1)} & $=$ & @{thm (rhs) Derivs_simps(1)}\\
+ − 1696 @{thm (lhs) Derivs_simps(2)} & $=$ & @{thm (rhs) Derivs_simps(2)}\\
+ − 1697 %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
+ − 1698 % & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
186
+ − 1699 \end{tabular}}
+ − 1700 \end{equation}
174
+ − 1701
+ − 1702 \noindent
245
+ − 1703 Note that in the last equation we use the list-cons operator written
199
+ − 1704 \mbox{@{text "_ :: _"}}. The only interesting case is the case of @{term "A\<star>"}
198
+ − 1705 where we use Property~\ref{langprops}@{text "(i)"} in order to infer that
203
+ − 1706 @{term "Deriv c (A\<star>) = Deriv c (A \<cdot> A\<star>)"}. We can then complete the proof by
245
+ − 1707 using the fifth equation and noting that @{term "Deriv c (A\<star>) \<subseteq> (Deriv
+ − 1708 c A) \<cdot> A\<star>"} provided @{text "[] \<in> A"}.
198
+ − 1709
+ − 1710 Brzozowski observed that the left-quotients for languages of
+ − 1711 regular expressions can be calculated directly using the notion of
+ − 1712 \emph{derivatives of a regular expression} \cite{Brzozowski64}. We define
+ − 1713 this notion in Isabelle/HOL as follows:
174
+ − 1714
+ − 1715 \begin{center}
+ − 1716 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
203
+ − 1717 @{thm (lhs) deriv.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(1)}\\
+ − 1718 @{thm (lhs) deriv.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(2)}\\
+ − 1719 @{thm (lhs) deriv.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(3)[where c'="d"]}\\
+ − 1720 @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1721 & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1722 @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
177
+ − 1723 & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
203
+ − 1724 @{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
177
+ − 1725 & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
203
+ − 1726 @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\
+ − 1727 @{thm (lhs) deriv.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(6)}\smallskip\\
+ − 1728 @{thm (lhs) derivs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(1)}\\
+ − 1729 @{thm (lhs) derivs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}\\
174
+ − 1730 \end{tabular}
+ − 1731 \end{center}
+ − 1732
+ − 1733 \noindent
198
+ − 1734 The last two clauses extend derivatives from characters to strings. The
193
+ − 1735 boolean function @{term "nullable r"} needed in the @{const Times}-case tests
197
+ − 1736 whether a regular expression can recognise the empty string. It can be defined as
+ − 1737 follows.
174
+ − 1738
+ − 1739 \begin{center}
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1740 \begin{tabular}{c}
174
+ − 1741 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ − 1742 @{thm (lhs) nullable.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
+ − 1743 @{thm (lhs) nullable.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(2)}\\
+ − 1744 @{thm (lhs) nullable.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(3)}\\
+ − 1745 @{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1746 & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1747 @{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1748 & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1749 @{thm (lhs) nullable.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(6)}\\
+ − 1750 \end{tabular}
+ − 1751 \end{tabular}
+ − 1752 \end{center}
+ − 1753
+ − 1754 \noindent
190
+ − 1755 By induction on the regular expression @{text r}, respectively on the string @{text s},
197
+ − 1756 one can easily show that left-quotients and derivatives of regular expressions
198
+ − 1757 relate as follows (see for example~\cite{Sakarovitch09}):
174
+ − 1758
+ − 1759 \begin{equation}\label{Dersders}
186
+ − 1760 \mbox{\begin{tabular}{c}
203
+ − 1761 @{thm Deriv_deriv}\\
+ − 1762 @{thm Derivs_derivs}
174
+ − 1763 \end{tabular}}
+ − 1764 \end{equation}
+ − 1765
+ − 1766 \noindent
248
+ − 1767 The importance of this fact in the context of the Myhill-Nerode Theorem is that
187
+ − 1768 we can use \eqref{mhders} and \eqref{Dersders} in order to
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1769 establish that
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1770
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1771 \begin{center}
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1772 @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}
203
+ − 1773 @{term "lang (derivs x r) = lang (derivs y r)"}.
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1774 \end{center}
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1775
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1776 \noindent
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1777 holds and hence
174
+ − 1778
186
+ − 1779 \begin{equation}
203
+ − 1780 @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "derivs x r = derivs y r"}
186
+ − 1781 \end{equation}
174
+ − 1782
+ − 1783
+ − 1784 \noindent
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1785 This means the right-hand side (seen as a relation) refines the Myhill-Nerode
248
+ − 1786 Relation. Consequently, we can use @{text
197
+ − 1787 "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a
+ − 1788 tagging-relation. However, in order to be useful for the second part of the
248
+ − 1789 Myhill-Nerode Theorem, we have to be able to establish that for the
197
+ − 1790 corresponding language there are only finitely many derivatives---thus
+ − 1791 ensuring that there are only finitely many equivalence
+ − 1792 classes. Unfortunately, this is not true in general. Sakarovitch gives an
+ − 1793 example where a regular expression has infinitely many derivatives
218
+ − 1794 w.r.t.~the language @{text "(ab)\<^isup>\<star> \<union> (ab)\<^isup>\<star>a"}, which is formally
+ − 1795 written in our notation as \mbox{@{text "{[a,b]}\<^isup>\<star> \<union> ({[a,b]}\<^isup>\<star> \<cdot> {[a]})"}}
198
+ − 1796 (see \cite[Page~141]{Sakarovitch09}).
197
+ − 1797
193
+ − 1798
+ − 1799 What Brzozowski \cite{Brzozowski64} established is that for every language there
199
+ − 1800 \emph{are} only finitely `dissimilar' derivatives for a regular
193
+ − 1801 expression. Two regular expressions are said to be \emph{similar} provided
+ − 1802 they can be identified using the using the @{text "ACI"}-identities:
+ − 1803
174
+ − 1804
187
+ − 1805 \begin{equation}\label{ACI}
+ − 1806 \mbox{\begin{tabular}{cl}
186
+ − 1807 (@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
+ − 1808 (@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
+ − 1809 (@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
187
+ − 1810 \end{tabular}}
+ − 1811 \end{equation}
174
+ − 1812
+ − 1813 \noindent
187
+ − 1814 Carrying this idea through, we must not consider the set of all derivatives,
199
+ − 1815 but the one modulo @{text "ACI"}. In principle, this can be done formally,
190
+ − 1816 but it is very painful in a theorem prover (since there is no
194
+ − 1817 direct characterisation of the set of dissimilar derivatives).
187
+ − 1818
174
+ − 1819
186
+ − 1820 Fortunately, there is a much simpler approach using \emph{partial
+ − 1821 derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined
+ − 1822 in Isabelle/HOL as follows:
173
+ − 1823
175
+ − 1824 \begin{center}
+ − 1825 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
203
+ − 1826 @{thm (lhs) pderiv.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(1)}\\
+ − 1827 @{thm (lhs) pderiv.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(2)}\\
+ − 1828 @{thm (lhs) pderiv.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(3)[where c'="d"]}\\
+ − 1829 @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1830 & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1831 @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
177
+ − 1832 & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
203
+ − 1833 @{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \<union> (pderiv c r\<^isub>2)"}\\
177
+ − 1834 & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
203
+ − 1835 @{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\
+ − 1836 @{thm (lhs) pderiv.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(6)}\smallskip\\
+ − 1837 @{thm (lhs) pderivs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(1)}\\
+ − 1838 @{thm (lhs) pderivs.simps(2)} & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
175
+ − 1839 \end{tabular}
+ − 1840 \end{center}
173
+ − 1841
186
+ − 1842 \noindent
187
+ − 1843 Again the last two clauses extend partial derivatives from characters to strings.
+ − 1844 Unlike `simple' derivatives, the functions for partial derivatives return sets of regular
+ − 1845 expressions. In the @{const Times} and @{const Star} cases we therefore use the
+ − 1846 auxiliary definition
186
+ − 1847
+ − 1848 \begin{center}
+ − 1849 @{text "TIMESS rs r \<equiv> {TIMES r' r | r' \<in> rs}"}
+ − 1850 \end{center}
+ − 1851
+ − 1852 \noindent
187
+ − 1853 in order to `sequence' a regular expression with a set of regular
+ − 1854 expressions. Note that in the last clause we first build the set of partial
+ − 1855 derivatives w.r.t~the character @{text c}, then build the image of this set under the
203
+ − 1856 function @{term "pderivs s"} and finally `union up' all resulting sets. It will be
190
+ − 1857 convenient to introduce for this the following abbreviation
187
+ − 1858
+ − 1859 \begin{center}
203
+ − 1860 @{abbrev "pderivs_set s rs"}
187
+ − 1861 \end{center}
+ − 1862
+ − 1863 \noindent
203
+ − 1864 which simplifies the last clause of @{const "pderivs"} to
187
+ − 1865
+ − 1866 \begin{center}
+ − 1867 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
203
+ − 1868 @{thm (lhs) pderivs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(2)}\\
187
+ − 1869 \end{tabular}
+ − 1870 \end{center}
+ − 1871
+ − 1872 Partial derivatives can be seen as having the @{text "ACI"}-identities already built in:
+ − 1873 taking the partial derivatives of the
+ − 1874 regular expressions in \eqref{ACI} gives us in each case
+ − 1875 equal sets. Antimirov \cite{Antimirov95} showed a similar result to
198
+ − 1876 \eqref{Dersders} for partial derivatives, namely
186
+ − 1877
190
+ − 1878 \begin{equation}\label{Derspders}
187
+ − 1879 \mbox{\begin{tabular}{lc}
203
+ − 1880 @{text "(i)"} & @{thm Deriv_pderiv}\\
+ − 1881 @{text "(ii)"} & @{thm Derivs_pderivs}
186
+ − 1882 \end{tabular}}
187
+ − 1883 \end{equation}
+ − 1884
+ − 1885 \begin{proof}
+ − 1886 The first fact is by a simple induction on @{text r}. For the second we slightly
+ − 1887 modify Antimirov's proof by performing an induction on @{text s} where we
194
+ − 1888 generalise over all @{text r}. That means in the @{text "cons"}-case the
187
+ − 1889 induction hypothesis is
+ − 1890
+ − 1891 \begin{center}
203
+ − 1892 @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)"}
187
+ − 1893 \end{center}
186
+ − 1894
+ − 1895 \noindent
187
+ − 1896 With this we can establish
+ − 1897
+ − 1898 \begin{center}
+ − 1899 \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}
203
+ − 1900 @{term "Derivs (c # s) (lang r)"}
+ − 1901 & @{text "="} & @{term "Derivs s (Deriv c (lang r))"} & by def.\\
+ − 1902 & @{text "="} & @{term "Derivs s (\<Union> lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
+ − 1903 & @{text "="} & @{term "\<Union> (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\
+ − 1904 & @{text "="} & @{term "\<Union> lang ` (\<Union> pderivs s ` (pderiv c r))"} & by IH\\
+ − 1905 & @{text "="} & @{term "\<Union> lang ` (pderivs (c # s) r)"} & by def.\\
187
+ − 1906 \end{tabular}
+ − 1907 \end{center}
+ − 1908
+ − 1909 \noindent
190
+ − 1910 Note that in order to apply the induction hypothesis in the fourth equation, we
+ − 1911 need the generalisation over all regular expressions @{text r}. The case for
+ − 1912 the empty string is routine and omitted.
187
+ − 1913 \end{proof}
+ − 1914
190
+ − 1915 \noindent
+ − 1916 Taking \eqref{Dersders} and \eqref{Derspders} together gives the relationship
+ − 1917 between languages of derivatives and partial derivatives
+ − 1918
+ − 1919 \begin{equation}
+ − 1920 \mbox{\begin{tabular}{lc}
203
+ − 1921 @{text "(i)"} & @{thm deriv_pderiv[symmetric]}\\
+ − 1922 @{text "(ii)"} & @{thm derivs_pderivs[symmetric]}
190
+ − 1923 \end{tabular}}
+ − 1924 \end{equation}
+ − 1925
+ − 1926 \noindent
+ − 1927 These two properties confirm the observation made earlier
193
+ − 1928 that by using sets, partial derivatives have the @{text "ACI"}-identities
190
+ − 1929 of derivatives already built in.
+ − 1930
245
+ − 1931 Antimirov also proved that for every language and every regular expression
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1932 there are only finitely many partial derivatives, whereby the set of partial
193
+ − 1933 derivatives of @{text r} w.r.t.~a language @{text A} is defined as
+ − 1934
+ − 1935 \begin{equation}\label{Pdersdef}
203
+ − 1936 @{thm pderivs_lang_def}
193
+ − 1937 \end{equation}
+ − 1938
+ − 1939 \begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}
+ − 1940 For every language @{text A} and every regular expression @{text r},
203
+ − 1941 \mbox{@{thm finite_pderivs_lang}}.
193
+ − 1942 \end{thrm}
+ − 1943
+ − 1944 \noindent
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1945 Antimirov's proof first establishes this theorem for the language @{term UNIV1},
193
+ − 1946 which is the set of all non-empty strings. For this he proves:
+ − 1947
198
+ − 1948 \begin{equation}\label{pdersunivone}
193
+ − 1949 \mbox{\begin{tabular}{l}
203
+ − 1950 @{thm pderivs_lang_Zero}\\
+ − 1951 @{thm pderivs_lang_One}\\
+ − 1952 @{thm pderivs_lang_Atom}\\
+ − 1953 @{thm pderivs_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1954 @{thm pderivs_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1955 @{thm pderivs_lang_Star}\\
193
+ − 1956 \end{tabular}}
+ − 1957 \end{equation}
+ − 1958
+ − 1959 \noindent
+ − 1960 from which one can deduce by induction on @{text r} that
+ − 1961
+ − 1962 \begin{center}
203
+ − 1963 @{thm finite_pderivs_lang_UNIV1}
193
+ − 1964 \end{center}
+ − 1965
+ − 1966 \noindent
+ − 1967 holds. Now Antimirov's theorem follows because
+ − 1968
+ − 1969 \begin{center}
203
+ − 1970 @{thm pderivs_lang_UNIV}\\
193
+ − 1971 \end{center}
+ − 1972
+ − 1973 \noindent
203
+ − 1974 and for all languages @{text "A"}, @{term "pderivs_lang A r"} is a subset of
+ − 1975 @{term "pderivs_lang UNIV r"}. Since we follow Antimirov's proof quite
199
+ − 1976 closely in our formalisation (only the last two cases of
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1977 \eqref{pdersunivone} involve some non-routine induction arguments), we omit
199
+ − 1978 the details.
193
+ − 1979
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 1980 Let us now return to our proof for the second direction in the Myhill-Nerode
248
+ − 1981 Theorem. The point of the above calculations is to use
201
+ − 1982 @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} as tagging-relation.
193
+ − 1983
+ − 1984
196
+ − 1985 \begin{proof}[Proof of Theorem~\ref{myhillnerodetwo} (second version)]
193
+ − 1986 Using \eqref{mhders}
+ − 1987 and \eqref{Derspders} we can easily infer that
+ − 1988
+ − 1989 \begin{center}
203
+ − 1990 @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pderivs x r = pderivs y r"}
193
+ − 1991 \end{center}
+ − 1992
+ − 1993 \noindent
201
+ − 1994 which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.
193
+ − 1995 So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}}
203
+ − 1996 holds if @{term "finite (UNIV // (=(\<lambda>x. pderivs x r)=))"}. In order to establish
193
+ − 1997 the latter, we can use Lemma~\ref{finone} and show that the range of the
203
+ − 1998 tagging-function \mbox{@{term "\<lambda>x. pderivs x r"}} is finite. For this recall Definition
193
+ − 1999 \ref{Pdersdef}, which gives us that
+ − 2000
+ − 2001 \begin{center}
203
+ − 2002 @{thm pderivs_lang_def[where A="UNIV", simplified]}
193
+ − 2003 \end{center}
+ − 2004
+ − 2005 \noindent
203
+ − 2006 Now the range of @{term "\<lambda>x. pderivs x r"} is a subset of @{term "Pow (pderivs_lang UNIV r)"},
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2007 which we know is finite by Theorem~\ref{antimirov}. Consequently there
245
+ − 2008 are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"}.
+ − 2009 This relation refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the
248
+ − 2010 second part of the Myhill-Nerode Theorem.
193
+ − 2011 \end{proof}
162
+ − 2012 *}
+ − 2013
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2014 section {* Closure Properties of Regular Languages\label{closure} *}
39
+ − 2015
186
+ − 2016 text {*
187
+ − 2017 \noindent
196
+ − 2018 The beauty of regular languages is that they are closed under many set
+ − 2019 operations. Closure under union, concatenation and Kleene-star are trivial
+ − 2020 to establish given our definition of regularity (recall Definition~\ref{regular}).
240
+ − 2021 More interesting in our setting is the closure under complement, because it seems difficult
196
+ − 2022 to construct a regular expression for the complement language by direct
+ − 2023 means. However the existence of such a regular expression can now be easily
248
+ − 2024 proved using both parts of the Myhill-Nerode Theorem, since
196
+ − 2025
186
+ − 2026 \begin{center}
+ − 2027 @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+ − 2028 \end{center}
+ − 2029
+ − 2030 \noindent
+ − 2031 holds for any strings @{text "s\<^isub>1"} and @{text
+ − 2032 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"}
196
+ − 2033 give rise to the same partitions. So if one is finite, the other is too, and
233
+ − 2034 vice versa. As noted earlier, our algorithm for solving equational systems
250
+ − 2035 actually calculates a regular expression for the complement language.
+ − 2036 Calculating such a regular expression via
196
+ − 2037 automata using the standard method would be quite involved. It includes the
+ − 2038 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
+ − 2039 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
+ − 2040 regular expression. Clearly not something you want to formalise in a theorem
+ − 2041 prover in which it is cumbersome to reason about automata.
186
+ − 2042
+ − 2043 Once closure under complement is established, closure under intersection
+ − 2044 and set difference is also easy, because
+ − 2045
+ − 2046 \begin{center}
+ − 2047 \begin{tabular}{c}
+ − 2048 @{term "A \<inter> B = - (- A \<union> - B)"}\\
+ − 2049 @{term "A - B = - (- A \<union> B)"}
+ − 2050 \end{tabular}
+ − 2051 \end{center}
+ − 2052
+ − 2053 \noindent
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2054 Since all finite languages are regular, then by closure under complement also
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2055 all co-finite languages. Closure of regular languages under reversal, that is
186
+ − 2056
+ − 2057 \begin{center}
+ − 2058 @{text "A\<^bsup>-1\<^esup> \<equiv> {s\<^bsup>-1\<^esup> | s \<in> A}"}
+ − 2059 \end{center}
+ − 2060
+ − 2061 \noindent
196
+ − 2062 can be shown with the help of the following operation defined recursively over
+ − 2063 regular expressions
186
+ − 2064
+ − 2065 \begin{center}
+ − 2066 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 2067 @{thm (lhs) Rev.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(1)}\\
+ − 2068 @{thm (lhs) Rev.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(2)}\\
+ − 2069 @{thm (lhs) Rev.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(3)}\\
+ − 2070 @{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 2071 @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 2072 @{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 2073 @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 2074 @{thm (lhs) Rev.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(6)}\\
+ − 2075 \end{tabular}
+ − 2076 \end{center}
+ − 2077
193
+ − 2078 \noindent
196
+ − 2079 For this operation we can show
186
+ − 2080
193
+ − 2081 \begin{center}
+ − 2082 @{text "(\<calL>(r))\<^bsup>-1\<^esup>"}~@{text "="}~@{thm (rhs) rev_lang}
+ − 2083 \end{center}
+ − 2084
+ − 2085 \noindent
196
+ − 2086 from which closure under reversal of regular languages follows.
193
+ − 2087
196
+ − 2088 A perhaps surprising fact is that regular languages are closed under any
+ − 2089 left-quotient. Define
193
+ − 2090
+ − 2091 \begin{center}
203
+ − 2092 @{abbrev "Deriv_lang B A"}
193
+ − 2093 \end{center}
186
+ − 2094
193
+ − 2095 \noindent
196
+ − 2096 and assume @{text B} is any language and @{text A} is regular, then @{term
203
+ − 2097 "Deriv_lang B A"} is regular. To see this consider the following argument
196
+ − 2098 using partial derivatives: From @{text A} being regular we know there exists
+ − 2099 a regular expression @{text r} such that @{term "A = lang r"}. We also know
203
+ − 2100 that @{term "pderivs_lang B r"} is finite for every language @{text B} and
196
+ − 2101 regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition
245
+ − 2102 and \eqref{Derspders} we have
196
+ − 2103
186
+ − 2104
193
+ − 2105 \begin{equation}\label{eqq}
203
+ − 2106 @{term "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"}
193
+ − 2107 \end{equation}
+ − 2108
+ − 2109 \noindent
203
+ − 2110 Since there are only finitely many regular expressions in @{term "pderivs_lang
198
+ − 2111 B r"}, we know by \eqref{uplus} that there exists a regular expression so that
203
+ − 2112 the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B
+ − 2113 r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
+ − 2114 @{term "Deriv_lang B A"} is regular.
233
+ − 2115
237
+ − 2116 Even more surprising is the fact that for \emph{every} language @{text A}, the language
258
+ − 2117 consisting of all (scattered) substrings of @{text A} is regular \cite{Haines69} (see also
247
+ − 2118 \cite{Shallit08, Gasarch09}).
258
+ − 2119 A \emph{(scattered) substring} can be obtained
233
+ − 2120 by striking out zero or more characters from a string. This can be defined
237
+ − 2121 inductively in Isabelle/HOL by the following three rules:
233
+ − 2122
+ − 2123 \begin{center}
+ − 2124 @{thm[mode=Axiom] emb0[where bs="x"]}\hspace{10mm}
+ − 2125 @{thm[mode=Rule] emb1[where as="x" and b="c" and bs="y"]}\hspace{10mm}
+ − 2126 @{thm[mode=Rule] emb2[where as="x" and a="c" and bs="y"]}
+ − 2127 \end{center}
+ − 2128
+ − 2129 \noindent
245
+ − 2130 It is straightforward to prove that @{text "\<preceq>"} is a partial order. Now define the
237
+ − 2131 \emph{language of substrings} and \emph{superstrings} of a language @{text A}
+ − 2132 respectively as
233
+ − 2133
+ − 2134 \begin{center}
+ − 2135 \begin{tabular}{l}
+ − 2136 @{thm SUBSEQ_def}\\
+ − 2137 @{thm SUPSEQ_def}
+ − 2138 \end{tabular}
+ − 2139 \end{center}
+ − 2140
+ − 2141 \noindent
+ − 2142 We like to establish
+ − 2143
247
+ − 2144 \begin{thrm}[Haines \cite{Haines69}]\label{subseqreg}
245
+ − 2145 For every language @{text A}, the languages @{text "(i)"} @{term "SUBSEQ A"} and
+ − 2146 @{text "(ii)"} @{term "SUPSEQ A"}
233
+ − 2147 are regular.
247
+ − 2148 \end{thrm}
233
+ − 2149
+ − 2150 \noindent
245
+ − 2151 Our proof follows the one given in \cite[Pages 92--95]{Shallit08}, except that we use
247
+ − 2152 Higman's Lemma, which is already proved in the Isabelle/HOL library
248
+ − 2153 \cite{Berghofer03}.\footnote{Unfortunately, Berghofer's formalisation of Higman's Lemma
247
+ − 2154 is restricted to 2-letter alphabets,
+ − 2155 which means also our formalisation of Theorem~\ref{subseqreg} is `tainted' with
+ − 2156 this constraint. However our methodology is applicable to any alphabet of finite size.}
256
+ − 2157 Higman's Lemma allows us to infer that every language @{text A} of antichains, satisfying
233
+ − 2158
+ − 2159 \begin{equation}\label{higman}
+ − 2160 @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"}
+ − 2161 \end{equation}
+ − 2162
+ − 2163 \noindent
+ − 2164 is finite.
+ − 2165
247
+ − 2166 The first step in our proof of Theorem~\ref{subseqreg} is to establish the
245
+ − 2167 following simple properties for @{term SUPSEQ}
233
+ − 2168
+ − 2169 \begin{equation}\label{supseqprops}
+ − 2170 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 2171 @{thm (lhs) SUPSEQ_simps(1)} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_simps(1)}\\
+ − 2172 @{thm (lhs) SUPSEQ_simps(2)} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_simps(2)}\\
+ − 2173 @{thm (lhs) SUPSEQ_atom} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_atom}\\
+ − 2174 @{thm (lhs) SUPSEQ_union} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_union}\\
+ − 2175 @{thm (lhs) SUPSEQ_conc} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_conc}\\
+ − 2176 @{thm (lhs) SUPSEQ_star} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_star}
+ − 2177 \end{tabular}}
+ − 2178 \end{equation}
+ − 2179
+ − 2180 \noindent
+ − 2181 whereby the last equation follows from the fact that @{term "A\<star>"} contains the
+ − 2182 empty string. With these properties at our disposal we can establish the lemma
+ − 2183
+ − 2184 \begin{lmm}
237
+ − 2185 If @{text A} is regular, then also @{term "SUPSEQ A"}.
233
+ − 2186 \end{lmm}
+ − 2187
+ − 2188 \begin{proof}
239
+ − 2189 Since our alphabet is finite, we have a regular expression, written @{text ALL}, that
240
+ − 2190 matches every string. Using this regular expression we can inductively define
239
+ − 2191 the operation @{text "r\<up>"}
233
+ − 2192
+ − 2193 \begin{center}
+ − 2194 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 2195 @{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\
+ − 2196 @{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\
239
+ − 2197 @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\
233
+ − 2198 @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &
+ − 2199 @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 2200 @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &
+ − 2201 @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 2202 @{thm (lhs) UP.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(6)}
+ − 2203 \end{tabular}
+ − 2204 \end{center}
+ − 2205
+ − 2206 \noindent
239
+ − 2207 and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows
251
+ − 2208 that @{term "SUPSEQ A"} is regular, provided @{text A} is.
233
+ − 2209 \end{proof}
+ − 2210
+ − 2211 \noindent
247
+ − 2212 Now we can prove the main lemma w.r.t.~@{const "SUPSEQ"}, namely
233
+ − 2213
+ − 2214 \begin{lmm}\label{mset}
+ − 2215 For every language @{text A}, there exists a finite language @{text M} such that
+ − 2216 \begin{center}
+ − 2217 \mbox{@{term "SUPSEQ M = SUPSEQ A"}}\;.
+ − 2218 \end{center}
+ − 2219 \end{lmm}
+ − 2220
+ − 2221 \begin{proof}
+ − 2222 For @{text M} we take the set of all minimal elements of @{text A}. An element @{text x}
237
+ − 2223 is said to be \emph{minimal} in @{text A} provided
233
+ − 2224
+ − 2225 \begin{center}
+ − 2226 @{thm minimal_def}
+ − 2227 \end{center}
+ − 2228
+ − 2229 \noindent
239
+ − 2230 By Higman's Lemma \eqref{higman} we know
237
+ − 2231 that @{term "M \<equiv> {x \<in> A. minimal x A}"} is finite, since every minimal element is incomparable,
233
+ − 2232 except with itself.
+ − 2233 It is also straightforward to show that @{term "SUPSEQ M \<subseteq> SUPSEQ A"}. For
240
+ − 2234 the other direction we have @{term "x \<in> SUPSEQ A"}. From this we obtain
245
+ − 2235 a @{text y} such that @{term "y \<in> A"} and @{term "y \<preceq> x"}. Since we have that
233
+ − 2236 the relation \mbox{@{term "{(y, x). y \<preceq> x \<and> x \<noteq> y}"}} is well-founded, there must
+ − 2237 be a minimal element @{text "z"} such that @{term "z \<in> A"} and @{term "z \<preceq> y"},
+ − 2238 and hence by transitivity also \mbox{@{term "z \<preceq> x"}} (here we deviate from the argument
+ − 2239 given in \cite{Shallit08}, because Isabelle/HOL provides already an extensive infrastructure
+ − 2240 for reasoning about well-foundedness). Since @{term "z"} is
237
+ − 2241 minimal and an element in @{term A}, we also know that @{term z} is in @{term M}.
240
+ − 2242 From this together with \mbox{@{term "z \<preceq> x"}}, we can infer that @{term x} is in
237
+ − 2243 @{term "SUPSEQ M"}, as required.
233
+ − 2244 \end{proof}
+ − 2245
+ − 2246 \noindent
247
+ − 2247 This lemma allows us to establish the second part of Theorem~\ref{subseqreg}.
233
+ − 2248
247
+ − 2249 \begin{proof}[Proof of the Second Part of Theorem~\ref{subseqreg}]
233
+ − 2250 Given any language @{text A}, by Lemma~\ref{mset} we know there exists
+ − 2251 a finite, and thus regular, language @{text M}. We further have @{term "SUPSEQ M = SUPSEQ A"},
+ − 2252 which establishes the second part.
+ − 2253 \end{proof}
+ − 2254
+ − 2255 \noindent
247
+ − 2256 In order to establish the first part of this theorem, we use the
237
+ − 2257 property proved in \cite{Shallit08}, namely that
233
+ − 2258
+ − 2259 \begin{equation}\label{compl}
+ − 2260 @{thm SUBSEQ_complement}
+ − 2261 \end{equation}
+ − 2262
237
+ − 2263 \noindent
247
+ − 2264 holds. Now the first part of Theorem~\ref{subseqreg} is a simple consequence of the second part.
237
+ − 2265
247
+ − 2266 \begin{proof}[Proof of the First Part of Theorem~\ref{subseqreg}]
+ − 2267 By the second part, we know the right-hand side of \eqref{compl}
237
+ − 2268 is regular, which means @{term "- SUBSEQ A"} is regular. But since
233
+ − 2269 we established already that regularity is preserved under complement, also @{term "SUBSEQ A"}
+ − 2270 must be regular.
+ − 2271 \end{proof}
240
+ − 2272
248
+ − 2273 Finally we like to show that the Myhill-Nerode Theorem is also convenient for establishing
245
+ − 2274 the non-regularity of languages. For this we use the following version of the Continuation
240
+ − 2275 Lemma (see for example~\cite{Rosenberg06}).
+ − 2276
+ − 2277 \begin{lmm}[Continuation Lemma]
257
+ − 2278 If a language @{text A} is regular and a set of strings @{text B} is infinite,
240
+ − 2279 then there exist two distinct strings @{text x} and @{text y} in @{text B}
+ − 2280 such that @{term "x \<approx>A y"}.
+ − 2281 \end{lmm}
+ − 2282
+ − 2283 \noindent
248
+ − 2284 This lemma can be easily deduced from the Myhill-Nerode Theorem and the Pigeonhole
240
+ − 2285 Principle: Since @{text A} is regular, there can be only finitely many
245
+ − 2286 equivalence classes. Hence an infinite set must contain
240
+ − 2287 at least two strings that are in the same equivalence class, that is
248
+ − 2288 they need to be related by the Myhill-Nerode Relation.
240
+ − 2289
+ − 2290 Using this lemma, it is straightforward to establish that the language
245
+ − 2291 \mbox{@{text "A \<equiv> \<Union>\<^isub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands
+ − 2292 for the strings consisting of @{text n} times the character a; similarly for
247
+ − 2293 @{text "b\<^isup>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^isub>n a\<^sup>n"}.
240
+ − 2294
+ − 2295 \begin{lmm}
247
+ − 2296 No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}.
240
+ − 2297 \end{lmm}
+ − 2298
+ − 2299 \begin{proof}
252
+ − 2300 After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"},
+ − 2301 the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}.
+ − 2302 That means we have to show that \mbox{@{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"}} leads to
+ − 2303 a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}.
+ − 2304 But since @{term "i \<noteq> j"}, @{text "a\<^sup>j @ b\<^sup>i \<notin> A"}. Therefore @{text "a\<^sup>i"} and @{text "a\<^sup>j"}
254
+ − 2305 cannot be Myhill-Nerode related by @{text "A"}, and we are done.
240
+ − 2306 \end{proof}
+ − 2307
+ − 2308 \noindent
252
+ − 2309 To conclude the proof of non-regularity for the language @{text A}, the
248
+ − 2310 Continuation Lemma and the lemma above lead to a contradiction assuming
+ − 2311 @{text A} is regular. Therefore the language @{text A} is not regular, as we
+ − 2312 wanted to show.
186
+ − 2313 *}
+ − 2314
117
+ − 2315
240
+ − 2316
54
+ − 2317 section {* Conclusion and Related Work *}
+ − 2318
92
+ − 2319 text {*
186
+ − 2320 \noindent
112
+ − 2321 In this paper we took the view that a regular language is one where there
115
+ − 2322 exists a regular expression that matches all of its strings. Regular
145
+ − 2323 expressions can conveniently be defined as a datatype in HOL-based theorem
+ − 2324 provers. For us it was therefore interesting to find out how far we can push
154
+ − 2325 this point of view. We have established in Isabelle/HOL both directions
248
+ − 2326 of the Myhill-Nerode Theorem.
132
+ − 2327 %
167
+ − 2328 \begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
132
+ − 2329 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
167
+ − 2330 \end{thrm}
186
+ − 2331
132
+ − 2332 \noindent
186
+ − 2333 Having formalised this theorem means we pushed our point of view quite
+ − 2334 far. Using this theorem we can obviously prove when a language is \emph{not}
+ − 2335 regular---by establishing that it has infinitely many equivalence classes
248
+ − 2336 generated by the Myhill-Nerode Relation (this is usually the purpose of the
198
+ − 2337 Pumping Lemma \cite{Kozen97}). We can also use it to establish the standard
186
+ − 2338 textbook results about closure properties of regular languages. Interesting
+ − 2339 is the case of closure under complement, because it seems difficult to
+ − 2340 construct a regular expression for the complement language by direct
+ − 2341 means. However the existence of such a regular expression can be easily
248
+ − 2342 proved using the Myhill-Nerode Theorem.
196
+ − 2343
248
+ − 2344 Our insistence on regular expressions for proving the Myhill-Nerode Theorem
+ − 2345 arose from the limitations of HOL, which is the logic underlying the popular theorem provers HOL4,
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2346 HOLlight and Isabelle/HOL. In order to guarantee consistency,
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2347 formalisations in HOL can only extend the logic with definitions that introduce a new concept in
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2348 terms of already existing notions. A convenient definition for automata
197
+ − 2349 (based on graphs) uses a polymorphic type for the state nodes. This allows
199
+ − 2350 us to use the standard operation for disjoint union whenever we need to compose two
198
+ − 2351 automata. Unfortunately, we cannot use such a polymorphic definition
199
+ − 2352 in HOL as part of the definition for regularity of a language (a predicate
248
+ − 2353 over sets of strings). Consider for example the following attempt:
112
+ − 2354
196
+ − 2355 \begin{center}
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2356 @{text "is_regular A \<equiv> \<exists>M(\<alpha>). is_dfa (M) \<and> \<calL>(M) = A"}
196
+ − 2357 \end{center}
116
+ − 2358
196
+ − 2359 \noindent
199
+ − 2360 In this definifion, the definiens is polymorphic in the type of the automata
248
+ − 2361 @{text "M"} (indicated by dependency on the type-variable @{text "\<alpha>"}), but the definiendum
+ − 2362 @{text "is_regular"} is not. Such definitions are excluded from HOL, because
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2363 they can lead easily to inconsistencies (see \cite{PittsHOL4} for a simple
199
+ − 2364 example). Also HOL does not contain type-quantifiers which would allow us to
+ − 2365 get rid of the polymorphism by quantifying over the type-variable @{text
+ − 2366 "\<alpha>"}. Therefore when defining regularity in terms of automata, the only
+ − 2367 natural way out in HOL is to resort to state nodes with an identity, for
+ − 2368 example a natural number. Unfortunatly, the consequence is that we have to
+ − 2369 be careful when combining two automata so that there is no clash between two
+ − 2370 such states. This makes formalisations quite fiddly and rather
+ − 2371 unpleasant. Regular expressions proved much more convenient for reasoning in
+ − 2372 HOL since they can be defined as inductive datatype and a reasoning
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2373 infrastructure comes for free. The definition of regularity in terms of
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2374 regular expressions poses no problem at all for HOL. We showed in this
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2375 paper that they can be used for establishing the central result in regular
248
+ − 2376 language theory---the Myhill-Nerode Theorem.
196
+ − 2377
+ − 2378 While regular expressions are convenient, they have some limitations. One is
+ − 2379 that there seems to be no method of calculating a minimal regular expression
+ − 2380 (for example in terms of length) for a regular language, like there is for
+ − 2381 automata. On the other hand, efficient regular expression matching, without
+ − 2382 using automata, poses no problem \cite{OwensReppyTuron09}. For an
+ − 2383 implementation of a simple regular expression matcher, whose correctness has
+ − 2384 been formally established, we refer the reader to Owens and Slind
245
+ − 2385 \cite{OwensSlind08}. In our opinion, their formalisation is considerably
+ − 2386 slicker than for example the approach to regular expression matching taken
+ − 2387 in \cite{Harper99} and \cite{Yi06}.
116
+ − 2388
196
+ − 2389 Our proof of the first direction is very much inspired by \emph{Brzozowski's
+ − 2390 algebraic method} used to convert a finite automaton to a regular expression
+ − 2391 \cite{Brzozowski64}. The close connection can be seen by considering the
+ − 2392 equivalence classes as the states of the minimal automaton for the regular
201
+ − 2393 language. However there are some subtle differences. Because our equivalence
248
+ − 2394 classes (or correspondingly states) arise from the Myhill-Nerode Relation, the most natural
196
+ − 2395 choice is to characterise each state with the set of strings starting from
+ − 2396 the initial state leading up to that state. Usually, however, the states are
+ − 2397 characterised as the strings starting from that state leading to the
+ − 2398 terminal states. The first choice has consequences about how the initial
+ − 2399 equational system is set up. We have the $\lambda$-term on our `initial
+ − 2400 state', while Brzozowski has it on the terminal states. This means we also
+ − 2401 need to reverse the direction of Arden's Lemma. We have not found anything
249
+ − 2402 in the `pencil-and-paper-reasoning' literature about our way of proving the
+ − 2403 first direction of the Myhill-Nerode Theorem, but it appears to be folklore.
112
+ − 2404
196
+ − 2405 We presented two proofs for the second direction of the Myhill-Nerode
248
+ − 2406 Theorem. One direct proof using tagging-functions and another using partial
198
+ − 2407 derivatives. This part of our work is where our method using regular
+ − 2408 expressions shines, because we can completely side-step the standard
+ − 2409 argument \cite{Kozen97} where automata need to be composed. However, it is
+ − 2410 also the direction where we had to spend most of the `conceptual' time, as
+ − 2411 our first proof based on tagging-functions is new for establishing the
248
+ − 2412 Myhill-Nerode Theorem. All standard proofs of this direction proceed by
198
+ − 2413 arguments over automata.
196
+ − 2414
198
+ − 2415 The indirect proof for the second direction arose from our interest in
245
+ − 2416 Brzozowski's derivatives for regular expression matching. While Brzozowski
+ − 2417 already established that there are only
196
+ − 2418 finitely many dissimilar derivatives for every regular expression, this
199
+ − 2419 result is not as straightforward to formalise in a theorem prover as one
+ − 2420 might wish. The reason is that the set of dissimilar derivatives is not
+ − 2421 defined inductively, but in terms of an ACI-equivalence relation. This
+ − 2422 difficulty prevented for example Krauss and Nipkow to prove termination of
+ − 2423 their equivalence checker for regular expressions
+ − 2424 \cite{KraussNipkow11}. Their checker is based on Brzozowski's derivatives
+ − 2425 and for their argument the lack of a formal proof of termination is not
+ − 2426 crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}). We
+ − 2427 expect that their development simplifies by using partial derivatives,
245
+ − 2428 instead of derivatives, and that the termination of the algorithm can be
+ − 2429 formally established (the main ingredient is
199
+ − 2430 Theorem~\ref{antimirov}). However, since partial derivatives use sets of
+ − 2431 regular expressions, one needs to carefully analyse whether the resulting
+ − 2432 algorithm is still executable. Given the existing infrastructure for
201
+ − 2433 executable sets in Isabelle/HOL \cite{Haftmann09}, it should.
199
+ − 2434
248
+ − 2435 Our formalisation of the Myhill-Nerode Theorem consists of 780 lines of
198
+ − 2436 Isabelle/Isar code for the first direction and 460 for the second (the one
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2437 based on tagging-functions), plus around 300 lines of standard material
199
+ − 2438 about regular languages. The formalisation of derivatives and partial
198
+ − 2439 derivatives shown in Section~\ref{derivatives} consists of 390 lines of
247
+ − 2440 code. The closure properties in Section~\ref{closure} (except Theorem~\ref{subseqreg})
+ − 2441 can be established in
+ − 2442 190 lines of code. The Continuation Lemma and the non-regularity of @{text "a\<^sup>n b\<^sup>n"}
253
+ − 2443 require 70 lines of code.
247
+ − 2444 The algorithm for solving equational systems, which we
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2445 used in the first direction, is conceptually relatively simple. Still the
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2446 use of sets over which the algorithm operates means it is not as easy to
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2447 formalise as one might hope. However, it seems sets cannot be avoided since
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2448 the `input' of the algorithm consists of equivalence classes and we cannot
248
+ − 2449 see how to reformulate the theory so that we can use lists or matrices. Lists would be
200
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2450 much easier to reason about, since we can define functions over them by
204856ef5573
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc
diff
changeset
+ − 2451 recursion. For sets we have to use set-comprehensions, which is slightly
248
+ − 2452 unwieldy. Matrices would allow us to use the slick formalisation by
+ − 2453 Nipkow of the Gauss-Jordan algorithm \cite{Nipkow11}.
172
+ − 2454
199
+ − 2455 While our formalisation might appear large, it should be seen
198
+ − 2456 in the context of the work done by Constable at al \cite{Constable00} who
248
+ − 2457 formalised the Myhill-Nerode Theorem in Nuprl using automata. They write
198
+ − 2458 that their four-member team needed something on the magnitude of 18 months
245
+ − 2459 for their formalisation. It is hard to gauge the size of a
+ − 2460 formalisation in Nurpl, but from what is shown in the Nuprl Math Library
+ − 2461 about their development it seems substantially larger than ours. We attribute
+ − 2462 this to our use of regular expressions, which meant we did not need to `fight'
+ − 2463 the theorem prover.
+ − 2464 Also, Filli\^atre reports that his formalisation in
+ − 2465 Coq of automata theory and Kleene's theorem is ``rather big''
+ − 2466 \cite{Filliatre97}. More recently, Almeida et al reported about another
218
+ − 2467 formalisation of regular languages in Coq \cite{Almeidaetal10}. Their
+ − 2468 main result is the
+ − 2469 correctness of Mirkin's construction of an automaton from a regular
+ − 2470 expression using partial derivatives. This took approximately 10600 lines
245
+ − 2471 of code. In terms of time, the estimate for our formalisation is that we
198
+ − 2472 needed approximately 3 months and this included the time to find our proof
218
+ − 2473 arguments. Unlike Constable et al, who were able to follow the Myhill-Nerode
+ − 2474 proof from \cite{HopcroftUllman69}, we had to find our own arguments. So for us the
245
+ − 2475 formalisation was not the bottleneck. The code of
218
+ − 2476 our formalisation can be found in the Archive of Formal Proofs at
259
+ − 2477 \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}
245
+ − 2478 \cite{myhillnerodeafp11}.\medskip
162
+ − 2479
+ − 2480 \noindent
173
+ − 2481 {\bf Acknowledgements:}
242
+ − 2482 We are grateful for the comments we received from Larry Paulson. Tobias
247
+ − 2483 Nipkow made us aware of the properties in Theorem~\ref{subseqreg} and Tjark
245
+ − 2484 Weber helped us with proving them.
92
+ − 2485 *}
+ − 2486
+ − 2487
24
+ − 2488 (*<*)
+ − 2489 end
+ − 2490 (*>*)