regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:3c9129f49846
+:990c12ab1562
 In case of graphs and matrices, this means we have to build our own
 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
 HOLlight support them with libraries. Even worse, reasoning about graphs and
 matrices can be a real hassle in HOL-based theorem provers.  Consider for
 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
-connecting the accepting states of $A_1$ to the initial state of $A_2$:
+connecting the accepting states of $A_1$ to the initial state of $A_2$:\\[-5.5mm]
+%
 \begin{center}
 \begin{tabular}{ccc}
 \begin{tikzpicture}[scale=0.8]
 %\draw[step=2mm] (-1,-1) grid (1,1);
 bit strings in the context of Presburger arithmetic.
 The only larger formalisations of automata theory
 are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
 In this paper, we will not attempt to formalise automata theory in
-Isabelle/HOL, but take a completely different approach to regular
+Isabelle/HOL, but take a different approach to regular
 languages. Instead of defining a regular language as one where there exists
 an automaton that recognises all strings of the language, we define a
 regular language as:
 \begin{definition}
 complementation, for regular languages.\smallskip
 \noindent
 {\bf Contributions:}
 There is an extensive literature on regular languages.
-To our knowledge, our proof of the Myhill-Nerode theorem is the
+To our best knowledge, our proof of the Myhill-Nerode theorem is the
 first that is based on regular expressions, only. We prove the part of this theorem
 stating that a regular expression has only finitely many partitions using certain
 tagging-functions. Again to our best knowledge, these tagging-functions have
 not been used before to establish the Myhill-Nerode theorem.
 *}
 \end{center}
 \noindent
 where the terms @{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"}. If viewed as an automaton, then every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+X\<^isub>i"}.
-corresponds roughly to a state whose name is @{text X\<^isub>i} and its predecessor states
+%The intuition behind the equational system is that every
-are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
+%equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
-predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be
+%corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
+%are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
+%predecessor states to @{text X\<^isub>i}.
+There can only be
 finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side
 since by assumption there are only finitely many
-equivalence classes and only finitely many characters. The term @{text
+equivalence classes and only finitely many characters.
-"\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
+The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the initial state, that
+is the equivalence 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}, 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 a character to the end of @{text Y}. This is also the
 reason why we have to use our reverse version of Arden's Lemma.}
+%In our initial equation system there can only be
+%finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side
+%since by assumption there are only finitely many
+%equivalence classes and only finitely many characters.
 Overloading the function @{text \<calL>} for the two kinds of terms in the
 equational system, we have
 \begin{center}
 @{text "\<calL>(Y, r) \<equiv>"} %
 \noindent
 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
 %
 \begin{equation}\label{inv2}
-@{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
+@{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
 \end{equation}
 \noindent
 The reason for adding the @{text \<lambda>}-marker to our initial equational system is
 to obtain this equation: it only holds with the marker, since none of
 \end{tabular}
 \end{center}
 \noindent
 The last definition we need applies @{term Iter} over and over until a condition
-@{text Cond} is \emph{not} satisfied anymore. The condition states that there
+@{text Cond} is \emph{not} satisfied anymore. This condition states that there
 are more than one equation left in the equational system @{text ES}. To solve
 an equational system we use Isabelle/HOL's @{text while}-operator as follows:
 \begin{center}
 @{thm Solve_def}
 every equivalence class in @{term "UNIV // \<approx>A"}. 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
 set of regular expressions @{text "rs"} such that
+@{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
-\begin{center}
-@{term "\<Union>(finals A) = L (\<Uplus>rs)"}
-\end{center}
-\noindent
 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.\qed
 \end{proof}
 *}
 We formally define the notion of a \emph{tagging-relation} 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 =tag= y \<equiv> tag x = tag y"}.
+@{text "x =tag= 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
 %
 \noindent
 and \emph{string subtraction}:
 %
 \begin{center}
-\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{text "[] - y \<equiv> []"}\hspace{10mm}
-@{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
+@{text "x - [] \<equiv> x"}\hspace{10mm}
-@{text "x - []"} & @{text "\<equiv>"} & @{text x}\\
+@{text "cx - dy \<equiv> if c = d then x - y else cx"}
-@{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\
-\end{tabular}
 \end{center}
 %
 \noindent
 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
 Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split'
 this string to be in @{term "A ;; B"}:
 %
 \begin{center}
+\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 \scalebox{0.7}{
 \begin{tikzpicture}
-\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'"}\hspace{4em}$ };
+\node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
-\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'"}\hspace{0.5em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
-\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}@{text z}\hspace{10.1em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
 node[midway, above=0.5em]{@{text x}};
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
 node[midway, below=0.5em]{@{term "x' \<in> A"}};
 \end{tikzpicture}}
+&
 \scalebox{0.7}{
 \begin{tikzpicture}
-\node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}@{text x}\hspace{6.5em}$ };
+\node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
-\node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}@{text "z'"}\hspace{2em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
-\node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}@{text "z - z'"}\hspace{6.1em}$  };
+\node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$  };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 (x.north west) -- ($(za.north west)+(0em,0em)$)
 node[midway, above=0.5em]{@{text x}};
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
 node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
 \end{tikzpicture}}
+\end{tabular}
 \end{center}
 %
 \noindent
 Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
 \end{center}
 %
 \noindent
 holds for any strings @{text "s\<^isub>1"} and @{text
 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
-partitions.  Proving the existence of such a regular expression via automata would
+partitions.  Proving the existence of such a regular expression via automata
+using the standard method would
 be quite involved. It includes the
 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
 regular expression.
 Lemma.
 We briefly considered using the method Brzozowski presented in the Appendix
 of~\cite{Brzozowski64} in order to prove the second direction of the
 Myhill-Nerode theorem. There he calculates the derivatives for regular
-expressions and shows that there can be only finitely many of them with
+expressions and shows that for every language there can be only
-respect to a language (if regarded equal modulo ACI). We could
+finitely many of them %derivations
-have used as the tag of a string @{text s} the set of derivatives of a regular expression
+(if regarded equal modulo ACI). We could
-generated by a language.  Using the fact that two strings are
+have used as tagging-function the set of derivatives of a regular expression
+with respect to a language.  Using the fact that two strings are
 Myhill-Nerode related whenever their derivative is the same, together with
 the fact that there are only finitely such derivatives
 would give us a similar argument as ours. However it seems not so easy to
-calculate the set of derivatives modulo ACI and then to count them. Therefore we preferred our
+calculate the set of derivatives modulo ACI. Therefore we preferred our
 direct method of using tagging-functions. This
 is also where our method shines, because we can completely side-step the
 standard argument \cite{Kozen97} where automata need to be composed, which
-as stated in the Introduction is not so convenient to formalise in a
+as stated in the Introduction is not so easy to formalise in a
 HOL-based theorem prover. However, it is also the direction where we had to
 spend most of the `conceptual' time, as our proof-argument based on tagging-functions
 is new for establishing the Myhill-Nerode theorem. All standard proofs
-of this direction proceed by arguments over automata.
+of this direction use %proceed by
+arguments over automata.\\[-6mm]%\medskip
+%
+%\noindent
+%{\bf Acknowledgements:} We are grateful for the comments we received from Larry
+%Paulson and the referees of the paper.
 *}
 (*<*)

changeset 159	990c12ab1562
parent 157	10d2d0cbe381
child 160	ea2e5acbfe4a