regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:fa8d33d13cb6
+:cf1c17431dab
 the second direction of the Myhill-Nerode theorem, we need 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}.
+relation by using derivatives of regular expressions~\cite{Brzozowski64}.
 Assume the following two definitions for the \emph{left-quotient} of a language,
 which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c}
 is a character and @{text s} a string, respectively:
 \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.
-The only interesting case above is the last one where we use Prop.~\ref{langprops}@{text "(i)"}
+The only interesting case is the last one where we use Prop.~\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 noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"}.
 Brzozowski observed that the left-quotients for languages of regular
 expressions can be calculated directly using the notion of \emph{derivatives
 \noindent
 The last two clauses extend derivatives from characters to strings---i.e.~list of
 characters. The list-cons operator is written \mbox{@{text "_ :: _"}}. The
 boolean function @{term "nullable r"} needed in the @{const Times}-case tests
-whether a regular expression can recognise the empty string:
+whether a regular expression can recognise the empty string. It can be defined as
+follows.
 \begin{center}
 \begin{tabular}{c@ {\hspace{10mm}}c}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{thm (lhs) nullable.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
 \end{tabular}
 \end{center}
 \noindent
 By induction on the regular expression @{text r}, respectively on the string @{text s},
-one can easily show that left-quotients and derivatives relate as follows
+one can easily show that left-quotients and derivatives of regular expressions
-\cite{Sakarovitch09}:
+relate as follows (for example \cite{Sakarovitch09}):
 \begin{equation}\label{Dersders}
 \mbox{\begin{tabular}{c}
 @{thm Der_der}\\
 @{thm Ders_ders}
 \end{tabular}}
 \end{equation}
 \noindent
-The importance in the context of the Myhill-Nerode theorem is that
+The importance of this fact in the context of the Myhill-Nerode theorem is that
 we can use \eqref{mhders} and \eqref{Dersders} in order to
 establish that @{term "x \<approx>(lang r) y"} is equivalent to
-@{term "lang (ders x r) = lang (ders y r)"}. Hence
+\mbox{@{term "lang (ders x r) = lang (ders y r)"}}. Hence
 \begin{equation}
 @{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
+which means the right-hand side (seen as relation) refines the Myhill-Nerode
-Myhill-Nerode relation.  Consequently, we can use
+relation.  Consequently, we can use @{text
-@{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a tagging-relation
+"\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a
-for the regular expression @{text r}. However, in
+tagging-relation. However, in order to be useful for the second part of the
-order to be useful for the second part of the Myhill-Nerode theorem, we also have to show that
+Myhill-Nerode theorem, we have to be able to establish that for the
-for the corresponding language there are only finitely many derivatives---thus ensuring
+corresponding language there are only finitely many derivatives---thus
-that there are only finitely many equivalence classes. Unfortunately, this
+ensuring that there are only finitely many equivalence
-is not true in general. Sakarovitch gives an example where a regular
+classes. Unfortunately, this is not true in general. Sakarovitch gives an
-expression  has infinitely many derivatives w.r.t.~the language
+example where a regular expression has infinitely many derivatives
-\mbox{@{term "({a} \<cdot> {b})\<star> \<union> ({a} \<cdot> {b})\<star> \<cdot> {a}"}}
+w.r.t.~the language \mbox{@{term "({a} \<cdot> {b})\<star> \<union> ({a} \<cdot> {b})\<star> \<cdot> {a}"}}
 \cite[Page~141]{Sakarovitch09}.
 What Brzozowski \cite{Brzozowski64} established is that for every language there
-\emph{are} only finitely `dissimilar' derivatives for a regular
+\emph{are} only finitely `dissimilar' derivatives of 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}
 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 notion in
 terms of already existing concepts. A convenient definition for automata
-(based on graphs) use a polymorphic type for the state nodes. This allows us
+(based on graphs) uses a polymorphic type for the state nodes. This allows
-to use the standard operation of disjoint union in order to compose two
+us to use the standard operation of disjoint union in order to compose two
-automata. But we cannot use such a polymorphic definition of automata in HOL
+automata. Unfortunately, we cannot use such a polymorphic definition of
-as part of the definition for regularity of a language (a set of strings).
+in HOL as part of the definition for regularity of a language (a
-Consider the following attempt
+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}

changeset 197	cf1c17431dab
parent 196	fa8d33d13cb6
child 198	b300f2c5d51d