regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:29915abff9c2
+:c8cb6914f4c8
 that matches all strings of @{text "A"}.
 \end{definition}
 \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
+free in HOL.
-done without automata crops up also in non-theorem prover
-contexts. For example, Gasarch asked in the Computational Complexity
+While our choice of using regular expressions is motivated by
-blog by \citeN{GasarchBlog} whether the complementation of
+shortcomings in theorem provers, the question whether formal
-regular-expression languages can be proved without using
+language theory can be done without automata crops up also in
-automata. He concluded
+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}
 ``{\it \ldots [b]ut is there a rigorous way to even state that?}''
 \end{quote}
 %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
 matching based on derivatives by \citeN{OwensSlind08}, and with an equivalence
 checker for regular expressions in Isabelle/HOL by \citeN{KraussNipkow11}
 \begin{proof}
 Finiteness is given by the assumption and the way how we set up the
 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
 Next we show that @{text Iter} preserves the invariant.
 given because @{const Arden} removes an equivalence class from @{text yrhs}
 and then @{const Subst_all} removes @{text Y} from the equational system.
 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
 We also need the fact that @{text Iter} decreases the termination measure.
 By assumption we know that @{text "ES"} is finite and has more than one element.
 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
 @{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
 This brings us to our property we want to establish for @{text Solve}.
 does not hold. By the stronger invariant we know there exists such a @{text "rhs"}
 with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
 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
 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
 there exists a regular expression.
 invariant and Lemma~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
 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
 Lemma~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
 of the Myhill-Nerode Theorem.
 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
 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
 Solving the equational system of our running example gives as solution for the
 two final equivalence classes:
 @{thm quot_atom_subset}
 \end{tabular}
 \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
 Much more interesting, however, are the inductive cases. They seem hard to be solved
 directly. The reader is invited to try.\footnote{The induction hypothesis is not strong enough
 provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
 \end{definition}
 \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
+defined over strings, see Fig.~\ref{tagfig}. These functions are parameterised by sets
-of strings @{text A} and @{text B} standing for the induction hypotheses.
+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
 as follows.
 \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}
 In order to establish finiteness of a set @{text A}, we shall use the following powerful
 principle from Isabelle/HOL's library.
 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
 From the assumptions we obtain \mbox{@{text "x \<in> X"}} and @{text "y \<in> Y"} with
 @{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}
 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
 We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}.
 From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
 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]}
 \end{center}
 holds. The range of @{term "tag_Plus A B"} is a subset of this product
 set---so finite. For the refinement proof-obligation, we know that @{term
 "(\<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
 The @{const TIMES}-case is slightly more complicated. We first prove the
 following lemma, which will aid the proof about refinement.
 of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the
 corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related'
 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>"}~
 @{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}
 such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
 {y\<^isub>s}"}. Unfolding the Myhill-Nerode Relation and together with the
 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
 The case for @{const Star} is similar to @{const TIMES}, but poses a few
 extra challenges.  To deal with them, we define first the notion of a \emph{string
 "y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
 y\<^isub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
 "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.
 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
 @{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 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}
 *}
 section {* Second Part proved using Partial Derivatives *}
 \end{center}
 \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
 Taking \eqref{Dersders} and \eqref{Derspders} together gives the relationship
 between languages of derivatives and partial derivatives
 \noindent
 Now the range of @{term "\<lambda>x. pderivs x r"} is a subset of @{term "Pow (pderivs_lang UNIV r)"},
 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}
 *}
 section {* Closure Properties of Regular Languages *}
 \end{tabular}
 \end{center}
 \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
 Now we can prove the main lemma w.r.t.~@{const "SUPSEQ"}, namely
 and hence by transitivity also \mbox{@{term "z \<preceq> x"}} (here we deviate from the argument
 given by \citeN{Shallit08}, because Isabelle/HOL provides already an extensive infrastructure
 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
 This lemma allows us to establish the second part of Theorem~\ref{subseqreg}.
 \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
 In order to establish the first part of this theorem, we use the
 property proved by \citeN{Shallit08}, namely that
 \begin{proof}[of the First Part of Theorem~\ref{subseqreg}]
 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
 the non-regularity of languages. For this we use the following version of the Continuation
 Lemma (see for example~\cite{Rosenberg06}).
 After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"},
 the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}.
 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
 To conclude the proof of non-regularity for the language @{text A}, the
 Continuation Lemma and the lemma above lead to a contradiction assuming
 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 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.
 %
 \begin{theorem}[Myhill-Nerode Theorem]\mbox{}\\
 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
 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).  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.
 %In order to guarantee consistency,
 %formalisations in HOL can only extend the logic with definitions that introduce a new concept in

changeset 383	c8cb6914f4c8
parent 381	99161cd17c0f
child 384	60bcf13adb77