24
+ − 1
(*<*)
+ − 2
theory Paper
94
+ − 3
imports "../Myhill" "LaTeXsugar"
24
+ − 4
begin
39
+ − 5
+ − 6
declare [[show_question_marks = false]]
+ − 7
54
+ − 8
consts
+ − 9
REL :: "(string \<times> string) \<Rightarrow> bool"
66
+ − 10
UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
54
+ − 11
70
+ − 12
abbreviation
+ − 13
"EClass x R \<equiv> R `` {x}"
54
+ − 14
92
+ − 15
abbreviation
+ − 16
"append_rexp2 r_itm r \<equiv> append_rexp r r_itm"
+ − 17
+ − 18
39
+ − 19
notation (latex output)
50
+ − 20
str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
75
+ − 21
str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
50
+ − 22
Seq (infixr "\<cdot>" 100) and
+ − 23
Star ("_\<^bsup>\<star>\<^esup>") and
+ − 24
pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
58
+ − 25
Suc ("_+1" [100] 100) and
54
+ − 26
quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
66
+ − 27
REL ("\<approx>") and
67
+ − 28
UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
82
+ − 29
L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
75
+ − 30
Lam ("\<lambda>'(_')" [100] 100) and
89
+ − 31
Trn ("'(_, _')" [100, 100] 100) and
71
+ − 32
EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
88
+ − 33
transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
92
+ − 34
Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
+ − 35
append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
112
+ − 36
append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
119
+ − 37
uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+ − 38
tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
121
+ − 39
tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+ − 40
tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+ − 41
tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+ − 42
tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
+ − 43
tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
119
+ − 44
lemma meta_eq_app:
+ − 45
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+ − 46
by auto
+ − 47
24
+ − 48
(*>*)
+ − 49
70
+ − 50
24
+ − 51
section {* Introduction *}
+ − 52
+ − 53
text {*
58
+ − 54
Regular languages are an important and well-understood subject in Computer
60
+ − 55
Science, with many beautiful theorems and many useful algorithms. There is a
66
+ − 56
wide range of textbooks on this subject, many of which are aimed at students
115
+ − 57
and contain very detailed `pencil-and-paper' proofs
60
+ − 58
(e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
101
+ − 59
formalising the theorems and by verifying formally the algorithms.
59
+ − 60
66
+ − 61
There is however a problem: the typical approach to regular languages is to
+ − 62
introduce finite automata and then define everything in terms of them. For
+ − 63
example, a regular language is normally defined as one whose strings are
+ − 64
recognised by a finite deterministic automaton. This approach has many
71
+ − 65
benefits. Among them is the fact that it is easy to convince oneself that
66
+ − 66
regular languages are closed under complementation: one just has to exchange
+ − 67
the accepting and non-accepting states in the corresponding automaton to
+ − 68
obtain an automaton for the complement language. The problem, however, lies with
67
+ − 69
formalising such reasoning in a HOL-based theorem prover, in our case
115
+ − 70
Isabelle/HOL. Automata are built up from states and transitions that
82
+ − 71
need to be represented as graphs, matrices or functions, none
+ − 72
of which can be defined as inductive datatype.
66
+ − 73
82
+ − 74
In case of graphs and matrices, this means we have to build our own
+ − 75
reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+ − 76
HOLlight support them with libraries. Even worse, reasoning about graphs and
+ − 77
matrices can be a real hassle in HOL-based theorem provers. Consider for
+ − 78
example the operation of sequencing two automata, say $A_1$ and $A_2$, by
+ − 79
connecting the accepting states of $A_1$ to the initial state of $A_2$:
60
+ − 80
+ − 81
\begin{center}
66
+ − 82
\begin{tabular}{ccc}
+ − 83
\begin{tikzpicture}[scale=0.8]
+ − 84
%\draw[step=2mm] (-1,-1) grid (1,1);
+ − 85
+ − 86
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 87
\draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 88
+ − 89
\node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 90
\node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 91
+ − 92
\node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 93
\node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 94
+ − 95
\node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 96
\node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 97
\node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 98
+ − 99
\draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 100
\draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 101
\end{tikzpicture}
+ − 102
+ − 103
&
+ − 104
+ − 105
\raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+ − 106
+ − 107
&
+ − 108
+ − 109
\begin{tikzpicture}[scale=0.8]
+ − 110
%\draw[step=2mm] (-1,-1) grid (1,1);
+ − 111
+ − 112
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 113
\draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 114
+ − 115
\node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 116
\node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 117
+ − 118
\node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 119
\node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 120
+ − 121
\node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 122
\node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 123
\node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 124
+ − 125
\draw (C) to [very thick, bend left=45] (B);
+ − 126
\draw (D) to [very thick, bend right=45] (B);
+ − 127
+ − 128
\draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 129
\draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 130
\end{tikzpicture}
+ − 131
+ − 132
\end{tabular}
60
+ − 133
\end{center}
+ − 134
+ − 135
\noindent
115
+ − 136
On `paper' we can define the corresponding graph in terms of the disjoint
88
+ − 137
union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
66
+ − 138
union, namely
82
+ − 139
%
+ − 140
\begin{equation}\label{disjointunion}
66
+ − 141
@{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
82
+ − 142
\end{equation}
60
+ − 143
61
+ − 144
\noindent
66
+ − 145
changes the type---the disjoint union is not a set, but a set of pairs.
+ − 146
Using this definition for disjoint unions means we do not have a single type for automata
92
+ − 147
and hence will not be able to state certain properties about \emph{all}
67
+ − 148
automata, since there is no type quantification available in HOL. An
+ − 149
alternative, which provides us with a single type for automata, is to give every
+ − 150
state node an identity, for example a natural
70
+ − 151
number, and then be careful to rename these identities apart whenever
67
+ − 152
connecting two automata. This results in clunky proofs
66
+ − 153
establishing that properties are invariant under renaming. Similarly,
67
+ − 154
connecting two automata represented as matrices results in very adhoc
66
+ − 155
constructions, which are not pleasant to reason about.
+ − 156
82
+ − 157
Functions are much better supported in Isabelle/HOL, but they still lead to similar
88
+ − 158
problems as with graphs. Composing, for example, two non-deterministic automata in parallel
93
+ − 159
requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
101
+ − 160
dismisses for this the option of using identities, because it leads according to
+ − 161
him to ``messy proofs''. He
103
+ − 162
opts for a variant of \eqref{disjointunion} using bit lists, but writes
82
+ − 163
+ − 164
\begin{quote}
93
+ − 165
\it%
+ − 166
\begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
101
+ − 167
`` & All lemmas appear obvious given a picture of the composition of automata\ldots
+ − 168
Yet their proofs require a painful amount of detail.''
+ − 169
\end{tabular}
+ − 170
\end{quote}
+ − 171
+ − 172
\noindent
+ − 173
and
+ − 174
+ − 175
\begin{quote}
+ − 176
\it%
+ − 177
\begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
93
+ − 178
`` & If the reader finds the above treatment in terms of bit lists revoltingly
101
+ − 179
concrete, I cannot disagree. A more abstract approach is clearly desirable.''
93
+ − 180
\end{tabular}
82
+ − 181
\end{quote}
101
+ − 182
+ − 183
82
+ − 184
\noindent
+ − 185
Moreover, it is not so clear how to conveniently impose a finiteness condition
+ − 186
upon functions in order to represent \emph{finite} automata. The best is
92
+ − 187
probably to resort to more advanced reasoning frameworks, such as \emph{locales}
+ − 188
or \emph{type classes},
110
+ − 189
which are \emph{not} avaiable in all HOL-based theorem provers.
82
+ − 190
66
+ − 191
Because of these problems to do with representing automata, there seems
+ − 192
to be no substantial formalisation of automata theory and regular languages
115
+ − 193
carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
+ − 194
the link between regular expressions and automata in
+ − 195
the context of lexing. Berghofer and Reiter \cite{BerghoferReiter09}
+ − 196
formalise automata working over
+ − 197
bit strings in the context of Presburger arithmetic.
114
+ − 198
The only larger formalisations of automata theory
115
+ − 199
are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
58
+ − 200
82
+ − 201
In this paper, we will not attempt to formalise automata theory in
+ − 202
Isabelle/HOL, but take a completely different approach to regular
+ − 203
languages. Instead of defining a regular language as one where there exists
+ − 204
an automaton that recognises all strings of the language, we define a
+ − 205
regular language as:
54
+ − 206
82
+ − 207
\begin{definition}
77
+ − 208
A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
54
+ − 209
strings of @{text "A"}.
+ − 210
\end{definition}
+ − 211
+ − 212
\noindent
110
+ − 213
The reason is that regular expressions, unlike graphs, matrices and functions, can
71
+ − 214
be easily defined as inductive datatype. Consequently a corresponding reasoning
+ − 215
infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
101
+ − 216
of regular expression matching based on derivatives \cite{OwensSlind08} and
+ − 217
with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}.
+ − 218
The purpose of this paper is to
71
+ − 219
show that a central result about regular languages---the Myhill-Nerode theorem---can
+ − 220
be recreated by only using regular expressions. This theorem gives necessary
+ − 221
and sufficient conditions for when a language is regular. As a corollary of this
67
+ − 222
theorem we can easily establish the usual closure properties, including
+ − 223
complementation, for regular languages.\smallskip
61
+ − 224
+ − 225
\noindent
88
+ − 226
{\bf Contributions:}
+ − 227
There is an extensive literature on regular languages.
+ − 228
To our knowledge, our proof of the Myhill-Nerode theorem is the
67
+ − 229
first that is based on regular expressions, only. We prove the part of this theorem
+ − 230
stating that a regular expression has only finitely many partitions using certain
+ − 231
tagging-functions. Again to our best knowledge, these tagging functions have
+ − 232
not been used before to establish the Myhill-Nerode theorem.
24
+ − 233
*}
+ − 234
50
+ − 235
section {* Preliminaries *}
+ − 236
+ − 237
text {*
67
+ − 238
Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
92
+ − 239
being represented by the empty list, written @{term "[]"}. \emph{Languages}
67
+ − 240
are sets of strings. The language containing all strings is written in
71
+ − 241
Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
90
+ − 242
is written @{term "A ;; B"} and a language raised to the power @{text n} is written
93
+ − 243
@{term "A \<up> n"}. They are defined as usual
54
+ − 244
+ − 245
\begin{center}
58
+ − 246
@{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+ − 247
\hspace{7mm}
+ − 248
@{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+ − 249
\hspace{7mm}
+ − 250
@{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
54
+ − 251
\end{center}
+ − 252
+ − 253
\noindent
113
+ − 254
where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
71
+ − 255
is defined as the union over all powers, namely @{thm Star_def}. In the paper
88
+ − 256
we will make use of the following properties of these constructions.
58
+ − 257
71
+ − 258
\begin{proposition}\label{langprops}\mbox{}\\
92
+ − 259
\begin{tabular}{@ {}ll}
+ − 260
(i) & @{thm star_cases} \\
+ − 261
(ii) & @{thm[mode=IfThen] pow_length}\\
+ − 262
(iii) & @{thm seq_Union_left} \\
71
+ − 263
\end{tabular}
+ − 264
\end{proposition}
+ − 265
+ − 266
\noindent
100
+ − 267
In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
113
+ − 268
string; this property states that if @{term "[] \<notin> A"} then the lengths of
100
+ − 269
the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}. We omit
+ − 270
the proofs for these properties, but invite the reader to consult our
123
+ − 271
formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
71
+ − 272
90
+ − 273
The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
+ − 274
equivalence relation @{term REL} is @{term "A // REL"}. We will write
71
+ − 275
@{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
+ − 276
as @{text "{y | y \<approx> x}"}.
+ − 277
+ − 278
51
+ − 279
Central to our proof will be the solution of equational systems
115
+ − 280
involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64},
93
+ − 281
which solves equations of the form @{term "X = A ;; X \<union> B"} provided
115
+ − 282
@{term "[] \<notin> A"}. However we will need the following `reverse'
123
+ − 283
version of Arden's lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
+ − 284
\mbox{@{term "X ;; A"}}).
50
+ − 285
75
+ − 286
\begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
86
+ − 287
If @{thm (prem 1) arden} then
115
+ − 288
@{thm (lhs) arden} if and only if
86
+ − 289
@{thm (rhs) arden}.
50
+ − 290
\end{lemma}
+ − 291
+ − 292
\begin{proof}
86
+ − 293
For the right-to-left direction we assume @{thm (rhs) arden} and show
+ − 294
that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
71
+ − 295
we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
50
+ − 296
which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both
+ − 297
sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
51
+ − 298
is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction.
50
+ − 299
86
+ − 300
For the other direction we assume @{thm (lhs) arden}. By a simple induction
51
+ − 301
on @{text n}, we can establish the property
50
+ − 302
+ − 303
\begin{center}
86
+ − 304
@{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
50
+ − 305
\end{center}
+ − 306
+ − 307
\noindent
+ − 308
Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
71
+ − 309
all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
+ − 310
of @{text "\<star>"}.
51
+ − 311
For the inclusion in the other direction we assume a string @{text s}
86
+ − 312
with length @{text k} is element in @{text X}. Since @{thm (prem 1) arden}
75
+ − 313
we know by Prop.~\ref{langprops}@{text "(ii)"} that
71
+ − 314
@{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
51
+ − 315
(the strings in @{term "X ;; (A \<up> Suc k)"} are all longer).
53
+ − 316
From @{text "(*)"} it follows then that
50
+ − 317
@{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
75
+ − 318
implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
71
+ − 319
this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
50
+ − 320
\end{proof}
67
+ − 321
+ − 322
\noindent
88
+ − 323
Regular expressions are defined as the inductive datatype
67
+ − 324
+ − 325
\begin{center}
+ − 326
@{text r} @{text "::="}
+ − 327
@{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 328
@{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 329
@{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 330
@{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 331
@{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 332
@{term "STAR r"}
+ − 333
\end{center}
+ − 334
+ − 335
\noindent
88
+ − 336
and the language matched by a regular expression is defined as
67
+ − 337
+ − 338
\begin{center}
+ − 339
\begin{tabular}{c@ {\hspace{10mm}}c}
+ − 340
\begin{tabular}{rcl}
+ − 341
@{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
+ − 342
@{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
+ − 343
@{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
+ − 344
\end{tabular}
+ − 345
&
+ − 346
\begin{tabular}{rcl}
+ − 347
@{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 348
@{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 349
@{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 350
@{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 351
@{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+ − 352
@{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+ − 353
\end{tabular}
+ − 354
\end{tabular}
+ − 355
\end{center}
70
+ − 356
100
+ − 357
Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
92
+ − 358
a regular expression that matches all languages of @{text rs}. We only need to know the existence
+ − 359
of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
93
+ − 360
@{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
100
+ − 361
set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
110
+ − 362
%
+ − 363
\begin{equation}\label{uplus}
+ − 364
\mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ − 365
\end{equation}
88
+ − 366
+ − 367
\noindent
90
+ − 368
holds, whereby @{text "\<calL> ` rs"} stands for the
+ − 369
image of the set @{text rs} under function @{text "\<calL>"}.
50
+ − 370
*}
39
+ − 371
100
+ − 372
section {* The Myhill-Nerode Theorem, First Part *}
54
+ − 373
+ − 374
text {*
77
+ − 375
The key definition in the Myhill-Nerode theorem is the
75
+ − 376
\emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
+ − 377
strings are related, provided there is no distinguishing extension in this
117
+ − 378
language. This can be defined as tertiary relation.
75
+ − 379
117
+ − 380
\begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
123
+ − 381
@{text y} are Myhill-Nerode related provided
117
+ − 382
\begin{center}
75
+ − 383
@{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
117
+ − 384
\end{center}
70
+ − 385
\end{definition}
+ − 386
71
+ − 387
\noindent
75
+ − 388
It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+ − 389
partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
108
+ − 390
equivalence classes. To illustrate this quotient construction, let us give a simple
101
+ − 391
example: consider the regular language containing just
92
+ − 392
the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
101
+ − 393
into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
90
+ − 394
as follows
+ − 395
+ − 396
\begin{center}
+ − 397
@{text "X\<^isub>1 = {[]}"}\hspace{5mm}
+ − 398
@{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
+ − 399
@{text "X\<^isub>3 = UNIV - {[], [c]}"}
+ − 400
\end{center}
+ − 401
+ − 402
One direction of the Myhill-Nerode theorem establishes
93
+ − 403
that if there are finitely many equivalence classes, like in the example above, then
+ − 404
the language is regular. In our setting we therefore have to show:
75
+ − 405
+ − 406
\begin{theorem}\label{myhillnerodeone}
96
+ − 407
@{thm[mode=IfThen] Myhill_Nerode1}
75
+ − 408
\end{theorem}
71
+ − 409
75
+ − 410
\noindent
90
+ − 411
To prove this theorem, we first define the set @{term "finals A"} as those equivalence
100
+ − 412
classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
75
+ − 413
%
71
+ − 414
\begin{equation}
70
+ − 415
@{thm finals_def}
71
+ − 416
\end{equation}
+ − 417
+ − 418
\noindent
92
+ − 419
In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
90
+ − 420
It is straightforward to show that in general @{thm lang_is_union_of_finals} and
79
+ − 421
@{thm finals_in_partitions} hold.
75
+ − 422
Therefore if we know that there exists a regular expression for every
100
+ − 423
equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
93
+ − 424
a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
98
+ − 425
that matches every string in @{text A}.
70
+ − 426
75
+ − 427
90
+ − 428
Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
79
+ − 429
regular expression for \emph{every} equivalence class, not just the ones
77
+ − 430
in @{term "finals A"}. We
93
+ − 431
first define the notion of \emph{one-character-transition} between
+ − 432
two equivalence classes
75
+ − 433
%
71
+ − 434
\begin{equation}
+ − 435
@{thm transition_def}
+ − 436
\end{equation}
70
+ − 437
71
+ − 438
\noindent
92
+ − 439
which means that if we concatenate the character @{text c} to the end of all
+ − 440
strings in the equivalence class @{text Y}, we obtain a subset of
77
+ − 441
@{text X}. Note that we do not define an automaton here, we merely relate two sets
110
+ − 442
(with the help of a character). In our concrete example we have
92
+ − 443
@{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any
93
+ − 444
other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
75
+ − 445
110
+ − 446
Next we build an \emph{initial equational system} that
75
+ − 447
contains an equation for each equivalence class. Suppose we have
+ − 448
the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+ − 449
contains the empty string @{text "[]"} (since equivalence classes are disjoint).
77
+ − 450
Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
75
+ − 451
+ − 452
\begin{center}
+ − 453
\begin{tabular}{rcl}
+ − 454
@{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
+ − 455
@{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+ − 456
& $\vdots$ \\
+ − 457
@{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+ − 458
\end{tabular}
+ − 459
\end{center}
70
+ − 460
75
+ − 461
\noindent
100
+ − 462
where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
+ − 463
stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
+ − 464
X\<^isub>i"}. There can only be
110
+ − 465
finitely many such terms in a right-hand side since by assumption there are only finitely many
100
+ − 466
equivalence classes and only finitely many characters. The term @{text
+ − 467
"\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
+ − 468
containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
115
+ − 469
single `initial' state in the equational system, which is different from
100
+ − 470
the method by Brzozowski \cite{Brzozowski64}, where he marks the
115
+ − 471
`terminal' states. We are forced to set up the equational system in our
+ − 472
way, because the Myhill-Nerode relation determines the `direction' of the
123
+ − 473
transitions---the successor `state' of an equivalence class @{text Y} can
+ − 474
be reached by adding a character to the end of @{text Y}. This is also the
100
+ − 475
reason why we have to use our reverse version of Arden's lemma.}
+ − 476
Overloading the function @{text \<calL>} for the two kinds of terms in the
92
+ − 477
equational system, we have
75
+ − 478
+ − 479
\begin{center}
92
+ − 480
@{text "\<calL>(Y, r) \<equiv>"} %
+ − 481
@{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
86
+ − 482
@{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
75
+ − 483
\end{center}
+ − 484
+ − 485
\noindent
100
+ − 486
and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
75
+ − 487
%
+ − 488
\begin{equation}\label{inv1}
83
+ − 489
@{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
75
+ − 490
\end{equation}
+ − 491
+ − 492
\noindent
+ − 493
hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ − 494
%
+ − 495
\begin{equation}\label{inv2}
83
+ − 496
@{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
75
+ − 497
\end{equation}
+ − 498
+ − 499
\noindent
101
+ − 500
The reason for adding the @{text \<lambda>}-marker to our initial equational system is
103
+ − 501
to obtain this equation: it only holds with the marker, since none of
108
+ − 502
the other terms contain the empty string. The point of the initial equational system is
+ − 503
that solving it means we will be able to extract a regular expression for every equivalence class.
100
+ − 504
101
+ − 505
Our representation for the equations in Isabelle/HOL are pairs,
108
+ − 506
where the first component is an equivalence class (a set of strings)
+ − 507
and the second component
101
+ − 508
is a set of terms. Given a set of equivalence
100
+ − 509
classes @{text CS}, our initial equational system @{term "Init CS"} is thus
101
+ − 510
formally defined as
104
+ − 511
%
+ − 512
\begin{equation}\label{initcs}
+ − 513
\mbox{\begin{tabular}{rcl}
100
+ − 514
@{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
+ − 515
@{text "if"}~@{term "[] \<in> X"}\\
+ − 516
& & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
+ − 517
& & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
+ − 518
@{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def}
104
+ − 519
\end{tabular}}
+ − 520
\end{equation}
100
+ − 521
+ − 522
+ − 523
+ − 524
\noindent
+ − 525
Because we use sets of terms
101
+ − 526
for representing the right-hand sides of equations, we can
100
+ − 527
prove \eqref{inv1} and \eqref{inv2} more concisely as
93
+ − 528
%
100
+ − 529
\begin{lemma}\label{inv}
+ − 530
If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
+ − 531
\end{lemma}
77
+ − 532
93
+ − 533
\noindent
92
+ − 534
Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
100
+ − 535
initial equational system into one in \emph{solved form} maintaining the invariant
108
+ − 536
in Lem.~\ref{inv}. From the solved form we will be able to read
89
+ − 537
off the regular expressions.
+ − 538
100
+ − 539
In order to transform an equational system into solved form, we have two
89
+ − 540
operations: one that takes an equation of the form @{text "X = rhs"} and removes
110
+ − 541
any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's
92
+ − 542
Lemma. The other operation takes an equation @{text "X = rhs"}
89
+ − 543
and substitutes @{text X} throughout the rest of the equational system
110
+ − 544
adjusting the remaining regular expressions appropriately. To define this adjustment
108
+ − 545
we define the \emph{append-operation} taking a term and a regular expression as argument
89
+ − 546
+ − 547
\begin{center}
92
+ − 548
@{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+ − 549
@{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
89
+ − 550
\end{center}
+ − 551
92
+ − 552
\noindent
108
+ − 553
We lift this operation to entire right-hand sides of equations, written as
93
+ − 554
@{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
101
+ − 555
the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
110
+ − 556
%
+ − 557
\begin{equation}\label{arden_def}
+ − 558
\mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
94
+ − 559
@{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 560
& & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 561
& & @{text "r' ="} & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+ − 562
& & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
110
+ − 563
\end{tabular}}
+ − 564
\end{equation}
93
+ − 565
+ − 566
\noindent
101
+ − 567
In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
110
+ − 568
then we calculate the combined regular expressions for all @{text r} coming
94
+ − 569
from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+ − 570
finally we append this regular expression to @{text rhs'}. It can be easily seen
110
+ − 571
that this operation mimics Arden's lemma on the level of equations. To ensure
+ − 572
the non-emptiness condition of Arden's lemma we say that a right-hand side is
+ − 573
\emph{ardenable} provided
+ − 574
+ − 575
\begin{center}
+ − 576
@{thm ardenable_def}
+ − 577
\end{center}
+ − 578
+ − 579
\noindent
+ − 580
This allows us to prove
+ − 581
+ − 582
\begin{lemma}\label{ardenable}
113
+ − 583
Given an equation @{text "X = rhs"}.
110
+ − 584
If @{text "X = \<Union>\<calL> ` rhs"},
115
+ − 585
@{thm (prem 2) Arden_keeps_eq}, and
110
+ − 586
@{thm (prem 3) Arden_keeps_eq}, then
+ − 587
@{text "X = \<Union>\<calL> ` (Arden X rhs)"}
+ − 588
\end{lemma}
+ − 589
+ − 590
\noindent
95
+ − 591
The \emph{substituion-operation} takes an equation
+ − 592
of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
94
+ − 593
+ − 594
\begin{center}
95
+ − 595
\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ − 596
@{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 597
& & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 598
& & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
+ − 599
& & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\
+ − 600
\end{tabular}
94
+ − 601
\end{center}
95
+ − 602
+ − 603
\noindent
110
+ − 604
We again delete first all occurrence of @{text "(X, r)"} in @{text rhs}; we then calculate
95
+ − 605
the regular expression corresponding to the deleted terms; finally we append this
+ − 606
regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+ − 607
the substitution operation we will arrange it so that @{text "xrhs"} does not contain
110
+ − 608
any occurrence of @{text X}.
96
+ − 609
100
+ − 610
With these two operation in place, we can define the operation that removes one equation
+ − 611
from an equational systems @{text ES}. The operation @{const Subst_all}
96
+ − 612
substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES};
100
+ − 613
@{const Remove} then completely removes such an equation from @{text ES} by substituting
110
+ − 614
it to the rest of the equational system, but first eliminating all recursive occurrences
96
+ − 615
of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+ − 616
+ − 617
\begin{center}
+ − 618
\begin{tabular}{rcl}
+ − 619
@{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+ − 620
@{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+ − 621
\end{tabular}
+ − 622
\end{center}
100
+ − 623
+ − 624
\noindent
110
+ − 625
Finally, we can define how an equational system should be solved. For this
107
+ − 626
we will need to iterate the process of eliminating equations until only one equation
100
+ − 627
will be left in the system. However, we not just want to have any equation
107
+ − 628
as being the last one, but the one involving the equivalence class for
+ − 629
which we want to calculate the regular
108
+ − 630
expression. Let us suppose this equivalence class is @{text X}.
107
+ − 631
Since @{text X} is the one to be solved, in every iteration step we have to pick an
108
+ − 632
equation to be eliminated that is different from @{text X}. In this way
+ − 633
@{text X} is kept to the final step. The choice is implemented using Hilbert's choice
107
+ − 634
operator, written @{text SOME} in the definition below.
100
+ − 635
+ − 636
\begin{center}
+ − 637
\begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+ − 638
@{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
+ − 639
& & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+ − 640
& & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\
+ − 641
\end{tabular}
+ − 642
\end{center}
+ − 643
+ − 644
\noindent
110
+ − 645
The last definition we need applies @{term Iter} over and over until a condition
+ − 646
@{text Cond} is \emph{not} satisfied anymore. The condition states that there
+ − 647
are more than one equation left in the equational system @{text ES}. To solve
+ − 648
an equational system we use Isabelle/HOL's @{text while}-operator as follows:
101
+ − 649
100
+ − 650
\begin{center}
+ − 651
@{thm Solve_def}
+ − 652
\end{center}
+ − 653
101
+ − 654
\noindent
103
+ − 655
We are not concerned here with the definition of this operator
115
+ − 656
(see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
103
+ − 657
in each @{const Iter}-step a single equation, and therefore
+ − 658
have a well-founded termination order by taking the cardinality
+ − 659
of the equational system @{text ES}. This enables us to prove
115
+ − 660
properties about our definition of @{const Solve} when we `call' it with
104
+ − 661
the equivalence class @{text X} and the initial equational system
+ − 662
@{term "Init (UNIV // \<approx>A)"} from
108
+ − 663
\eqref{initcs} using the principle:
110
+ − 664
%
+ − 665
\begin{equation}\label{whileprinciple}
+ − 666
\mbox{\begin{tabular}{l}
103
+ − 667
@{term "invariant (Init (UNIV // \<approx>A))"} \\
+ − 668
@{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+ − 669
@{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+ − 670
@{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+ − 671
\hline
+ − 672
\multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
110
+ − 673
\end{tabular}}
+ − 674
\end{equation}
103
+ − 675
+ − 676
\noindent
104
+ − 677
This principle states that given an invariant (which we will specify below)
+ − 678
we can prove a property
+ − 679
@{text "P"} involving @{const Solve}. For this we have to discharge the following
+ − 680
proof obligations: first the
113
+ − 681
initial equational system satisfies the invariant; second the iteration
104
+ − 682
step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond} holds;
113
+ − 683
third @{text "Iter"} decreases the termination order, and fourth that
104
+ − 684
once the condition does not hold anymore then the property @{text P} must hold.
103
+ − 685
104
+ − 686
The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
108
+ − 687
returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
104
+ − 688
that this equational system still satisfies the invariant. In order to get
+ − 689
the proof through, the invariant is composed of the following six properties:
103
+ − 690
+ − 691
\begin{center}
104
+ − 692
\begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+ − 693
@{text "invariant ES"} & @{text "\<equiv>"} &
103
+ − 694
@{term "finite ES"} & @{text "(finiteness)"}\\
+ − 695
& @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
104
+ − 696
& @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
+ − 697
& @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
+ − 698
& & & @{text "(distinctness)"}\\
110
+ − 699
& @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
104
+ − 700
& @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
103
+ − 701
\end{tabular}
+ − 702
\end{center}
+ − 703
104
+ − 704
\noindent
+ − 705
The first two ensure that the equational system is always finite (number of equations
115
+ − 706
and number of terms in each equation); the second makes sure the `meaning' of the
108
+ − 707
equations is preserved under our transformations. The other properties are a bit more
+ − 708
technical, but are needed to get our proof through. Distinctness states that every
110
+ − 709
equation in the system is distinct. Ardenable ensures that we can always
+ − 710
apply the arden operation.
108
+ − 711
The last property states that every @{text rhs} can only contain equivalence classes
+ − 712
for which there is an equation. Therefore @{text lhss} is just the set containing
+ − 713
the first components of an equational system,
+ − 714
while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
123
+ − 715
form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
110
+ − 716
and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
108
+ − 717
104
+ − 718
110
+ − 719
It is straightforward to prove that the initial equational system satisfies the
105
+ − 720
invariant.
+ − 721
110
+ − 722
\begin{lemma}\label{invzero}
104
+ − 723
@{thm[mode=IfThen] Init_ES_satisfies_invariant}
+ − 724
\end{lemma}
+ − 725
105
+ − 726
\begin{proof}
+ − 727
Finiteness is given by the assumption and the way how we set up the
+ − 728
initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
+ − 729
follows from the fact that the equivalence classes are disjoint. The ardenable
113
+ − 730
property also follows from the setup of the initial equational system, as does
105
+ − 731
validity.\qed
+ − 732
\end{proof}
+ − 733
113
+ − 734
\noindent
+ − 735
Next we show that @{text Iter} preserves the invariant.
+ − 736
110
+ − 737
\begin{lemma}\label{iterone}
104
+ − 738
@{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
+ − 739
\end{lemma}
+ − 740
107
+ − 741
\begin{proof}
110
+ − 742
This boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
+ − 743
and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
+ − 744
preserves the invariant.
+ − 745
We prove this as follows:
+ − 746
+ − 747
\begin{center}
+ − 748
@{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+ − 749
@{thm (concl) Subst_all_satisfies_invariant}
+ − 750
\end{center}
+ − 751
+ − 752
\noindent
+ − 753
Finiteness is straightforward, as @{const Subst} and @{const Arden} operations
116
+ − 754
keep the equational system finite. These operations also preserve soundness
113
+ − 755
and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
+ − 756
The property ardenable is clearly preserved because the append-operation
110
+ − 757
cannot make a regular expression to match the empty string. Validity is
+ − 758
given because @{const Arden} removes an equivalence class from @{text yrhs}
+ − 759
and then @{const Subst_all} removes @{text Y} from the equational system.
+ − 760
Having proved the implication above, we can replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+ − 761
which matches with our proof-obligation of @{const "Subst_all"}. Since
+ − 762
\mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use our assumption
+ − 763
to complete the proof.\qed
107
+ − 764
\end{proof}
+ − 765
113
+ − 766
\noindent
+ − 767
We also need the fact that @{text Iter} decreases the termination measure.
+ − 768
110
+ − 769
\begin{lemma}\label{itertwo}
104
+ − 770
@{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
+ − 771
\end{lemma}
+ − 772
105
+ − 773
\begin{proof}
+ − 774
By assumption we know that @{text "ES"} is finite and has more than one element.
+ − 775
Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
110
+ − 776
@{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
105
+ − 777
that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+ − 778
removes the equation @{text "Y = yrhs"} from the system, and therefore
+ − 779
the cardinality of @{const Iter} strictly decreases.\qed
+ − 780
\end{proof}
+ − 781
113
+ − 782
\noindent
+ − 783
This brings us to our property we want establish for @{text Solve}.
+ − 784
+ − 785
104
+ − 786
\begin{lemma}
+ − 787
If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+ − 788
a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+ − 789
and @{term "invariant {(X, rhs)}"}.
+ − 790
\end{lemma}
+ − 791
107
+ − 792
\begin{proof}
110
+ − 793
In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+ − 794
stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
+ − 795
that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ − 796
in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
113
+ − 797
Therefore our invariant cannot be just @{term "invariant ES"}, but must be
110
+ − 798
@{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
+ − 799
@{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+ − 800
the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+ − 801
Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+ − 802
modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+ − 803
Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+ − 804
we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ − 805
and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
113
+ − 806
does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
110
+ − 807
with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
123
+ − 808
of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
110
+ − 809
for which the invariant holds. This allows us to conclude that
113
+ − 810
@{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
+ − 811
as needed.\qed
107
+ − 812
\end{proof}
+ − 813
106
+ − 814
\noindent
+ − 815
With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+ − 816
there exists a regular expression.
+ − 817
105
+ − 818
\begin{lemma}\label{every_eqcl_has_reg}
+ − 819
@{thm[mode=IfThen] every_eqcl_has_reg}
+ − 820
\end{lemma}
+ − 821
+ − 822
\begin{proof}
+ − 823
By the preceeding Lemma, we know that there exists a @{text "rhs"} such
+ − 824
that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+ − 825
and that the invariant holds for this equation. That means we
+ − 826
know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
109
+ − 827
this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
123
+ − 828
invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
106
+ − 829
we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
+ − 830
removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
113
+ − 831
This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
106
+ − 832
So we can collect those (finitely many) regular expressions and have @{term "X = L (\<Uplus>rs)"}.
+ − 833
With this we can conclude the proof.\qed
105
+ − 834
\end{proof}
+ − 835
106
+ − 836
\noindent
+ − 837
Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
+ − 838
of the Myhill-Nerode theorem.
105
+ − 839
106
+ − 840
\begin{proof}[of Thm.~\ref{myhillnerodeone}]
123
+ − 841
By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
105
+ − 842
every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
110
+ − 843
a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
123
+ − 844
in @{term "finals A"} there exists a regular expression. Moreover by assumption
106
+ − 845
we know that @{term "finals A"} must be finite, and therefore there must be a finite
105
+ − 846
set of regular expressions @{text "rs"} such that
+ − 847
+ − 848
\begin{center}
+ − 849
@{term "\<Union>(finals A) = L (\<Uplus>rs)"}
+ − 850
\end{center}
+ − 851
+ − 852
\noindent
+ − 853
Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
107
+ − 854
as the regular expression that is needed in the theorem.\qed
105
+ − 855
\end{proof}
54
+ − 856
*}
+ − 857
100
+ − 858
+ − 859
+ − 860
+ − 861
section {* Myhill-Nerode, Second Part *}
39
+ − 862
+ − 863
text {*
116
+ − 864
We will prove in this section the second part of the Myhill-Nerode
+ − 865
theorem. It can be formulated in our setting as follows.
39
+ − 866
54
+ − 867
\begin{theorem}
112
+ − 868
Given @{text "r"} is a regular expressions, then @{thm Myhill_Nerode2}.
54
+ − 869
\end{theorem}
39
+ − 870
116
+ − 871
\noindent
+ − 872
The proof will be by induction on the structure of @{text r}. It turns out
+ − 873
the base cases are straightforward.
+ − 874
+ − 875
+ − 876
\begin{proof}[Base Cases]
+ − 877
The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because
+ − 878
we can easily establish
39
+ − 879
114
+ − 880
\begin{center}
+ − 881
\begin{tabular}{l}
+ − 882
@{thm quot_null_eq}\\
+ − 883
@{thm quot_empty_subset}\\
+ − 884
@{thm quot_char_subset}
+ − 885
\end{tabular}
+ − 886
\end{center}
+ − 887
116
+ − 888
\noindent
+ − 889
hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
114
+ − 890
\end{proof}
109
+ − 891
116
+ − 892
\noindent
117
+ − 893
Much more interesting, however, are the inductive cases. They seem hard to be solved
+ − 894
directly. The reader is invited to try.
+ − 895
+ − 896
Our method will rely on some
118
+ − 897
\emph{tagging functions} defined over strings. Given the inductive hypothesis, it will
119
+ − 898
be easy to prove that the range of these tagging functions is finite
+ − 899
(the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
123
+ − 900
With this we will be able to infer that the tagging functions, seen as relations,
117
+ − 901
give rise to finitely many equivalence classes of @{const UNIV}. Finally we
+ − 902
will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which
123
+ − 903
implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"}
+ − 904
is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
+ − 905
We formally define the notion of a \emph{tagging-relation} as follows.
117
+ − 906
123
+ − 907
\begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
119
+ − 908
and @{text y} are \emph{tag-related} provided
117
+ − 909
\begin{center}
+ − 910
@{text "x =tag= y \<equiv> tag x = tag y"}
+ − 911
\end{center}
+ − 912
\end{definition}
+ − 913
118
+ − 914
\noindent
123
+ − 915
In order to establish finiteness of a set @{text A}, we shall use the following powerful
118
+ − 916
principle from Isabelle/HOL's library.
+ − 917
%
+ − 918
\begin{equation}\label{finiteimageD}
+ − 919
@{thm[mode=IfThen] finite_imageD}
+ − 920
\end{equation}
+ − 921
+ − 922
\noindent
123
+ − 923
It states that if an image of a set under an injective function @{text f} (injective over this set)
118
+ − 924
is finite, then @{text A} itself must be finite. We can use it to establish the following
+ − 925
two lemmas.
+ − 926
117
+ − 927
\begin{lemma}\label{finone}
+ − 928
@{thm[mode=IfThen] finite_eq_tag_rel}
+ − 929
\end{lemma}
+ − 930
+ − 931
\begin{proof}
119
+ − 932
We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
123
+ − 933
@{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
119
+ − 934
finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+ − 935
and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+ − 936
assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
123
+ − 937
From the assumption we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with
+ − 938
@{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
+ − 939
turn means that the equivalence classes @{text X}
119
+ − 940
and @{text Y} must be equal.\qed
117
+ − 941
\end{proof}
+ − 942
+ − 943
\begin{lemma}\label{fintwo}
123
+ − 944
Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
118
+ − 945
@{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+ − 946
If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+ − 947
then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
117
+ − 948
\end{lemma}
+ − 949
+ − 950
\begin{proof}
123
+ − 951
We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
118
+ − 952
be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
+ − 953
@{text "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{text "Pow (UNIV // R\<^isub>1)"},
+ − 954
which is finite by assumption. What remains to be shown is that @{text f} is injective
+ − 955
on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
+ − 956
classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+ − 957
@{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+ − 958
@{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
+ − 959
We know there exists a @{text x} with @{term "X = R\<^isub>2 `` {x}"}
+ − 960
and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
123
+ − 961
and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+ − 962
such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
118
+ − 963
are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
+ − 964
they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
117
+ − 965
\end{proof}
+ − 966
+ − 967
\noindent
119
+ − 968
Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
117
+ − 969
that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose
119
+ − 970
range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
123
+ − 971
Let us attempt the @{const ALT}-case first.
119
+ − 972
+ − 973
\begin{proof}[@{const "ALT"}-Case]
+ − 974
We take as tagging function
+ − 975
+ − 976
\begin{center}
+ − 977
@{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+ − 978
\end{center}
117
+ − 979
119
+ − 980
\noindent
+ − 981
where @{text "A"} and @{text "B"} are some arbitrary languages.
+ − 982
We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ − 983
then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
123
+ − 984
@{term "tag_str_ALT A B"} is a subset of this product set, so finite. It remains to be shown
120
+ − 985
that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
+ − 986
showing
+ − 987
%
+ − 988
\begin{center}
+ − 989
@{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+ − 990
\end{center}
109
+ − 991
120
+ − 992
\noindent
+ − 993
which by unfolding the Myhill-Nerode relation is identical to
+ − 994
%
+ − 995
\begin{equation}\label{pattern}
+ − 996
@{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
+ − 997
\end{equation}
+ − 998
+ − 999
\noindent
+ − 1000
since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
123
+ − 1001
\eqref{pattern} we just have to unfold the definition of the tagging-relation and analyse
+ − 1002
in which set, @{text A} or @{text B}, the string @{term "x @ z"} is.
+ − 1003
The definition of the tagging-function will give us in each case the
+ − 1004
information to infer that @{text "y @ z \<in> A \<union> B"}.
+ − 1005
Finally we
120
+ − 1006
can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
119
+ − 1007
\end{proof}
+ − 1008
109
+ − 1009
121
+ − 1010
\noindent
+ − 1011
The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
123
+ − 1012
they are slightly more complicated. In the @{const SEQ}-case we essentially have
+ − 1013
to be able to infer that
+ − 1014
+ − 1015
\begin{center}
+ − 1016
@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+ − 1017
\end{center}
+ − 1018
+ − 1019
\noindent
+ − 1020
using the information given by the appropriate tagging function. The complication
124
+ − 1021
is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
+ − 1022
(this was easy in case of @{term "A \<union> B"}). For this we define the
+ − 1023
notions of \emph{string prefixes}
+ − 1024
+ − 1025
\begin{center}
+ − 1026
@{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+ − 1027
@{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+ − 1028
\end{center}
121
+ − 1029
124
+ − 1030
\noindent
+ − 1031
and \emph{string subtraction}:
+ − 1032
+ − 1033
\begin{center}
+ − 1034
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ − 1035
@{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
+ − 1036
@{text "x - []"} & @{text "\<equiv>"} & @{text x}\\
+ − 1037
@{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\
+ − 1038
\end{tabular}
+ − 1039
\end{center}
+ − 1040
+ − 1041
\noindent
+ − 1042
where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
125
+ − 1043
Now assuming @{term "x @ z \<in> A ;; B"} there are only two possible ways how this string
126
+ − 1044
can be `distributed' over @{term "A ;; B"}:
121
+ − 1045
125
+ − 1046
\begin{center}
+ − 1047
\scalebox{0.7}{
+ − 1048
\begin{tikzpicture}
+ − 1049
\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}x'\hspace{4em}$ };
+ − 1050
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - x'\hspace{0.5em}$ };
+ − 1051
\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}z\hspace{10.1em}$ };
+ − 1052
+ − 1053
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1054
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ − 1055
node[midway, above=0.5em]{$x$};
+ − 1056
+ − 1057
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1058
(z.north west) -- ($(z.north east)+(0em,0em)$)
+ − 1059
node[midway, above=0.5em]{$z$};
+ − 1060
+ − 1061
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1062
($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ − 1063
node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+ − 1064
+ − 1065
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1066
($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ − 1067
node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
+ − 1068
+ − 1069
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1070
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ − 1071
node[midway, below=0.5em]{@{term "x' \<in> A"}};
+ − 1072
\end{tikzpicture}}
+ − 1073
+ − 1074
\scalebox{0.7}{
+ − 1075
\begin{tikzpicture}
+ − 1076
\node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ };
+ − 1077
\node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}z'\hspace{2em}$ };
+ − 1078
\node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - z'\hspace{6.1em}$ };
+ − 1079
+ − 1080
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1081
(x.north west) -- ($(za.north west)+(0em,0em)$)
+ − 1082
node[midway, above=0.5em]{$x$};
+ − 1083
+ − 1084
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1085
($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+ − 1086
node[midway, above=0.8em]{$z$};
+ − 1087
+ − 1088
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1089
($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+ − 1090
node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+ − 1091
+ − 1092
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1093
($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+ − 1094
node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
+ − 1095
+ − 1096
\draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1097
($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+ − 1098
node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
+ − 1099
\end{tikzpicture}}
+ − 1100
\end{center}
+ − 1101
+ − 1102
\noindent
+ − 1103
Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
+ − 1104
or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
126
+ − 1105
In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the
125
+ − 1106
following tagging-function
121
+ − 1107
+ − 1108
\begin{center}
+ − 1109
@{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+ − 1110
\end{center}
125
+ − 1111
+ − 1112
\noindent
+ − 1113
with the idea ???
+ − 1114
+ − 1115
\begin{proof}[@{const SEQ}-Case]
+ − 1116
+ − 1117
121
+ − 1118
\end{proof}
+ − 1119
+ − 1120
\begin{proof}[@{const STAR}-Case]
+ − 1121
+ − 1122
\begin{center}
+ − 1123
@{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
+ − 1124
\end{center}
+ − 1125
\end{proof}
39
+ − 1126
*}
+ − 1127
+ − 1128
117
+ − 1129
54
+ − 1130
section {* Conclusion and Related Work *}
+ − 1131
92
+ − 1132
text {*
112
+ − 1133
In this paper we took the view that a regular language is one where there
115
+ − 1134
exists a regular expression that matches all of its strings. Regular
+ − 1135
expressions can conveniently be defined as a datatype in a HOL-based theorem
112
+ − 1136
prover. For us it was therefore interesting to find out how far we can push
+ − 1137
this point of view.
+ − 1138
+ − 1139
Having formalised the Myhill-Nerode theorem means we
+ − 1140
pushed quite far. Using this theorem we can obviously prove when a language
+ − 1141
is \emph{not} regular---by establishing that it has infinitely many
+ − 1142
equivalence classes generated by the Myhill-Nerode relation (this is usually
+ − 1143
the purpose of the pumping lemma \cite{Kozen97}). We can also use it to
+ − 1144
establish the standard textbook results about closure properties of regular
+ − 1145
languages. Interesting is the case of closure under complement, because
+ − 1146
it seems difficult to construct a regular expression for the complement
113
+ − 1147
language by direct means. However the existence of such a regular expression
+ − 1148
can be easily proved using the Myhill-Nerode theorem since
92
+ − 1149
112
+ − 1150
\begin{center}
+ − 1151
@{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+ − 1152
\end{center}
+ − 1153
+ − 1154
\noindent
+ − 1155
holds for any strings @{text "s\<^isub>1"} and @{text
114
+ − 1156
"s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
+ − 1157
partitions. Proving the existence of such a regular expression via automata would
+ − 1158
be quite involved. It includes the
112
+ − 1159
steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
+ − 1160
"\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
+ − 1161
regular expression.
+ − 1162
116
+ − 1163
While regular expressions are convenient in formalisations, they have some
122
+ − 1164
limitations. One is that there seems to be no method of calculating a
123
+ − 1165
minimal regular expression (for example in terms of length) for a regular
+ − 1166
language, like there is
+ − 1167
for automata. On the other hand, efficient regular expression matching,
+ − 1168
without using automata, poses no problem \cite{OwensReppyTuron09}.
+ − 1169
For an implementation of a simple regular expression matcher,
122
+ − 1170
whose correctness has been formally established, we refer the reader to
+ − 1171
Owens and Slind \cite{OwensSlind08}.
116
+ − 1172
+ − 1173
121
+ − 1174
Our formalisation consists of 790 lines of Isabelle/Isar code for the first
123
+ − 1175
direction and 475 for the second, plus around 300 lines of standard material about
122
+ − 1176
regular languages. While this might be seen as too large to count as a
+ − 1177
concise proof pearl, this should be seen in the context of the work done by
+ − 1178
Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
+ − 1179
in Nuprl using automata. They write that their four-member team needed
+ − 1180
something on the magnitute of 18 months for their formalisation. The
+ − 1181
estimate for our formalisation is that we needed approximately 3 months and
+ − 1182
this included the time to find our proof arguments. Unlike Constable et al,
+ − 1183
who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
+ − 1184
find our own arguments. So for us the formalisation was not the
+ − 1185
bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
+ − 1186
from what is shown in the Nuprl Math Library about their development it
+ − 1187
seems substantially larger than ours. The code of ours can be found in the
+ − 1188
Mercurial Repository at
113
+ − 1189
+ − 1190
\begin{center}
123
+ − 1191
\url{http://www4.in.tum.de/~urbanc/regexp.html}
113
+ − 1192
\end{center}
+ − 1193
112
+ − 1194
+ − 1195
Our proof of the first direction is very much inspired by \emph{Brzozowski's
+ − 1196
algebraic mehod} used to convert a finite automaton to a regular
113
+ − 1197
expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
111
+ − 1198
classes as the states of the minimal automaton for the regular language.
114
+ − 1199
However there are some subtle differences. Since we identify equivalence
111
+ − 1200
classes with the states of the automaton, then the most natural choice is to
+ − 1201
characterise each state with the set of strings starting from the initial
113
+ − 1202
state leading up to that state. Usually, however, the states are characterised as the
123
+ − 1203
strings starting from that state leading to the terminal states. The first
+ − 1204
choice has consequences about how the initial equational system is set up. We have
115
+ − 1205
the $\lambda$-term on our `initial state', while Brzozowski has it on the
111
+ − 1206
terminal states. This means we also need to reverse the direction of Arden's
+ − 1207
lemma.
92
+ − 1208
112
+ − 1209
We briefly considered using the method Brzozowski presented in the Appendix
113
+ − 1210
of~\cite{Brzozowski64} in order to prove the second direction of the
112
+ − 1211
Myhill-Nerode theorem. There he calculates the derivatives for regular
+ − 1212
expressions and shows that there can be only finitely many of them. We could
114
+ − 1213
have used as the tag of a string @{text s} the derivative of a regular expression
112
+ − 1214
generated with respect to @{text s}. Using the fact that two strings are
123
+ − 1215
Myhill-Nerode related whenever their derivative is the same, together with
112
+ − 1216
the fact that there are only finitely many derivatives for a regular
122
+ − 1217
expression would give us a similar argument as ours. However it seems not so easy to
112
+ − 1218
calculate the derivatives and then to count them. Therefore we preferred our
123
+ − 1219
direct method of using tagging-functions. This
112
+ − 1220
is also where our method shines, because we can completely side-step the
+ − 1221
standard argument \cite{Kozen97} where automata need to be composed, which
113
+ − 1222
as stated in the Introduction is not so convenient to formalise in a
121
+ − 1223
HOL-based theorem prover. However, it is also the direction where we had to
123
+ − 1224
spend most of the `conceptual' time, as our proof-argument based on tagging-functions
+ − 1225
is new for establishing the Myhill-Nerode theorem. All standard proofs
+ − 1226
of this direction proceed by arguments over automata.
111
+ − 1227
92
+ − 1228
*}
+ − 1229
+ − 1230
24
+ − 1231
(*<*)
+ − 1232
end
+ − 1233
(*>*)