diff -r 92ca56c1a199 -r 288637d9dcde Journal/JAR-review2
--- /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