# HG changeset patch # User urbanc # Date 1315494482 0 # Node ID 47446f111550d20b46c8e0ac8115c14197f6032e # Parent 087e6c255e33062794f19ca210def78f0ea92b1f one more itteration on the paper diff -r 087e6c255e33 -r 47446f111550 Journal/Paper.thy --- a/Journal/Paper.thy Wed Sep 07 18:17:56 2011 +0000 +++ b/Journal/Paper.thy Thu Sep 08 15:08:02 2011 +0000 @@ -320,7 +320,7 @@ changes the type---the disjoint union is not a set, but a set of pairs. Using this definition for disjoint union means we do not have a single type for the states of automata. As a result we will not be able to - define in our fomalisation a regular language as one for which there exists + define a regular language as one for which there exists an automaton that recognises all its strings (Definition~\ref{baddef}). This is because we cannot make a definition in HOL that is only polymorphic in the state type, but not in the predicate for regularity; and there is no @@ -386,7 +386,7 @@ establishing properties about regular languages. However, paper proofs about automata often involve subtle side-conditions which are easily overlooked, but which make formal reasoning rather painful. For example - Kozen's proof of the Myhill-Nerode theorem requires that automata do not + Kozen's proof of the Myhill-Nerode Theorem requires that automata do not have inaccessible states \cite{Kozen97}. Another subtle side-condition is completeness of automata, that is automata need to have total transition functions and at most one `sink' state from which there is no connection to @@ -423,17 +423,17 @@ matching based on derivatives \cite{OwensSlind08} and with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}. The main purpose of this paper is to show that a central result about regular - languages---the Myhill-Nerode theorem---can be recreated by only using + languages---the Myhill-Nerode Theorem---can be recreated by only using regular expressions. This theorem gives necessary and sufficient conditions for when a language is regular. As a corollary of this theorem we can easily establish the usual closure properties, including complementation, for regular languages. We use the continuation lemma \cite{Rosenberg06}, - which is also a corollary of the Myhill-Nerode theorem, for establishing + which is also a corollary of the Myhill-Nerode Theorem, for establishing the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip \noindent {\bf Contributions:} There is an extensive literature on regular languages. - To our best knowledge, our proof of the Myhill-Nerode theorem is the first + To our best knowledge, our proof of the Myhill-Nerode Theorem is the first that is based on regular expressions, only. The part of this theorem stating that finitely many partitions imply regularity of the language is proved by an argument about solving equational systems. This argument appears to be @@ -441,12 +441,12 @@ certain tagging-functions, and another indirect proof using Antimirov's partial derivatives \cite{Antimirov95}. Again to our best knowledge, the tagging-functions have not been used before for establishing the Myhill-Nerode - theorem. Derivatives of regular expressions have been used recently quite + Theorem. Derivatives of regular expressions have been used recently quite widely in the literature; partial derivatives, in contrast, attract much less attention. However, partial derivatives are more suitable in the - context of the Myhill-Nerode theorem, since it is easier to establish + context of the Myhill-Nerode Theorem, since it is easier to establish formally their finiteness result. We are not aware of any proof that uses - either of them for proving the Myhill-Nerode theorem. + either of them for proving the Myhill-Nerode Theorem. *} section {* Preliminaries *} @@ -614,8 +614,8 @@ text {* \noindent - The key definition in the Myhill-Nerode theorem is the - \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two + The key definition in the Myhill-Nerode Theorem is the + \emph{Myhill-Nerode Relation}, which states that w.r.t.~a language two strings are related, provided there is no distinguishing extension in this language. This can be defined as a tertiary relation. @@ -644,7 +644,7 @@ \end{tabular} \end{center} - One direction of the Myhill-Nerode theorem establishes + One direction of the Myhill-Nerode Theorem establishes that if there are finitely many equivalence classes, like in the example above, then the language is regular. In our setting we therefore have to show: @@ -732,7 +732,7 @@ 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 + 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 reversed version of Arden's Lemma.} @@ -1152,7 +1152,7 @@ \noindent Lemma~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction - of the Myhill-Nerode theorem. + of the Myhill-Nerode Theorem. \begin{proof}[Proof of Theorem~\ref{myhillnerodeone}] By Lemma~\ref{every_eqcl_has_reg} we know that there exists a regular expression for @@ -1183,7 +1183,7 @@ text {* \noindent In this section we will give a proof for establishing the second - part of the Myhill-Nerode theorem. It can be formulated in our setting as follows: + part of the Myhill-Nerode Theorem. It can be formulated in our setting as follows: \begin{thrm}\label{myhillnerodetwo} Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}. @@ -1259,7 +1259,7 @@ \end{dfntn} \noindent - For constructing @{text R}, will rely on some \emph{tagging-functions} + For constructing @{text R}, we will rely on some \emph{tagging-functions} defined over strings. Given the inductive hypothesis, 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 @@ -1498,7 +1498,7 @@ "z\<^isub>s"} such that @{term "x @ z\<^isub>p \ A"} and @{text "z\<^isub>s \ B"}. By the assumption about @{term "tag_Times A B"} we have @{term "\A `` {x} = \A `` {y}"} and thus @{term "x \A y"}. Hence by the Myhill-Nerode - relation @{term "y @ z\<^isub>p \ A"} holds. Using @{text "z\<^isub>s \ B"}, + Relation @{term "y @ z\<^isub>p \ A"} holds. Using @{text "z\<^isub>s \ B"}, we can conclude in this case with @{term "y @ z \ A \ B"} (recall @{text "z\<^isub>p @ z\<^isub>s = z"}). @@ -1519,7 +1519,7 @@ \noindent This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"} such that @{term "y\<^isub>p \ A"} and @{term "\B `` {x\<^isub>s} = \B `` - {y\<^isub>s}"}. Unfolding the Myhill-Nerode relation and together with the + {y\<^isub>s}"}. Unfolding the Myhill-Nerode Relation and together with the facts that @{text "x\<^isub>p \ A"} and \mbox{@{text "x\<^isub>s @ z \ B"}}, we obtain @{term "y\<^isub>p \ A"} and @{text "y\<^isub>s @ z \ B"}, as needed in this case. We again can complete the @{const TIMES}-case by setting @{text @@ -1634,7 +1634,7 @@ \noindent From this we know there exist a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"} with @{term "y\<^isub>p \ A\"} and also @{term "x\<^isub>s \A - y\<^isub>s"}. Unfolding the Myhill-Nerode relation we know @{term + y\<^isub>s"}. Unfolding the Myhill-Nerode Relation we know @{term "y\<^isub>s @ z\<^isub>a \ A"}. We also know that @{term "z\<^isub>b \ A\"}. Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \ A\"}, which means @{term "y @ z \ A\"}. The last step is to set @@ -1647,7 +1647,7 @@ text {* \noindent As we have seen in the previous section, in order to establish - the second direction of the Myhill-Nerode theorem, it is sufficient to find + the second direction of the Myhill-Nerode Theorem, it is sufficient to find a more refined relation than @{term "\(lang r)"} for which we can show that there are only finitely many equivalence classes. So far we showed this directly by induction on @{text "r"} using tagging-functions. @@ -1674,7 +1674,7 @@ \noindent where we apply the left-quotient to a set of languages and then combine the results. - Clearly we have the following equivalence between the Myhill-Nerode relation + Clearly we have the following equivalence between the Myhill-Nerode Relation (Definition~\ref{myhillneroderel}) and left-quotients \begin{equation}\label{mhders} @@ -1764,7 +1764,7 @@ \end{equation} \noindent - The importance of this fact in the context of the Myhill-Nerode theorem is that + The importance of this fact in the context of the Myhill-Nerode Theorem is that we can use \eqref{mhders} and \eqref{Dersders} in order to establish that @@ -1783,10 +1783,10 @@ \noindent This means the right-hand side (seen as a relation) refines the Myhill-Nerode - relation. Consequently, we can use @{text + Relation. Consequently, we can use @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as a tagging-relation. However, in order to be useful for the second part of the - Myhill-Nerode theorem, we have to be able to establish that for the + Myhill-Nerode Theorem, we have to be able to establish that for the corresponding language there are only finitely many derivatives---thus ensuring that there are only finitely many equivalence classes. Unfortunately, this is not true in general. Sakarovitch gives an @@ -1978,7 +1978,7 @@ the details. Let us now return to our proof for the second direction in the Myhill-Nerode - theorem. The point of the above calculations is to use + Theorem. The point of the above calculations is to use @{text "\<^raw:$\threesim$>\<^bsub>(\x. pders x r)\<^esub>"} as tagging-relation. @@ -2007,7 +2007,7 @@ which we know is finite by Theorem~\ref{antimirov}. Consequently there are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\x. pders x r)\<^esub>"}. This relation refines @{term "\(lang r)"}, and therefore we can again conclude the - second part of the Myhill-Nerode theorem. + second part of the Myhill-Nerode Theorem. \end{proof} *} @@ -2021,7 +2021,7 @@ More interesting in our setting is the closure under complement, because it seems difficult to construct a regular expression for the complement language by direct means. However the existence of such a regular expression can now be easily - proved using both parts of the Myhill-Nerode theorem, since + proved using both parts of the Myhill-Nerode Theorem, since \begin{center} @{term "s\<^isub>1 \A s\<^isub>2"} if and only if @{term "s\<^isub>1 \(-A) s\<^isub>2"} @@ -2150,7 +2150,7 @@ \noindent Our proof follows the one given in \cite[Pages 92--95]{Shallit08}, except that we use Higman's Lemma, which is already proved in the Isabelle/HOL library - \cite{Berghofer03}.\footnote{Unfortunately, Berghofer's formalisation of Higman's lemma + \cite{Berghofer03}.\footnote{Unfortunately, Berghofer's formalisation of Higman's Lemma is restricted to 2-letter alphabets, which means also our formalisation of Theorem~\ref{subseqreg} is `tainted' with this constraint. However our methodology is applicable to any alphabet of finite size.} @@ -2270,7 +2270,7 @@ must be regular. \end{proof} - Finally we like to show that the Myhill-Nerode theorem is also convenient for establishing + 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}). @@ -2281,11 +2281,11 @@ \end{lmm} \noindent - This lemma can be easily deduced from the Myhill-Nerode theorem and the Pigeonhole + This lemma can be easily deduced from the Myhill-Nerode Theorem and the Pigeonhole Principle: Since @{text A} is regular, there can be only finitely many equivalence classes. Hence an infinite set must contain at least two strings that are in the same equivalence class, that is - they need to be related by the Myhill-Nerode relation. + they need to be related by the Myhill-Nerode Relation. Using this lemma, it is straightforward to establish that the language \mbox{@{text "A \ \\<^isub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands @@ -2305,8 +2305,10 @@ \end{proof} \noindent - To conclude, this lemma and the Continuation Lemma leads to a contradiction assuming @{text A} - is regular. Therefore the language @{text A} is not regular, as we wanted to show. + To conclude the proof on non-regularity of language @{text A}, the + Continuation Lemma and the lemma above lead to a contradiction assuming + @{text A} is regular. Therefore the language @{text A} is not regular, as we + wanted to show. *} @@ -2320,7 +2322,7 @@ expressions can conveniently be defined as a datatype in HOL-based theorem provers. For us it was therefore interesting to find out how far we can push this point of view. We have established in Isabelle/HOL both directions - of the Myhill-Nerode theorem. + of the Myhill-Nerode Theorem. % \begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\ A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}. @@ -2330,16 +2332,16 @@ Having formalised this theorem means we pushed our point of view quite far. Using this theorem we can obviously prove when a language is \emph{not} regular---by establishing that it has infinitely many equivalence classes - generated by the Myhill-Nerode relation (this is usually the purpose of the + generated by the Myhill-Nerode Relation (this is usually the purpose of the Pumping Lemma \cite{Kozen97}). We can also use it to establish the standard textbook results about closure properties of regular languages. Interesting is the case of closure under complement, because it seems difficult to construct a regular expression for the complement language by direct means. However the existence of such a regular expression can be easily - proved using the Myhill-Nerode theorem. + proved using the Myhill-Nerode Theorem. - Our insistence on regular expressions for proving the Myhill-Nerode theorem - arose from the limitations of HOL, used in the popular theorem provers HOL4, + Our insistence on regular expressions for proving the Myhill-Nerode Theorem + arose from the limitations of HOL, which is the logic underlying the popular theorem provers HOL4, HOLlight and Isabelle/HOL. In order to guarantee consistency, formalisations in HOL can only extend the logic with definitions that introduce a new concept in terms of already existing notions. A convenient definition for automata @@ -2347,7 +2349,7 @@ us to use the standard operation for disjoint union whenever we need to compose two automata. Unfortunately, we cannot use such a polymorphic definition in HOL as part of the definition for regularity of a language (a predicate - over set of strings). Consider for example the following attempt: + over sets of strings). Consider for example the following attempt: \begin{center} @{text "is_regular A \ \M(\). is_dfa (M) \ \(M) = A"} @@ -2355,8 +2357,8 @@ \noindent In this definifion, the definiens is polymorphic in the type of the automata - @{text "M"} (indicated by dependency on @{text "\"}), but the definiendum - @{text "is_regular"} is not. Such definitions are excluded in HOL, because + @{text "M"} (indicated by dependency on the type-variable @{text "\"}), but the definiendum + @{text "is_regular"} is not. Such definitions are excluded from HOL, because they can lead easily to inconsistencies (see \cite{PittsHOL4} for a simple example). Also HOL does not contain type-quantifiers which would allow us to get rid of the polymorphism by quantifying over the type-variable @{text @@ -2370,7 +2372,7 @@ infrastructure comes for free. The definition of regularity in terms of regular expressions poses no problem at all for HOL. We showed in this paper that they can be used for establishing the central result in regular - language theory---the Myhill-Nerode theorem. + language theory---the Myhill-Nerode Theorem. While regular expressions are convenient, they have some limitations. One is that there seems to be no method of calculating a minimal regular expression @@ -2388,7 +2390,7 @@ \cite{Brzozowski64}. The close connection can be seen by considering the equivalence classes as the states of the minimal automaton for the regular language. However there are some subtle differences. Because our equivalence - classes (or correspondingly states) arise from the Myhil-Nerode Relation, the most natural + classes (or correspondingly states) arise from the Myhill-Nerode Relation, the most natural choice is to characterise each state with the set of strings starting from the initial state leading up to that state. Usually, however, the states are characterised as the strings starting from that state leading to the @@ -2397,16 +2399,16 @@ state', while Brzozowski has it on the terminal states. This means we also need to reverse the direction of Arden's Lemma. We have not found anything in the literature about our way of proving the first direction of the - Myhill-Nerode theorem, but it appears to be folklore. + 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 + 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 \cite{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 + 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 @@ -2429,7 +2431,7 @@ algorithm is still executable. Given the existing infrastructure for executable sets in Isabelle/HOL \cite{Haftmann09}, it should. - Our formalisation of the Myhill-Nerode theorem consists of 780 lines of + Our formalisation of the Myhill-Nerode Theorem consists of 780 lines of Isabelle/Isar code for the first direction and 460 for the second (the one based on tagging-functions), plus around 300 lines of standard material about regular languages. The formalisation of derivatives and partial @@ -2443,14 +2445,15 @@ use of sets over which the algorithm operates means it is not as easy to formalise as one might hope. However, it seems sets cannot be avoided since the `input' of the algorithm consists of equivalence classes and we cannot - see how to reformulate the theory so that we can use lists. Lists would be + see how to reformulate the theory so that we can use lists or matrices. Lists would be much easier to reason about, since we can define functions over them by recursion. For sets we have to use set-comprehensions, which is slightly - unwieldy. + unwieldy. Matrices would allow us to use the slick formalisation by + Nipkow of the Gauss-Jordan algorithm \cite{Nipkow11}. While our formalisation might appear large, it should be seen in the context of the work done by Constable at al \cite{Constable00} who - formalised the Myhill-Nerode theorem in Nuprl using automata. They write + formalised the Myhill-Nerode Theorem in Nuprl using automata. They write that their four-member team needed something on the magnitude of 18 months for their formalisation. It is hard to gauge the size of a formalisation in Nurpl, but from what is shown in the Nuprl Math Library diff -r 087e6c255e33 -r 47446f111550 Journal/document/root.bib --- a/Journal/document/root.bib Wed Sep 07 18:17:56 2011 +0000 +++ b/Journal/document/root.bib Thu Sep 08 15:08:02 2011 +0000 @@ -1,5 +1,15 @@ +@incollection{Nipkow11, + author = {T.~Nipkow}, + title = {{G}auss-{J}ordan {E}limination for {M}atrices {R}epresented as {F}unctions}, + booktitle = {The Archive of Formal Proofs}, + editor = {G.~Klein and T.~Nipkow and L.~Paulson}, + publisher = {\url{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml}}, + year = 2011, + note = {Formal proof development}, + ISSN = {2150-914x} +} @Article{Haines69, author = {L.~H.~Haines}, diff -r 087e6c255e33 -r 47446f111550 Journal/document/root.tex --- a/Journal/document/root.tex Wed Sep 07 18:17:56 2011 +0000 +++ b/Journal/document/root.tex Thu Sep 08 15:08:02 2011 +0000 @@ -57,7 +57,7 @@ graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular expressions can be defined conveniently as a datatype and a corresponding reasoning infrastructure comes for free. We show in this paper that a central -result from formal language theory---the Myhill-Nerode theorem---can be +result from formal language theory---the Myhill-Nerode Theorem---can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow. \end{abstract}