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