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