--- a/Journal/Paper.thy Thu Jul 28 17:52:36 2011 +0000
+++ b/Journal/Paper.thy Sun Jul 31 10:27:41 2011 +0000
@@ -39,8 +39,8 @@
notation (latex output)
- str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
- str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
+ str_eq ("\<approx>\<^bsub>_\<^esub>") and
+ str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and
conc (infixr "\<cdot>" 100) and
star ("_\<^bsup>\<star>\<^esup>") and
pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
@@ -59,13 +59,13 @@
Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
- tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
- tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
- tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
- tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
- tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
- tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
- tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
+ tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
+ tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
+ tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+ tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+ tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
+ tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
+ tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
Delta ("\<Delta>'(_')") and
nullable ("\<delta>'(_')") and
Cons ("_ :: _" [100, 100] 100)
@@ -74,6 +74,10 @@
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
by auto
+lemma str_eq_def':
+ shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)"
+unfolding str_eq_def by simp
+
lemma conc_def':
"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}"
unfolding conc_def by simp
@@ -174,7 +178,7 @@
\begin{center}
\begin{tabular}{ccc}
- \begin{tikzpicture}[scale=0.9]
+ \begin{tikzpicture}[scale=1]
%\draw[step=2mm] (-1,-1) grid (1,1);
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
@@ -190,8 +194,8 @@
\node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
- \draw (-0.6,0.0) node {\footnotesize$A_1$};
- \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ \draw (-0.6,0.0) node {\small$A_1$};
+ \draw ( 0.6,0.0) node {\small$A_2$};
\end{tikzpicture}
&
@@ -200,7 +204,7 @@
&
- \begin{tikzpicture}[scale=0.9]
+ \begin{tikzpicture}[scale=1]
%\draw[step=2mm] (-1,-1) grid (1,1);
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
@@ -219,8 +223,8 @@
\draw (C) to [very thick, bend left=45] (B);
\draw (D) to [very thick, bend right=45] (B);
- \draw (-0.6,0.0) node {\footnotesize$A_1$};
- \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ \draw (-0.6,0.0) node {\small$A_1$};
+ \draw ( 0.6,0.0) node {\small$A_2$};
\end{tikzpicture}
\end{tabular}
@@ -300,7 +304,7 @@
everything is crystal clear. However, paper proofs about automata often
involve subtle side-conditions which are easily overlooked, but which make
formal reasoning rather painful. For example Kozen's proof of the
- Myhill-Nerode theorem requires that the automata do not have inaccessible
+ Myhill-Nerode theorem requires that automata do not have inaccessible
states \cite{Kozen97}. Another subtle side-condition is completeness of
automata, that is automata need to have total transition functions and at most one
`sink' state from which there is no connection to a final state (Brozowski
@@ -346,7 +350,7 @@
To our best knowledge, our proof of the Myhill-Nerode theorem is the first
that is based on regular expressions, only. The part of this theorem stating
that finitely many partitions imply regularity of the language is proved by
- an argument about solving equational sytems. This argument appears to be
+ an argument about solving equational systems. This argument appears to be
folklore. For the other part, we give two proofs: one direct proof using
certain tagging-functions, and another indirect proof using Antimirov's
partial derivatives \cite{Antimirov95}. Again to our best knowledge, the
@@ -403,10 +407,11 @@
the proofs for these properties, but invite the reader to consult our
formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
- The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
- equivalence relation @{term REL} is @{term "A // REL"}. We will write
- @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
- as \mbox{@{text "{y | y \<approx> x}"}}.
+ The notation in Isabelle/HOL for the quotient of a language @{text A}
+ according to an equivalence relation @{term REL} is @{term "A // REL"}. We
+ will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as
+ \mbox{@{text "{y | y \<approx> x}"}}, and have @{text "x \<approx> y"} if and only if @{text
+ "\<lbrakk>x\<rbrakk>\<^isub>\<approx> = \<lbrakk>y\<rbrakk>\<^isub>\<approx>"}.
Central to our proof will be the solution of equational systems
@@ -426,9 +431,9 @@
\begin{proof}
For the right-to-left direction we assume @{thm (rhs) arden} and show
that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
- we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
- which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both
- sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
+ we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
+ which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
+ sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction.
For the other direction we assume @{thm (lhs) arden}. By a simple induction
@@ -515,7 +520,7 @@
Given a language @{text A}, two strings @{text x} and
@{text y} are Myhill-Nerode related provided
\begin{center}
- @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
+ @{thm str_eq_def'}
\end{center}
\end{dfntn}
@@ -641,7 +646,7 @@
\noindent
where @{text "d\<^isub>1\<dots>d\<^isub>n"} is the sequence of all characters
- except @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
+ but not containing @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
characters.
Overloading the function @{text \<calL>} for the two kinds of terms in the
@@ -1067,7 +1072,7 @@
text {*
\noindent
- In this section and the next we will give two proofs for establishing the second
+ In this section we will give a proof for establishing the second
part of the Myhill-Nerode theorem. It can be formulated in our setting as follows:
\begin{thrm}
@@ -1075,7 +1080,7 @@
\end{thrm}
\noindent
- The first proof will be by induction on the structure of @{text r}. It turns out
+ The proof will be by induction on the structure of @{text r}. It turns out
the base cases are straightforward.
@@ -1099,11 +1104,11 @@
Much more interesting, however, are the inductive cases. They seem hard to solve
directly. The reader is invited to try.
- In order how to see how our first proof proceeds we use the following suggestive picture
- from Constable et al \cite{Constable00}:
+ In order to see how our proof proceeds consider the following suggestive picture
+ taken from Constable et al \cite{Constable00}:
- \begin{center}
- \begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
+ \begin{equation}\label{pics}
+ \mbox{\begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
\begin{tikzpicture}[scale=1]
%Circle
\draw[thick] (0,0) circle (1.1);
@@ -1129,10 +1134,17 @@
\draw (\a: 0.77) node {$a_{\l}$};
\end{tikzpicture}\\
@{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
- Our first proof will rely on some
+ \noindent
+ The relation @{term "\<approx>(lang r)"} partitions the set of all strings into some
+ equivalence classes. To show that there are only finitely many of
+ them, it suffices to show in each induction step the existence of another
+ relation, say @{text R}, for which we can show that there are finitely many
+ equivalence classes and which refines @{term "\<approx>(lang r)"}. A relation @{text
+ "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text
+ "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will rely on some
\emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will
be easy to prove that the \emph{range} of these tagging-functions is finite.
The range of a function @{text f} is defined as
@@ -1142,13 +1154,14 @@
\end{center}
\noindent
- that means we take the image of @{text f} w.r.t.~all elements in the domain.
- With this we will be able to infer that the tagging-functions, seen as relations,
- give rise to finitely many equivalence classes of @{const UNIV}. Finally we
- will show that the tagging-relations are more refined than @{term "\<approx>(lang r)"}, which
- implies that @{term "UNIV // \<approx>(lang r)"} must also be finite---a relation @{text "R\<^isub>1"}
- is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
- We formally define the notion of a \emph{tagging-relation} as follows.
+ that means we take the image of @{text f} w.r.t.~all elements in the
+ domain. With this we will be able to infer that the tagging-functions, seen
+ as relations, give rise to finitely many equivalence classes of @{const
+ UNIV}. Finally we will show that the tagging-relations are more refined than
+ @{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
+ also be finite. We formally define the notion of a \emph{tagging-relation}
+ as follows.
+
\begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
and @{text y} are \emph{tag-related} provided
@@ -1212,7 +1225,7 @@
\noindent
Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
- that @{term "UNIV // \<approx>(lang r)"} is finite, we have to find a tagging-function whose
+ that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
Let us attempt the @{const PLUS}-case first.
@@ -1220,14 +1233,14 @@
We take as tagging-function
%
\begin{center}
- @{thm tag_str_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
+ @{thm tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
\end{center}
\noindent
where @{text "A"} and @{text "B"} are some arbitrary languages.
We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
- @{term "tag_str_Plus A B"} is a subset of this product set---so finite. It remains to be shown
+ @{term "tag_Plus A B"} is a subset of this product set---so finite. It remains to be shown
that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
showing
%
@@ -1269,17 +1282,21 @@
notions of \emph{string prefixes}
%
\begin{center}
- @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+ \begin{tabular}{l}
+ @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\
@{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+ \end{tabular}
\end{center}
%
\noindent
and \emph{string subtraction}:
%
\begin{center}
- @{text "[] - y \<equiv> []"}\hspace{10mm}
- @{text "x - [] \<equiv> x"}\hspace{10mm}
- @{text "cx - dy \<equiv> if c = d then x - y else cx"}
+ \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
+ @{text "x - []"} & @{text "\<equiv>"} & @{text "x"}\\
+ @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}
+ \end{tabular}
\end{center}
%
\noindent
@@ -1289,8 +1306,8 @@
this string to be in @{term "A \<cdot> B"}:
%
\begin{center}
- \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
- \scalebox{0.7}{
+ \begin{tabular}{c}
+ \scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
@@ -1316,8 +1333,8 @@
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{@{term "x' \<in> A"}};
\end{tikzpicture}}
- &
- \scalebox{0.7}{
+ \\
+ \scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
@@ -1353,7 +1370,7 @@
following tagging-function
%
\begin{center}
- @{thm tag_str_Times_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+ @{thm tag_Times_def[where ?A="A" and ?B="B", THEN meta_eq_app]}
\end{center}
\noindent
@@ -1363,11 +1380,11 @@
\begin{proof}[@{const TIMES}-Case]
If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
- @{term "tag_str_TIMES A B"} is a subset of this product set, and therefore finite.
+ @{term "tag_Times 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_TIMES A B x = tag_str_TIMES A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
+ @{term "\<forall>z. tag_Times A B x = tag_Times A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
\end{center}
%
\noindent
@@ -1380,7 +1397,7 @@
\end{center}
%
\noindent
- and by the assumption about @{term "tag_str_TIMES A B"} also
+ and by the assumption about @{term "tag_Times A B"} also
%
\begin{center}
@{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
@@ -1395,7 +1412,7 @@
@{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
- By the assumption about @{term "tag_str_TIMES A B"} we have
+ By the assumption about @{term "tag_Times A B"} we have
@{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const TIMES}-case
@@ -1467,17 +1484,17 @@
the following tagging-function:
%
\begin{center}
- @{thm tag_str_Star_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
+ @{thm tag_Star_def[where ?A="A", THEN meta_eq_app]}\smallskip
\end{center}
\begin{proof}[@{const Star}-Case]
If @{term "finite (UNIV // \<approx>A)"}
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.
+ @{term "tag_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>"}
+ @{term "\<forall>z. tag_Star A x = tag_Star A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
\end{center}
%
\noindent