regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:b300f2c5d51d
+:11c3c302fa2e
 section {* Second Part proved using Partial Derivatives\label{derivatives} *}
 text {*
 \noindent
 As we have seen in the previous section, in order to establish
-the second direction of the Myhill-Nerode theorem, we need to find
+the second direction of the Myhill-Nerode theorem, it is sufficient to find
 a more refined relation than @{term "\<approx>(lang r)"} for which we can
 show that there are only finitely many equivalence classes. So far we
 showed this directly by induction on @{text "r"} using tagging-functions.
 However, there is also  an indirect method to come up with such a refined
 relation by using derivatives of regular expressions~\cite{Brzozowski64}.
 \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.  In the last equation we use the list-cons operator written
+accordingly.  Note also that in the last equation we use the list-cons operator written
-\mbox{@{text "_ :: _"}}.  The only interesting case is the @{text "A\<star>"}-case
+\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 "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can then complete the proof by
 using the fifth equation and noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der
 c A) \<cdot> A\<star>"}.
 @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
 \end{equation}
 \noindent
-which means the right-hand side (seen as relation) refines the Myhill-Nerode
+which means the right-hand side (seen as a relation) refines the Myhill-Nerode
 relation.  Consequently, we can use @{text
 "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a
 tagging-relation. However, in order to be useful for the second part of the
 Myhill-Nerode theorem, we have to be able to establish that for the
 corresponding language there are only finitely many derivatives---thus
 w.r.t.~the language \mbox{@{term "({a} \<cdot> {b})\<star> \<union> ({a} \<cdot> {b})\<star> \<cdot> {a}"}}
 (see \cite[Page~141]{Sakarovitch09}).
 What Brzozowski \cite{Brzozowski64} established is that for every language there
-\emph{are} only finitely `dissimilar' derivatives of a regular
+\emph{are} only finitely `dissimilar' derivatives for a regular
 expression. Two regular expressions are said to be \emph{similar} provided
 they can be identified using the using the @{text "ACI"}-identities:
 \begin{equation}\label{ACI}
 \end{tabular}}
 \end{equation}
 \noindent
 Carrying this idea through, we must not consider the set of all derivatives,
