--- a/Paper/Paper.thy Thu Feb 10 05:57:56 2011 +0000
+++ b/Paper/Paper.thy Thu Feb 10 08:40:38 2011 +0000
@@ -146,13 +146,18 @@
Functions are much better supported in Isabelle/HOL, but they still lead to similar
problems as with graphs. Composing, for example, two non-deterministic automata in parallel
- poses again the problem of how to implement disjoint unions. Nipkow \cite{Nipkow98}
- dismisses the option of using identities, because it leads to ``messy proofs''. He
+ requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
+ dismisses the option of using identities, because it leads according to him to ``messy proofs''. He
opts for a variant of \eqref{disjointunion} using bitlists, but writes
\begin{quote}
- \it ``If the reader finds the above treatment in terms of bit lists revoltingly
- concrete, \phantom{``}I cannot disagree.''
+ \it%
+ \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
+ `` & If the reader finds the above treatment in terms of bit lists revoltingly
+ concrete, I cannot disagree.''\\
+ `` & All lemmas appear obvious given a picture of the composition of automata\ldots
+ Yet their proofs require a painful amount of detail.''
+ \end{tabular}
\end{quote}
\noindent
@@ -160,11 +165,11 @@
upon functions in order to represent \emph{finite} automata. The best is
probably to resort to more advanced reasoning frameworks, such as \emph{locales}
or \emph{type classes},
- which are not avaiable in all HOL-based theorem provers.
+ which are not avaiable in \emph{all} HOL-based theorem provers.
Because of these problems to do with representing automata, there seems
to be no substantial formalisation of automata theory and regular languages
- carried out in a HOL-based theorem prover. Nipkow establishes in
+ carried out in HOL-based theorem provers. Nipkow establishes in
\cite{Nipkow98} the link between regular expressions and automata in
the restricted context of lexing. The only larger formalisations of automata theory
are carried out in Nuprl \cite{Constable00} and in Coq (for example
@@ -210,7 +215,7 @@
are sets of strings. The language containing all strings is written in
Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
is written @{term "A ;; B"} and a language raised to the power @{text n} is written
- @{term "A \<up> n"}. Their definitions are
+ @{term "A \<up> n"}. They are defined as usual
\begin{center}
@{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
@@ -247,7 +252,7 @@
Central to our proof will be the solution of equational systems
involving sets of languages. For this we will use Arden's lemma \cite{Brzozowski64}
- which solves equations of the form @{term "X = A ;; X \<union> B"} in case
+ which solves equations of the form @{term "X = A ;; X \<union> B"} provided
@{term "[] \<notin> A"}. However we will need the following ``reverse''
version of Arden's lemma.
@@ -325,18 +330,16 @@
Given a set of regular expressions @{text rs}, we will make use of the operation of generating
a regular expression that matches all languages of @{text rs}. We only need to know the existence
of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
- @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This function, roughly speaking, folds @{const ALT} over the
+ @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
set @{text rs} with @{const NULL} for the empty set. We can prove that for finite sets @{text rs}
\begin{center}
- @{thm (lhs) folds_alt_simp}@{text "= \<Union> (\<calL> ` rs)"}
+ @{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}
\end{center}
\noindent
holds, whereby @{text "\<calL> ` rs"} stands for the
image of the set @{text rs} under function @{text "\<calL>"}.
-
-
*}
section {* Finite Partitions Imply Regularity of a Language *}
@@ -354,7 +357,7 @@
\noindent
It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
- equivalence classes. An example is the regular language containing just
+ equivalence classes. Let us give an example: consider the regular language containing just
the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
into the three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
as follows
@@ -366,8 +369,8 @@
\end{center}
One direction of the Myhill-Nerode theorem establishes
- that if there are finitely many equivalence classes, then the language is
- regular. In our setting we therefore have to show:
+ that if there are finitely many equivalence classes, like in the example above, then
+ the language is regular. In our setting we therefore have to show:
\begin{theorem}\label{myhillnerodeone}
@{thm[mode=IfThen] hard_direction}
@@ -387,14 +390,15 @@
@{thm finals_in_partitions} hold.
Therefore if we know that there exists a regular expression for every
equivalence class in @{term "finals A"} (which by assumption must be
- a finite set), then we can using @{text "\<bigplus>"} obtain a regular expression
+ a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
using that matches every string in @{text A}.
Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
regular expression for \emph{every} equivalence class, not just the ones
in @{term "finals A"}. We
- first define the notion of \emph{one-character-transition} between equivalence classes
+ first define the notion of \emph{one-character-transition} between
+ two equivalence classes
%
\begin{equation}
@{thm transition_def}
@@ -406,7 +410,7 @@
@{text X}. Note that we do not define an automaton here, we merely relate two sets
(with the help of a regular expression). In our concrete example we have
@{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any
- other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text c}.
+ other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
Next we build an equational system that
contains an equation for each equivalence class. Suppose we have
@@ -425,19 +429,21 @@
\noindent
where the pairs @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions
- @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. There can only be finitely many such
- transitions since there are only finitely many equivalence classes
- and finitely many characters.
+ @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. Our internal represeantation for the right-hand
+ sides are sets of terms.
+ There can only be finitely many such
+ terms since there are only finitely many equivalence classes
+ and only finitely many characters.
The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence
- class containing @{text "[]"}. (As an aside note that we mark, roughly speaking, the
+ class containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
single ``initial'' state in the equational system, which is different from
- the method by Brzozowski \cite{Brzozowski64}: he marks the ``terminal''
- states. We are forced to set up the equational system in this way, because
+ the method by Brzozowski \cite{Brzozowski64}, where he marks the ``terminal''
+ states. We are forced to set up the equational system in our way, because
the Myhill-Nerode relation determines the ``direction'' of the transitions.
The successor ``state'' of an equivalence class @{text Y} can be reached by adding
characters to the end of @{text Y}. This is also the reason why we have to use
- our reverse version of Arden's lemma.)
- Overloading the function @{text L} for the two kinds of terms in the
+ our reverse version of Arden's lemma.}
+ Overloading the function @{text \<calL>} for the two kinds of terms in the
equational system, we have
\begin{center}
@@ -463,17 +469,23 @@
\noindent
The reason for adding the @{text \<lambda>}-marker to our equational system is
to obtain this equation: it only holds in this form since none of
- the other terms contain the empty string.
-
+ the other terms contain the empty string. Since we use sets for representing
+ the right-hans side we can write \eqref{inv1} and \eqref{inv2} more
+ concisely for an equation of the form @{text "X = rhs"} as
+ %
+ \begin{equation}\label{inv}
+ \mbox{@{text "X = \<Union> (\<calL> ` rhs)"}}
+ \end{equation}
+ \noindent
Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
- equational system into a \emph{solved form} maintaining the invariants
- \eqref{inv1} and \eqref{inv2}. From the solved form we will be able to read
+ equational system into a \emph{solved form} maintaining the invariant
+ \eqref{inv}. From the solved form we will be able to read
off the regular expressions.
In order to transform an equational system into solved form, we have two main
operations: one that takes an equation of the form @{text "X = rhs"} and removes
- the recursive occurences of @{text X} in @{text rhs} using our variant of Arden's
+ the recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's
Lemma. The other operation takes an equation @{text "X = rhs"}
and substitutes @{text X} throughout the rest of the equational system
adjusting the remaining regular expressions approriately. To define this adjustment
@@ -486,12 +498,21 @@
\noindent
which we also lift to entire right-hand sides of equations, written as
- @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}.
-
+ @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
+ the \emph{arden-operation}, which takes an equivalence class @{text X} and
+ a rhs of an equation.
\begin{center}
@{thm arden_op_def}
\end{center}
+
+ \noindent
+ The term left of $\triangleright$ deletes all terms of the form @{text "(X, r)"};
+ the term on the right calculates first the combinded regular expressions for all
+ @{text r} in the @{text "(X, r)"}, forms the star and appends it to the remaining
+ terms in the @{text rhs}. It can be easily seen that this operation mimics Arden's
+ lemma on the level of equations.
+
*}
section {* Regular Expressions Generate Finitely Many Partitions *}