24
+ − 1 (*<*)
+ − 2 theory Paper
172
+ − 3 imports "../Closures"
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"
175
+ − 37 abbreviation "TIMESS \<equiv> Times_set"
172
+ − 38 abbreviation "STAR \<equiv> Star"
+ − 39
+ − 40
39
+ − 41 notation (latex output)
50
+ − 42 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
75
+ − 43 str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
172
+ − 44 conc (infixr "\<cdot>" 100) and
+ − 45 star ("_\<^bsup>\<star>\<^esup>") 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
172
+ − 51 lang ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
174
+ − 52 lang_trm ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
75
+ − 53 Lam ("\<lambda>'(_')" [100] 100) and
89
+ − 54 Trn ("'(_, _')" [100, 100] 100) and
71
+ − 55 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
88
+ − 56 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
92
+ − 57 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
162
+ − 58 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+ − 59 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
172
+ − 60
119
+ − 61 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
174
+ − 62 tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
+ − 63 tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
172
+ − 64 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+ − 65 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+ − 66 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
174
+ − 67 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
+ − 68 tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
+ − 69 Delta ("\<Delta>'(_')") and
+ − 70 nullable ("\<delta>'(_')")
167
+ − 71
119
+ − 72 lemma meta_eq_app:
+ − 73 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+ − 74 by auto
+ − 75
172
+ − 76 lemma conc_def':
+ − 77 "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}"
+ − 78 unfolding conc_def by simp
+ − 79
+ − 80 lemma conc_Union_left:
+ − 81 shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))"
+ − 82 unfolding conc_def by auto
+ − 83
+ − 84 lemma test:
+ − 85 assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
+ − 86 shows "X = \<Union> (lang_trm ` rhs)"
+ − 87 using assms l_eq_r_in_eqs by (simp)
+ − 88
+ − 89
167
+ − 90 (* THEOREMS *)
+ − 91
+ − 92 notation (Rule output)
+ − 93 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ − 94
+ − 95 syntax (Rule output)
+ − 96 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 97 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+ − 98
+ − 99 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ − 100 ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+ − 101
+ − 102 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ − 103
+ − 104 notation (Axiom output)
+ − 105 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+ − 106
+ − 107 notation (IfThen output)
+ − 108 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 109 syntax (IfThen output)
+ − 110 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 111 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 112 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ − 113 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ − 114
+ − 115 notation (IfThenNoBox output)
+ − 116 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 117 syntax (IfThenNoBox output)
+ − 118 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 119 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 120 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ − 121 "_asm" :: "prop \<Rightarrow> asms" ("_")
+ − 122
+ − 123
24
+ − 124 (*>*)
+ − 125
70
+ − 126
24
+ − 127 section {* Introduction *}
+ − 128
+ − 129 text {*
167
+ − 130 \noindent
58
+ − 131 Regular languages are an important and well-understood subject in Computer
60
+ − 132 Science, with many beautiful theorems and many useful algorithms. There is a
66
+ − 133 wide range of textbooks on this subject, many of which are aimed at students
175
+ − 134 and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97,
+ − 135 HopcroftUllman69}). It seems natural to exercise theorem provers by
172
+ − 136 formalising the theorems and by verifying formally the algorithms. A
+ − 137 popular choice for a theorem prover would be one based on Higher-Order Logic
175
+ − 138 (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
+ − 139 presented in this paper we will use the latter. HOL is a predicate calculus
+ − 140 that allows quantification over predicate variables. Its type system is
+ − 141 based on Church's Simple Theory of Types \cite{Church40}. Although
+ − 142 many mathematical concepts can be conveniently expressed in HOL, there are some
+ − 143 limitations that hurt badly, if one attempts a simple-minded formalisation
+ − 144 of regular languages in it.
+ − 145
+ − 146 The typical approach to regular languages is to introduce finite automata
+ − 147 and then define everything in terms of them \cite{Kozen97}. For example,
+ − 148 a regular language is normally defined as:
59
+ − 149
175
+ − 150 \begin{dfntn}\label{baddef}
+ − 151 A language @{text A} is \emph{regular}, provided there is a
+ − 152 finite deterministic automaton that recognises all strings of @{text "A"}.
+ − 153 \end{dfntn}
+ − 154
+ − 155 \noindent
+ − 156 This approach has many benefits. Among them is the fact that it is easy to
+ − 157 convince oneself that regular languages are closed under complementation:
+ − 158 one just has to exchange the accepting and non-accepting states in the
+ − 159 corresponding automaton to obtain an automaton for the complement language.
+ − 160 The problem, however, lies with formalising such reasoning in a HOL-based
+ − 161 theorem prover. Automata are built up from states and transitions that need
+ − 162 to be represented as graphs, matrices or functions, none of which can be
+ − 163 defined as an inductive datatype.
66
+ − 164
82
+ − 165 In case of graphs and matrices, this means we have to build our own
+ − 166 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+ − 167 HOLlight support them with libraries. Even worse, reasoning about graphs and
172
+ − 168 matrices can be a real hassle in HOL-based theorem provers, because
+ − 169 we have to be able to combine automata. Consider for
82
+ − 170 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
167
+ − 171 connecting the accepting states of $A_1$ to the initial state of $A_2$:
159
+ − 172 %
172
+ − 173
60
+ − 174 \begin{center}
66
+ − 175 \begin{tabular}{ccc}
172
+ − 176 \begin{tikzpicture}[scale=0.9]
66
+ − 177 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 178
+ − 179 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 180 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 181
+ − 182 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 183 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 184
+ − 185 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 186 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 187
+ − 188 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 189 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 190 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 191
+ − 192 \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 193 \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 194 \end{tikzpicture}
+ − 195
+ − 196 &
+ − 197
+ − 198 \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+ − 199
+ − 200 &
+ − 201
172
+ − 202 \begin{tikzpicture}[scale=0.9]
66
+ − 203 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 204
+ − 205 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 206 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 207
+ − 208 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 209 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 210
+ − 211 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 212 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 213
+ − 214 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 215 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 216 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 217
+ − 218 \draw (C) to [very thick, bend left=45] (B);
+ − 219 \draw (D) to [very thick, bend right=45] (B);
+ − 220
+ − 221 \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 222 \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 223 \end{tikzpicture}
+ − 224
+ − 225 \end{tabular}
60
+ − 226 \end{center}
+ − 227
+ − 228 \noindent
172
+ − 229 On `paper' or a theorem prover based on set-theory, we can define the corresponding
+ − 230 graph in terms of the disjoint
88
+ − 231 union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
66
+ − 232 union, namely
82
+ − 233 %
+ − 234 \begin{equation}\label{disjointunion}
172
+ − 235 @{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
+ − 236 \end{equation}
60
+ − 237
61
+ − 238 \noindent
173
+ − 239 changes the type---the disjoint union is not a set, but a set of
+ − 240 pairs. Using this definition for disjoint union means we do not have a
+ − 241 single type for automata. As a result we will not be able to define a regular
+ − 242 language as one for which there exists an automaton that recognises all its
175
+ − 243 strings. This is because we cannot make a definition in HOL that is polymorphic in
+ − 244 the state type and also there is no type quantification available in HOL (unlike
+ − 245 in Coq, for example).
172
+ − 246
+ − 247 An alternative, which provides us with a single type for automata, is to give every
67
+ − 248 state node an identity, for example a natural
70
+ − 249 number, and then be careful to rename these identities apart whenever
67
+ − 250 connecting two automata. This results in clunky proofs
66
+ − 251 establishing that properties are invariant under renaming. Similarly,
67
+ − 252 connecting two automata represented as matrices results in very adhoc
66
+ − 253 constructions, which are not pleasant to reason about.
+ − 254
82
+ − 255 Functions are much better supported in Isabelle/HOL, but they still lead to similar
88
+ − 256 problems as with graphs. Composing, for example, two non-deterministic automata in parallel
93
+ − 257 requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
101
+ − 258 dismisses for this the option of using identities, because it leads according to
+ − 259 him to ``messy proofs''. He
103
+ − 260 opts for a variant of \eqref{disjointunion} using bit lists, but writes
82
+ − 261
+ − 262 \begin{quote}
93
+ − 263 \it%
+ − 264 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
101
+ − 265 `` & All lemmas appear obvious given a picture of the composition of automata\ldots
+ − 266 Yet their proofs require a painful amount of detail.''
+ − 267 \end{tabular}
+ − 268 \end{quote}
+ − 269
+ − 270 \noindent
+ − 271 and
+ − 272
+ − 273 \begin{quote}
+ − 274 \it%
+ − 275 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
93
+ − 276 `` & If the reader finds the above treatment in terms of bit lists revoltingly
101
+ − 277 concrete, I cannot disagree. A more abstract approach is clearly desirable.''
93
+ − 278 \end{tabular}
82
+ − 279 \end{quote}
101
+ − 280
+ − 281
82
+ − 282 \noindent
172
+ − 283 Moreover, it is not so clear how to conveniently impose a finiteness
+ − 284 condition upon functions in order to represent \emph{finite} automata. The
+ − 285 best is probably to resort to more advanced reasoning frameworks, such as
+ − 286 \emph{locales} or \emph{type classes}, which are \emph{not} available in all
+ − 287 HOL-based theorem provers.
82
+ − 288
172
+ − 289 Because of these problems to do with representing automata, there seems to
+ − 290 be no substantial formalisation of automata theory and regular languages
+ − 291 carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
+ − 292 the link between regular expressions and automata in the context of
+ − 293 lexing. Berghofer and Reiter \cite{BerghoferReiter09} formalise automata
+ − 294 working over bit strings in the context of Presburger arithmetic. The only
+ − 295 larger formalisations of automata theory are carried out in Nuprl
+ − 296 \cite{Constable00} and in Coq \cite{Filliatre97}.
162
+ − 297
175
+ − 298 Also one might consider automata theory as well-worn stock material where
+ − 299 everything is crystal clear. However, paper proofs about automata often
+ − 300 involve subtle side-conditions which are easily overlooked, but which make
+ − 301 formal reasoning rather painful. For example Kozen's proof of the
+ − 302 Myhill-Nerode theorem requires that the automata do not have inaccessible
+ − 303 states \cite{Kozen97}. Another subtle side-condition is completeness of
+ − 304 automata: automata need to have total transition functions and at most one
+ − 305 `sink' state from which there is no connection to a final state (Brozowski
+ − 306 mentions this side-condition in connection with state complexity
173
+ − 307 \cite{Brozowski10}). Such side-conditions mean that if we define a regular
175
+ − 308 language as one for which there exists \emph{a} finite automaton that
+ − 309 recognises all its strings (Def.~\ref{baddef}), then we need a lemma which
+ − 310 ensures that another equivalent can be found satisfying the
+ − 311 side-condition. Unfortunately, such `little' and `obvious' lemmas make
+ − 312 formalisations of automata theory hair-pulling experiences.
173
+ − 313
175
+ − 314
82
+ − 315 In this paper, we will not attempt to formalise automata theory in
173
+ − 316 Isabelle/HOL nor will we attempt to formalise automata proofs from the
172
+ − 317 literature, but take a different approach to regular languages than is
+ − 318 usually taken. Instead of defining a regular language as one where there
+ − 319 exists an automaton that recognises all strings of the language, we define a
82
+ − 320 regular language as:
54
+ − 321
167
+ − 322 \begin{dfntn}
77
+ − 323 A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
54
+ − 324 strings of @{text "A"}.
167
+ − 325 \end{dfntn}
54
+ − 326
+ − 327 \noindent
172
+ − 328 The reason is that regular expressions, unlike graphs, matrices and
175
+ − 329 functions, can be easily defined as an inductive datatype. A reasoning
+ − 330 infrastructure (like induction and recursion) comes then for free in
+ − 331 HOL. Moreover, no side-conditions will be needed for regular expressions,
+ − 332 like we usually need for automata. This convenience of regular expressions has
+ − 333 recently been exploited in HOL4 with a formalisation of regular expression
+ − 334 matching based on derivatives \cite{OwensSlind08} and with an equivalence
+ − 335 checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}. The
+ − 336 main purpose of this paper is to show that a central result about regular
+ − 337 languages---the Myhill-Nerode theorem---can be recreated by only using
+ − 338 regular expressions. This theorem gives necessary and sufficient conditions
+ − 339 for when a language is regular. As a corollary of this theorem we can easily
+ − 340 establish the usual closure properties, including complementation, for
+ − 341 regular languages.\medskip
61
+ − 342
174
+ − 343 \noindent
175
+ − 344 {\bf Contributions:} There is an extensive literature on regular languages.
+ − 345 To our best knowledge, our proof of the Myhill-Nerode theorem is the first
+ − 346 that is based on regular expressions, only. The part of this theorem stating
+ − 347 that finitely many partitions imply regularity of the language is proved by
+ − 348 an argument about solving equational sytems. This argument appears to be
+ − 349 folklore. For the other part, we give two proofs: one direct proof using
+ − 350 certain tagging-functions, and another indirect proof using Antimirov's
+ − 351 partial derivatives \cite{Antimirov95}. Again to our best knowledge, the
+ − 352 tagging-functions have not been used before to establish the Myhill-Nerode
+ − 353 theorem. Derivatives of regular expressions have been used widely in the
+ − 354 literature about regular expressions. However, partial derivatives are more
+ − 355 suitable in the context of the Myhill-Nerode theorem, since it is easier to
+ − 356 establish formally their finiteness result.
+ − 357
24
+ − 358 *}
+ − 359
50
+ − 360 section {* Preliminaries *}
+ − 361
+ − 362 text {*
172
+ − 363 \noindent
67
+ − 364 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
92
+ − 365 being represented by the empty list, written @{term "[]"}. \emph{Languages}
67
+ − 366 are sets of strings. The language containing all strings is written in
71
+ − 367 Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
167
+ − 368 is written @{term "A \<cdot> B"} and a language raised to the power @{text n} is written
93
+ − 369 @{term "A \<up> n"}. They are defined as usual
54
+ − 370
+ − 371 \begin{center}
172
+ − 372 @{thm conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}
58
+ − 373 \hspace{7mm}
172
+ − 374 @{thm lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}
58
+ − 375 \hspace{7mm}
172
+ − 376 @{thm lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
54
+ − 377 \end{center}
+ − 378
+ − 379 \noindent
113
+ − 380 where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
172
+ − 381 is defined as the union over all powers, namely @{thm star_def}. In the paper
88
+ − 382 we will make use of the following properties of these constructions.
58
+ − 383
167
+ − 384 \begin{prpstn}\label{langprops}\mbox{}\\
92
+ − 385 \begin{tabular}{@ {}ll}
+ − 386 (i) & @{thm star_cases} \\
+ − 387 (ii) & @{thm[mode=IfThen] pow_length}\\
172
+ − 388 (iii) & @{thm conc_Union_left} \\
71
+ − 389 \end{tabular}
167
+ − 390 \end{prpstn}
71
+ − 391
+ − 392 \noindent
100
+ − 393 In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
156
+ − 394 string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
100
+ − 395 the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}. We omit
+ − 396 the proofs for these properties, but invite the reader to consult our
123
+ − 397 formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
71
+ − 398
90
+ − 399 The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
+ − 400 equivalence relation @{term REL} is @{term "A // REL"}. We will write
71
+ − 401 @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
156
+ − 402 as \mbox{@{text "{y | y \<approx> x}"}}.
71
+ − 403
+ − 404
51
+ − 405 Central to our proof will be the solution of equational systems
156
+ − 406 involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
167
+ − 407 which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
115
+ − 408 @{term "[] \<notin> A"}. However we will need the following `reverse'
167
+ − 409 version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to
+ − 410 \mbox{@{term "X \<cdot> A"}}).
50
+ − 411
167
+ − 412 \begin{lmm}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
86
+ − 413 If @{thm (prem 1) arden} then
115
+ − 414 @{thm (lhs) arden} if and only if
86
+ − 415 @{thm (rhs) arden}.
167
+ − 416 \end{lmm}
50
+ − 417
+ − 418 \begin{proof}
86
+ − 419 For the right-to-left direction we assume @{thm (rhs) arden} and show
+ − 420 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
167
+ − 421 we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
+ − 422 which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both
+ − 423 sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
+ − 424 is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction.
50
+ − 425
86
+ − 426 For the other direction we assume @{thm (lhs) arden}. By a simple induction
51
+ − 427 on @{text n}, we can establish the property
50
+ − 428
+ − 429 \begin{center}
86
+ − 430 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
50
+ − 431 \end{center}
+ − 432
+ − 433 \noindent
167
+ − 434 Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
+ − 435 all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
71
+ − 436 of @{text "\<star>"}.
51
+ − 437 For the inclusion in the other direction we assume a string @{text s}
134
+ − 438 with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
75
+ − 439 we know by Prop.~\ref{langprops}@{text "(ii)"} that
167
+ − 440 @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
+ − 441 (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
53
+ − 442 From @{text "(*)"} it follows then that
167
+ − 443 @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
+ − 444 implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
174
+ − 445 this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
50
+ − 446 \end{proof}
67
+ − 447
+ − 448 \noindent
88
+ − 449 Regular expressions are defined as the inductive datatype
67
+ − 450
+ − 451 \begin{center}
+ − 452 @{text r} @{text "::="}
173
+ − 453 @{term ZERO}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 454 @{term ONE}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 455 @{term "ATOM c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 456 @{term "TIMES r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 457 @{term "PLUS r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
67
+ − 458 @{term "STAR r"}
+ − 459 \end{center}
+ − 460
+ − 461 \noindent
88
+ − 462 and the language matched by a regular expression is defined as
67
+ − 463
+ − 464 \begin{center}
+ − 465 \begin{tabular}{c@ {\hspace{10mm}}c}
+ − 466 \begin{tabular}{rcl}
172
+ − 467 @{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
+ − 468 @{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\
+ − 469 @{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\
67
+ − 470 \end{tabular}
+ − 471 &
+ − 472 \begin{tabular}{rcl}
172
+ − 473 @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 474 @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+ − 475 @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 476 @{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+ − 477 @{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+ − 478 @{thm (rhs) lang.simps(6)[where r="r"]}\\
67
+ − 479 \end{tabular}
+ − 480 \end{tabular}
+ − 481 \end{center}
70
+ − 482
100
+ − 483 Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
132
+ − 484 a regular expression that matches the union of all languages of @{text rs}. We only need to know the
+ − 485 existence
92
+ − 486 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
173
+ − 487 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const PLUS} over the
+ − 488 set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}
110
+ − 489 %
+ − 490 \begin{equation}\label{uplus}
+ − 491 \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ − 492 \end{equation}
88
+ − 493
+ − 494 \noindent
90
+ − 495 holds, whereby @{text "\<calL> ` rs"} stands for the
+ − 496 image of the set @{text rs} under function @{text "\<calL>"}.
50
+ − 497 *}
39
+ − 498
132
+ − 499
133
+ − 500 section {* The Myhill-Nerode Theorem, First Part *}
54
+ − 501
+ − 502 text {*
174
+ − 503 \footnote{Folklore: Henzinger (arden-DFA-regexp.pdf); Hofmann}
172
+ − 504
+ − 505 \noindent
77
+ − 506 The key definition in the Myhill-Nerode theorem is the
75
+ − 507 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
+ − 508 strings are related, provided there is no distinguishing extension in this
154
+ − 509 language. This can be defined as a tertiary relation.
75
+ − 510
174
+ − 511 \begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel}
+ − 512 Given a language @{text A}, two strings @{text x} and
123
+ − 513 @{text y} are Myhill-Nerode related provided
117
+ − 514 \begin{center}
75
+ − 515 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
117
+ − 516 \end{center}
167
+ − 517 \end{dfntn}
70
+ − 518
71
+ − 519 \noindent
75
+ − 520 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+ − 521 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
108
+ − 522 equivalence classes. To illustrate this quotient construction, let us give a simple
101
+ − 523 example: consider the regular language containing just
92
+ − 524 the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
101
+ − 525 into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
90
+ − 526 as follows
+ − 527
+ − 528 \begin{center}
+ − 529 @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
+ − 530 @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
+ − 531 @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+ − 532 \end{center}
+ − 533
+ − 534 One direction of the Myhill-Nerode theorem establishes
93
+ − 535 that if there are finitely many equivalence classes, like in the example above, then
+ − 536 the language is regular. In our setting we therefore have to show:
75
+ − 537
167
+ − 538 \begin{thrm}\label{myhillnerodeone}
96
+ − 539 @{thm[mode=IfThen] Myhill_Nerode1}
167
+ − 540 \end{thrm}
71
+ − 541
75
+ − 542 \noindent
90
+ − 543 To prove this theorem, we first define the set @{term "finals A"} as those equivalence
100
+ − 544 classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
75
+ − 545 %
71
+ − 546 \begin{equation}
70
+ − 547 @{thm finals_def}
71
+ − 548 \end{equation}
+ − 549
+ − 550 \noindent
132
+ − 551 In our running example, @{text "X\<^isub>2"} is the only
+ − 552 equivalence class in @{term "finals {[c]}"}.
174
+ − 553 It is straightforward to show that in general
+ − 554
+ − 555 \begin{center}
+ − 556 @{thm lang_is_union_of_finals}\hspace{15mm}
+ − 557 @{thm finals_in_partitions}
+ − 558 \end{center}
+ − 559
+ − 560 \noindent
+ − 561 hold.
75
+ − 562 Therefore if we know that there exists a regular expression for every
100
+ − 563 equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
93
+ − 564 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
98
+ − 565 that matches every string in @{text A}.
70
+ − 566
75
+ − 567
90
+ − 568 Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
79
+ − 569 regular expression for \emph{every} equivalence class, not just the ones
77
+ − 570 in @{term "finals A"}. We
93
+ − 571 first define the notion of \emph{one-character-transition} between
+ − 572 two equivalence classes
75
+ − 573 %
71
+ − 574 \begin{equation}
+ − 575 @{thm transition_def}
+ − 576 \end{equation}
70
+ − 577
71
+ − 578 \noindent
92
+ − 579 which means that if we concatenate the character @{text c} to the end of all
+ − 580 strings in the equivalence class @{text Y}, we obtain a subset of
77
+ − 581 @{text X}. Note that we do not define an automaton here, we merely relate two sets
110
+ − 582 (with the help of a character). In our concrete example we have
92
+ − 583 @{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
+ − 584 other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
75
+ − 585
156
+ − 586 Next we construct an \emph{initial equational system} that
+ − 587 contains an equation for each equivalence class. We first give
+ − 588 an informal description of this construction. Suppose we have
75
+ − 589 the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+ − 590 contains the empty string @{text "[]"} (since equivalence classes are disjoint).
77
+ − 591 Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
75
+ − 592
+ − 593 \begin{center}
+ − 594 \begin{tabular}{rcl}
173
+ − 595 @{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)"} \\
+ − 596 @{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
+ − 597 & $\vdots$ \\
173
+ − 598 @{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
+ − 599 \end{tabular}
+ − 600 \end{center}
70
+ − 601
75
+ − 602 \noindent
173
+ − 603 where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"}
100
+ − 604 stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
159
+ − 605 X\<^isub>i"}.
+ − 606 %The intuition behind the equational system is that every
+ − 607 %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+ − 608 %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
+ − 609 %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
+ − 610 %predecessor states to @{text X\<^isub>i}.
+ − 611 There can only be
173
+ − 612 finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} in a right-hand side
156
+ − 613 since by assumption there are only finitely many
159
+ − 614 equivalence classes and only finitely many characters.
173
+ − 615 The term @{text "\<lambda>(ONE)"} in the first equation acts as a marker for the initial state, that
159
+ − 616 is the equivalence class
100
+ − 617 containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
115
+ − 618 single `initial' state in the equational system, which is different from
100
+ − 619 the method by Brzozowski \cite{Brzozowski64}, where he marks the
115
+ − 620 `terminal' states. We are forced to set up the equational system in our
+ − 621 way, because the Myhill-Nerode relation determines the `direction' of the
123
+ − 622 transitions---the successor `state' of an equivalence class @{text Y} can
+ − 623 be reached by adding a character to the end of @{text Y}. This is also the
156
+ − 624 reason why we have to use our reverse version of Arden's Lemma.}
159
+ − 625 %In our initial equation system there can only be
173
+ − 626 %finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} in a right-hand side
159
+ − 627 %since by assumption there are only finitely many
+ − 628 %equivalence classes and only finitely many characters.
100
+ − 629 Overloading the function @{text \<calL>} for the two kinds of terms in the
92
+ − 630 equational system, we have
75
+ − 631
+ − 632 \begin{center}
92
+ − 633 @{text "\<calL>(Y, r) \<equiv>"} %
172
+ − 634 @{thm (rhs) lang_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+ − 635 @{thm lang_trm.simps(1)[where r="r", THEN eq_reflection]}
75
+ − 636 \end{center}
+ − 637
+ − 638 \noindent
100
+ − 639 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
75
+ − 640 %
+ − 641 \begin{equation}\label{inv1}
173
+ − 642 @{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
+ − 643 \end{equation}
+ − 644
+ − 645 \noindent
+ − 646 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ − 647 %
+ − 648 \begin{equation}\label{inv2}
173
+ − 649 @{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
+ − 650 \end{equation}
+ − 651
+ − 652 \noindent
160
+ − 653 holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is
103
+ − 654 to obtain this equation: it only holds with the marker, since none of
108
+ − 655 the other terms contain the empty string. The point of the initial equational system is
+ − 656 that solving it means we will be able to extract a regular expression for every equivalence class.
100
+ − 657
101
+ − 658 Our representation for the equations in Isabelle/HOL are pairs,
108
+ − 659 where the first component is an equivalence class (a set of strings)
+ − 660 and the second component
101
+ − 661 is a set of terms. Given a set of equivalence
100
+ − 662 classes @{text CS}, our initial equational system @{term "Init CS"} is thus
101
+ − 663 formally defined as
104
+ − 664 %
+ − 665 \begin{equation}\label{initcs}
+ − 666 \mbox{\begin{tabular}{rcl}
100
+ − 667 @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
+ − 668 @{text "if"}~@{term "[] \<in> X"}\\
173
+ − 669 & & @{text "then"}~@{term "{Trn Y (ATOM c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam ONE}"}\\
+ − 670 & & @{text "else"}~@{term "{Trn Y (ATOM c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
100
+ − 671 @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def}
104
+ − 672 \end{tabular}}
+ − 673 \end{equation}
100
+ − 674
+ − 675
+ − 676
+ − 677 \noindent
+ − 678 Because we use sets of terms
101
+ − 679 for representing the right-hand sides of equations, we can
100
+ − 680 prove \eqref{inv1} and \eqref{inv2} more concisely as
93
+ − 681 %
167
+ − 682 \begin{lmm}\label{inv}
100
+ − 683 If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
167
+ − 684 \end{lmm}
77
+ − 685
93
+ − 686 \noindent
92
+ − 687 Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
100
+ − 688 initial equational system into one in \emph{solved form} maintaining the invariant
108
+ − 689 in Lem.~\ref{inv}. From the solved form we will be able to read
89
+ − 690 off the regular expressions.
+ − 691
100
+ − 692 In order to transform an equational system into solved form, we have two
89
+ − 693 operations: one that takes an equation of the form @{text "X = rhs"} and removes
110
+ − 694 any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's
92
+ − 695 Lemma. The other operation takes an equation @{text "X = rhs"}
89
+ − 696 and substitutes @{text X} throughout the rest of the equational system
110
+ − 697 adjusting the remaining regular expressions appropriately. To define this adjustment
108
+ − 698 we define the \emph{append-operation} taking a term and a regular expression as argument
89
+ − 699
+ − 700 \begin{center}
162
+ − 701 @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+ − 702 @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
89
+ − 703 \end{center}
+ − 704
92
+ − 705 \noindent
108
+ − 706 We lift this operation to entire right-hand sides of equations, written as
162
+ − 707 @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
101
+ − 708 the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
110
+ − 709 %
+ − 710 \begin{equation}\label{arden_def}
+ − 711 \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
94
+ − 712 @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 713 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 714 & & @{text "r' ="} & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+ − 715 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
110
+ − 716 \end{tabular}}
+ − 717 \end{equation}
93
+ − 718
+ − 719 \noindent
101
+ − 720 In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
110
+ − 721 then we calculate the combined regular expressions for all @{text r} coming
94
+ − 722 from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+ − 723 finally we append this regular expression to @{text rhs'}. It can be easily seen
156
+ − 724 that this operation mimics Arden's Lemma on the level of equations. To ensure
+ − 725 the non-emptiness condition of Arden's Lemma we say that a right-hand side is
154
+ − 726 @{text ardenable} provided
110
+ − 727
+ − 728 \begin{center}
+ − 729 @{thm ardenable_def}
+ − 730 \end{center}
+ − 731
+ − 732 \noindent
156
+ − 733 This allows us to prove a version of Arden's Lemma on the level of equations.
110
+ − 734
167
+ − 735 \begin{lmm}\label{ardenable}
113
+ − 736 Given an equation @{text "X = rhs"}.
110
+ − 737 If @{text "X = \<Union>\<calL> ` rhs"},
115
+ − 738 @{thm (prem 2) Arden_keeps_eq}, and
110
+ − 739 @{thm (prem 3) Arden_keeps_eq}, then
135
+ − 740 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
167
+ − 741 \end{lmm}
110
+ − 742
+ − 743 \noindent
156
+ − 744 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
+ − 745 but we can still ensure that it holds troughout our algorithm of transforming equations
+ − 746 into solved form. The \emph{substitution-operation} takes an equation
95
+ − 747 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
94
+ − 748
+ − 749 \begin{center}
95
+ − 750 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ − 751 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 752 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 753 & & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
+ − 754 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\
+ − 755 \end{tabular}
94
+ − 756 \end{center}
95
+ − 757
+ − 758 \noindent
134
+ − 759 We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
95
+ − 760 the regular expression corresponding to the deleted terms; finally we append this
+ − 761 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+ − 762 the substitution operation we will arrange it so that @{text "xrhs"} does not contain
110
+ − 763 any occurrence of @{text X}.
96
+ − 764
134
+ − 765 With these two operations in place, we can define the operation that removes one equation
100
+ − 766 from an equational systems @{text ES}. The operation @{const Subst_all}
96
+ − 767 substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES};
100
+ − 768 @{const Remove} then completely removes such an equation from @{text ES} by substituting
110
+ − 769 it to the rest of the equational system, but first eliminating all recursive occurrences
96
+ − 770 of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+ − 771
+ − 772 \begin{center}
+ − 773 \begin{tabular}{rcl}
+ − 774 @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+ − 775 @{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+ − 776 \end{tabular}
+ − 777 \end{center}
100
+ − 778
+ − 779 \noindent
110
+ − 780 Finally, we can define how an equational system should be solved. For this
107
+ − 781 we will need to iterate the process of eliminating equations until only one equation
154
+ − 782 will be left in the system. However, we do not just want to have any equation
107
+ − 783 as being the last one, but the one involving the equivalence class for
+ − 784 which we want to calculate the regular
108
+ − 785 expression. Let us suppose this equivalence class is @{text X}.
107
+ − 786 Since @{text X} is the one to be solved, in every iteration step we have to pick an
108
+ − 787 equation to be eliminated that is different from @{text X}. In this way
+ − 788 @{text X} is kept to the final step. The choice is implemented using Hilbert's choice
107
+ − 789 operator, written @{text SOME} in the definition below.
100
+ − 790
+ − 791 \begin{center}
+ − 792 \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+ − 793 @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
+ − 794 & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+ − 795 & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\
+ − 796 \end{tabular}
+ − 797 \end{center}
+ − 798
+ − 799 \noindent
110
+ − 800 The last definition we need applies @{term Iter} over and over until a condition
159
+ − 801 @{text Cond} is \emph{not} satisfied anymore. This condition states that there
110
+ − 802 are more than one equation left in the equational system @{text ES}. To solve
+ − 803 an equational system we use Isabelle/HOL's @{text while}-operator as follows:
101
+ − 804
100
+ − 805 \begin{center}
+ − 806 @{thm Solve_def}
+ − 807 \end{center}
+ − 808
101
+ − 809 \noindent
103
+ − 810 We are not concerned here with the definition of this operator
115
+ − 811 (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
103
+ − 812 in each @{const Iter}-step a single equation, and therefore
+ − 813 have a well-founded termination order by taking the cardinality
+ − 814 of the equational system @{text ES}. This enables us to prove
115
+ − 815 properties about our definition of @{const Solve} when we `call' it with
104
+ − 816 the equivalence class @{text X} and the initial equational system
+ − 817 @{term "Init (UNIV // \<approx>A)"} from
108
+ − 818 \eqref{initcs} using the principle:
110
+ − 819 %
+ − 820 \begin{equation}\label{whileprinciple}
+ − 821 \mbox{\begin{tabular}{l}
103
+ − 822 @{term "invariant (Init (UNIV // \<approx>A))"} \\
+ − 823 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+ − 824 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+ − 825 @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+ − 826 \hline
+ − 827 \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
110
+ − 828 \end{tabular}}
+ − 829 \end{equation}
103
+ − 830
+ − 831 \noindent
104
+ − 832 This principle states that given an invariant (which we will specify below)
+ − 833 we can prove a property
+ − 834 @{text "P"} involving @{const Solve}. For this we have to discharge the following
+ − 835 proof obligations: first the
113
+ − 836 initial equational system satisfies the invariant; second the iteration
154
+ − 837 step @{text "Iter"} preserves the invariant as long as the condition @{term Cond} holds;
113
+ − 838 third @{text "Iter"} decreases the termination order, and fourth that
104
+ − 839 once the condition does not hold anymore then the property @{text P} must hold.
103
+ − 840
104
+ − 841 The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
108
+ − 842 returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
104
+ − 843 that this equational system still satisfies the invariant. In order to get
+ − 844 the proof through, the invariant is composed of the following six properties:
103
+ − 845
+ − 846 \begin{center}
104
+ − 847 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+ − 848 @{text "invariant ES"} & @{text "\<equiv>"} &
103
+ − 849 @{term "finite ES"} & @{text "(finiteness)"}\\
+ − 850 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
104
+ − 851 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
162
+ − 852 & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
104
+ − 853 & & & @{text "(distinctness)"}\\
110
+ − 854 & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
162
+ − 855 & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
103
+ − 856 \end{tabular}
+ − 857 \end{center}
+ − 858
104
+ − 859 \noindent
+ − 860 The first two ensure that the equational system is always finite (number of equations
160
+ − 861 and number of terms in each equation); the third makes sure the `meaning' of the
108
+ − 862 equations is preserved under our transformations. The other properties are a bit more
+ − 863 technical, but are needed to get our proof through. Distinctness states that every
154
+ − 864 equation in the system is distinct. @{text Ardenable} ensures that we can always
156
+ − 865 apply the @{text Arden} operation.
108
+ − 866 The last property states that every @{text rhs} can only contain equivalence classes
+ − 867 for which there is an equation. Therefore @{text lhss} is just the set containing
+ − 868 the first components of an equational system,
+ − 869 while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
123
+ − 870 form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
110
+ − 871 and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
108
+ − 872
104
+ − 873
110
+ − 874 It is straightforward to prove that the initial equational system satisfies the
105
+ − 875 invariant.
+ − 876
167
+ − 877 \begin{lmm}\label{invzero}
104
+ − 878 @{thm[mode=IfThen] Init_ES_satisfies_invariant}
167
+ − 879 \end{lmm}
104
+ − 880
105
+ − 881 \begin{proof}
+ − 882 Finiteness is given by the assumption and the way how we set up the
+ − 883 initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
154
+ − 884 follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
113
+ − 885 property also follows from the setup of the initial equational system, as does
174
+ − 886 validity.
105
+ − 887 \end{proof}
+ − 888
113
+ − 889 \noindent
+ − 890 Next we show that @{text Iter} preserves the invariant.
+ − 891
167
+ − 892 \begin{lmm}\label{iterone}
104
+ − 893 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
167
+ − 894 \end{lmm}
104
+ − 895
107
+ − 896 \begin{proof}
156
+ − 897 The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
110
+ − 898 and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
+ − 899 preserves the invariant.
+ − 900 We prove this as follows:
+ − 901
+ − 902 \begin{center}
+ − 903 @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+ − 904 @{thm (concl) Subst_all_satisfies_invariant}
+ − 905 \end{center}
+ − 906
+ − 907 \noindent
156
+ − 908 Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations
116
+ − 909 keep the equational system finite. These operations also preserve soundness
113
+ − 910 and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
154
+ − 911 The property @{text ardenable} is clearly preserved because the append-operation
110
+ − 912 cannot make a regular expression to match the empty string. Validity is
+ − 913 given because @{const Arden} removes an equivalence class from @{text yrhs}
+ − 914 and then @{const Subst_all} removes @{text Y} from the equational system.
132
+ − 915 Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
110
+ − 916 which matches with our proof-obligation of @{const "Subst_all"}. Since
132
+ − 917 \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption
174
+ − 918 to complete the proof.
107
+ − 919 \end{proof}
+ − 920
113
+ − 921 \noindent
+ − 922 We also need the fact that @{text Iter} decreases the termination measure.
+ − 923
167
+ − 924 \begin{lmm}\label{itertwo}
104
+ − 925 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
167
+ − 926 \end{lmm}
104
+ − 927
105
+ − 928 \begin{proof}
+ − 929 By assumption we know that @{text "ES"} is finite and has more than one element.
+ − 930 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
110
+ − 931 @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
105
+ − 932 that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+ − 933 removes the equation @{text "Y = yrhs"} from the system, and therefore
174
+ − 934 the cardinality of @{const Iter} strictly decreases.
105
+ − 935 \end{proof}
+ − 936
113
+ − 937 \noindent
134
+ − 938 This brings us to our property we want to establish for @{text Solve}.
113
+ − 939
+ − 940
167
+ − 941 \begin{lmm}
104
+ − 942 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+ − 943 a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+ − 944 and @{term "invariant {(X, rhs)}"}.
167
+ − 945 \end{lmm}
104
+ − 946
107
+ − 947 \begin{proof}
110
+ − 948 In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+ − 949 stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
+ − 950 that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ − 951 in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
113
+ − 952 Therefore our invariant cannot be just @{term "invariant ES"}, but must be
110
+ − 953 @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
+ − 954 @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+ − 955 the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+ − 956 Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+ − 957 modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+ − 958 Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+ − 959 we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ − 960 and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
113
+ − 961 does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
110
+ − 962 with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
123
+ − 963 of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
110
+ − 964 for which the invariant holds. This allows us to conclude that
113
+ − 965 @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
174
+ − 966 as needed.
107
+ − 967 \end{proof}
+ − 968
106
+ − 969 \noindent
+ − 970 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+ − 971 there exists a regular expression.
+ − 972
167
+ − 973 \begin{lmm}\label{every_eqcl_has_reg}
105
+ − 974 @{thm[mode=IfThen] every_eqcl_has_reg}
167
+ − 975 \end{lmm}
105
+ − 976
+ − 977 \begin{proof}
138
+ − 978 By the preceding lemma, we know that there exists a @{text "rhs"} such
105
+ − 979 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+ − 980 and that the invariant holds for this equation. That means we
+ − 981 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
109
+ − 982 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
123
+ − 983 invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
156
+ − 984 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
106
+ − 985 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
113
+ − 986 This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
154
+ − 987 So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
174
+ − 988 With this we can conclude the proof.
105
+ − 989 \end{proof}
+ − 990
106
+ − 991 \noindent
+ − 992 Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
+ − 993 of the Myhill-Nerode theorem.
105
+ − 994
106
+ − 995 \begin{proof}[of Thm.~\ref{myhillnerodeone}]
123
+ − 996 By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
105
+ − 997 every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
110
+ − 998 a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
123
+ − 999 in @{term "finals A"} there exists a regular expression. Moreover by assumption
106
+ − 1000 we know that @{term "finals A"} must be finite, and therefore there must be a finite
105
+ − 1001 set of regular expressions @{text "rs"} such that
159
+ − 1002 @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
105
+ − 1003 Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
174
+ − 1004 as the regular expression that is needed in the theorem.
105
+ − 1005 \end{proof}
54
+ − 1006 *}
+ − 1007
100
+ − 1008
+ − 1009
+ − 1010
+ − 1011 section {* Myhill-Nerode, Second Part *}
39
+ − 1012
+ − 1013 text {*
173
+ − 1014 \noindent
174
+ − 1015 In this section and the next we will give two proofs for establishing the second
+ − 1016 part of the Myhill-Nerode theorem. It can be formulated in our setting as follows:
39
+ − 1017
167
+ − 1018 \begin{thrm}
135
+ − 1019 Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
167
+ − 1020 \end{thrm}
39
+ − 1021
116
+ − 1022 \noindent
174
+ − 1023 The first proof will be by induction on the structure of @{text r}. It turns out
116
+ − 1024 the base cases are straightforward.
+ − 1025
+ − 1026
+ − 1027 \begin{proof}[Base Cases]
173
+ − 1028 The cases for @{const ZERO}, @{const ONE} and @{const ATOM} are routine, because
149
+ − 1029 we can easily establish that
39
+ − 1030
114
+ − 1031 \begin{center}
+ − 1032 \begin{tabular}{l}
172
+ − 1033 @{thm quot_zero_eq}\\
+ − 1034 @{thm quot_one_subset}\\
+ − 1035 @{thm quot_atom_subset}
114
+ − 1036 \end{tabular}
+ − 1037 \end{center}
+ − 1038
116
+ − 1039 \noindent
174
+ − 1040 hold, which shows that @{term "UNIV // \<approx>(lang r)"} must be finite.
114
+ − 1041 \end{proof}
109
+ − 1042
116
+ − 1043 \noindent
154
+ − 1044 Much more interesting, however, are the inductive cases. They seem hard to solve
117
+ − 1045 directly. The reader is invited to try.
+ − 1046
174
+ − 1047 Our first proof will rely on some
138
+ − 1048 \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will
174
+ − 1049 be easy to prove that the \emph{range} of these tagging-functions is finite.
+ − 1050 The range of a function @{text f} is defined as
+ − 1051
+ − 1052 \begin{center}
+ − 1053 @{text "range f \<equiv> f ` UNIV"}
+ − 1054 \end{center}
+ − 1055
+ − 1056 \noindent
+ − 1057 that means we take the image of @{text f} w.r.t.~all elements in the domain.
135
+ − 1058 With this we will be able to infer that the tagging-functions, seen as relations,
117
+ − 1059 give rise to finitely many equivalence classes of @{const UNIV}. Finally we
174
+ − 1060 will show that the tagging-relations are more refined than @{term "\<approx>(lang r)"}, which
+ − 1061 implies that @{term "UNIV // \<approx>(lang r)"} must also be finite---a relation @{text "R\<^isub>1"}
+ − 1062 is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
123
+ − 1063 We formally define the notion of a \emph{tagging-relation} as follows.
117
+ − 1064
167
+ − 1065 \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
119
+ − 1066 and @{text y} are \emph{tag-related} provided
117
+ − 1067 \begin{center}
174
+ − 1068 @{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
117
+ − 1069 \end{center}
167
+ − 1070 \end{dfntn}
117
+ − 1071
145
+ − 1072
123
+ − 1073 In order to establish finiteness of a set @{text A}, we shall use the following powerful
118
+ − 1074 principle from Isabelle/HOL's library.
+ − 1075 %
+ − 1076 \begin{equation}\label{finiteimageD}
+ − 1077 @{thm[mode=IfThen] finite_imageD}
+ − 1078 \end{equation}
+ − 1079
+ − 1080 \noindent
123
+ − 1081 It states that if an image of a set under an injective function @{text f} (injective over this set)
131
+ − 1082 is finite, then the set @{text A} itself must be finite. We can use it to establish the following
118
+ − 1083 two lemmas.
+ − 1084
167
+ − 1085 \begin{lmm}\label{finone}
117
+ − 1086 @{thm[mode=IfThen] finite_eq_tag_rel}
167
+ − 1087 \end{lmm}
117
+ − 1088
+ − 1089 \begin{proof}
119
+ − 1090 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
123
+ − 1091 @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
119
+ − 1092 finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+ − 1093 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+ − 1094 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
149
+ − 1095 From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with
123
+ − 1096 @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
+ − 1097 turn means that the equivalence classes @{text X}
174
+ − 1098 and @{text Y} must be equal.
117
+ − 1099 \end{proof}
+ − 1100
167
+ − 1101 \begin{lmm}\label{fintwo}
123
+ − 1102 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
118
+ − 1103 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+ − 1104 If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+ − 1105 then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
167
+ − 1106 \end{lmm}
117
+ − 1107
+ − 1108 \begin{proof}
123
+ − 1109 We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
118
+ − 1110 be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
135
+ − 1111 @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
174
+ − 1112 which must be finite by assumption. What remains to be shown is that @{text f} is injective
118
+ − 1113 on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
+ − 1114 classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+ − 1115 @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+ − 1116 @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
135
+ − 1117 We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}.
+ − 1118 From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
123
+ − 1119 and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+ − 1120 such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
118
+ − 1121 are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
174
+ − 1122 they must also be @{text "R\<^isub>2"}-related, as we need to show.
117
+ − 1123 \end{proof}
+ − 1124
+ − 1125 \noindent
119
+ − 1126 Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
174
+ − 1127 that @{term "UNIV // \<approx>(lang r)"} is finite, we have to find a tagging-function whose
+ − 1128 range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
173
+ − 1129 Let us attempt the @{const PLUS}-case first.
119
+ − 1130
173
+ − 1131 \begin{proof}[@{const "PLUS"}-Case]
135
+ − 1132 We take as tagging-function
132
+ − 1133 %
119
+ − 1134 \begin{center}
172
+ − 1135 @{thm tag_str_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
119
+ − 1136 \end{center}
117
+ − 1137
119
+ − 1138 \noindent
+ − 1139 where @{text "A"} and @{text "B"} are some arbitrary languages.
+ − 1140 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ − 1141 then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
174
+ − 1142 @{term "tag_str_Plus A B"} is a subset of this product set---so finite. It remains to be shown
120
+ − 1143 that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
+ − 1144 showing
+ − 1145 %
+ − 1146 \begin{center}
+ − 1147 @{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"}
+ − 1148 \end{center}
132
+ − 1149 %
120
+ − 1150 \noindent
+ − 1151 which by unfolding the Myhill-Nerode relation is identical to
+ − 1152 %
+ − 1153 \begin{equation}\label{pattern}
+ − 1154 @{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"}
+ − 1155 \end{equation}
132
+ − 1156 %
120
+ − 1157 \noindent
+ − 1158 since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
142
+ − 1159 \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse
123
+ − 1160 in which set, @{text A} or @{text B}, the string @{term "x @ z"} is.
+ − 1161 The definition of the tagging-function will give us in each case the
+ − 1162 information to infer that @{text "y @ z \<in> A \<union> B"}.
+ − 1163 Finally we
174
+ − 1164 can discharge this case by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
119
+ − 1165 \end{proof}
+ − 1166
109
+ − 1167
121
+ − 1168 \noindent
+ − 1169 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
173
+ − 1170 they are slightly more complicated. In the @{const TIMES}-case we essentially have
123
+ − 1171 to be able to infer that
132
+ − 1172 %
123
+ − 1173 \begin{center}
167
+ − 1174 @{text "\<dots>"}@{term "x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
123
+ − 1175 \end{center}
132
+ − 1176 %
123
+ − 1177 \noindent
135
+ − 1178 using the information given by the appropriate tagging-function. The complication
167
+ − 1179 is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}
135
+ − 1180 (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
124
+ − 1181 notions of \emph{string prefixes}
132
+ − 1182 %
124
+ − 1183 \begin{center}
+ − 1184 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+ − 1185 @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+ − 1186 \end{center}
132
+ − 1187 %
124
+ − 1188 \noindent
+ − 1189 and \emph{string subtraction}:
132
+ − 1190 %
124
+ − 1191 \begin{center}
159
+ − 1192 @{text "[] - y \<equiv> []"}\hspace{10mm}
+ − 1193 @{text "x - [] \<equiv> x"}\hspace{10mm}
+ − 1194 @{text "cx - dy \<equiv> if c = d then x - y else cx"}
124
+ − 1195 \end{center}
132
+ − 1196 %
124
+ − 1197 \noindent
142
+ − 1198 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
132
+ − 1199
167
+ − 1200 Now assuming @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split'
+ − 1201 this string to be in @{term "A \<cdot> B"}:
132
+ − 1202 %
125
+ − 1203 \begin{center}
159
+ − 1204 \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
125
+ − 1205 \scalebox{0.7}{
+ − 1206 \begin{tikzpicture}
159
+ − 1207 \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
+ − 1208 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
+ − 1209 \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
125
+ − 1210
+ − 1211 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1212 (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
128
+ − 1213 node[midway, above=0.5em]{@{text x}};
125
+ − 1214
+ − 1215 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1216 (z.north west) -- ($(z.north east)+(0em,0em)$)
128
+ − 1217 node[midway, above=0.5em]{@{text z}};
125
+ − 1218
+ − 1219 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1220 ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
167
+ − 1221 node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
125
+ − 1222
+ − 1223 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1224 ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ − 1225 node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
+ − 1226
+ − 1227 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1228 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ − 1229 node[midway, below=0.5em]{@{term "x' \<in> A"}};
+ − 1230 \end{tikzpicture}}
159
+ − 1231 &
125
+ − 1232 \scalebox{0.7}{
+ − 1233 \begin{tikzpicture}
159
+ − 1234 \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
+ − 1235 \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
+ − 1236 \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$ };
125
+ − 1237
+ − 1238 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1239 (x.north west) -- ($(za.north west)+(0em,0em)$)
128
+ − 1240 node[midway, above=0.5em]{@{text x}};
125
+ − 1241
+ − 1242 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1243 ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
128
+ − 1244 node[midway, above=0.5em]{@{text z}};
125
+ − 1245
+ − 1246 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1247 ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
167
+ − 1248 node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
125
+ − 1249
+ − 1250 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1251 ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+ − 1252 node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
+ − 1253
+ − 1254 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1255 ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+ − 1256 node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
+ − 1257 \end{tikzpicture}}
159
+ − 1258 \end{tabular}
125
+ − 1259 \end{center}
132
+ − 1260 %
125
+ − 1261 \noindent
156
+ − 1262 Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
+ − 1263 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
167
+ − 1264 In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the
125
+ − 1265 following tagging-function
132
+ − 1266 %
121
+ − 1267 \begin{center}
172
+ − 1268 @{thm tag_str_Times_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
121
+ − 1269 \end{center}
125
+ − 1270
+ − 1271 \noindent
132
+ − 1272 with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
127
+ − 1273 is in the language @{text B}.
125
+ − 1274
173
+ − 1275 \begin{proof}[@{const TIMES}-Case]
127
+ − 1276 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ − 1277 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
173
+ − 1278 @{term "tag_str_TIMES A B"} is a subset of this product set, and therefore finite.
130
+ − 1279 We have to show injectivity of this tagging-function as
132
+ − 1280 %
127
+ − 1281 \begin{center}
173
+ − 1282 @{term "\<forall>z. tag_str_TIMES A B x = tag_str_TIMES A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
127
+ − 1283 \end{center}
132
+ − 1284 %
127
+ − 1285 \noindent
128
+ − 1286 There are two cases to be considered (see pictures above). First, there exists
+ − 1287 a @{text "x'"} such that
127
+ − 1288 @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
132
+ − 1289 %
127
+ − 1290 \begin{center}
+ − 1291 @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
+ − 1292 \end{center}
132
+ − 1293 %
127
+ − 1294 \noindent
173
+ − 1295 and by the assumption about @{term "tag_str_TIMES A B"} also
132
+ − 1296 %
127
+ − 1297 \begin{center}
+ − 1298 @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
+ − 1299 \end{center}
132
+ − 1300 %
127
+ − 1301 \noindent
+ − 1302 That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and
+ − 1303 @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
+ − 1304 @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
+ − 1305 relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
+ − 1306 have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
167
+ − 1307 @{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
127
+ − 1308
+ − 1309 Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
173
+ − 1310 By the assumption about @{term "tag_str_TIMES A B"} we have
127
+ − 1311 @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
134
+ − 1312 relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
173
+ − 1313 with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const TIMES}-case
174
+ − 1314 by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
121
+ − 1315 \end{proof}
128
+ − 1316
+ − 1317 \noindent
173
+ − 1318 The case for @{const STAR} is similar to @{const TIMES}, but poses a few extra challenges. When
137
+ − 1319 we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the
130
+ − 1320 empty string, we
128
+ − 1321 have the following picture:
132
+ − 1322 %
128
+ − 1323 \begin{center}
+ − 1324 \scalebox{0.7}{
+ − 1325 \begin{tikzpicture}
+ − 1326 \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
+ − 1327 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
+ − 1328 \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
+ − 1329 \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
+ − 1330
+ − 1331 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1332 (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ − 1333 node[midway, above=0.5em]{@{text x}};
+ − 1334
+ − 1335 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1336 (za.north west) -- ($(zb.north east)+(0em,0em)$)
+ − 1337 node[midway, above=0.5em]{@{text z}};
+ − 1338
+ − 1339 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1340 ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+ − 1341 node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
+ − 1342
+ − 1343 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1344 ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ − 1345 node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
+ − 1346
+ − 1347 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1348 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
136
+ − 1349 node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
128
+ − 1350
+ − 1351 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1352 ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
136
+ − 1353 node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
128
+ − 1354
+ − 1355 \draw[decoration={brace,transform={yscale=3}},decorate]
+ − 1356 ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
136
+ − 1357 node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
128
+ − 1358 \end{tikzpicture}}
+ − 1359 \end{center}
132
+ − 1360 %
128
+ − 1361 \noindent
135
+ − 1362 We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
+ − 1363 @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string
128
+ − 1364 @{text "[]"} would do.
135
+ − 1365 There are potentially many such prefixes, but there can only be finitely many of them (the
128
+ − 1366 string @{text x} is finite). Let us therefore choose the longest one and call it
+ − 1367 @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
135
+ − 1368 know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
+ − 1369 this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
+ − 1370 and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
128
+ − 1371 otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
+ − 1372 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
+ − 1373 @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
135
+ − 1374 @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
128
+ − 1375 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
145
+ − 1376 `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.
128
+ − 1377
135
+ − 1378 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
128
+ − 1379 the following tagging-function:
132
+ − 1380 %
121
+ − 1381 \begin{center}
172
+ − 1382 @{thm tag_str_Star_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
121
+ − 1383 \end{center}
128
+ − 1384
+ − 1385 \begin{proof}[@{const STAR}-Case]
130
+ − 1386 If @{term "finite (UNIV // \<approx>A)"}
+ − 1387 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
+ − 1388 @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
+ − 1389 Again we have to show injectivity of this tagging-function as
132
+ − 1390 %
130
+ − 1391 \begin{center}
+ − 1392 @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
+ − 1393 \end{center}
132
+ − 1394 %
130
+ − 1395 \noindent
+ − 1396 We first need to consider the case that @{text x} is the empty string.
+ − 1397 From the assumption we can infer @{text y} is the empty string and
135
+ − 1398 clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
134
+ − 1399 string, we can divide the string @{text "x @ z"} as shown in the picture
135
+ − 1400 above. By the tagging-function we have
132
+ − 1401 %
130
+ − 1402 \begin{center}
+ − 1403 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
+ − 1404 \end{center}
132
+ − 1405 %
130
+ − 1406 \noindent
+ − 1407 which by assumption is equal to
132
+ − 1408 %
130
+ − 1409 \begin{center}
+ − 1410 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
+ − 1411 \end{center}
132
+ − 1412 %
130
+ − 1413 \noindent
135
+ − 1414 and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"}
132
+ − 1415 and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
135
+ − 1416 relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
+ − 1417 Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
174
+ − 1418 @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "lang r"} and
+ − 1419 complete the proof.
121
+ − 1420 \end{proof}
39
+ − 1421 *}
+ − 1422
162
+ − 1423 section {* Second Part based on Partial Derivatives *}
+ − 1424
+ − 1425 text {*
173
+ − 1426 \noindent
+ − 1427 As we have seen in the previous section, in order to establish
+ − 1428 the second direction of the Myhill-Nerode theorem, we need to find
174
+ − 1429 a more refined relation than @{term "\<approx>(lang r)"} for which we can
+ − 1430 show that there are only finitely many equivalence classes. So far we
+ − 1431 showed this by induction on @{text "r"}. However, there is also
+ − 1432 an indirect method to come up with such a refined relation. Assume
+ − 1433 the following two definitions for a left-quotient of a language, which
+ − 1434 we write as @{term "Der c A"} and @{term "Ders s A"} where
+ − 1435 @{text c} is a character and @{text s} a string:
+ − 1436
+ − 1437 \begin{center}
+ − 1438 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
+ − 1439 @{thm (lhs) Der_def} & @{text "\<equiv>"} & @{thm (rhs) Der_def}\\
+ − 1440 @{thm (lhs) Ders_def} & @{text "\<equiv>"} & @{thm (rhs) Ders_def}\\
+ − 1441 \end{tabular}
+ − 1442 \end{center}
+ − 1443
+ − 1444 \noindent
+ − 1445 Now clearly we have the following relation between the Myhill-Nerode relation
+ − 1446 (Definition~\ref{myhillneroderel}) and left-quotients
+ − 1447
+ − 1448 \begin{equation}\label{mhders}
+ − 1449 @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
+ − 1450 \end{equation}
+ − 1451
+ − 1452 \noindent
+ − 1453 It is realtively easy to establish the following identidies for left-quotients:
+ − 1454
+ − 1455 \begin{center}
+ − 1456 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
+ − 1457 @{thm (lhs) Der_zero} & $=$ & @{thm (rhs) Der_zero}\\
+ − 1458 @{thm (lhs) Der_one} & $=$ & @{thm (rhs) Der_one}\\
+ − 1459 @{thm (lhs) Der_atom} & $=$ & @{thm (rhs) Der_atom}\\
+ − 1460 @{thm (lhs) Der_union} & $=$ & @{thm (rhs) Der_union}\\
+ − 1461 @{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
+ − 1462 @{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\
+ − 1463 \end{tabular}
+ − 1464 \end{center}
+ − 1465
+ − 1466 \noindent
+ − 1467 where @{text "\<Delta>"} is a function that tests whether the empty string
+ − 1468 is in the language and returns @{term "{[]}"} or @{term "{}"}, respectively.
+ − 1469 The only interesting case above is the last one where we use Prop.~\ref{langprops}
+ − 1470 in order to infer that @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can
+ − 1471 then complete the proof by observing that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"}.
+ − 1472
+ − 1473 Brzozowski observed that the left-quotients for languages of regular
+ − 1474 expressions can be calculated directly via the notion of \emph{derivatives
+ − 1475 of a regular expressions} \cite{Brzozowski64} which we define in Isabelle/HOL as
+ − 1476 follows:
+ − 1477
+ − 1478 \begin{center}
+ − 1479 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ − 1480 @{thm (lhs) der.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(1)}\\
+ − 1481 @{thm (lhs) der.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
+ − 1482 @{thm (lhs) der.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) der.simps(3)[where c'="d"]}\\
+ − 1483 @{thm (lhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1484 & @{text "\<equiv>"} & @{thm (rhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1485 @{thm (lhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1486 & @{text "\<equiv>"}\\
+ − 1487 \multicolumn{3}{@ {\hspace{5mm}}l@ {}}{@{thm (rhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}}\\
+ − 1488 @{thm (lhs) der.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(6)}\smallskip\\
+ − 1489 @{thm (lhs) ders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) ders.simps(1)}\\
+ − 1490 @{thm (lhs) ders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) ders.simps(2)}\\
+ − 1491 \end{tabular}
+ − 1492 \end{center}
+ − 1493
+ − 1494 \noindent
+ − 1495 The function @{term "nullable r"} tests whether the regular expression
+ − 1496 can recognise the empty string:
+ − 1497
+ − 1498 \begin{center}
+ − 1499 \begin{tabular}{cc}
+ − 1500 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ − 1501 @{thm (lhs) nullable.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
+ − 1502 @{thm (lhs) nullable.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(2)}\\
+ − 1503 @{thm (lhs) nullable.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(3)}\\
+ − 1504 \end{tabular} &
+ − 1505 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ − 1506 @{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1507 & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1508 @{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1509 & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1510 @{thm (lhs) nullable.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(6)}\\
+ − 1511 \end{tabular}
+ − 1512 \end{tabular}
+ − 1513 \end{center}
+ − 1514
+ − 1515 \noindent
+ − 1516 Brzozowski proved
+ − 1517
+ − 1518 \begin{equation}\label{Dersders}
+ − 1519 \mbox{\begin{tabular}{l}
+ − 1520 @{thm Der_der}\\
+ − 1521 @{thm Ders_ders}
+ − 1522 \end{tabular}}
+ − 1523 \end{equation}
+ − 1524
+ − 1525 \noindent
+ − 1526 where the first is by induction on @{text r} and the second by a simple
+ − 1527 calculation.
+ − 1528
+ − 1529 The importance in the context of the Myhill-Nerode theorem is that
+ − 1530 we can use \eqref{mhders} and \eqref{Dersders} in order to derive
+ − 1531
+ − 1532 \begin{center}
+ − 1533 @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}
+ − 1534 @{term "lang (ders x r) = lang (ders y r)"}
+ − 1535 \end{center}
+ − 1536
+ − 1537 \noindent
+ − 1538 which means @{term "x \<approx>(lang r) y"} provided @{term "ders x r = ders y r"}.
+ − 1539 Consequently, we can use as the tagging relation
+ − 1540 @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, which we know refines @{term "\<approx>(lang r)"}.
+ − 1541 This almost helps us because Brozowski also proved that there for every
+ − 1542 language there are only
+ − 1543 finitely `dissimilar' derivatives for a regular expression. Two regulare
+ − 1544 expressions are similar if they can be identified using the using the
+ − 1545 ACI-identities
+ − 1546
+ − 1547 \begin{center}
+ − 1548 \begin{tabular}{cl}
+ − 1549 (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)"}\\
+ − 1550 (C) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
+ − 1551 (I) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
+ − 1552 \end{tabular}
+ − 1553 \end{center}
+ − 1554
+ − 1555 \noindent
+ − 1556 Without the indentification, we unfortunately obtain infinitely many
+ − 1557 derivations (an example is given in \cite[Page~141]{Sakarovitch09}).
+ − 1558 Reasoning modulo ACI can be done, but it is very painful in a theorem prover.
+ − 1559
175
+ − 1560 Fortunately, there is a much simpler approach using partial
+ − 1561 derivatives introduced by Antimirov \cite{Antimirov95}.
173
+ − 1562
175
+ − 1563 \begin{center}
+ − 1564 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ − 1565 @{thm (lhs) pder.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(1)}\\
+ − 1566 @{thm (lhs) pder.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(2)}\\
+ − 1567 @{thm (lhs) pder.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(3)[where c'="d"]}\\
+ − 1568 @{thm (lhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1569 & @{text "\<equiv>"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 1570 @{thm (lhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ − 1571 & @{text "\<equiv>"}\\
+ − 1572 \multicolumn{3}{@ {\hspace{20mm}}l@ {}}{@{thm (rhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}}\\
+ − 1573 @{thm (lhs) pder.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(6)}\smallskip\\
+ − 1574 @{thm (lhs) pders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(1)}\\
+ − 1575 @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+ − 1576 \end{tabular}
+ − 1577 \end{center}
173
+ − 1578
162
+ − 1579 *}
+ − 1580
+ − 1581 section {* Closure Properties *}
39
+ − 1582
117
+ − 1583
54
+ − 1584 section {* Conclusion and Related Work *}
+ − 1585
92
+ − 1586 text {*
112
+ − 1587 In this paper we took the view that a regular language is one where there
115
+ − 1588 exists a regular expression that matches all of its strings. Regular
145
+ − 1589 expressions can conveniently be defined as a datatype in HOL-based theorem
+ − 1590 provers. For us it was therefore interesting to find out how far we can push
154
+ − 1591 this point of view. We have established in Isabelle/HOL both directions
+ − 1592 of the Myhill-Nerode theorem.
132
+ − 1593 %
167
+ − 1594 \begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
132
+ − 1595 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
167
+ − 1596 \end{thrm}
132
+ − 1597 %
+ − 1598 \noindent
+ − 1599 Having formalised this theorem means we
+ − 1600 pushed our point of view quite far. Using this theorem we can obviously prove when a language
112
+ − 1601 is \emph{not} regular---by establishing that it has infinitely many
+ − 1602 equivalence classes generated by the Myhill-Nerode relation (this is usually
+ − 1603 the purpose of the pumping lemma \cite{Kozen97}). We can also use it to
+ − 1604 establish the standard textbook results about closure properties of regular
+ − 1605 languages. Interesting is the case of closure under complement, because
+ − 1606 it seems difficult to construct a regular expression for the complement
113
+ − 1607 language by direct means. However the existence of such a regular expression
+ − 1608 can be easily proved using the Myhill-Nerode theorem since
132
+ − 1609 %
112
+ − 1610 \begin{center}
+ − 1611 @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+ − 1612 \end{center}
132
+ − 1613 %
112
+ − 1614 \noindent
+ − 1615 holds for any strings @{text "s\<^isub>1"} and @{text
114
+ − 1616 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
159
+ − 1617 partitions. Proving the existence of such a regular expression via automata
+ − 1618 using the standard method would
114
+ − 1619 be quite involved. It includes the
112
+ − 1620 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
+ − 1621 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
+ − 1622 regular expression.
+ − 1623
116
+ − 1624 While regular expressions are convenient in formalisations, they have some
122
+ − 1625 limitations. One is that there seems to be no method of calculating a
123
+ − 1626 minimal regular expression (for example in terms of length) for a regular
+ − 1627 language, like there is
+ − 1628 for automata. On the other hand, efficient regular expression matching,
+ − 1629 without using automata, poses no problem \cite{OwensReppyTuron09}.
+ − 1630 For an implementation of a simple regular expression matcher,
122
+ − 1631 whose correctness has been formally established, we refer the reader to
+ − 1632 Owens and Slind \cite{OwensSlind08}.
116
+ − 1633
+ − 1634
143
+ − 1635 Our formalisation consists of 780 lines of Isabelle/Isar code for the first
149
+ − 1636 direction and 460 for the second, plus around 300 lines of standard material about
122
+ − 1637 regular languages. While this might be seen as too large to count as a
+ − 1638 concise proof pearl, this should be seen in the context of the work done by
+ − 1639 Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
+ − 1640 in Nuprl using automata. They write that their four-member team needed
134
+ − 1641 something on the magnitude of 18 months for their formalisation. The
122
+ − 1642 estimate for our formalisation is that we needed approximately 3 months and
+ − 1643 this included the time to find our proof arguments. Unlike Constable et al,
+ − 1644 who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
+ − 1645 find our own arguments. So for us the formalisation was not the
+ − 1646 bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
+ − 1647 from what is shown in the Nuprl Math Library about their development it
+ − 1648 seems substantially larger than ours. The code of ours can be found in the
+ − 1649 Mercurial Repository at
132
+ − 1650 \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
113
+ − 1651
112
+ − 1652
+ − 1653 Our proof of the first direction is very much inspired by \emph{Brzozowski's
134
+ − 1654 algebraic method} used to convert a finite automaton to a regular
113
+ − 1655 expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
111
+ − 1656 classes as the states of the minimal automaton for the regular language.
114
+ − 1657 However there are some subtle differences. Since we identify equivalence
111
+ − 1658 classes with the states of the automaton, then the most natural choice is to
+ − 1659 characterise each state with the set of strings starting from the initial
113
+ − 1660 state leading up to that state. Usually, however, the states are characterised as the
123
+ − 1661 strings starting from that state leading to the terminal states. The first
+ − 1662 choice has consequences about how the initial equational system is set up. We have
115
+ − 1663 the $\lambda$-term on our `initial state', while Brzozowski has it on the
111
+ − 1664 terminal states. This means we also need to reverse the direction of Arden's
156
+ − 1665 Lemma.
92
+ − 1666
162
+ − 1667 This is also where our method shines, because we can completely
+ − 1668 side-step the standard argument \cite{Kozen97} where automata need
+ − 1669 to be composed, which as stated in the Introduction is not so easy
+ − 1670 to formalise in a HOL-based theorem prover. However, it is also the
+ − 1671 direction where we had to spend most of the `conceptual' time, as
+ − 1672 our proof-argument based on tagging-functions is new for
+ − 1673 establishing the Myhill-Nerode theorem. All standard proofs of this
+ − 1674 direction proceed by arguments over automata.\medskip
172
+ − 1675
173
+ − 1676 We expect that the development of Krauss \& Nipkow gets easier by
+ − 1677 using partial derivatives.\medskip
162
+ − 1678
+ − 1679 \noindent
173
+ − 1680 {\bf Acknowledgements:}
+ − 1681 We are grateful for the comments we received from Larry
162
+ − 1682 Paulson.
111
+ − 1683
92
+ − 1684 *}
+ − 1685
+ − 1686
24
+ − 1687 (*<*)
+ − 1688 end
+ − 1689 (*>*)