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