-but the ones modulo @{text "ACI"}.  In principle, this can be done formally,
+but the one modulo @{text "ACI"}.  In principle, this can be done formally,
 but it is very painful in a theorem prover (since there is no
 direct characterisation of the set of dissimilar derivatives).
 Fortunately, there is a much simpler approach using \emph{partial
 For every language @{text A} and every regular expression @{text r},
 \mbox{@{thm finite_pders_lang}}.
 \end{thrm}
 \noindent
-Antimirov's argument first shows this theorem for the language @{term UNIV1},
+Antimirov's proof first shows this theorem for the language @{term UNIV1},
 which is the set of all non-empty strings. For this he proves:
 \begin{equation}\label{pdersunivone}
 \mbox{\begin{tabular}{l}
 @{thm pders_lang_Zero}\\
 \begin{center}
 @{thm pders_lang_UNIV}\\
 \end{center}
 \noindent
-and for all languages @{text "A"}, @{thm pders_lang_subset[where B="UNIV",
+and for all languages @{text "A"}, @{term "pders_lang A r"} is a subset of
-simplified]} holds.  Since we follow Antimirov's proof quite closely in our
+@{term "pders_lang UNIV r"}.  Since we follow Antimirov's proof quite
-formalisation (only the last two cases of \eqref{pdersunivone} involve some
+closely in our formalisation (only the last two cases of
-non-routine induction argument), we omit the details.
+\eqref{pdersunivone} involve some non-routine induction argument), we omit
+the details.
 Let us now return to our proof about the second direction in the Myhill-Nerode
 theorem. The point of the above calculations is to use
 @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as tagging-relation.
 proved using the Myhill-Nerode theorem.
 Our insistence on regular expressions for proving the Myhill-Nerode theorem
 arose from the limitations of HOL, on which the popular theorem provers HOL4,
 HOLlight and Isabelle/HOL are based. In order to guarantee consistency,
-formalisations can only extend HOL by definitions that introduce a new concept in
+formalisations can extend HOL with definitions that introduce a new concept in
-terms of already existing notions. A convenient definition for automata
+only terms of already existing notions. A convenient definition for automata
 (based on graphs) uses a polymorphic type for the state nodes. This allows
-us to use the standard operation of disjoint union in order to compose two
+us to use the standard operation for disjoint union whenever we need to compose two
 automata. Unfortunately, we cannot use such a polymorphic definition
-in HOL as part of the definition for regularity of a language (a
+in HOL as part of the definition for regularity of a language (a predicate
-set of strings).  Consider the following attempt
+over set of strings).  Consider the following attempt:
 \begin{center}
 @{text "is_regular A \<equiv> \<exists>M(\<alpha>). is_finite_automata (M) \<and> \<calL>(M) = A"}
 \end{center}
 \noindent
-which means the definiens is polymorphic in the type of the automata @{text
+In this definifion, the definiens is polymorphic in the type of the automata
-"M"}, but the definiendum @{text "is_regular"} is not. Such definitions are
+@{text "M"} (indicated by the @{text "\<alpha>"}), but the definiendum @{text
-excluded in HOL, because they can lead easily to inconsistencies (see
+"is_regular"} is not. Such definitions are excluded in HOL, because they can
-\cite{PittsHOL4} for a simple example). Also HOL does not contain
+lead easily to inconsistencies (see \cite{PittsHOL4} for a simple
-type-quantifiers which would allow us to get rid of the polymorphism by
+example). Also HOL does not contain type-quantifiers which would allow us to
-quantifying over the type-variable @{text "\<alpha>"}. Therefore when defining
+get rid of the polymorphism by quantifying over the type-variable @{text
-regularity in terms of automata, the only natural way out in HOL is to use
+"\<alpha>"}. Therefore when defining regularity in terms of automata, the only
-state nodes with an identity, for example a natural number. Unfortunatly,
+natural way out in HOL is to resort to state nodes with an identity, for
-the consequence is that we have to be careful when combining two automata so
+example a natural number. Unfortunatly, the consequence is that we have to
-that there is no clash between two such states. This makes formalisations
+be careful when combining two automata so that there is no clash between two
-quite fiddly and rather unpleasant. Regular expressions proved much more
+such states. This makes formalisations quite fiddly and rather
-convenient for reasoning in HOL and we showed they can be used for
+unpleasant. Regular expressions proved much more convenient for reasoning in
-establishing the central result in regular language theory: the Myhill-Nerode
+HOL since they can be defined as inductive datatype and a reasoning
-theorem.
+infrastructure comes for free. We showed they can be used for establishing
+the central result in regular language theory---the Myhill-Nerode theorem.
 While regular expressions are convenient, they have some limitations. One is
 that there seems to be no method of calculating a minimal regular expression
 (for example in terms of length) for a regular language, like there is for
 automata. On the other hand, efficient regular expression matching, without
 \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
 finitely many dissimilar derivatives for every regular expression, this
-result is not as straightforward to formalise in a theorem prover. The
+result is not as straightforward to formalise in a theorem prover as one
-reason is that the set of dissimilar derivatives is not defined inductively,
+might wish. The reason is that the set of dissimilar derivatives is not
-but in terms of an ACI-equivalence relation. This difficulty prevented for
+defined inductively, but in terms of an ACI-equivalence relation. This
-example Krauss and Nipkow to prove termination of their equivalence checker
+difficulty prevented for example Krauss and Nipkow to prove termination of
-for regular expressions \cite{KraussNipkow11}. Their checker is based on
+their equivalence checker for regular expressions
-derivatives and for their argument the lack of a formal proof of termination
+\cite{KraussNipkow11}. Their checker is based on Brzozowski's derivatives
-is not crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}).
+and for their argument the lack of a formal proof of termination is not
-We expect that their development simplifies by using partial derivatives,
+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. However, since partial derivatives use sets of regular
+formally established (the main incredience is
-expressions, one needs to carefully analyse whether the resulting algorithm
+Theorem~\ref{antimirov}). However, since partial derivatives use sets of
-is still executable. Given the existing infrastructure for executable sets
+regular expressions, one needs to carefully analyse whether the resulting
-in Isabelle/HOL, it should.
+algorithm is still executable. Given the existing infrastructure for
+executable sets in Isabelle/HOL, it should.
 Our formalisation of the Myhill-Nerode theorem consists of 780 lines of
 Isabelle/Isar code for the first direction and 460 for the second (the one
 based on tagging functions), plus around 300 lines of standard material
-about regular languages. The formalisation about derivatives and partial
+about regular languages. The formalisation of derivatives and partial
 derivatives shown in Section~\ref{derivatives} consists of 390 lines of
 code.  The algorithm for solving equational systems, which we used in the
 first direction, is conceptually relatively simple. Still the use of sets
 over which the algorithm operates means it is not as easy to formalise as
 one might hope. However, it seems sets cannot be avoided since the `input'
 of the algorithm consists of equivalence classes and we cannot see how to
 reformulate the theory so that we can use lists. Lists would be much easier
-to reason about, since we can define function over them by recursion. For
+to reason about, since we can define functions over them by recursion. For
-sets we have to use set-comprehensions.
+sets we have to use set-comprehensions, which is slightly unwieldy.
-While our formalisation might be seen large, it should be seen
+While our formalisation might appear large, it should be seen
 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. The estimate for our formalisation is that we
 needed approximately 3 months and this included the time to find our proof

changeset 199	11c3c302fa2e
parent 198	b300f2c5d51d
child 200	204856ef5573