
diff -r a9598a206c41 -r 40b8d485ce8d Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Sep 06 02:52:26 2011 +0000
+++ b/Journal/Paper.thy	Wed Sep 07 09:28:13 2011 +0000
@@ -382,7 +382,7 @@
   larger formalisations of automata theory are carried out in Nuprl
   \cite{Constable00} and in Coq, e.g.~\cite{Filliatre97,Almeidaetal10}.
 
-  Also one might consider that automata are convenient `vehicles' for
+  Also, one might consider automata as just convenient `vehicles' for
   establishing properties about regular languages.  However, paper proofs
   about automata often involve subtle side-conditions which are easily
   overlooked, but which make formal reasoning rather painful. For example
@@ -397,8 +397,8 @@
   Definition~\ref{baddef}), then we need a lemma which ensures that another
   equivalent one can be found satisfying the side-condition, and also need to
   make sure our operations on automata preserve them. Unfortunately, such
-  `little' and `obvious' lemmas make a formalisation of automata theory a
-  hair-pulling experience.
+  `little' and `obvious' lemmas make formalisations of automata theory 
+  hair-pulling experiences.
 
   In this paper, we will not attempt to formalise automata theory in
   Isabelle/HOL nor will we attempt to formalise automata proofs from the
@@ -426,9 +426,9 @@
   regular expressions. This theorem gives necessary and sufficient conditions
   for when a language is regular. As a corollary of this theorem we can easily
   establish the usual closure properties, including complementation, for
-  regular languages. We also use in one example the continuation lemma, which
-  is based on Myhill-Nerode, for establishing non-regularity of languages 
-  \cite{Rosenberg06}.\medskip
+  regular languages. We use the continuation lemma \cite{Rosenberg06}, 
+  which is also a corollary of the Myhill-Nerode theorem, for establishing 
+  the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip
   
   \noindent 
   {\bf Contributions:} There is an extensive literature on regular languages.
@@ -439,7 +439,7 @@
   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
-  tagging-functions have not been used before to establish the Myhill-Nerode
+  tagging-functions have not been used before for establishing the Myhill-Nerode
   theorem. Derivatives of regular expressions have been used recently quite
   widely in the literature; partial derivatives, in contrast, attract much
   less attention. However, partial derivatives are more suitable in the
@@ -1166,11 +1166,12 @@
   \end{proof}
 
   \noindent
-  Note that solving our equational system also gives us a method for
-  calculating the regular expression for a complement of a regular language:
-  similar to the construction on automata, if we combine all regular
+  Note that our algorithm for solving equational systems provides also a method for
+  calculating a regular expression for the complement of a regular language:
+  if we combine all regular
   expressions corresponding to equivalence classes not in @{term "finals A"},
