--- a/Journal/Paper.thy Wed Jul 10 13:28:24 2013 +0100
+++ b/Journal/Paper.thy Wed Jul 10 17:47:30 2013 +0100
@@ -563,7 +563,7 @@
Central to our proof will be the solution of equational systems
involving equivalence classes of languages. For this we will use Arden's Lemma
- (see for example \cite[Page 100]{Sakarovitch09}),
+ (see for example \citet[Page 100]{Sakarovitch09}),
which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
@{term "[] \<notin> A"}. However we will need the following `reversed'
version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to
@@ -659,16 +659,18 @@
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. To illustrate this quotient construction, let us give a simple
- example: consider the regular language containing just
- the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
- into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
+ example: consider the regular language built up over the alphabet @{term "{a, b}"} and
+ containing just the string two strings @{text "[a]"} and @{text "[a, b]"}. The
+ relation @{term "\<approx>({[a], [a, b]})"} partitions @{text UNIV}
+ into four equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"}, @{text "X\<^isub>3"} and @{text "X\<^isub>4"}
as follows
\begin{center}
\begin{tabular}{l}
@{text "X\<^isub>1 = {[]}"}\\
- @{text "X\<^isub>2 = {[c]}"}\\
- @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+ @{text "X\<^isub>2 = {[a]}"}\\
+ @{text "X\<^isub>3 = {[a, b]}"}\\
+ @{text "X\<^isub>4 = UNIV - {[], [a], [a, b]}"}
\end{tabular}
\end{center}
@@ -689,8 +691,8 @@
\end{equation}
\noindent
- In our running example, @{text "X\<^isub>2"} is the only
- equivalence class in @{term "finals {[c]}"}.
+ In our running example, @{text "X\<^isub>2"} and @{text "X\<^isub>3"} are the only
+ equivalence classes in @{term "finals {[a], [a, b]}"}.
It is straightforward to show that in general
%
\begin{equation}\label{finalprops}
@@ -723,10 +725,16 @@
%Note that we do not define formally an automaton here,
%we merely relate two sets
%(with the help of a character).
- In our concrete example we have
- @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<^isub>i\<Rightarrow> X\<^isub>3"} with @{text "d\<^isub>i"} being any
- other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>c\<^isub>j\<Rightarrow> X\<^isub>3"} for any
- character @{text "c\<^isub>j"}.
+ In our concrete example we have
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{term "X\<^isub>1 \<Turnstile>a\<Rightarrow> X\<^isub>2"},\; @{term "X\<^isub>1 \<Turnstile>b\<Rightarrow> X\<^isub>4"};\\
+ @{term "X\<^isub>2 \<Turnstile>b\<Rightarrow> X\<^isub>3"},\; @{term "X\<^isub>2 \<Turnstile>a\<Rightarrow> X\<^isub>4"};\\
+ @{term "X\<^isub>3 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>3 \<Turnstile>b\<Rightarrow> X\<^isub>4"} and\\
+ @{term "X\<^isub>4 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>4 \<Turnstile>b\<Rightarrow> X\<^isub>4"}.
+ \end{tabular}
+ \end{center}
Next we construct an \emph{initial equational system} that
contains an equation for each equivalence class. We first give
@@ -773,17 +781,14 @@
\begin{equation}\label{exmpcs}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
- @{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM c)"}\\
- @{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>1, ATOM d\<^isub>1) + \<dots> + (X\<^isub>1, ATOM d\<^isub>n)"}\\
- & & \mbox{}\hspace{10mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}
+ @{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM a)"}\\
+ @{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>2, ATOM b)"}\\
+ @{term "X\<^isub>4"} & @{text "="} & @{text "(X\<^isub>1, ATOM b) + (X\<^isub>2, ATOM a) + (X\<^isub>3, ATOM a)"}\\
+ & & \mbox{}\hspace{0mm}@{text "+ (X\<^isub>3, ATOM b) + (X\<^isub>4, ATOM a) + (X\<^isub>4, ATOM b)"}\\
\end{tabular}}
\end{equation}
-
+
\noindent
- where @{text "d\<^isub>1\<dots>d\<^isub>n"} is the sequence of all characters
- but not containing @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
- characters.
-
Overloading the function @{text \<calL>} for the two kinds of terms in the
equational system, we have
@@ -883,26 +888,23 @@
then we calculate the combined regular expressions for all @{text r} coming
from the deleted @{text "(X, r)"}, and take the @{const Star} of it;
finally we append this regular expression to @{text rhs'}. If we apply this
- operation to the right-hand side of @{text "X\<^isub>3"} in \eqref{exmpcs}, we obtain
+ operation to the right-hand side of @{text "X\<^isub>4"} in \eqref{exmpcs}, we obtain
the equation:
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{term "X\<^isub>3"} & @{text "="} &
- @{text "(X\<^isub>1, TIMES (ATOM d\<^isub>1) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m})) + \<dots> "}\\
- & & \mbox{}\hspace{13mm}
- @{text "\<dots> + (X\<^isub>1, TIMES (ATOM d\<^isub>n) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}))"}
+ @{term "X\<^isub>4"} & @{text "="} &
+ @{text "(X\<^isub>1, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+ & & @{text "(X\<^isub>2, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+ & & @{text "(X\<^isub>3, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+ & & @{text "(X\<^isub>3, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b}))"}
\end{tabular}
\end{center}
\noindent
- That means we eliminated the recursive occurrence of @{text "X\<^isub>3"} on the
- right-hand side. Note we used the abbreviation
- @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}"}
- to stand for a regular expression that matches with every character. In
- our algorithm we are only interested in the existence of such a regular expression
- and do not specify it any further.
+ That means we eliminated the recursive occurrence of @{text "X\<^isub>4"} on the
+ right-hand side.
It can be easily seen that the @{text "Arden"}-operation mimics Arden's
Lemma on the level of equations. To ensure the non-emptiness condition of
@@ -951,7 +953,7 @@
%
\begin{equation}\label{exmpresult}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{term "X\<^isub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM c))"}
+ @{term "X\<^isub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM a))"}
\end{tabular}}
\end{equation}
@@ -1194,7 +1196,15 @@
\begin{proof}[of Theorem~\ref{myhillnerodeone}]
By Lemma~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
- every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
+ every equivalence class in @{term "UNIV // \<approx>A"}:
+
+ \[
+ \mbox{if}\;@{term "X \<in> (UNIV // \<approx>A)"}\;\mbox{then there exists a}\;
+ @{text "r"}\;\mbox{such that}\;@{term "X = lang r"}
+ \]\smallskip
+
+ \noindent
+ Since @{text "finals A"} is
a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
in @{term "finals A"} there exists a regular expression. Moreover by assumption
we know that @{term "finals A"} must be finite, and therefore there must be a finite
@@ -1205,12 +1215,27 @@
\end{proof}
\noindent
+ Solving the equational system of our running example gives as solution for the
+ two final equivalence classes:
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{text "X\<^isub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
+ @{text "X\<^isub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Combining them with $\bigplus$ gives us a regular expression for the language @{text "{[a], [a, b]}"}.
+
Note that our algorithm for solving equational systems provides also a method for
calculating a regular expression for the complement of a regular language:
if we combine all regular
- expressions corresponding to equivalence classes not in @{term "finals A"},
+ expressions corresponding to equivalence classes not in @{term "finals A"}
+ (in the running example @{text "X\<^isub>1"} and @{text "X\<^isub>4"}),
then we obtain a regular expression for the complement language @{term "- A"}.
This is similar to the usual construction of a `complement automaton'.
+
*}
section {* Myhill-Nerode, Second Part *}
@@ -1296,10 +1321,13 @@
\noindent
For constructing @{text R}, we will rely on some \emph{tagging-functions}
- defined over strings. Given the inductive hypothesis, it will be easy to
+ defined over strings, see Fig.~\ref{tagfig}. They are parameterised by sets
+ of strings @{text A} and @{text B} standing for the induction hypotheses.
+ Given the inductive hypotheses, it will be easy to
prove that the \emph{range} of these tagging-functions is finite. The range
of a function @{text f} is defined as
+
\begin{center}
@{text "range f \<equiv> f ` UNIV"}
\end{center}
@@ -1334,6 +1362,24 @@
is finite, then the set @{text A} itself must be finite. We can use it to establish the following
two lemmas.
+ \begin{figure}[t]
+ \normalsize
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{thm (lhs) tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]} &
+ @{text "\<equiv>"} &
+ @{thm (rhs) tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]} \\
+ @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"} & @{text "\<equiv>"} &
+ @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}\\
+ @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]} & @{text "\<equiv>"} &
+ @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
+ \end{tabular}
+ \caption{Three tagging functions used the cases for @{term "PLUS"}, @{term "TIMES"} and @{term "STAR"}
+ regular expressions. The sets @{text A} and @{text B} are arbitrary languages instantiated
+ in the proof with the induction hypotheses. \emph{Partitions} is a function
+ that generates all possible partitions of a string.\label{tagfig}}
+ \end{figure}
+
+
\begin{lemma}\label{finone}
@{thm[mode=IfThen] finite_eq_tag_rel}
\end{lemma}
@@ -1379,7 +1425,7 @@
Chaining Lemma~\ref{finone} and \ref{fintwo} together, means in order to show
that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
- Let us attempt the @{const PLUS}-case first. We take as tagging-function
+ Let us attempt the @{const PLUS}-case first. We take as tagging-function from Fig.~\ref{tagfig}
\begin{center}
@{thm tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
@@ -1510,7 +1556,7 @@
tagging-function in the @{const Times}-case as:
\begin{center}
- @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~
+ @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"}~@{text "\<equiv>"}~
@{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
\end{center}
@@ -1679,6 +1725,58 @@
A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set
@{text "A"} to @{term "lang r"} and thus complete the proof.
\end{proof}
+
+ \begin{rmk}
+ While our proof using tagging functions might seem like a rabbit pulled
+ out of a hat, the intuition behind can be rationalised taking the
+ view that the equivalence classes @{term "UNIV // \<approx>(lang r)"} stand for the
+ states of the minimal automaton for the language @{term "lang r"}. The theorem
+ amounts to showing that this minimal automaton has finitely many states.
+ However, by showing that our @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} relation
+ refines @{term "\<approx>A"} we do not actually have to show that the minimal automata
+ has finitely many states, but only that we can show finiteness for an
+ automaton with at least as many states and which can recognise the same
+ language. By performing the induction over the regular expression @{text r},
+ this means we have to construct inductively an automaton in
+ the cases for @{term PLUS}, @{term TIMES} and @{term STAR}.
+
+ In the @{text PLUS}-case, we can assume finitely many equivalence classes of the form
+ @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"} and @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>B\<^esub>"}, each standing for an automaton recognising the
+ languages @{text A} and @{text B} respectively.
+ The @{text "+tag"} function constructs pairs of the form @{text "(\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>, \<lbrakk>_\<rbrakk>\<^bsub>\<approx>B\<^esub>)"}
+ which can be seen as the states of an automaton recognising the language
+ \mbox{@{term "A \<union> B"}}. This is the usual product construction of automata:
+ Given a string @{text x}, the first automata will be in the state @{text "\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>"}
+ after recognising @{text x} (similarly @{text "\<lbrakk>x\<rbrakk>\<^bsub>\<approx>B\<^esub>"} for the other automaton). The product
+ automaton will be in the state \mbox{@{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, \<lbrakk>x\<rbrakk>\<^bsub>\<approx>B\<^esub>)"}}, which is accepting
+ if at least one component is an accepting state.
+
+ The @{text "TIMES"}-case is a bit more complicated---essentially we
+ need to sequentially compose the two automata with the states @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"},
+ respectively @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>B\<^esub>"}. We achieve this sequential composition by
+ taking the first automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"} and append on each of its accepting
+ state the automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>B\<^esub>"}. Unfortunately, this does not lead directly
+ to a correct composition, since the automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"} might have consumed
+ some of the input needed for the automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>B\<^esub>"} to succeed. The
+ textbook construction for sequentially composing two automata circumvents this
+ problem by connecting the terminating states of the first automaton via
+ an epsilon-transition to the initial state of the second automaton (see for
+ example \citeN{Kozen97}). In the absence of any epsilon-transition analogue in our work,
+ we let the second automaton
+ start in all possible states that may have been reached if the first
+ automaton had not consumed the input meant for the second. We achieve this
+ by having a set of states as the second component generated by our
+ @{text "\<times>tag"} function (see second clause in Fig.~\ref{tagfig}).
+ A state of this sequentially composed automaton is accepting, if the first
+ component is accepting and at least one state in the set is also accepting.
+
+ The idea behind the @{text "STAR"}-case is similar to the @{text "TIMES"}-case.
+ We assume some automaton has consumed some strictly smaller part of the input;
+ we need to check that from the state we ended up in a terminal state in the
+ automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"}. Since we do not know from which state this will
+ succeed, we need to run the automaton from all possible states we could have
+ ended up in. Therefore the @{text "\<star>tag"} function generates a set of states.
+ \end{rmk}
*}
section {* Second Part proved using Partial Derivatives *}
@@ -2211,12 +2309,12 @@
%
\begin{equation}\label{supseqprops}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{thm (lhs) SUPSEQ_simps(1)} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_simps(1)}\\
- @{thm (lhs) SUPSEQ_simps(2)} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_simps(2)}\\
- @{thm (lhs) SUPSEQ_atom} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_atom}\\
- @{thm (lhs) SUPSEQ_union} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_union}\\
- @{thm (lhs) SUPSEQ_conc} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_conc}\\
- @{thm (lhs) SUPSEQ_star} & @{text "\<equiv>"} & @{thm (rhs) SUPSEQ_star}
+ @{thm (lhs) SUPSEQ_simps(1)} & @{text "="} & @{thm (rhs) SUPSEQ_simps(1)}\\
+ @{thm (lhs) SUPSEQ_simps(2)} & @{text "="} & @{thm (rhs) SUPSEQ_simps(2)}\\
+ @{thm (lhs) SUPSEQ_atom} & @{text "="} & @{thm (rhs) SUPSEQ_atom}\\
+ @{thm (lhs) SUPSEQ_union} & @{text "="} & @{thm (rhs) SUPSEQ_union}\\
+ @{thm (lhs) SUPSEQ_conc} & @{text "="} & @{thm (rhs) SUPSEQ_conc}\\
+ @{thm (lhs) SUPSEQ_star} & @{text "="} & @{thm (rhs) SUPSEQ_star}
\end{tabular}}
\end{equation}
@@ -2365,24 +2463,9 @@
exists a regular expression that matches all of its strings. Regular
expressions can conveniently be defined as a datatype in theorem
provers. For us it was therefore interesting to find out how far we can push
- this point of view. But this question whether formal language theory can
- be done without automata crops up also in non-theorem prover contexts. For
- example, Gasarch asked in the Computational Complexity blog by \citeN{GasarchBlog}
- whether the complementation of
- regular-expression languages can be proved without using automata. He concluded
-
- \begin{quote}
- {\it \ldots it can't be done}
- \end{quote}
-
- \noindent
- and even pondered
-
- \begin{quote}
- {\it \ldots [b]ut is there a rigorous way to even state that?}
- \end{quote}
-
- \noindent
+ this point of view. But this question whether regular language theory can
+ be done without automata crops up also in non-theorem prover contexts. Recall
+ Gasarch's speculation cited in the Introduction.
We have established in Isabelle/HOL both directions
of the Myhill-Nerode Theorem.
%
@@ -2398,7 +2481,7 @@
Pumping Lemma). We can also use it to establish the standard
textbook results about closure properties of regular languages. The case of
closure under complement follows easily from the Myhill-Nerode Theorem.
- So our answer to Gasarch is ``{\it it can be done!''}
+ So our answer to Gasarch is ``{\it yes we can!''}
%Our insistence on regular expressions for proving the Myhill-Nerode Theorem
%arose from the problem of defining formally the regularity of a language.
@@ -2465,15 +2548,15 @@
in the `pencil-and-paper-reasoning' literature about our way of proving the
first direction of the Myhill-Nerode Theorem, but it appears to be folklore.
- We presented two proofs for the second direction of the Myhill-Nerode
- Theorem. One direct proof using tagging-functions and another using partial
- derivatives. This part of our work is where our method using regular
- expressions shines, because we can completely side-step the standard
- argument (for example used by \citeN{Kozen97}) where automata need to be composed. However, it is
- also the direction where we had to spend most of the `conceptual' time, as
- our first proof based on tagging-functions is new for establishing the
- Myhill-Nerode Theorem. All standard proofs of this direction proceed by
- arguments over automata.
+ We presented two proofs for the second direction of the
+ Myhill-Nerode Theorem. One direct proof using tagging-functions and
+ another using partial derivatives. This part of our work is where
+ our method using regular expressions shines, because we can perform
+ an induction on the structure of refular expressions. However, it is
+ also the direction where we had to spend most of the `conceptual'
+ time, as our first proof based on tagging-functions is new for
+ establishing the Myhill-Nerode Theorem. All standard proofs of this
+ direction proceed by arguments over automata.
The indirect proof for the second direction arose from our interest in
Brzozowski's derivatives for regular expression matching. While \citeN{Brzozowski64}