# HG changeset patch # User urbanc # Date 1313566989 0 # Node ID 11c3c302fa2e8be7fb05727a84fe859be1c87615 # Parent b300f2c5d51d73aeb9b1a69157e47aa09ca769cd a little tuning diff -r b300f2c5d51d -r 11c3c302fa2e Journal/Paper.thy --- a/Journal/Paper.thy Tue Aug 16 10:21:14 2011 +0000 +++ b/Journal/Paper.thy Wed Aug 17 07:43:09 2011 +0000 @@ -1562,7 +1562,7 @@ text {* \noindent As we have seen in the previous section, in order to establish - the second direction of the Myhill-Nerode theorem, we need to find + the second direction of the Myhill-Nerode theorem, it is sufficient to find a more refined relation than @{term "\<approx>(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. @@ -1617,8 +1617,8 @@ \noindent where @{text "\<Delta>"} in the fifth line is a function that tests whether the empty string is in the language and returns @{term "{[]}"} or @{term "{}"}, - accordingly. In the last equation we use the list-cons operator written - \mbox{@{text "_ :: _"}}. The only interesting case is the @{text "A\<star>"}-case + accordingly. Note also that in the last equation we use the list-cons operator written + \mbox{@{text "_ :: _"}}. The only interesting case is the case of @{term "A\<star>"} where we use Property~\ref{langprops}@{text "(i)"} in order to infer that @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can then complete the proof by using the fifth equation and noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der @@ -1694,7 +1694,7 @@ \noindent - which means the right-hand side (seen as relation) refines the Myhill-Nerode + which means the right-hand side (seen as a relation) refines the Myhill-Nerode relation. Consequently, we can use @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a tagging-relation. However, in order to be useful for the second part of the @@ -1708,7 +1708,7 @@ What Brzozowski \cite{Brzozowski64} established is that for every language there - \emph{are} only finitely `dissimilar' derivatives of a regular + \emph{are} only finitely `dissimilar' derivatives for a regular expression. Two regular expressions are said to be \emph{similar} provided they can be identified using the using the @{text "ACI"}-identities: @@ -1723,7 +1723,7 @@ \noindent Carrying this idea through, we must not consider the set of all derivatives, - but the ones modulo @{text "ACI"}. In principle, this can be done formally, + but the one modulo @{text "ACI"}. In principle, this can be done formally, but it is very painful in a theorem prover (since there is no direct characterisation of the set of dissimilar derivatives). @@ -1853,7 +1853,7 @@ \end{thrm} \noindent - Antimirov's argument first shows this theorem for the language @{term UNIV1}, + Antimirov's proof first shows this theorem for the language @{term UNIV1}, which is the set of all non-empty strings. For this he proves: \begin{equation}\label{pdersunivone} @@ -1882,11 +1882,11 @@ \end{center} \noindent - and for all languages @{text "A"}, @{thm pders_lang_subset[where B="UNIV", - simplified]} holds. Since we follow Antimirov's proof quite closely in our - formalisation (only the last two cases of \eqref{pdersunivone} involve some - non-routine induction argument), we omit the details. - + and for all languages @{text "A"}, @{term "pders_lang A r"} is a subset of + @{term "pders_lang UNIV r"}. Since we follow Antimirov's proof quite + closely in our formalisation (only the last two cases of + \eqref{pdersunivone} involve some non-routine induction argument), we omit + the details. Let us now return to our proof about the second direction in the Myhill-Nerode theorem. The point of the above calculations is to use @@ -2053,33 +2053,34 @@ Our insistence on regular expressions for proving the Myhill-Nerode theorem arose from the limitations of HOL, on which the popular theorem provers HOL4, HOLlight and Isabelle/HOL are based. In order to guarantee consistency, - formalisations can only extend HOL by definitions that introduce a new concept in - terms of already existing notions. A convenient definition for automata + formalisations can extend HOL with definitions that introduce a new concept in + only terms of already existing notions. A convenient definition for automata (based on graphs) uses a polymorphic type for the state nodes. This allows - us to use the standard operation of disjoint union in order to compose two + 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 - set of strings). Consider the following attempt + in HOL as part of the definition for regularity of a language (a predicate + over set of strings). Consider the following attempt: \begin{center} @{text "is_regular A \<equiv> \<exists>M(\<alpha>). is_finite_automata (M) \<and> \<calL>(M) = A"} \end{center} \noindent - which means the definiens is polymorphic in the type of the automata @{text - "M"}, but the definiendum @{text "is_regular"} is not. Such definitions are - excluded in 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 "\<alpha>"}. Therefore when defining - regularity in terms of automata, the only natural way out in HOL is to use - state nodes with an identity, for example a natural number. Unfortunatly, - the consequence is that we have to be careful when combining two automata so - that there is no clash between two such states. This makes formalisations - quite fiddly and rather unpleasant. Regular expressions proved much more - convenient for reasoning in HOL and we showed they can be used for - establishing the central result in regular language theory: the Myhill-Nerode - theorem. + In this definifion, the definiens is polymorphic in the type of the automata + @{text "M"} (indicated by the @{text "\<alpha>"}), but the definiendum @{text + "is_regular"} is not. Such definitions are excluded in 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 + "\<alpha>"}. Therefore when defining regularity in terms of automata, the only + natural way out in HOL is to resort to state nodes with an identity, for + example a natural number. Unfortunatly, the consequence is that we have to + be careful when combining two automata so that there is no clash between two + such states. This makes formalisations quite fiddly and rather + unpleasant. Regular expressions proved much more convenient for reasoning in + HOL since they can be defined as inductive datatype and a reasoning + infrastructure comes for free. We showed they can be used for establishing + the central result in regular 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 @@ -2124,24 +2125,27 @@ in \cite{Harper99} and \cite{Yi06}. While Brzozowski's derivatives lead to a simple regular expression matcher and he established that there are only finitely many dissimilar derivatives for every regular expression, this - result is not as straightforward to formalise in a theorem prover. The - reason is that the set of dissimilar derivatives is not defined inductively, - but in terms of an ACI-equivalence relation. This difficulty prevented for - example Krauss and Nipkow to prove termination of their equivalence checker - for regular expressions \cite{KraussNipkow11}. Their checker is based on - derivatives and for their argument the lack of a formal proof of termination - is not crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}). - We expect that their development simplifies by using partial derivatives, + result is not as straightforward to formalise in a theorem prover as one + might wish. The reason is that the set of dissimilar derivatives is not + defined inductively, but in terms of an ACI-equivalence relation. This + difficulty prevented for example Krauss and Nipkow to prove termination of + their equivalence checker for regular expressions + \cite{KraussNipkow11}. Their checker is based on Brzozowski's derivatives + and for their argument the lack of a formal proof of termination is not + crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}). We + expect that their development simplifies by using partial derivatives, instead of derivatives, and that termination of the algorithm can be - formally established. However, since partial derivatives use sets of regular - expressions, one needs to carefully analyse whether the resulting algorithm - is still executable. Given the existing infrastructure for executable sets - in Isabelle/HOL, it should. + formally established (the main incredience is + Theorem~\ref{antimirov}). However, since partial derivatives use sets of + regular expressions, one needs to carefully analyse whether the resulting + algorithm is still executable. Given the existing infrastructure for + executable sets in Isabelle/HOL, it should. + 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 about derivatives and partial + about regular languages. The formalisation of derivatives and partial derivatives shown in Section~\ref{derivatives} consists of 390 lines of code. The algorithm for solving equational systems, which we used in the first direction, is conceptually relatively simple. Still the use of sets @@ -2149,10 +2153,10 @@ 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 much easier - to reason about, since we can define function over them by recursion. For - sets we have to use set-comprehensions. + to reason about, since we can define functions over them by recursion. For + sets we have to use set-comprehensions, which is slightly unwieldy. - While our formalisation might be seen large, it should be seen + 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 that their four-member team needed something on the magnitude of 18 months diff -r b300f2c5d51d -r 11c3c302fa2e Journal/document/root.bib --- a/Journal/document/root.bib Tue Aug 16 10:21:14 2011 +0000 +++ b/Journal/document/root.bib Wed Aug 17 07:43:09 2011 +0000 @@ -1,6 +1,6 @@ @article{Harper99, author = {R.~Harper}, - title = {Proof-Directed Debugging}, + title = {{P}roof-{D}irected {D}ebugging}, journal = {Journal of Functional Programming}, volume = {9}, number = {4}, @@ -10,8 +10,8 @@ @article{Yi06, author = {K.~Yi}, - title = {Educational Pearl: 'Proof-directed debugging' revisited - for a first-order version}, + title = {{E}ducational {P}earl: `{P}roof-{D}irected {D}ebugging' {R}evisited + for a {F}irst-{O}rder {V}ersion}, journal = {Journal of Functional Programming}, volume = {16}, number = {6}, @@ -177,12 +177,13 @@ @inproceedings{WuZhangUrban11, author = {C.~Wu and X.~Zhang and C.~Urban}, - title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, + title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions + ({P}roof {P}earl)}, booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving}, year = {2011}, - pages = {???}, + pages = {341--356}, series = {LNCS}, - volume = {???} + volume = {6898} }