1 

     2 Reviewer #1: This paper demonstrates that a) the Myhill-Nerode theorem can be

     3 proved without relying on the notion of automata and b) argues

     4 shallowly thorough the paper that not having to formalize the notion

     5 of automata is easier.

     6 

     7 While I do agree that point a) is a an interesting theoretical

     8 contribution that deserves publication, I disagree with the second

     9 argument.

    10 

    11 It should be noted that the handling of the notion of automata has

    12 been difficult historically for two reasons. On the one hand, giving

    13 an identifier to every state of an automata indeed yields proofs that

    14 may be characterized as "clunky" (even if the wording is a bit

    15 strong), but is a necessary condition for efficient implementation of

    16 automata algorithms. This yields sizable formalizations as is

    17 demonstrated by the Lammich and Tuerk's work or Braibant and Pous's

    18 work [1]. On the other hand, it seems to be the case that the

    19 "principle of definition" in HOL makes it impossible to use parametric

    20 definitions of automata (but there is no problem with such a

    21 definition in Coq).

    22 

    23 But, the startup cost of a formalization depends on the scope of what

    24 one intends to formalize. Perhaps Braibant concedes that your

    25 development is more concise that his, yet Braibant's work dealt with

    26 the formalization of an _efficient_ decision procedure for Kleene

    27 algebras that required _two_ formalizations of automata (the matrices

    28 are only used in the proof of correctness of this decision procedure,

    29 while the computational part uses efficient representations for DAGs

    30 -- see for instance [1] p. 21 or Braibant's thesis p. 49). I am only

    31 adding emphasis here to demonstrate that this does not compare easily

    32 with the formalization of the proof of Myhill-Nerode by itself.

    33 

    34 (At this point, let me comment on your answer: "As far as we know

    35 Braibant also uses ssreflect".  It is not the case. One may wonder to

    36 what extent the use of ssreflect there could have alleviated the

    37 "intrinsic difficulties of working with rectangular matrices".)

    38 

    39 In the same fashion, Lammich and Tuerk's work uses efficient

    40 data-structures (.e.g, for collections, automatas), and some amount of

    41 data-refinement to link various representations together. 

    42 

    43 My most stringent remark about the paper is that it should make clear

    44 from the beginning whether or not the algorithms are computational,

    45 and if they are executable, how efficient. Then, comparing with the

    46 two aforementioned work will make sense. 

    47 

    48 In fact, I have been made aware of the following work [2] that do

    49 formalize automata and regular language theory without using explicit

    50 identifiers for state numbers in automata. The upside is that it

    51 yields much smoother proofs than previous works in Coq. The downside

    52 is that this formalization strategy does not yield efficient algorithm

    53 for automata constructions. I reckon that this is a technical report

    54 that should be taken with a grain of salt in the context of this

    55 review, but I think that it gives evidence that it is not always the

    56 case that the startup cost is higher with automata rather than with

    57 regular expressions: they formalize the Myhill-Nerode theorem,

    58 Kleene's theorem, the relationships between various representations of

    59 regular languages in around 1500 lines of ssreflect/Coq. (Again, let

    60 me emphasize that this is not a computational representation of

    61 automata, and thus, it does not easily compare in terms of size with

    62 Lammich and Tuerk's work or Braibant and Pous's work.) I think this

    63 work would make for a much more relevant comparison with your work. 

    64 

    65 I agree that comparing with related work is hard, and that the authors

    66 have already been careful in their comparison with the formalization

    67 sizes from other works. Yet, I am afraid an uninformed outsider would

    68 miss the distinction between related work that are executable and

    69 efficient and this formalization. 

    70 

    71 

    72 Minor comments about the paper

    73 ==============================

    74 

    75 - I am still confused about the explanation about the way the

    76 equational system is set up (your comment in the conclusion does not

    77 help me to pinpoint why you have to do that): I understand that

    78 Brzozowski annotates the final states with lambdas, and propagates

    79 them to the unique initial state. On the other hand you start with a

    80 set of equivalence classes, and you want to compute a regular

    81 expression for all classes that are in finals. In other words, I still

    82 fail to see why the following system does not suit your needs

    83 

    84 X1 = a,X2 + b,X4 

    85 X2 = b,X3 + a,X4 + lambda(ONE)

    86 X3 = a,X4 + b,X4 + lambda(ONE)

    87 X4 = a,X4 + b,X4

    88 

    89 with L(r,X) = L(r) \cdot X

    90 

    91 and then propagate the equation to compute to compute a value for

    92 X1. (And, you could draw the automata underlying the transitions at

    93 the top of p. 7 to help the reader understand what is going on, and

    94 the relationship with the current equational system.)

    95 

    96 Maybe it is simply that you could have done it, but that it would have

    97 been less pleasant to work with in the context of a Myhill-Nerode

    98 relation?

    99 

   100 - I really appreciate the rephrasing of section 4, especially the

   101 final remark. I think it clearly helps the reader to understand the

   102 proof arguments, and the relationship with automata. 

   103 

   104 - I concur with the second reviewer to say that the executability of

   105 the first half of the M-N theorem should be discussed in the

   106 conclusion. Moreover, I am puzzled by your comments in the response to

   107 reviewers: to what extent does your formalization need to be

   108 _modified_ to make it executable? Do you need to change the code, or

   109 to add more things? (More precisely, you discuss the executability of

   110 the second half of the M-N theorem -- that constructs a partition of

   111 the set of strings -- in the conclusion, in the context of Haftmann

   112 executable sets; you should do the same for the first-half---that

   113 constructs a regular expression). I am not sure I am happy with the

   114 things you wrote about executable sets, because it is not clear from

   115 my point of view if you need to modify the code, or add things. 

   116 

   117 - More generally, it should be made clear that when you say algorithm,

   118 the reader should not understand it as something that is computable as

   119 it is. In particular, I think that the following sentence is

   120 misleading: "our algorithm for solving equational systems actually

   121 calculates a regular expression for the complement language." You

   122 actually define such an expression, but it seems not possible, as it

   123 is, to open the box to see what is inside.

   124 

   125 - You answered: 

   126 

   127 > In our opinion, Coquand and Siles' development strongly justifies our

   128 > comment about formalisation of Brzozowski's argument being painful.

   129 > If you like to have this reference added in the paper, we are happy

   130 > to do so.

   131 

   132 I think that it is worth adding a comment like this one either in

   133 section 5 (at the beginning of p. 20) or in the conclusion.

   134 

   135 - There are still some spell-checking mistakes in the paper, e.g.,

   136   "refular" p. 26, and 

   137 

   138 - The authors provide a detailed figure for the number of line of code

   139   of Almeida et al's implementation of Mirkin construction, but there

   140   is no such figure for some of other works that are cited. Maybe this

   141   number could be dropped, or similar figures could be given for other

   142   works, in order to give a more accurate picture.

   143 

   144 - I wonder if you have direction for future works, that would satisfy

   145   your predicate "results from regular language theory, not results

   146   from automata theory". It would be nice to give a few examples if

   147   you have some in mind. 

   148 

   149 

   150 

   151 [1] Deciding Kleene algebras in Coq, Thomas Braibant, Damien Pous

   152 http://dx.doi.org/10.2168/LMCS-8(1:16)2012

   153 

   154 [2] A Constructive Theory of Regular Languages in Coq, Christian

   155 Doczkal and Jan-Oliver Kaiser and Gert Smolka

   156 http://www.ps.uni-saarland.de/Publications/details/DoczkalEtAl:2013:A-Constructive.html