--- a/Paper/Paper.thy Wed Feb 09 12:34:30 2011 +0000
+++ b/Paper/Paper.thy Thu Feb 10 05:57:56 2011 +0000
@@ -12,6 +12,10 @@
abbreviation
"EClass x R \<equiv> R `` {x}"
+abbreviation
+ "append_rexp2 r_itm r \<equiv> append_rexp r r_itm"
+
+
notation (latex output)
str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
@@ -27,7 +31,10 @@
Trn ("'(_, _')" [100, 100] 100) and
EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
- Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999)
+ Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
+ append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+ append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100)
+
(*>*)
@@ -127,7 +134,7 @@
\noindent
changes the type---the disjoint union is not a set, but a set of pairs.
Using this definition for disjoint unions means we do not have a single type for automata
- and hence will not be able to state properties about \emph{all}
+ and hence will not be able to state certain properties about \emph{all}
automata, since there is no type quantification available in HOL. An
alternative, which provides us with a single type for automata, is to give every
state node an identity, for example a natural
@@ -141,23 +148,25 @@
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
- opts for a variant of \eqref{disjointunion}, but writes
+ 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, I cannot disagree.''
+ concrete, \phantom{``}I cannot disagree.''
\end{quote}
\noindent
Moreover, it is not so clear how to conveniently impose a finiteness condition
upon functions in order to represent \emph{finite} automata. The best is
- probably to resort to more advanced reasoning frameworks, such as \emph{locales}.
+ 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.
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
\cite{Nipkow98} the link between regular expressions and automata in
- the context of lexing. The only larger formalisations of automata theory
+ the restricted context of lexing. The only larger formalisations of automata theory
are carried out in Nuprl \cite{Constable00} and in Coq (for example
\cite{Filliatre97}).
@@ -197,7 +206,7 @@
text {*
Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
- being represented by the empty list, written @{term "[]"}. \emph{Languages}
+ being represented by the empty list, written @{term "[]"}. \emph{Languages}
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
@@ -217,14 +226,16 @@
we will make use of the following properties of these constructions.
\begin{proposition}\label{langprops}\mbox{}\\
- \begin{tabular}{@ {}ll@ {\hspace{10mm}}ll}
- (i) & @{thm star_cases} & (ii) & @{thm[mode=IfThen] pow_length}\\
- (iii) & @{thm seq_Union_left} &
+ \begin{tabular}{@ {}ll}
+ (i) & @{thm star_cases} \\
+ (ii) & @{thm[mode=IfThen] pow_length}\\
+ (iii) & @{thm seq_Union_left} \\
\end{tabular}
\end{proposition}
\noindent
- We omit the proofs, but invite the reader to consult
+ In @{text "(ii)"} we use the notation @{term "length s"} for the length of a string.
+ We omit the proofs for these properties, but invite the reader to consult
our formalisation.\footnote{Available at ???}
@@ -311,9 +322,9 @@
\end{tabular}
\end{center}
- Given a set of regular expressions @{text rs}, we will need the operation of generating
- a corresponding regular expressions that matches all languages of @{text rs}. We only need the existence
- of such a regular expressions and therefore we use Isabelle's @{const "fold_graph"} and Hilbert's
+ 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
set @{text rs} with @{const NULL} for the empty set. We can prove that for finite sets @{text rs}
@@ -344,7 +355,7 @@
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
- the string @{text "[c]"}, then @{term "\<approx>({[c]})"} partitions @{text UNIV}
+ 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
@@ -371,31 +382,31 @@
\end{equation}
\noindent
- In our running example, @{text "X\<^isub>1"} is the only equivalence class in @{term "finals {[c]}"}.
+ In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
It is straightforward to show that in general @{thm lang_is_union_of_finals} and
@{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 obtain a regular expression using @{text "\<bigplus>"}
- that matches every string in @{text A}.
+ a finite set), then we can using @{text "\<bigplus>"} 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{transition} between equivalence classes
+ first define the notion of \emph{one-character-transition} between equivalence classes
%
\begin{equation}
@{thm transition_def}
\end{equation}
\noindent
- which means that if we concatenate all strings matching the regular expression @{text r}
- to the end of all strings in the equivalence class @{text Y}, we obtain a subset of
+ which means that if we concatenate the character @{text c} to the end of all
+ strings in the equivalence class @{text Y}, we obtain a subset of
@{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>(CHAR c)\<Rightarrow> X\<^isub>2"} and @{term "X\<^isub>1 \<Turnstile>r\<Rightarrow> X\<^isub>3"} with @{text r} being any
- other regular expression than @{const EMPTY} and @{term "CHAR c"}.
+ @{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}.
Next we build an equational system that
contains an equation for each equivalence class. Suppose we have
@@ -414,20 +425,24 @@
\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>(CHAR c\<^isub>i\<^isub>j)\<Rightarrow> X\<^isub>i"}. The term @{text "\<lambda>(EMPTY)"} acts as a marker for the equivalence
- class containing @{text "[]"}. (Note that we mark, roughly speaking, the
+ @{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.
+ 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
single ``initial'' state in the equational system, which is different from
- the method by Brzozowski \cite{Brzozowski64}, since he marks the ``terminal''
+ 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 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
- equational system as follows
+ equational system, we have
\begin{center}
- @{thm L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+ @{text "\<calL>(Y, r) \<equiv>"} %
+ @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
@{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
\end{center}
@@ -447,11 +462,11 @@
\noindent
The reason for adding the @{text \<lambda>}-marker to our equational system is
- to obtain this equation, which only holds in this form since none of
+ to obtain this equation: it only holds in this form since none of
the other terms contain the empty string.
- Our proof of Thm.~\ref{myhillnerodeone} will be by transforming the
+ 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
off the regular expressions.
@@ -459,17 +474,24 @@
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
- Lemma (Lem.~\ref{arden}). The other operation takes an equation @{text "X = rhs"}
+ Lemma. The other operation takes an equation @{text "X = rhs"}
and substitutes @{text X} throughout the rest of the equational system
- adjusting the regular expressions approriately. To define them we need the
- operation
+ adjusting the remaining regular expressions approriately. To define this adjustment
+ we define the \emph{append-operation}
\begin{center}
- @{thm attach_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
- @{thm attach_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+ @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
\end{center}
+ \noindent
+ which we also lift to entire right-hand sides of equations, written as
+ @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}.
+
+ \begin{center}
+ @{thm arden_op_def}
+ \end{center}
*}
section {* Regular Expressions Generate Finitely Many Partitions *}
@@ -498,6 +520,17 @@
section {* Conclusion and Related Work *}
+text {*
+ In this paper we took the view that a regular language as one where there exists
+ a regular expression that matches all its strings. For us it was important to find
+ out how far we can push this point of view. Having formalised the Myhill-Nerode
+ theorem means pushed very far. Having the Myhill-Nerode theorem means we can
+ formalise much of the textbook results in this subject.
+
+
+*}
+
+
(*<*)
end
(*>*)
\ No newline at end of file