diff -r 3c9129f49846 -r 990c12ab1562 Paper/Paper.thy --- a/Paper/Paper.thy Thu Apr 28 03:24:20 2011 +0000 +++ b/Paper/Paper.thy Wed May 04 07:05:59 2011 +0000 @@ -76,8 +76,8 @@ 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] @@ -199,7 +199,7 @@ 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: @@ -225,7 +225,7 @@ \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 @@ -465,14 +465,18 @@ \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 \c\<^isub>i\<^isub>j\ - X\<^isub>i"}. If viewed as an automaton, then every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system - corresponds roughly to a state 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}. In our initial equation system there can only be + X\<^isub>i"}. + %The intuition behind the equational system is that every + %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system + %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 - "\(EMPTY)"} in the first equation acts as a marker for the equivalence class + equivalence classes and only finitely many characters. + The term @{text "\(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 @@ -481,6 +485,10 @@ 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 \} for the two kinds of terms in the equational system, we have @@ -501,7 +509,7 @@ hold. Similarly for @{text "X\<^isub>1"} we can show the following equation % \begin{equation}\label{inv2} - @{text "X\<^isub>1 = \(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \ \ \ \(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \ \(\(EMPTY))"}. + @{text "X\<^isub>1 = \(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \ \ \ \(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \ \(\(EMPTY))"}. \end{equation} \noindent @@ -653,7 +661,7 @@ \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: @@ -854,12 +862,7 @@ 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 - - \begin{center} - @{term "\(finals A) = L (\rs)"} - \end{center} - - \noindent + @{term "\(finals A) = L (\rs)"}. Since the left-hand side is equal to @{text A}, we can use @{term "\rs"} as the regular expression that is needed in the theorem.\qed \end{proof} @@ -917,7 +920,7 @@ \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 \ tag x = tag y"}. + @{text "x =tag= y \ tag x = tag y"}\;. \end{center} \end{definition} @@ -1041,11 +1044,9 @@ and \emph{string subtraction}: % \begin{center} - \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} - @{text "[] - y"} & @{text "\"} & @{text "[]"}\\ - @{text "x - []"} & @{text "\"} & @{text x}\\ - @{text "cx - dy"} & @{text "\"} & @{text "if c = d then x - y else cx"}\\ - \end{tabular} + @{text "[] - y \ []"}\hspace{10mm} + @{text "x - [] \ x"}\hspace{10mm} + @{text "cx - dy \ if c = d then x - y else cx"} \end{center} % \noindent @@ -1055,11 +1056,12 @@ 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, 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 xxa] (z) { $\hspace{10.1em}@{text z}\hspace{10.1em}$ }; + \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.2em}@{text "x - x'"}\hspace{0.2em}$ }; + \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)$) @@ -1081,12 +1083,12 @@ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{term "x' \ 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, right=-0.03em of x] (za) { $\hspace{2em}@{text "z'"}\hspace{2em}$ }; - \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] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ }; + \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{2.6em}@{text "z - z'"}\hspace{2.6em}$ }; \draw[decoration={brace,transform={yscale=3}},decorate] (x.north west) -- ($(za.north west)+(0em,0em)$) @@ -1108,6 +1110,7 @@ ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$) node[midway, below=0.5em]{@{text "(z - z') \ B"}}; \end{tikzpicture}} + \end{tabular} \end{center} % \noindent @@ -1307,7 +1310,8 @@ \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 "\"} non-deterministic automaton @{text "\"} deterministic automaton @{text "\"} complement automaton @{text "\"} @@ -1359,22 +1363,28 @@ 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 - respect to a language (if regarded equal modulo ACI). We could - have used as the tag of a string @{text s} the set of derivatives of a regular expression - generated by a language. Using the fact that two strings are + expressions and shows that for every language there can be only + finitely many of them %derivations + (if regarded equal modulo ACI). We could + 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. *}