--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/JAR-review2	Sat Sep 14 14:08:19 2013 +0100
@@ -0,0 +1,156 @@
+
+Reviewer #1: This paper demonstrates that a) the Myhill-Nerode theorem can be
+proved without relying on the notion of automata and b) argues
+shallowly thorough the paper that not having to formalize the notion
+of automata is easier.
+
+While I do agree that point a) is a an interesting theoretical
+contribution that deserves publication, I disagree with the second
+argument.
+
+It should be noted that the handling of the notion of automata has
+been difficult historically for two reasons. On the one hand, giving
+an identifier to every state of an automata indeed yields proofs that
+may be characterized as "clunky" (even if the wording is a bit
+strong), but is a necessary condition for efficient implementation of
+automata algorithms. This yields sizable formalizations as is
+demonstrated by the Lammich and Tuerk's work or Braibant and Pous's
+work [1]. On the other hand, it seems to be the case that the
+"principle of definition" in HOL makes it impossible to use parametric
+definitions of automata (but there is no problem with such a
+definition in Coq).
+
+But, the startup cost of a formalization depends on the scope of what
+one intends to formalize. Perhaps Braibant concedes that your
+development is more concise that his, yet Braibant's work dealt with
+the formalization of an _efficient_ decision procedure for Kleene
+algebras that required _two_ formalizations of automata (the matrices
+are only used in the proof of correctness of this decision procedure,
+while the computational part uses efficient representations for DAGs
+-- see for instance [1] p. 21 or Braibant's thesis p. 49). I am only
+adding emphasis here to demonstrate that this does not compare easily
+with the formalization of the proof of Myhill-Nerode by itself.
+
+(At this point, let me comment on your answer: "As far as we know
+Braibant also uses ssreflect".  It is not the case. One may wonder to
+what extent the use of ssreflect there could have alleviated the
+"intrinsic difficulties of working with rectangular matrices".)
+
+In the same fashion, Lammich and Tuerk's work uses efficient
+data-structures (.e.g, for collections, automatas), and some amount of
+data-refinement to link various representations together. 
+
+My most stringent remark about the paper is that it should make clear
+from the beginning whether or not the algorithms are computational,
+and if they are executable, how efficient. Then, comparing with the
+two aforementioned work will make sense. 
+
+In fact, I have been made aware of the following work [2] that do
+formalize automata and regular language theory without using explicit
+identifiers for state numbers in automata. The upside is that it
+yields much smoother proofs than previous works in Coq. The downside
+is that this formalization strategy does not yield efficient algorithm
+for automata constructions. I reckon that this is a technical report
+that should be taken with a grain of salt in the context of this
+review, but I think that it gives evidence that it is not always the
+case that the startup cost is higher with automata rather than with
+regular expressions: they formalize the Myhill-Nerode theorem,
+Kleene's theorem, the relationships between various representations of
+regular languages in around 1500 lines of ssreflect/Coq. (Again, let
+me emphasize that this is not a computational representation of
+automata, and thus, it does not easily compare in terms of size with
+Lammich and Tuerk's work or Braibant and Pous's work.) I think this
+work would make for a much more relevant comparison with your work. 
+
+I agree that comparing with related work is hard, and that the authors
+have already been careful in their comparison with the formalization
+sizes from other works. Yet, I am afraid an uninformed outsider would
+miss the distinction between related work that are executable and
+efficient and this formalization. 
+
+
+Minor comments about the paper
+==============================
+
+- I am still confused about the explanation about the way the
+equational system is set up (your comment in the conclusion does not
+help me to pinpoint why you have to do that): I understand that
+Brzozowski annotates the final states with lambdas, and propagates
+them to the unique initial state. On the other hand you start with a
+set of equivalence classes, and you want to compute a regular
+expression for all classes that are in finals. In other words, I still
+fail to see why the following system does not suit your needs
+
+X1 = a,X2 + b,X4 
+X2 = b,X3 + a,X4 + lambda(ONE)
+X3 = a,X4 + b,X4 + lambda(ONE)
+X4 = a,X4 + b,X4
+
+with L(r,X) = L(r) \cdot X
+
+and then propagate the equation to compute to compute a value for
+X1. (And, you could draw the automata underlying the transitions at
+the top of p. 7 to help the reader understand what is going on, and
+the relationship with the current equational system.)
+
+Maybe it is simply that you could have done it, but that it would have
+been less pleasant to work with in the context of a Myhill-Nerode
+relation?
+
+- I really appreciate the rephrasing of section 4, especially the
+final remark. I think it clearly helps the reader to understand the
+proof arguments, and the relationship with automata. 
+
+- I concur with the second reviewer to say that the executability of
+the first half of the M-N theorem should be discussed in the
+conclusion. Moreover, I am puzzled by your comments in the response to
+reviewers: to what extent does your formalization need to be
+_modified_ to make it executable? Do you need to change the code, or
+to add more things? (More precisely, you discuss the executability of
+the second half of the M-N theorem -- that constructs a partition of
+the set of strings -- in the conclusion, in the context of Haftmann
+executable sets; you should do the same for the first-half---that
+constructs a regular expression). I am not sure I am happy with the
+things you wrote about executable sets, because it is not clear from
+my point of view if you need to modify the code, or add things. 
+
+- More generally, it should be made clear that when you say algorithm,
+the reader should not understand it as something that is computable as
+it is. In particular, I think that the following sentence is
+misleading: "our algorithm for solving equational systems actually
+calculates a regular expression for the complement language." You
+actually define such an expression, but it seems not possible, as it
+is, to open the box to see what is inside.
+
+- You answered: 
+
+> In our opinion, Coquand and Siles' development strongly justifies our
+> comment about formalisation of Brzozowski's argument being painful.
+> If you like to have this reference added in the paper, we are happy
+> to do so.
+
+I think that it is worth adding a comment like this one either in
+section 5 (at the beginning of p. 20) or in the conclusion.
+
+- There are still some spell-checking mistakes in the paper, e.g.,
+  "refular" p. 26, and 
+
+- The authors provide a detailed figure for the number of line of code
+  of Almeida et al's implementation of Mirkin construction, but there
+  is no such figure for some of other works that are cited. Maybe this
+  number could be dropped, or similar figures could be given for other
+  works, in order to give a more accurate picture.
+
+- I wonder if you have direction for future works, that would satisfy
+  your predicate "results from regular language theory, not results
+  from automata theory". It would be nice to give a few examples if
+  you have some in mind. 
+
+
+
+[1] Deciding Kleene algebras in Coq, Thomas Braibant, Damien Pous
+http://dx.doi.org/10.2168/LMCS-8(1:16)2012
+
+[2] A Constructive Theory of Regular Languages in Coq, Christian
+Doczkal and Jan-Oliver Kaiser and Gert Smolka
+http://www.ps.uni-saarland.de/Publications/details/DoczkalEtAl:2013:A-Constructive.html

--- a/Journal/Paper.thy	Thu Sep 12 17:20:48 2013 +0100
+++ b/Journal/Paper.thy	Sat Sep 14 14:08:19 2013 +0100
@@ -341,10 +341,10 @@
   not in the predicate for regularity; and there is no type
   quantification available in HOL.\footnote{Slind already pointed out
   this problem in an email to the HOL4 mailing list on 21st April
-  2005.} Coq, for example, has quantification over types and thus can
-  state such a definition.  This has been recently exploited in a
-  slick formalisation of the Myhill-Nerode theorem in Coq by
-  \citeN{XXX}.
+  2005.} Systems such as Coq permit quantification over types and thus can
+  state such a definition.  This has been recently exploited in an
+  elegant and short formalisation of the Myhill-Nerode theorem in Coq by
+  \citeN{Smolka13}, but as said this is not avaible to us working in Isabelle/HOL.
 
   An alternative, which provides us with a single type for states of automata,
   is to give every state node an identity, for example a natural number, and
