# HG changeset patch # User Christian Urban # Date 1384103239 0 # Node ID 87d3306acca80aae7c59836d23310b79f38cfd9a # Parent 5c283ecefda6899ef41a79df0163325ec363329f added small comments diff -r 5c283ecefda6 -r 87d3306acca8 Journal/Paper.thy --- a/Journal/Paper.thy Thu Oct 03 15:29:03 2013 +0100 +++ b/Journal/Paper.thy Sun Nov 10 17:07:19 2013 +0000 @@ -496,8 +496,8 @@ 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 - folklore. For the other part, we give two proofs: one direct proof using + an argument about solving equational systems. This argument requires a + `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 @@ -2502,7 +2502,7 @@ 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. @@ -2551,8 +2551,9 @@ 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}. + 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 @@ -2566,8 +2567,8 @@ 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 - first direction of the Myhill-Nerode Theorem, but it appears to be folklore. + in the literature about our way of proving the + 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 @@ -2677,6 +2678,16 @@ 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 diff -r 5c283ecefda6 -r 87d3306acca8 journal.pdf Binary file journal.pdf has changed