--- a/Paper/Paper.thy Thu Apr 28 03:24:20 2011 +0000
+++ b/Paper/Paper.thy Wed May 04 07:05:59 2011 +0000
@@ -76,8 +76,8 @@
HOLlight support them with libraries. Even worse, reasoning about graphs and
matrices can be a real hassle in HOL-based theorem provers. Consider for
example the operation of sequencing two automata, say $A_1$ and $A_2$, by
- connecting the accepting states of $A_1$ to the initial state of $A_2$:
-
+ connecting the accepting states of $A_1$ to the initial state of $A_2$:\\[-5.5mm]
+ %
\begin{center}
\begin{tabular}{ccc}
\begin{tikzpicture}[scale=0.8]
@@ -199,7 +199,7 @@
are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
In this paper, we will not attempt to formalise automata theory in
- Isabelle/HOL, but take a completely different approach to regular
+ Isabelle/HOL, but take a different approach to regular
languages. Instead of defining a regular language as one where there exists
an automaton that recognises all strings of the language, we define a
regular language as:
@@ -225,7 +225,7 @@
\noindent
{\bf Contributions:}
There is an extensive literature on regular languages.
- To our knowledge, our proof of the Myhill-Nerode theorem is the
+ To our best knowledge, our proof of the Myhill-Nerode theorem is the
first that is based on regular expressions, only. We prove the part of this theorem
stating that a regular expression has only finitely many partitions using certain
tagging-functions. Again to our best knowledge, these tagging-functions have
@@ -465,14 +465,18 @@
\noindent
where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
- X\<^isub>i"}. If viewed as an automaton, then every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
- corresponds roughly to a state whose name is @{text X\<^isub>i} and its predecessor states
- are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
- predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be
+ X\<^isub>i"}.
+ %The intuition behind the equational system is that every
+ %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+ %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
+ %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
+ %predecessor states to @{text X\<^isub>i}.
+ There can only be
finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side
since by assumption there are only finitely many
- equivalence classes and only finitely many characters. The term @{text
- "\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
+ equivalence classes and only finitely many characters.
+ The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the initial state, that
+ is the equivalence class
containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
single `initial' state in the equational system, which is different from
the method by Brzozowski \cite{Brzozowski64}, where he marks the
@@ -481,6 +485,10 @@
transitions---the successor `state' of an equivalence class @{text Y} can
be reached by adding a character to the end of @{text Y}. This is also the
reason why we have to use our reverse version of Arden's Lemma.}
+ %In our initial equation system there can only be
+ %finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side
+ %since by assumption there are only finitely many
+ %equivalence classes and only finitely many characters.
Overloading the function @{text \<calL>} for the two kinds of terms in the
equational system, we have
@@ -501,7 +509,7 @@
hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
%
\begin{equation}\label{inv2}
- @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
+ @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
\end{equation}
\noindent
@@ -653,7 +661,7 @@
\noindent
The last definition we need applies @{term Iter} over and over until a condition
- @{text Cond} is \emph{not} satisfied anymore. The condition states that there
+ @{text Cond} is \emph{not} satisfied anymore. This condition states that there
are more than one equation left in the equational system @{text ES}. To solve
an equational system we use Isabelle/HOL's @{text while}-operator as follows:
@@ -854,12 +862,7 @@
in @{term "finals A"} there exists a regular expression. Moreover by assumption
we know that @{term "finals A"} must be finite, and therefore there must be a finite
set of regular expressions @{text "rs"} such that
-
- \begin{center}
- @{term "\<Union>(finals A) = L (\<Uplus>rs)"}
- \end{center}
-
- \noindent
+ @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
as the regular expression that is needed in the theorem.\qed
\end{proof}
@@ -917,7 +920,7 @@
\begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
and @{text y} are \emph{tag-related} provided
\begin{center}
- @{text "x =tag= y \<equiv> tag x = tag y"}.
+ @{text "x =tag= y \<equiv> tag x = tag y"}\;.
\end{center}
\end{definition}
@@ -1041,11 +1044,9 @@
and \emph{string subtraction}:
%
\begin{center}
- \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}
+ @{text "[] - y \<equiv> []"}\hspace{10mm}
+ @{text "x - [] \<equiv> x"}\hspace{10mm}
+ @{text "cx - dy \<equiv> if c = d then x - y else cx"}
\end{center}
%
\noindent
@@ -1055,11 +1056,12 @@
this string to be in @{term "A ;; B"}:
%
\begin{center}
+ \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
\scalebox{0.7}{
\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'"}\hspace{4em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'"}\hspace{0.5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}@{text z}\hspace{10.1em}$ };
+ \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}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
@@ -1081,12 +1083,12 @@
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{@{term "x' \<in> A"}};
\end{tikzpicture}}
-
+ &
\scalebox{0.7}{
\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}@{text x}\hspace{6.5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}@{text "z'"}\hspace{2em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}@{text "z - z'"}\hspace{6.1em}$ };
+ \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}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(x.north west) -- ($(za.north west)+(0em,0em)$)
@@ -1108,6 +1110,7 @@
($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
\end{tikzpicture}}
+ \end{tabular}
\end{center}
%
\noindent
@@ -1307,7 +1310,8 @@
\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
- partitions. Proving the existence of such a regular expression via automata would
+ partitions. Proving the existence of such a regular expression via automata
+ using the standard method would
be quite involved. It includes the
steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
"\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
@@ -1359,22 +1363,28 @@
We briefly considered using the method Brzozowski presented in the Appendix
of~\cite{Brzozowski64} in order to prove the second direction of the
Myhill-Nerode theorem. There he calculates the derivatives for regular
- expressions and shows that there can be only finitely many of them with
- respect to a language (if regarded equal modulo ACI). We could
- have used as the tag of a string @{text s} the set of derivatives of a regular expression
- generated by a language. Using the fact that two strings are
+ expressions and shows that for every language there can be only
+ finitely many of them %derivations
+ (if regarded equal modulo ACI). We could
+ have used as tagging-function the set of derivatives of a regular expression
+ with respect to a language. Using the fact that two strings are
Myhill-Nerode related whenever their derivative is the same, together with
the fact that there are only finitely such derivatives
would give us a similar argument as ours. However it seems not so easy to
- calculate the set of derivatives modulo ACI and then to count them. Therefore we preferred our
+ calculate the set of derivatives modulo ACI. Therefore we preferred our
direct method of using tagging-functions. This
is also where our method shines, because we can completely side-step the
standard argument \cite{Kozen97} where automata need to be composed, which
- as stated in the Introduction is not so convenient to formalise in a
+ as stated in the Introduction is not so easy to formalise in a
HOL-based theorem prover. However, it is also the direction where we had to
spend most of the `conceptual' time, as our proof-argument based on tagging-functions
is new for establishing the Myhill-Nerode theorem. All standard proofs
- of this direction proceed by arguments over automata.
+ of this direction use %proceed by
+ arguments over automata.\\[-6mm]%\medskip
+ %
+ %\noindent
+ %{\bf Acknowledgements:} We are grateful for the comments we received from Larry
+ %Paulson and the referees of the paper.
*}