--- a/Journal/Paper.thy Wed Aug 03 13:56:01 2011 +0000
+++ b/Journal/Paper.thy Wed Aug 03 17:08:31 2011 +0000
@@ -48,6 +48,7 @@
quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
REL ("\<approx>") and
UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
+ lang ("\<^raw:\ensuremath{\cal{L}}>" 101) and
lang ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
lang_trm ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
Lam ("\<lambda>'(_')" [100] 100) and
@@ -68,7 +69,11 @@
tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
Delta ("\<Delta>'(_')") and
nullable ("\<delta>'(_')") and
- Cons ("_ :: _" [100, 100] 100)
+ Cons ("_ :: _" [100, 100] 100) and
+ Rev ("Rev _" [1000] 100) and
+ Der ("Der _ _" [1000, 1000] 100) and
+ ONE ("ONE" 999) and
+ ZERO ("ZERO" 999)
lemma meta_eq_app:
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -307,9 +312,9 @@
Myhill-Nerode theorem requires that automata do not have inaccessible
states \cite{Kozen97}. Another subtle side-condition is completeness of
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 (Brozowski
+ `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{Brozowski10}). Such side-conditions mean that if we define a regular
+ 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 need a lemma which
ensures that another equivalent can be found satisfying the
@@ -324,9 +329,9 @@
exists an automaton that recognises all its strings, we define a
regular language as:
- \begin{dfntn}
- A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
- strings of @{text "A"}.
+ \begin{dfntn}\label{regular}
+ A language @{text A} is \emph{regular}, provided there is a regular expression
+ that matches all strings of @{text "A"}.
\end{dfntn}
\noindent
@@ -1465,7 +1470,7 @@
There are potentially many such prefixes, but there can only be finitely many of them (the
string @{text x} is finite). Let us therefore choose the longest one and call it
@{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
- know it is in @{term "A\<star>"} and it is not the empty string. By Lemma~\ref{langprops}@{text "(i)"},
+ know it is in @{term "A\<star>"} and it is not the empty string. By Prop.~\ref{langprops}@{text "(i)"},
we can separate
this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
@@ -1542,8 +1547,8 @@
\end{center}
\noindent
- Now clearly we have the following relation between the Myhill-Nerode relation
- (Definition~\ref{myhillneroderel}) and left-quotients
+ Clearly we have the following relation between the Myhill-Nerode relation
+ (Def.~\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"}
@@ -1552,16 +1557,20 @@
\noindent
It is realtively easy to establish the following properties for left-quotients:
- \begin{center}
- \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
+ \begin{equation}
+ \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
@{thm (lhs) Der_zero} & $=$ & @{thm (rhs) Der_zero}\\
@{thm (lhs) Der_one} & $=$ & @{thm (rhs) Der_one}\\
@{thm (lhs) Der_atom} & $=$ & @{thm (rhs) Der_atom}\\
@{thm (lhs) Der_union} & $=$ & @{thm (rhs) Der_union}\\
@{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
@{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\
- \end{tabular}
- \end{center}
+ @{thm (lhs) Ders_nil} & $=$ & @{thm (rhs) Ders_nil}\\
+ @{thm (lhs) Ders_cons} & $=$ & @{thm (rhs) Ders_cons}\\
+ %@{thm (lhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
+ % & @{thm (rhs) Ders_append[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
@@ -1572,7 +1581,7 @@
Brzozowski observed that the left-quotients for languages of regular
expressions can be calculated directly via the notion of \emph{derivatives
- of a regular expressions} \cite{Brzozowski64} which we define in Isabelle/HOL as
+ of a regular expression} \cite{Brzozowski64}, which we define in Isabelle/HOL as
follows:
\begin{center}
@@ -1594,8 +1603,10 @@
\end{center}
\noindent
- The function @{term "nullable r"} tests whether the regular expression
- can recognise the empty string:
+ The last two lines extend @{const der} to strings (list of characters) where
+ list-cons is written \mbox{@{text "_ :: _"}}. The 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}
@@ -1615,52 +1626,56 @@
\end{center}
\noindent
- Brzozowski proved
+ By induction on the regular expression @{text r}, respectively the string @{text s},
+ one can easily show that left-quotients and derivatives relate as follows
+ \cite{Sakarovitch09}:
\begin{equation}\label{Dersders}
- \mbox{\begin{tabular}{l}
+ \mbox{\begin{tabular}{c}
@{thm Der_der}\\
@{thm Ders_ders}
\end{tabular}}
\end{equation}
\noindent
- where the first is by induction on @{text r} and the second by a simple
- calculation.
+ The importance in the context of the Myhill-Nerode theorem is that
+ we can use \eqref{mhders} and the equations above in order to
+ establish that @{term "x \<approx>(lang r) y"} if and only if
+ @{term "lang (ders x r) = lang (ders y r)"}. From this we obtain
- The importance in the context of the Myhill-Nerode theorem is that
- we can use \eqref{mhders} and \eqref{Dersders} in order to derive
+ \begin{equation}
+ @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
+ \end{equation}
- \begin{center}
- @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}
- @{term "lang (ders x r) = lang (ders y r)"}
- \end{center}
\noindent
- which means @{term "x \<approx>(lang r) y"} provided @{term "ders x r = ders y r"}.
- Consequently, we can use as the tagging relation
- @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, which we know refines @{term "\<approx>(lang r)"}.
- This almost helps us because Brozowski also proved that there for every
- language there are only
- finitely `dissimilar' derivatives for a regular expression. Two regulare
- expressions are similar if they can be identified using the using the
- ACI-identities
+ Consequently, we can use as the tagging relation @{text
+ "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, since it refines
+ @{term "\<approx>(lang r)"}. However, in order to be useful in the Myhill-Nerode
+ theorem, we have to show that for a language there are only finitely many
+ derivatives. Unfortunately, this is not true in general: Sakarovitch gives
+ an example with infinitely many derivatives
+ \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved is
+ that for every language there \emph{are} 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{center}
\begin{tabular}{cl}
- (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)"}\\
- (C) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
- (I) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
+ (@{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"}\\
+ (@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
\end{tabular}
\end{center}
\noindent
- Without the indentification, we unfortunately obtain infinitely many
- derivations (an example is given in \cite[Page~141]{Sakarovitch09}).
- Reasoning modulo ACI can be done, but it is very painful in a theorem prover.
+ Carrying this idea through menas we now have to reasoning modulo @{text "ACI"}.
+ This can be done, but it is very painful in a theorem prover (since there is
+ no direct characterisation of the set of dissimlar derivatives).
- Fortunately, there is a much simpler approach using partial
- derivatives introduced by Antimirov \cite{Antimirov95}.
+ Fortunately, there is a much simpler approach using \emph{partial
+ derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined
+ in Isabelle/HOL as follows:
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
@@ -1680,14 +1695,101 @@
\end{tabular}
\end{center}
+ \noindent
+ Unlike `simple' derivatives, these functions return a set of regular
+ expressions. In the @{const Times} and @{const Star} cases we use
+
+ \begin{center}
+ @{text "TIMESS rs r \<equiv> {TIMES r' r | r' \<in> rs}"}
+ \end{center}
+
+ \noindent
+ in order to `sequence' a regular expressions with respect to a set of regular
+ expresions. Note that in the last case we first build the set of partial derivatives
+ w.r.t~@{text c}, then build the image of this set under the function @{term "pders s"}
+ and finally `union up' all resulting sets. Note also that in some sense, partial
+ derivatives have the @{text "ACI"}-identities already build in. Antimirov
+ \cite{Antimirov95}
+ showed
+
+ \begin{equation}
+ \mbox{\begin{tabular}{c}
+ @{thm Der_pder}\\
+ @{thm Ders_pders}
+ \end{tabular}}
+ \end{equation}
+
+ \noindent
+ and proved that for every language and regular expression there are only finitely
+ many partial derivatives.
*}
section {* Closure Properties *}
+text {*
+ The beautiful characteristics of regular languages is that they are closed
+ under many operations. Closure under union, sequencencing and Kleene-star
+ are trivial to establish given our definition of regularity (Def.~\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
+
+ \begin{center}
+ @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+ \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.
+
+ Once closure under complement is established, closure under intersection
+ and set difference is also easy, because
+
+ \begin{center}
+ \begin{tabular}{c}
+ @{term "A \<inter> B = - (- A \<union> - B)"}\\
+ @{term "A - B = - (- A \<union> B)"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Closure of regular languages under reversal, which means
+
+ \begin{center}
+ @{text "A\<^bsup>-1\<^esup> \<equiv> {s\<^bsup>-1\<^esup> | s \<in> A}"}
+ \end{center}
+
+ \noindent
+ can be shown with the help of the following operation defined on regular
+ expressions
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{thm (lhs) Rev.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(1)}\\
+ @{thm (lhs) Rev.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(2)}\\
+ @{thm (lhs) Rev.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(3)}\\
+ @{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ @{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}
+
+
+ In connection with left-quotient, the perhaps surprising fact is that
+ regular languages are closed under any left-quotient.
+
+
+*}
+
section {* Conclusion and Related Work *}
text {*
+ \noindent
In this paper we took the view that a regular language is one where there
exists a regular expression that matches all of its strings. Regular
expressions can conveniently be defined as a datatype in HOL-based theorem
@@ -1698,32 +1800,23 @@
\begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
\end{thrm}
- %
+
\noindent
- Having formalised this theorem means we
- pushed our point of view quite far. Using this theorem we can obviously prove when a language
- is \emph{not} regular---by establishing that it has infinitely many
- equivalence classes generated by the Myhill-Nerode relation (this is usually
- the purpose of the pumping lemma \cite{Kozen97}). We can also use it to
- establish the standard textbook results about closure properties of regular
- languages. Interesting is the case of 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 be easily proved using the Myhill-Nerode theorem since
- %
- \begin{center}
- @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
- \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. Proving the existence of such a regular expression via automata
- using the standard method would
- be quite involved. It includes the
- steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
- "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
- regular expression.
+ Having formalised this theorem means we pushed our point of view quite
+ far. Using this theorem we can obviously prove when a language is \emph{not}
+ regular---by establishing that it has infinitely many equivalence classes
+ generated by the Myhill-Nerode relation (this is usually the purpose of the
+ pumping lemma \cite{Kozen97}). We can also use it to establish the standard
+ textbook results about closure properties of regular languages. Interesting
+ is the case of 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 be easily
+ proved using the Myhill-Nerode theorem. Proving the existence of such a
+ regular expression via automata using the standard method would be quite
+ involved. It includes the steps: regular expression @{text "\<Rightarrow>"}
+ non-deterministic automaton @{text "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"}
+ complement automaton @{text "\<Rightarrow>"} regular expression.
+
While regular expressions are convenient in formalisations, they have some
limitations. One is that there seems to be no method of calculating a
@@ -1737,23 +1830,23 @@
Our formalisation consists of 780 lines of Isabelle/Isar code for the first
- direction and 460 for the second, plus around 300 lines of standard material about
- regular languages. While this might be seen as too large to count as a
- concise proof pearl, this 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 arguments. Unlike Constable et al,
- who were able to follow the proofs 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. The code of ours can be found in the
- Mercurial Repository at
+ direction and 460 for the second, plus around 300 lines of standard material
+ about regular languages. While this might be seen 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
+ arguments. Unlike Constable et al, who were able to follow the proofs 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. The code of
+ ours can be found in the Mercurial Repository at
\mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
+
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 \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
--- a/Journal/document/root.bib Wed Aug 03 13:56:01 2011 +0000
+++ b/Journal/document/root.bib Wed Aug 03 17:08:31 2011 +0000
@@ -11,7 +11,7 @@
@Unpublished{KraussNipkow11,
- author = {A.~Kraus and T.~Nipkow},
+ author = {A.~Krauss and T.~Nipkow},
title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
note = {To appear in Journal of Automated Reasoning},
year = {2011}
@@ -130,8 +130,8 @@
pages = {291--319}
}
-@ARTICLE{Brozowski10,
- author = {J.~Brozowski},
+@ARTICLE{Brzozowski10,
+ author = {J.~A.~Brzozowski},
title = {{Q}uotient {C}omplexity of {R}egular {L}anguages},
journal = {Journal of Automata, Languages and Combinatorics},
volume = {15},
@@ -150,7 +150,7 @@
@inproceedings{WuZhangUrban11,
author = {C.~Wu and X.~Zhang and C.~Urban},
title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
- booktitle = {Proc.~of the 2nd 1st Conference on Interactive Theorem Proving},
+ booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving},
year = {2011},
pages = {???},
series = {LNCS},