--- a/Journal/Paper.thy Thu Aug 11 16:55:41 2011 +0000
+++ b/Journal/Paper.thy Thu Aug 11 23:11:39 2011 +0000
@@ -42,7 +42,7 @@
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
@@ -66,14 +66,17 @@
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"
@@ -152,7 +155,9 @@
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:
@@ -204,7 +209,7 @@
&
- \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+ \raisebox{2.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
&
@@ -316,7 +321,7 @@
(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.
@@ -1095,7 +1100,7 @@
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}
@@ -1560,13 +1565,13 @@
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
- an indirect method to come up with such a refined relation by using
- derivatives of regular expressions \cite{Brzozowski64}.
+ 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}.
- 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}
@@ -1576,7 +1581,7 @@
\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"}
@@ -1584,15 +1589,15 @@
\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
- (Def.~\ref{myhillneroderel}) and left-quotients
+ Clearly we have the following equivalence between the Myhill-Nerode relation
+ (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}
@@ -1610,16 +1615,16 @@
\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
- of a regular expression} \cite{Brzozowski64}, which we define in Isabelle/HOL as
- follows:
+ expressions can be calculated directly using the notion of \emph{derivatives
+ of a regular expression} \cite{Brzozowski64}. We define this notion in
+ Isabelle/HOL as follows:
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
@@ -1642,7 +1647,7 @@
\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}
@@ -1687,19 +1692,22 @@
\noindent
which means the right-hand side (seen as relation) refines the
- Myhill-Nerode relation. Consequently, we can use
+ 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
- \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved
- is that for every language there \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:
+ expression has infinitely many derivatives 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
+ 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}
@@ -1756,7 +1764,7 @@
convenient to introduce for this the following abbreviation
\begin{center}
- @{abbrev "pderss s A"}
+ @{abbrev "pderss s rs"}
\end{center}
\noindent
@@ -1824,11 +1832,88 @@
\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 *}
@@ -1837,7 +1922,7 @@
\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
@@ -1850,7 +1935,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.
+ 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
@@ -1886,11 +1972,39 @@
\end{tabular}
\end{center}
+ \noindent
+ For this operation we can so
- In connection with left-quotient, the perhaps surprising fact is that
- 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.
+
*}