@@ -470,6 +470,9 @@
   ``{\it \ldots [b]ut is there a rigorous way to even state that?}'' 
   \end{quote} 
 
+  \noindent
+  We shall give an answer to these questions with our paper.
+
   %Moreover, no side-conditions will be needed for regular expressions,
   %like we need for automata. 
  
@@ -773,14 +776,7 @@
   equivalence classes and only finitely many characters.
   The term @{text "\<lambda>(ONE)"} in the first equation acts as a marker for the initial state, that
   is the equivalence class
-  containing the empty string @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
-  single `initial' state in the equational system, which is different from
-  the method by \citeN{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
-  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.}
+  containing the empty string @{text "[]"}.
   In our running example we have the initial equational system
   %
   \begin{equation}\label{exmpcs}
@@ -793,7 +789,17 @@
   \end{tabular}}
   \end{equation}
 
-  \noindent
+  Note that we mark, roughly speaking, the
+  single `initial' state in the equational system, which is different from
+  the method by \citeN{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
+  transitions---the successor `state' of an equivalence class @{text Y} can
+  be reached by adding a character to the end of @{text Y}. If we had defined
+  our equations the `Brzozowski-way', then our variables do not correspond to 
+  the equivalence classes generated by the Myhill-Nerode relation. This need of reverse marking is also the
+  reason why we have to use our reversed version of Arden's Lemma.
+
   Overloading the function @{text \<calL>} for the two kinds of terms in the
   equational system, we have
   
@@ -818,10 +824,12 @@
   \end{equation}
 
   \noindent
-  holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is 
+  holds. Again note that the reason for adding the @{text \<lambda>}-marker to our initial equational system is 
   to obtain this equation: it only holds with the marker, since none of 
-  the other terms contain the empty string. The point of the initial equational system is
-  that solving it means we will be able to extract a regular expression for every equivalence class. 
+  the other terms contain the empty string. 
+  The point of the initial equational system is
+  that solving it means we will be able to extract a regular expression for every equivalence class
+  generated by the Myhill-Nerode relation. 
 
   Our representation for the equations in Isabelle/HOL are pairs,
   where the first component is an equivalence class (a set of strings)
@@ -1958,8 +1966,11 @@
   \noindent
   Carrying this idea through, we must not consider the set of all derivatives,
   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).