-  we obtain a regular expression for the complement @{term "- A"}.
+  then we obtain a regular expression for the complement language @{term "- A"}.
+  This is similar to the usual construction of a `complement automaton'.
 *}
 
 
@@ -1252,7 +1253,7 @@
   R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. 
 
   \begin{dfntn}
-  A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}
+  A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"}
   provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. 
   \end{dfntn}
 
@@ -1698,14 +1699,12 @@
   \end{equation}
 
   \noindent
-  where @{text "\<Delta>"} in the fifth line is a function that tests whether the
-  empty string is in the language and returns @{term "{[]}"} or @{term "{}"},
-  accordingly.  Note also that in the last equation we use the list-cons operator written
+  Note that in the last equation we use the list-cons operator written
   \mbox{@{text "_ :: _"}}.  The only interesting case is the case of @{term "A\<star>"}
   where we use Property~\ref{langprops}@{text "(i)"} in order to infer that
   @{term "Deriv c (A\<star>) = Deriv c (A \<cdot> A\<star>)"}. We can then complete the proof by
-  using the fifth equation and noting that @{term "Delta A \<cdot> Deriv c (A\<star>) \<subseteq> (Deriv
-  c A) \<cdot> A\<star>"}. 
+  using the fifth equation and noting that @{term "Deriv c (A\<star>) \<subseteq> (Deriv
+  c A) \<cdot> A\<star>"} provided @{text "[] \<in> A"}. 
 
   Brzozowski observed that the left-quotients for languages of
   regular expressions can be calculated directly using the notion of
@@ -1928,7 +1927,7 @@
   that by using sets, partial derivatives have the @{text "ACI"}-identities
   of derivatives already built in. 
 
-  Antimirov also proved that for every language and regular expression 
+  Antimirov also proved that for every language and every regular expression 
   there are only finitely many partial derivatives, whereby the set of partial
   derivatives of @{text r} w.r.t.~a language @{text A} is defined as
 
@@ -2005,8 +2004,8 @@
   \noindent
   Now the range of @{term "\<lambda>x. pderivs x r"} is a subset of @{term "Pow (pderivs_lang UNIV r)"},
   which we know is finite by Theorem~\ref{antimirov}. Consequently there 
-  are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"},
-  which refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the 
+  are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"}.
+  This relation refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the 
   second part of the Myhill-Nerode theorem.
   \end{proof}
 *}
@@ -2099,7 +2098,7 @@
   a regular expression @{text r} such that @{term "A = lang r"}. We also know
   that @{term "pderivs_lang B r"} is finite for every language @{text B} and 
   regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition 
-  and \eqref{Derspders} therefore
+  and \eqref{Derspders} we have
 
   
   \begin{equation}\label{eqq}
@@ -2126,7 +2125,7 @@
   \end{center}
 
   \noindent
-  It can be easily proved that @{text "\<preceq>"} is a partial order. Now define the 
+  It is straightforward to prove that @{text "\<preceq>"} is a partial order. Now define the 
   \emph{language of substrings} and \emph{superstrings} of a language @{text A} 
   respectively as
 
@@ -2141,12 +2140,13 @@
   We like to establish
 
   \begin{lmm}\label{subseqreg}
-  For every language @{text A}, the languages @{term "SUBSEQ A"} and @{term "SUPSEQ A"}
+  For every language @{text A}, the languages @{text "(i)"} @{term "SUBSEQ A"} and 
+  @{text "(ii)"} @{term "SUPSEQ A"}
   are regular.
   \end{lmm}
 
   \noindent
-  Our proof follows the one given in \cite[92--95]{Shallit08}, except that we use
+  Our proof follows the one given in \cite[Pages 92--95]{Shallit08}, except that we use
   Higman's Lemma, which is already proved in the Isabelle/HOL library \cite{Berghofer03}. 
   Higman's Lemma allows us to infer that every set @{text A} of antichains, satisfying
 
@@ -2158,7 +2158,7 @@
   is finite.
 
   The first step in our proof of Lemma~\ref{subseqreg} is to establish the 
-  following properties for @{term SUPSEQ}
+  following simple properties for @{term SUPSEQ}
 
   \begin{equation}\label{supseqprops}
   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -2226,7 +2226,7 @@
   except with itself.
   It is also straightforward to show that @{term "SUPSEQ M \<subseteq> SUPSEQ A"}. For
   the other direction we have  @{term "x \<in> SUPSEQ A"}. From this we obtain 
-  a @{text y} such that @{term "y \<in> A"} and @{term "y \<preceq> x"}. Since we know that
+  a @{text y} such that @{term "y \<in> A"} and @{term "y \<preceq> x"}. Since we have that
   the relation \mbox{@{term "{(y, x). y \<preceq> x \<and> x \<noteq> y}"}} is well-founded, there must
   be a minimal element @{text "z"} such that @{term "z \<in> A"} and @{term "z \<preceq> y"}, 
   and hence by transitivity also \mbox{@{term "z \<preceq> x"}} (here we deviate from the argument 
@@ -2265,11 +2265,11 @@
   \end{proof}
 
   Finally we like to show that the Myhill-Nerode theorem is also convenient for establishing 
-  non-regularity of languages. For this we use the following version of the Continuation
+  the non-regularity of languages. For this we use the following version of the Continuation
   Lemma (see for example~\cite{Rosenberg06}).
 
   \begin{lmm}[Continuation Lemma]
-  If the language @{text A} is regular and the set @{text B} is infinite,
+  If a language @{text A} is regular and a set @{text B} is infinite,
   then there exist two distinct strings @{text x} and @{text y} in @{text B} 
   such that @{term "x \<approx>A y"}.
   \end{lmm}
@@ -2277,14 +2277,14 @@
   \noindent
   This lemma can be easily deduced from the Myhill-Nerode theorem and the Pigeonhole
   Principle: Since @{text A} is regular, there can be only finitely many 
-  equivalence classes by the Myhill-Nerode relation. Hence an infinite set must contain 
+  equivalence classes. Hence an infinite set must contain 
   at least two strings that are in the same equivalence class, that is
   they need to be related by the Myhill-Nerode relation.
 
   Using this lemma, it is straightforward to establish that the language 
-  \mbox{@{text "A \<equiv> \<Union>\<^isub>n a\<^sup>n @ b\<^sup>n"}}, where @{text "a\<^sup>n"} stands
-  for the strings consisting of @{text n} times the character a, is not
-  regular. For this consider the infinite set @{text "B \<equiv> \<Union>\<^isub>n a\<^sup>n"}.
+  \mbox{@{text "A \<equiv> \<Union>\<^isub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands
+  for the strings consisting of @{text n} times the character a; similarly for
+  @{text "b\<^isub>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^isub>n a\<^sup>n"}.
 
   \begin{lmm}
   No two distinct strings in @{text "B"} are Myhill-Nerode related by @{text A}.
@@ -2373,7 +2373,9 @@
   using automata, poses no problem \cite{OwensReppyTuron09}.  For an
   implementation of a simple regular expression matcher, whose correctness has
   been formally established, we refer the reader to Owens and Slind
-  \cite{OwensSlind08}.
+  \cite{OwensSlind08}. In our opinion, their formalisation is considerably
+  slicker than for example the approach to regular expression matching taken
+  in \cite{Harper99} and \cite{Yi06}.
 
   Our proof of the first direction is very much inspired by \emph{Brzozowski's
   algebraic method} used to convert a finite automaton to a regular expression
@@ -2402,12 +2404,8 @@
   arguments over automata.
   
   The indirect proof for the second direction arose from our interest in
-  Brzozowski's derivatives for regular expression matching. A corresponding
-  regular expression matcher has been formalised by Owens and Slind in HOL4
-  \cite{OwensSlind08}. In our opinion, their formalisation is considerably
-  slicker than for example the approach to regular expression matching taken
-  in \cite{Harper99} and \cite{Yi06}. While Brzozowski's derivatives lead to a
-  simple regular expression matcher and he established that there are only
+  Brzozowski's derivatives for regular expression matching.  While Brzozowski 
+  already established that there are only
   finitely many dissimilar derivatives for every regular expression, this
   result is not as straightforward to formalise in a theorem prover as one
   might wish. The reason is that the set of dissimilar derivatives is not
@@ -2418,8 +2416,8 @@
   and for their argument the lack of a formal proof of termination is not
   crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}).  We
   expect that their development simplifies by using partial derivatives,
-  instead of derivatives, and that termination of the algorithm can be
-  formally established (the main incredience is
+  instead of derivatives, and that the termination of the algorithm can be
+  formally established (the main ingredient is
   Theorem~\ref{antimirov}). However, since partial derivatives use sets of
   regular expressions, one needs to carefully analyse whether the resulting
   algorithm is still executable. Given the existing infrastructure for
@@ -2445,32 +2443,32 @@
   in the context of the work done by Constable at al \cite{Constable00} who
   formalised the Myhill-Nerode theorem in Nuprl using automata. They write
   that their four-member team needed something on the magnitude of 18 months
-  for their formalisation. Also, Filli\^atre reports that his formalisation in 
-  Coq of automata theory and Kleene's theorem is ``rather big''. 
-  \cite{Filliatre97} More recently, Almeida et al reported about another 
+  for their formalisation. It is hard to gauge the size of a
+  formalisation in Nurpl, but from what is shown in the Nuprl Math Library
+  about their development it seems substantially larger than ours. We attribute
+  this to our use of regular expressions, which meant we did not need to `fight' 
+  the theorem prover.
+  Also, Filli\^atre reports that his formalisation in 
+  Coq of automata theory and Kleene's theorem is ``rather big'' 
+  \cite{Filliatre97}. More recently, Almeida et al reported about another 
   formalisation of regular languages in Coq \cite{Almeidaetal10}. Their 
   main result is the
   correctness of Mirkin's construction of an automaton from a regular
   expression using partial derivatives. This took approximately 10600 lines
-  of code.  The estimate for our formalisation is that we
+  of code.  In terms of time, the estimate for our formalisation is that we
   needed approximately 3 months and this included the time to find our proof
   arguments. Unlike Constable et al, who were able to follow the Myhill-Nerode 
   proof from \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the
-  formalisation was not the bottleneck. It is hard to gauge the size of a
-  formalisation in Nurpl, but from what is shown in the Nuprl Math Library
-  about their development it seems substantially larger than ours. We attribute
-  this to our use of regular expressions, which meant we did not need to `fight' 
-  the theorem prover. The code of
+  formalisation was not the bottleneck.  The code of
   our formalisation can be found in the Archive of Formal Proofs at
-  \mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip
+  \mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} 
+  \cite{myhillnerodeafp11}.\medskip
   
   \noindent
   {\bf Acknowledgements:}
   We are grateful for the comments we received from Larry Paulson.  Tobias
   Nipkow made us aware of the properties in Lemma~\ref{subseqreg} and Tjark
-  Weber helped us with their proofs.
-
-
+  Weber helped us with proving them.
 *}
 
 




