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