regexp: comparison Journal/JAR-response

equal deleted inserted replaced

-:99161cd17c0f
+:29915abff9c2
 > formalize. I would rather improve on the underlying tools, or develop
 > new ways to formalize this notion.
 We disagree in that we should not take the opportunity of using
 regular expressions when they lead to simpler formalisations
-in regular language theory. We have already found that many structural
+in regular language theory. We have already found as one "application"
-inductions that only regular expressions afford are good learning
+that many structural inductions over regular expressions are good learning
 tools for students in order to come to grips with formal reasoning.
 > - Lemma 21 already appears in Brzozowski (1964) who attributes it to
 >  Arden. I think there is little value in distinguishing the two
 We agree that Brzozowski (1964) gives the statement of Arden's lemma, but
 no proof, for which he refers to Arden (1960). Unfortunately, we do not have
 access to this book and guess that this applies to many contemporary readers.
 Our reference to Sakarovitch is motivated by the fact that he gives
-explicitly a proof (XXX CHECK).
+explicitly a proof.
 > - I am puzzled by the one-character transition relation between
 >   equivalence classes (p. 6). The $X_i$ correspond to the states of
 >   the minimal automaton that recognizes $L$ (and you even agree with
 >   that in the Related Work section!). Therefore, I disagree with your
 shows (although they left out the details in their paper) that the
 set of derivatives is inductively finite.
 In our opinion, Coquand and Siles' development strongly justifies our
 comment about formalisation of Brzozowski's argument being painful.
-If you like to add this as a reference in the paper, we are happy
+If you like to have this reference added in the paper, we are happy
 to do so.
 > - Section 6, p20, previous to last paragraph: you say that the
 >   construction of the complement regular expression involves several
 >   transformations: you could shave off the construction of the
 >   non-deterministic automaton, since it can be avoided using
 >   Antimirov's construction of a DFA (as you do).
-We feel that our sequence adequately represents procedure
+We feel that our sequence adequately represents the procedure
 that is used by informed outsiders and that is usually
 taught to students. Antimirov's construction using partial
 derivatives is unfortunately not widely known, which we hope
 we can help to change with this paper.
 >   operator. On the other hand, in Coq, it is often involved to prove
 >   decidability results, which may make it more difficult to formalize
 >   some of the arguments you are using. Is it possible in Isabelle/HOL
 >   to track what are the uses of classical logic that you use?
-In theory there is a way to track all classical uses in Isabelle,
+In theory there is a way to track all classical uses in Isabelle/HOL,
 but this can be practically unfeasible, since proof terms can be
 gigantic (therefore the Isabelle/HOL follows the LCF approach
 where only theorems need to be recorded for correctness). Having
-said that there is one obvious place in our proof where we used
+said that, there is one obvious place in our proof where we used
 a "classical" shortcut by using + for generating a single regular
 expression from a finite set of expressions. This would need better
 "explanation" in a constructive proof. There are no other inherent
-classical shortcuts in the proof. But as said before opening we
+classical shortcuts in the proof. But as said before, we think opening
-think opening this can-of-worms is beside the focus of the paper.
+this can-of-worms is beside the focus of the paper.
 >  In particular, I am worried about the last sentence on page 24: how do
 >  you make these sets computational?
 >   Myhill-Nerode theorem is an algorithm that minimize automata: could
 >   you provide, for instance, an algorithm that compute the number of
 >   equivalences classes of your Myhill-Nerode relation?
 We have attempted to be very careful with our comments about the
-formalisation sizes from other works. Our intention is only to draw
+formalisation sizes from other works. Our point is to draw
-attention to the somewhat surprising point, namely that formalisation
+attention to the somewhat surprising fact, namely that formalisation
 using automata (either out of choice or being forced) led to
 formalisations where the people in question had to fight their
 theorem prover. On the other hand, our formalisation could rely
 on the fact that regular expressions are inductive datatypes which
 are generally well-supported by theorem prover reasoning. We hope
 >   context of the ssreflect dialect. For instance, you may have a look
 >   at Dénès M, Mörtberg A, Siles V.  2012.  A refinement-based approach
 >   to computational algebra in COQ. ITP 2012. It does not seem that
 >   there is a particular problem with the use of matrices.
-We relied completely on the comment by (expert formaliser in Coq) Braibant
+We relied completely on the comment by (we assume expert formaliser in Coq)
-from his thesis which explicitly states
+Braibant from his thesis which explicitly states:
 | Note that while they [Wu, Zhang, Urban] justify their work by the fact
 | that formalising automata ``can be a real hassle in HOL-based provers'',
 | and that neither Isabelle/HOL nor HOL4 nor HOL-light support matrices and
 | graphs with libraries, we did not encounter such difficulties in Coq
 > sometimes less than perfect; 2. a spell-checker should be used; 3. the
 > typography is occasionally dubious; and that 4. it all needs to be
 > re-read with more care.
 We have improved the paper. Please let us know if we
-overlooked any more errors.
+overlooked any other errors.
 > Finally, the conclusion and related work sections are reasonable.  I
 > think the conclusion could usefully discuss the executability of the
 > algorithm in the first half of the M-N proof.
 Informally, the algorithm is clearly executable. But we have not
-attempted this with our formalisation.
+attempted this with our formalisation or modified the formalisation
+so that it becomes executable by Isabelle/HOL.
 > Also, the conclusion discusses the Brzozowski's algebraic method in
 > this context, and argues that the equational constraints that appear
 > in this paper are not quite the same as a minimal automaton. It's
 > clear that, yes, they are a little different, but it still seems to

changeset 382	29915abff9c2
parent 381	99161cd17c0f
child 384	60bcf13adb77