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