+  but it is very painful in a theorem prover---since there is no
+  direct characterisation of the set of dissimilar derivatives. Therefore
+  \citeN{CoquandSiles12} who follow through this idea had to `stand on their  heads' and
+  first formalise the quite intricate notion of \emph{inductively finite sets} in 
+  order to formalise this property.
 
 
   Fortunately, there is a much simpler approach using \emph{partial
@@ -2668,7 +2679,8 @@
   
   Our future work will focus on formalising the regular expression matchers
   developed by \citeN{Sulzmann12} which generate variable assignments for
-  regular expression submatching.\smallskip
+  regular expression sub-matching. For this they use both, derivatives and
+  partial derivatives of regular expressions.\smallskip
 
   \noindent
   {\bf Acknowledgements:}

--- a/Journal/document/root.bib	Thu Sep 12 17:20:48 2013 +0100
+++ b/Journal/document/root.bib	Sat Sep 14 14:08:19 2013 +0100
@@ -426,10 +426,22 @@
   year = 	"2002",
 }
 
-@InProceedings{Sulzmann12,
-  title =	"M.~Sulzmann and K.~Z.~M.~Lu",
-  author =	"XXX", 
-  booktitle =	"Proc. of XXX",
-  year = 	"2012",
-  pages =	"XXX"
+@inproceedings{Sulzmann12,
+  author    = {M.~Sulzmann and K.~Z.~M.~Lu},
+  title     = {{R}egular {E}xpression {S}ub-{M}atching using {P}artial {D}erivatives},
+  booktitle = {Proc.~of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP)},
+  year      = {2012},
+  pages     = {79--90},
+  publisher = {ACM}
 }
+
+
+
+@Unpublished{Smolka13,
+  author =       {C.~Doczkal and J.~O.~Kaiser and G.~Smolka},
+  title =        {{A} {C}onstructive {T}heory of {R}egular {L}anguages in {C}oq},
+  note =         {Accepted for publication in {\it Proc.~of the 3rd International Conference on 
+                  Certified Programs and Proofs}},
+  year =         {2013}
+}
+

Binary file journal.pdf has changed