--- 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
--- 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}
}