regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:ce24ed955cca
+:2a5ac68db24b
 notation (latex output)
 str_eq ("\<approx>\<^bsub>_\<^esub>") and
 str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and
 conc (infixr "\<cdot>" 100) and
-star ("_\<^bsup>\<star>\<^esup>") and
+star ("_\<^bsup>\<star>\<^esup>" [101] 200) and
 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
 Suc ("_+1" [100] 100) and
 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
 REL ("\<approx>") and
 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
 tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and
 tag_Times ("\<times>tag _ _" [100, 100] 100) and
 tag_Times ("\<times>tag _ _ _" [100, 100, 100] 100) and
 tag_Star ("\<star>tag _" [100] 100) and
 tag_Star ("\<star>tag _ _" [100, 100] 100) and
-tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
+tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>" [100] 100) and
 Delta ("\<Delta>'(_')") and
 nullable ("\<delta>'(_')") and
 Cons ("_ :: _" [100, 100] 100) and
 Rev ("Rev _" [1000] 100) and
 Der ("Der _ _" [1000, 1000] 100) and
 ONE ("ONE" 999) and
-ZERO ("ZERO" 999)
+ZERO ("ZERO" 999) and
+pders_lang ("pderl") and
+UNIV1 ("UNIV\<^isup>+") and
+Ders_lang ("Derl")
 lemma meta_eq_app:
 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
 by auto
 presented in this paper we will use the latter. HOL is a predicate calculus
 that allows quantification over predicate variables. Its type system is
 based on Church's Simple Theory of Types \cite{Church40}.  Although many
 mathematical concepts can be conveniently expressed in HOL, there are some
 limitations that hurt badly, if one attempts a simple-minded formalisation
-of regular languages in it.  The typical approach to regular languages is to
+of regular languages in it.
+The typical approach to regular languages is to
 introduce finite automata and then define everything in terms of them
 \cite{Kozen97}.  For example, a regular language is normally defined as:
 \begin{dfntn}\label{baddef}
 A language @{text A} is \emph{regular}, provided there is a
 \draw ( 0.6,0.0) node {\small$A_2$};
 \end{tikzpicture}
 &
