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

We are very grateful to the reviewer deciding the paper is a worthy 
contribution. We are especially grateful since this opinion is despite 
disagreement with parts of the paper. Thank you very much!

> 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).

We agree with this summary. We cited the work by Doczal et al and wrote 
that their quantification over types is not available to us. 

   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 Doczkal 
   et al. (2013), but as said this is not available to us working in 
   Isabelle/HOL.

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

We have attempted to not touch upon efficiency and algorithmic issues, since 
they are an distraction for our topic at hand, that is reasoning about inductive
structures, of which regular expressions are one instance. If you use more
efficient datastructures, then it is expected that reasoning will be
more difficult. The point of the paper is to prove the Myhill-Nerode theorem
with only inductive structures, which are well-supported in all interactive 
theorem provers we are aware off. 

> (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".)

Noted. We will not make this claim and have not done so in the paper.

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

Please note that the 14 kloc we cited for the Lammich/Tuerk work is
the automata library, not the formalisation built on top of it.
Also Lammich and Tuerk have told us that reasoning about graphs 
with state names is undesirable. If they had a better representation
available (which they had _not_, since they formalise Hopcroft's
algorithm), they would have used this one and establish that it is 
"equivalent" to the more efficient version with efficient data-
structures. In their case there is no alternative formalising a library
about graphs etc. We have shown that in case of the Myhill-Nerode theorem
there is an alternative. We have been very careful to make claims about
being the first ones who have done so. However, we believe we are,
but certainly our proofs are not present in the literature (this
might have something to do with the fact that the Myhill-Nerode
theorem requires the reversal of Brzozowski and Arden...see
comment further below).
 
> 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. 

As stated earlier, we do not like to make computational issues
explicit as they are a distraction in our opinion. The logic behind 
Isabelle/HOL and all HOL-based theorem provers is not a computational logic, 
in the sense that it is not about computable functions (unlike Coq). There 
are "uncomputable" features in HOL such as the axiom of choice (which we
make use of in our formalisation). We still use the terminology "algorithm"
in the widely-used sense of algorithms that contain "do-not-care"
nondetermism. For example, unification algorithms are usually explained and 
proved correct as transition system over sets of equations. They are not
executable in the Turing-machine sense, since they leave implicit
the order in which the equations should be analysed and which
rules should "fire" if there are more than one applicable. They
are also "imperfect" as the notion of (potentially infinite) sets
cannot be implemented, in general, as a computable function, but 
they can be reasoned about in Isabelle/HOL and other theorem provers.

Still we hope that the reviewer agrees with us and with the many uses 
in the literature (unification is only one example which commits this 
"sin"), it is nevertheless perfectly sensible to call such "things" 
algorithms. Although they cannot be directly implemented, they can be
implemented once choices are made explicit and datastructures 
fixed. Similarly, our formalisation uses a do-not-care approach
for building a regular expression out of a set of regular expressions
(see equation (2)).  It also leaves the order of equations that should be 
analysed under-specified. But if all these choices are made explicit, we
have an algorithm that is implementable in code. But as the explanation
already indicates, it is quite a digression from our main topic of
reasoning about inductive structures.

If we further contemplate the efficiency of the algorithm we 
(under)specified, then our best guess is that it is exponential in the 
worst case, just like the "naive" unification algorithm is exponential 
if sharing is not treated carefully. 

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

We cited this work and commented on it (see above).

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

In order to get meaningful work done, we have to depend on readers 
carefully reading the paper and obtaining required background material.
I am afraid, there is no other way around. 

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

We used in the paper the much stronger formulation of being
_forced_ to set up the equational system in our way. And we even
now have made the earlier comment about this issue, which was 
placed in a footnote, to be part of the main text (see paragraph after 
equation (6)). 

While your equational system and computations generate a regular
expression, it does not take into account the assumption from 
the first direction of the Myhill-Nerode theorem. Recall that the 
assumption is that there are finitely many equivalence classes 
by the Myhill-Nerode relation. Therefore we have to make our equations
to be in agreement with these equivalence classes, which the properties
in equation (7) and (8) make explicit. We further have to maintain
this agreement during the solution of the equational system. 

Your equational system is _not_ in agreement with the equivalence 
classes: consider that 

   X1 = {[]}
   X2 = {[a]}
   X3 = {[a, b]}
   X4 = UNIV − {[], [a], [a, b]} 

hold, which is not true for the equations you have set up (under the
natural interpretation you have given). Another point is that it is always the
case that only one equivalence class in the Myhill-Nerode theorem contains 
the empty string. Therefore it cannot be the case that there are more than 
one (initial) equation containing the marker lambda(ONE), which translates 
into the empty string under the natural interpretation. So we are
of the opinion that for the Myhill-Nerode theorem you are really forced 
to "reverse" the standard approaches. Please let us know, if this 
clarifies this issue for you.

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

Thank you.

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

The first half is about the Myhill-Nerode relation partitioning the sets of 
all strings into equivalence classes. Our remark applies to this "half".

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

See comment above. We really not want to open up this can of worms.

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

It is possible as long as you make the "do-not-care" non-determinism 
explicit and fix appropriate datastructures for computations. 

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

We added to page 20:

  Therefore Coquand and Siles (2011) who follow through this idea 
  had to spend extra effort and first formalise the quite intricate 
  notion of inductively finite sets in order to formalise this property.

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

We are not 100% sure about this comment. We have not selected the
explicit numbers for the Lammich-Tuerk and Almeida et al works because of  
"name-and-shaming" or because of a "beauty contest". Rather to illustrate 
a trend. We asked about the numbers for the Lammich-Tuerk work. They 
also confirmed with us that their automata-with-names approach is painful 
to work with. Unfortunately they have not written this in their paper 
such that we could have cited it. Filliatre makes explicitly such a comment 
in his paper, which we have cited. Braibant equally wrote that he reckons 
that our formalisation is more concise. There is no way we can give a number 
in terms of lines-of-code for the formalisation in Nuprl. We believe 
the number for the Almeida et al work is accurate (and not even the
biggest formalisation from the ones listed, but one which is about
one specific topic).  

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

We added the work by Sulzmann and Lu who work on regular expression
sub-matching using derivatives of regular expressions. We would like
to formalise this work. Thank you very much for suggesting future work.