regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:5c283ecefda6
+:87d3306acca8
 \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
 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
+an argument about solving equational systems.  This argument requires a
-folklore. For the other part, we give two proofs: one direct proof using
+`reversed' version of Arden's Lemma. For the other part, we give two proofs: one direct proof using
 certain tagging-functions, and another indirect proof using Antimirov's
 partial derivatives (\citeyear{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
 widely in the literature; partial derivatives, in contrast, attract much
 regular---by establishing that it has infinitely many equivalence classes
 generated by the Myhill-Nerode Relation (this is usually the purpose of the
 Pumping Lemma).  We can also use it to establish the standard
 textbook results about closure properties of regular languages. The case of
 closure under complement follows easily from the Myhill-Nerode Theorem.
-So our answer to Gasarch is ``{\it yes we can''}!
+So our answer to Gasarch is `{\it yes we can'}!
 %Our insistence on regular expressions for proving the Myhill-Nerode Theorem
 %arose from the problem of defining formally the regularity of a language.
 %In order to guarantee consistency,
 %formalisations in HOL can only extend the logic with definitions that introduce a new concept in
 using automata, poses no problem as shown by \citeN{OwensReppyTuron09}.  For an
 implementation of a simple regular expression matcher, whose correctness has
 been formally established, we refer the reader to
 \citeN{OwensSlind08}. In our opinion, their formalisation is considerably
 slicker than for example the approach to regular expression matching taken
 by \citeN{Harper99} and by \citeN{Yi06}.
 Our proof of the first direction is very much inspired by \emph{Brzozowski's
 algebraic method} \citeyear{Brzozowski64} used to convert a finite automaton to a regular expression.
 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
 characterised as the strings starting from that state leading to the
 terminal states.  The first choice has consequences about how the initial
 equational system is set up. We have the $\lambda$-term on our `initial
 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 `pencil-and-paper-reasoning' literature about our way of proving the
+in the literature about our way of proving the
-first direction of the Myhill-Nerode Theorem, but it appears to be folklore.
+first direction of the Myhill-Nerode Theorem.
 We presented two proofs for the second direction of the
 Myhill-Nerode 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 perform
 then regular expressions are easier to work with formally.
 The code of
 our formalisation \cite{myhillnerodeafp11} can be found in the Archive of Formal Proofs at
 \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}.
+In this paper we leave out a discussion
+about the computational content of our proofs. While the described algorithms
+(for instance for solving our equational systems) are exectuable as is, we
+have cut some `computational corners' in our formalisation. For example, we did
+not specify which particular equation should be chosen in each step, rather
+proved that any choice will do. Similarly with our $\bigplus$-operation, we
+did not specify the order in which the regular expression should be composed, rather
+proved that any composition with @{term PLUS} will do.
 Our future work will focus on formalising the regular expression matchers
 developed by \citeN{Sulzmann12} which generate variable assignments for
 regular expression sub-matching. For this they use both, derivatives and
 partial derivatives of regular expressions.\smallskip

changeset 392	87d3306acca8
parent 388	0da31edd95b9