-\raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+\raisebox{2.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
 &
 \begin{tikzpicture}[scale=1]
 %\draw[step=2mm] (-1,-1) grid (1,1);
 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
 (Brzozowski mentions this side-condition in the context of state complexity
 of automata \cite{Brzozowski10}). Such side-conditions mean that if we
 define a regular language as one for which there exists \emph{a} finite
-automaton that recognises all its strings (see Def.~\ref{baddef}), then we
+automaton that recognises all its strings (see Definition~\ref{baddef}), then we
 need a lemma which ensures that another equivalent one can be found
 satisfying the side-condition. Unfortunately, such `little' and `obvious'
 lemmas make a formalisation of automata theory a hair-pulling experience.
 text {*
 \noindent
 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}
+\begin{thrm}\label{myhillnerodetwo}
 Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
 \end{thrm}
 \noindent
 The proof will be by induction on the structure of @{text r}. It turns out
 \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
 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 by induction on @{text "r"}. However, there is also
+showed this directly by induction on @{text "r"} using tagging-functions.
-an indirect method to come up with such a refined relation by using
+However, there is also  an indirect method to come up with such a refined
-derivatives of regular expressions \cite{Brzozowski64}.
+relation by using derivatives of regular expressions \cite{Brzozowski64}.
-Assume the following two definitions for a \emph{left-quotient} of a language,
+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:
+is a character and @{text s} a string, respectively:
 \begin{center}
 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
 @{thm (lhs) Der_def}  & @{text "\<equiv>"} & @{thm (rhs) Der_def}\\
 @{thm (lhs) Ders_def} & @{text "\<equiv>"} & @{thm (rhs) Ders_def}\\
 \end{tabular}
 \end{center}
 \noindent
-In order to aid readability, we shall also make use of the following abbreviation
+In order to aid readability, we shall make use of the following abbreviation
 \begin{center}
 @{abbrev "Derss s As"}
 \end{center}
 \noindent
 where we apply the left-quotient to a set of languages and then combine the results.
-Clearly we have the following relation between the Myhill-Nerode relation
+Clearly we have the following equivalence between the Myhill-Nerode relation
-(Def.~\ref{myhillneroderel}) and left-quotients
+(Definition~\ref{myhillneroderel}) and left-quotients
 \begin{equation}\label{mhders}
 @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
 \end{equation}
 \noindent
-It is also straightforward to establish the following properties for left-quotients:
+It is also straightforward to establish the following properties of left-quotients
 \begin{equation}
 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
 @{thm (lhs) Der_simps(1)} & $=$ & @{thm (rhs) Der_simps(1)}\\
 @{thm (lhs) Der_simps(2)} & $=$ & @{thm (rhs) Der_simps(2)}\\
 %   & @{thm (rhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
 \end{tabular}}
 \end{equation}
 \noindent
-where @{text "\<Delta>"} is a function that tests whether the empty string
+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)"}
 in order to infer that @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can
-then complete the proof by observing that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"}.
+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 via the notion of \emph{derivatives
+expressions can be calculated directly using the notion of \emph{derivatives
-of a regular expression} \cite{Brzozowski64}, which we define in Isabelle/HOL as
+of a regular expression} \cite{Brzozowski64}. We define this notion in
-follows:
+Isabelle/HOL as follows:
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{thm (lhs) der.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(1)}\\
 @{thm (lhs) der.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
 \end{center}
 \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
-function @{term "nullable r"} needed in the @{const Times}-case tests
+boolean function @{term "nullable r"} needed in the @{const Times}-case tests
 whether a regular expression can recognise the empty string:
 \begin{center}
 \begin{tabular}{c@ {\hspace{10mm}}c}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 \end{equation}
 \noindent
 which means the right-hand side (seen as relation) refines the
 Myhill-Nerode relation.  Consequently, we can use
 @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a tagging-relation
 for the regular expression @{text r}. However, in
-order to be useful for teh second part of the Myhill-Nerode theorem, we also have to show that
+order to be useful for the second part of the Myhill-Nerode theorem, we also have to show that
 for the corresponding language there are only finitely many derivatives---thus ensuring
 that there are only finitely many equivalence classes. Unfortunately, this
 is not true in general. Sakarovitch gives an example where a regular
-expression  has infinitely many derivatives w.r.t.~a language
+expression  has infinitely many derivatives w.r.t.~the language
-\cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved
+\mbox{@{term "({a} \<cdot> {b})\<star> \<union> ({a} \<cdot> {b})\<star> \<cdot> {a}"}}
-is that for every language there \emph{are} only finitely `dissimilar'
+\cite[Page~141]{Sakarovitch09}.
-derivatives for a regular expression. Two regular expressions are said to be
-\emph{similar} provided they can be identified using the using the @{text
+What Brzozowski \cite{Brzozowski64} established is that for every language there
-"ACI"}-identities:
+\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}
 \mbox{\begin{tabular}{cl}
 (@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
 (@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
 derivatives w.r.t~the character @{text c}, then build the image of this set under the
 function @{term "pders s"} and finally `union up' all resulting sets. It will be
 convenient to introduce for this the following abbreviation
 \begin{center}
-@{abbrev "pderss s A"}
+@{abbrev "pderss s rs"}
 \end{center}
 \noindent
 which simplifies the last clause of @{const "pders"} to
 \end{tabular}}
 \end{equation}
 \noindent
 These two properties confirm the observation made earlier
-that by using sets, partial derivatives have the @{text "ACI"}-identidies
+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
-there are only finitely many partial derivatives.
+there are only finitely many partial derivatives, whereby the partial
+derivatives of @{text r} w.r.t.~a language @{text A} is defined as
+\begin{equation}\label{Pdersdef}
+@{thm pders_lang_def}
+\end{equation}
+\begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}
+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},
+which is the set of all non-empty strings. For this he proves:
+\begin{equation}
+\mbox{\begin{tabular}{l}
+@{thm pders_lang_Zero}\\
+@{thm pders_lang_One}\\
+@{thm pders_lang_Atom}\\
+@{thm pders_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm pders_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm pders_lang_Star}\\
+\end{tabular}}
+\end{equation}
+\noindent
+from which one can deduce by induction on @{text r} that
+\begin{center}
+@{thm finite_pders_lang_UNIV1}
+\end{center}
+\noindent
+holds. Now Antimirov's theorem follows because
+\begin{center}
+@{thm pders_lang_UNIV}\\
+\end{center}
+\noindent
+and for all languages @{text "A"}, @{thm pders_lang_subset[where B="UNIV",
+simplified]} holds.  Since we follow Antimirov's proof quite closely in our
+formalisation, we omit the details.
+Let us return to our proof of 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.
+\begin{proof}[Proof of Theorem~\ref{myhillnerodetwo}]
+Using \eqref{mhders}
+and \eqref{Derspders} we can easily infer that
+\begin{center}
+@{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pders x r = pders y r"}
+\end{center}
+\noindent
+which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.
+So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}}
+holds if @{term "finite (UNIV // (=(\<lambda>x. pders x r)=))"}. In order to establish
+the latter, we can use Lemma~\ref{finone} and show that the range of the
+tagging-function \mbox{@{term "\<lambda>x. pders x r"}} is finite. For this recall Definition
+\ref{Pdersdef}, which gives us that
+\begin{center}
+@{thm pders_lang_def[where A="UNIV", simplified]}
+\end{center}
+\noindent
+Now the range of @{term "\<lambda>x. pders x r"} is a subset of @{term "Pow (pders_lang UNIV r)"},
+which we know is finite by Theorem~\ref{antimirov}. This means there
+are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"},
+and we can again conclude the second part of the Myhill-Nerode theorem.
+\end{proof}
 *}
 section {* Closure Properties *}
 text {*
 \noindent
 The real beauty of regular languages is that they are closed
 under almost all set operations. Closure under union, concatenation and Kleene-star
-are trivial to establish given our definition of regularity (Def.~\ref{regular}).
+are trivial to establish given our definition of regularity (Definition~\ref{regular}).
 More interesting is the closure under complement, because
 it seems difficult to construct a regular expression for the complement
 language by direct means. However the existence of such a regular expression
 can now be easily proved using the Myhill-Nerode theorem since
 \end{center}
 \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.
+give rise to the same partitions. So if one is finite, the other is too and the
+other way around.
 Once closure under complement is established, closure under intersection
 and set difference is also easy, because
 \begin{center}
 @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
 @{thm (lhs) Rev.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(6)}\\
 \end{tabular}
 \end{center}
+\noindent
-In connection with left-quotient, the perhaps surprising fact is that
+For this operation we can so
-regular languages are closed under any left-quotient.
+\begin{center}
+@{text "(\<calL>(r))\<^bsup>-1\<^esup>"}~@{text "="}~@{thm (rhs) rev_lang}
+\end{center}
+\noindent
+from which closure under reversal follows.
+The perhaps the most surprising fact is that regular languages are closed under any
+left-quotient. Define
+\begin{center}
+@{abbrev "Ders_lang B A"}
+\end{center}
+\noindent
+and assume @{text A} is regular. From this we know there exists a regular
+expression @{text r} such that @{term "A = lang r"}. We also know that
+@{term "pders_lang B r"} is finite. By definition and Lemma~\ref{Derspders}
+\begin{equation}\label{eqq}
+@{term "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"}
+\end{equation}
+\noindent
+Since there are only finitely many regular expressions in @{term "pders_lang B r"}
+by Theorem~\ref{antimirov}, we know that the right-hand side of \eqref{eqq}, is
+equal to @{term "lang (\<Uplus>(pders_lang B r))"} using \eqref{uplus}. Hence
+the regular expression @{term "pders_lang B r"} verifies that @{term "Ders_lang B A"}
+is regular.
 *}
 section {* Conclusion and Related Work *}

changeset 193	2a5ac68db24b
parent 190	b73478aaf33e
child 194	5347d7556487