--- a/Paper/Paper.thy Sun Feb 20 17:47:54 2011 +0000
+++ b/Paper/Paper.thy Sun Feb 20 18:54:31 2011 +0000
@@ -355,7 +355,8 @@
\end{center}
Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
- a regular expression that matches all languages of @{text rs}. We only need to know the existence
+ a regular expression that matches the union of all languages of @{text rs}. We only need to know the
+ existence
of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
@{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
@@ -369,7 +370,8 @@
image of the set @{text rs} under function @{text "\<calL>"}.
*}
-section {* The Myhill-Nerode Theorem, First Part *}
+
+section {* The Myhill-Nerode Theorem *}
text {*
The key definition in the Myhill-Nerode theorem is the
@@ -416,7 +418,8 @@
\end{equation}
\noindent
- In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
+ In our running example, @{text "X\<^isub>2"} is the only
+ equivalence class in @{term "finals {[c]}"}.
It is straightforward to show that in general @{thm lang_is_union_of_finals} and
@{thm finals_in_partitions} hold.
Therefore if we know that there exists a regular expression for every
@@ -577,7 +580,7 @@
\end{center}
\noindent
- This allows us to prove
+ This allows us to prove a version of Arden's lemma on the level of equations.
\begin{lemma}\label{ardenable}
Given an equation @{text "X = rhs"}.
@@ -757,9 +760,9 @@
cannot make a regular expression to match the empty string. Validity is
given because @{const Arden} removes an equivalence class from @{text yrhs}
and then @{const Subst_all} removes @{text Y} from the equational system.
- Having proved the implication above, we can replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+ Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
which matches with our proof-obligation of @{const "Subst_all"}. Since
- \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use our assumption
+ \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption
to complete the proof.\qed
\end{proof}
@@ -972,7 +975,7 @@
\begin{proof}[@{const "ALT"}-Case]
We take as tagging function
-
+ %
\begin{center}
@{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
\end{center}
@@ -988,14 +991,14 @@
\begin{center}
@{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
\end{center}
-
+ %
\noindent
which by unfolding the Myhill-Nerode relation is identical to
%
\begin{equation}\label{pattern}
@{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
\end{equation}
-
+ %
\noindent
since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
\eqref{pattern} we just have to unfold the definition of the tagging-relation and analyse
@@ -1011,25 +1014,25 @@
The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
they are slightly more complicated. In the @{const SEQ}-case we essentially have
to be able to infer that
-
+ %
\begin{center}
@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
\end{center}
-
+ %
\noindent
using the information given by the appropriate tagging function. The complication
is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
(this was easy in case of @{term "A \<union> B"}). For this we define the
notions of \emph{string prefixes}
-
+ %
\begin{center}
@{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
@{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
\end{center}
-
+ %
\noindent
and \emph{string subtraction}:
-
+ %
\begin{center}
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
@@ -1037,12 +1040,13 @@
@{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\
\end{tabular}
\end{center}
-
+ %
\noindent
where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
+
Now assuming @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split'
this string to be in @{term "A ;; B"}:
-
+ %
\begin{center}
\scalebox{0.7}{
\begin{tikzpicture}
@@ -1098,19 +1102,19 @@
node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
\end{tikzpicture}}
\end{center}
-
+ %
\noindent
Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the
following tagging-function
-
+ %
\begin{center}
@{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
\end{center}
\noindent
- with the idea that in the first split we have to make sure that @{text "x - x'"}
+ with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
is in the language @{text B}.
\begin{proof}[@{const SEQ}-Case]
@@ -1118,27 +1122,27 @@
then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
@{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
We have to show injectivity of this tagging-function as
-
+ %
\begin{center}
@{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
\end{center}
-
+ %
\noindent
There are two cases to be considered (see pictures above). First, there exists
a @{text "x'"} such that
@{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
-
+ %
\begin{center}
@{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
\end{center}
-
+ %
\noindent
and by the assumption about @{term "tag_str_SEQ A B"} also
-
+ %
\begin{center}
@{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
\end{center}
-
+ %
\noindent
That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and
@{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
@@ -1160,7 +1164,7 @@
we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the
empty string, we
have the following picture:
-
+ %
\begin{center}
\scalebox{0.7}{
\begin{tikzpicture}
@@ -1198,7 +1202,7 @@
node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
\end{tikzpicture}}
\end{center}
-
+ %
\noindent
We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"},
@{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string
@@ -1218,9 +1222,9 @@
In order to show that @{text "x @ z \<in> A\<star>"} implies @{text "y @ z \<in> A\<star>"}, we use
the following tagging-function:
-
+ %
\begin{center}
- @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
+ @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
\end{center}
\begin{proof}[@{const STAR}-Case]
@@ -1228,36 +1232,36 @@
then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
@{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
Again we have to show injectivity of this tagging-function as
-
+ %
\begin{center}
@{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
\end{center}
-
+ %
\noindent
We first need to consider the case that @{text x} is the empty string.
From the assumption we can infer @{text y} is the empty string and
clearly have @{text "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
string, we can devide the string @{text "x @ z"} as shown in the picture
above. By the tagging function we have
-
+ %
\begin{center}
@{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
\end{center}
-
+ %
\noindent
which by assumption is equal to
-
+ %
\begin{center}
@{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
\end{center}
-
+ %
\noindent
- and we know that we have a @{text "y'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"} and @{text "y'\<^isub>m\<^isub>a\<^isub>x < y"}
- and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y'\<^isub>m\<^isub>a\<^isub>x)"}. Unfolding the Myhill-Nerode
- relation we know @{term "(y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}. We also know that @{text "z\<^isub>b \<in> A\<star>"}.
- Therefore, finally, @{text "y'\<^isub>m\<^isub>a\<^isub>x @ ((y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
- @{term "y @ z \<in> A\<star>"}. As a last step we have to set @{text "A"} to @{text "L r"} and
- complete the proof.
+ and we know that we have a @{text "y' \<in> A\<star>"} and @{text "y' < y"}
+ and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
+ relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{text "z\<^isub>b \<in> A\<star>"}.
+ Therefore, finally, @{text "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+ @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{text "L r"} and
+ complete the proof.\qed
\end{proof}
*}
@@ -1270,10 +1274,16 @@
exists a regular expression that matches all of its strings. Regular
expressions can conveniently be defined as a datatype in a HOL-based theorem
prover. For us it was therefore interesting to find out how far we can push
- this point of view.
-
- Having formalised the Myhill-Nerode theorem means we
- pushed quite far. Using this theorem we can obviously prove when a language
+ this point of view. We have establised both directions of the Myhill-Nerode
+ theorem.
+ %
+ \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+ A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
+ \end{theorem}
+ %
+ \noindent
+ Having formalised this theorem means we
+ pushed our point of view quite far. Using this theorem we can obviously prove when a language
is \emph{not} regular---by establishing that it has infinitely many
equivalence classes generated by the Myhill-Nerode relation (this is usually
the purpose of the pumping lemma \cite{Kozen97}). We can also use it to
@@ -1282,11 +1292,11 @@
it seems difficult to construct a regular expression for the complement
language by direct means. However the existence of such a regular expression
can be easily proved using the Myhill-Nerode theorem since
-
+ %
\begin{center}
@{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
\end{center}
-
+ %
\noindent
holds for any strings @{text "s\<^isub>1"} and @{text
"s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
@@ -1322,10 +1332,7 @@
from what is shown in the Nuprl Math Library about their development it
seems substantially larger than ours. The code of ours can be found in the
Mercurial Repository at
-
- \begin{center}
- \url{http://www4.in.tum.de/~urbanc/regexp.html}
- \end{center}
+ \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
Our proof of the first direction is very much inspired by \emph{Brzozowski's