--- a/Journal/Paper.thy Wed Jul 10 17:59:00 2013 +0100
+++ b/Journal/Paper.thy Thu Jul 11 12:07:11 2013 +0100
@@ -442,16 +442,20 @@
\noindent
We then want to `forget' automata completely and see how far we come
- with formalising results from regular language theory. The reason
+ with formalising results from regular language theory by only using regular
+ expressions. The reason
is that regular expressions, unlike graphs, matrices and
functions, can be defined as an inductive datatype and a reasoning
infrastructure for them (like induction and recursion) comes for
- free in HOL. 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
+ free in HOL.
+
+ While our choice of using regular expressions is motivated by
+ shortcomings in theorem provers, the 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}''
@@ -466,8 +470,7 @@
%Moreover, no side-conditions will be needed for regular expressions,
%like we need for automata.
- \noindent
- We will give an answer to these questions in this paper.
+
The convenience of regular expressions has
recently been exploited in HOL4 with a formalisation of regular expression
@@ -1077,7 +1080,7 @@
initial equational system. Soundness is proved in Lemma~\ref{inv}. Distinctness
follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
property also follows from the setup of the initial equational system, as does
- validity.
+ validity.\qed
\end{proof}
\noindent
@@ -1114,7 +1117,7 @@
Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
which matches with our proof-obligation of @{const "Subst_all"}. Since
\mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption
- to complete the proof.
+ to complete the proof.\qed
\end{proof}
\noindent
@@ -1133,7 +1136,7 @@
@{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
removes the equation @{text "Y = yrhs"} from the system, and therefore
- the cardinality of @{const Iter} strictly decreases.
+ the cardinality of @{const Iter} strictly decreases.\qed
\end{proof}
\noindent
@@ -1165,7 +1168,7 @@
of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
for which the invariant holds. This allows us to conclude that
@{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
- as needed.
+ as needed.\qed
\end{proof}
\noindent
@@ -1187,7 +1190,7 @@
removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = lang (\<Uplus>rs)"}.
- With this we can conclude the proof.
+ With this we can conclude the proof.\qed
\end{proof}
\noindent
@@ -1211,7 +1214,7 @@
set of regular expressions @{text "rs"} such that
@{term "\<Union>(finals A) = lang (\<Uplus>rs)"}.
Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
- as the regular expression that is needed in the theorem.
+ as the regular expression that is needed in the theorem.\qed
\end{proof}
\noindent
@@ -1267,7 +1270,7 @@
\end{center}
\noindent
- hold, which shows that @{term "UNIV // \<approx>(lang r)"} must be finite.
+ hold, which shows that @{term "UNIV // \<approx>(lang r)"} must be finite.\qed
\end{proof}
\noindent
@@ -1321,8 +1324,9 @@
\noindent
For constructing @{text R}, we will rely on some \emph{tagging-functions}
- defined over strings, see Fig.~\ref{tagfig}. They are parameterised by sets
- of strings @{text A} and @{text B} standing for the induction hypotheses.
+ defined over strings, see Fig.~\ref{tagfig}. These functions are parameterised by sets
+ of strings @{text A} and @{text B} standing for arbitrary languages and will
+ by instantiated with 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
@@ -1344,9 +1348,9 @@
\begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
and @{text y} are \emph{tag-related} provided
- \begin{center}
+ \[
@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
- \end{center}
+ \]
\end{definition}
@@ -1394,7 +1398,7 @@
@{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
turn means that the equivalence classes @{text X}
and @{text Y} must be equal. Therefore \eqref{finiteimageD} allows us to conclude
- with @{thm (concl) finite_eq_tag_rel}.
+ with @{thm (concl) finite_eq_tag_rel}.\qed
\end{proof}
\begin{lemma}\label{fintwo}
@@ -1418,14 +1422,14 @@
and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
- they must also be @{text "R\<^isub>2"}-related, as we need to show.
+ they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
\end{proof}
\noindent
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 from Fig.~\ref{tagfig}
+ Let us attempt the @{const PLUS}-case first. We take from Fig.~\ref{tagfig}
\begin{center}
@{thm tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
@@ -1446,7 +1450,7 @@
"(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"}, as we needed to
show. Finally we can discharge this case by setting @{text A} to @{term
- "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
+ "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.\qed
\end{proof}
\noindent
@@ -1553,7 +1557,7 @@
to @{text "y\<^isub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
This will solve the second case.
Taking the two requirements, @{text "("}@{text "*"}@{text ")"} and @{text "(**)"}, together we define the
- tagging-function in the @{const Times}-case as:
+ tagging-function in the @{const Times}-case as (see Fig.~\ref{tagfig}):
\begin{center}
@{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"}~@{text "\<equiv>"}~
@@ -1608,7 +1612,7 @@
facts that @{text "x\<^isub>p \<in> A"} and \mbox{@{text "x\<^isub>s @ z \<in> B"}}, we
obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
this case. We again can complete the @{const TIMES}-case by setting @{text
- A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
+ A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.\qed
\end{proof}
\noindent
@@ -1723,12 +1727,12 @@
"y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
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.
+ @{text "A"} to @{term "lang r"} and thus complete the proof.\qed
\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
+ out of a hat, the intuition behind can be somewhat 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.
@@ -1771,11 +1775,15 @@
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 assume some automaton has consumed some strictly smaller part of the input in @{text "A\<^isup>\<star>"};
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
+ automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"} can be reached. 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.
+ ended up in. Therefore the @{text "\<star>tag"} function generates again a set of states.
+
+ However, note that while the automata view sheds some light behind the idea of the
+ tagging functions, our proof only works because we can perform a structural
+ induction on the regular expression @{text r}.
\end{rmk}
*}
@@ -2044,7 +2052,7 @@
\noindent
Note that in order to apply the induction hypothesis in the fourth equation, we
need the generalisation over all regular expressions @{text r}. The case for
- the empty string is routine and omitted.
+ the empty string is routine and omitted.\qed
\end{proof}
\noindent
@@ -2142,7 +2150,7 @@
which we know is finite by Theorem~\ref{antimirov}. Consequently there
are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"}.
This relation refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the
- second part of the Myhill-Nerode Theorem.
+ second part of the Myhill-Nerode Theorem.\qed
\end{proof}
*}
@@ -2346,7 +2354,7 @@
\noindent
and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows
- that @{term "SUPSEQ A"} is regular, provided @{text A} is.
+ that @{term "SUPSEQ A"} is regular, provided @{text A} is.\qed
\end{proof}
\noindent
@@ -2381,7 +2389,7 @@
for reasoning about well-foundedness). Since @{term "z"} is
minimal and an element in @{term A}, we also know that @{term z} is in @{term M}.
From this together with \mbox{@{term "z \<preceq> x"}}, we can infer that @{term x} is in
- @{term "SUPSEQ M"}, as required.
+ @{term "SUPSEQ M"}, as required.\qed
\end{proof}
\noindent
@@ -2390,7 +2398,7 @@
\begin{proof}[of the Second Part of Theorem~\ref{subseqreg}]
Given any language @{text A}, by Lemma~\ref{mset} we know there exists
a finite, and thus regular, language @{text M}. We further have @{term "SUPSEQ M = SUPSEQ A"},
- which establishes the second part.
+ which establishes the second part.\qed
\end{proof}
\noindent
@@ -2408,7 +2416,7 @@
By the second part, we know the right-hand side of \eqref{compl}
is regular, which means @{term "- SUBSEQ A"} is regular. But since
we established already that regularity is preserved under complement (using Myhill-Nerode),
- also @{term "SUBSEQ A"} must be regular.
+ also @{term "SUBSEQ A"} must be regular.\qed
\end{proof}
Finally we like to show that the Myhill-Nerode Theorem is also convenient for establishing
@@ -2443,7 +2451,7 @@
That means we have to show that @{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"} leads to
a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}.
But since @{term "i \<noteq> j"}, @{text "a\<^sup>j @ b\<^sup>i \<notin> A"}. Therefore @{text "a\<^sup>i"} and @{text "a\<^sup>j"}
- cannot be Myhill-Nerode related by @{text "A"}, and we are done.
+ cannot be Myhill-Nerode related by @{text "A"}, and we are done.\qed
\end{proof}
\noindent
@@ -2461,11 +2469,11 @@
\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 theorem
+ expressions can be conveniently 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 regular language theory can
be done without automata crops up also in non-theorem prover contexts. Recall
- Gasarch's speculation cited in the Introduction.
+ Gasarch's comment cited in the Introduction.
We have established in Isabelle/HOL both directions
of the Myhill-Nerode Theorem.
%
@@ -2481,7 +2489,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 yes we can!''}
+ 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.