regexp: comparison Journal/JAR-response

equal deleted inserted replaced

-:c8cb6914f4c8
+:60bcf13adb77
 unusual in that we do not need to provide a version of Kleene's theorem.
 All results are obtained without formally needing a definition for automata.
 If we would need Kleene's theorem as part of our arguments, then we would
 need such a definition.
-To make our intention with the paper more clear, we moved the quote
+To make our intention with the paper clearer, we moved the quote
 by Gasarch from the Conclusion to the Introduction. In this quote he asks
 whether the complementation of regular-expression languages can be proved
 without using automata. In this way we sharpen our motivation by being
 theorem prover related, but also of general interest. See quotations and
 changes right after Definition 2, p. 3.
 > representation of the objects of the formalization (and hence have
 > consequences on its intricacies).
 Yes, we agree with the reviewer that *if* one is in the business of
 proving the correctness of, for example, Hopcroft's algorithm or the
-NFA-to-DFA conversion, which are based on "concrete" automata, then yes
+NFA-to-DFA conversion, which are all based on "concrete" notions of
-one clearly has to use the usual notion of the automata somewhere, even
+automata, then yes one clearly has to use the usual notion of the
-might have to start from it.
+automata somewhere, even might have to start from it.
 However, we disagree with the interpretation that our comparison is
-misleading.  Our claim that usual `paper' definitions do not translate
+misleading.  Our claim that usual 'paper' definitions do not translate
 smoothly into formalised definitions is not a claim just by us and
-independent of any numbers: We referenced in the paper to a concrete
+independent of any numbers: We referenced in the paper a concrete
 problem pointed out already in Slind's email cited on the bottom of
 p. 2. In the context of HOL4, he made the observation
 | A student who is attempting to prove the pumping lemma for regular
 | languages came across the following problem. Suppose a DFA is
 We agree "that underlying our arguments are automata proofs", but
 we argued without constructing automata explicitly. This is the very point
 and contribution of the paper. If we construct automata explicitly, the
 formalised proof of Myhill-Nerode theorem will become much larger as
 can be seen in existing work. By abandoning automata and relying only on
-regular  expressions, we get a much simpler formalised proof of MN theorem.
+regular expressions, we get a much smoother formalised proof of MN theorem.
 > To sum up, I think there is a significant value to come up with fresh
 > arguments that makes it easier to formalize existing pen-and-paper
 > proofs and textbooks. Yet, the arguments presented in this paper are
 > not really new (they look like inlinings, even if the authors chose
 > 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 as one "application"
+in regular language theory. We have already found as one successful
-that many structural inductions over regular expressions are good learning
+"application" that many structural inductions over regular expressions
-tools for students in order to come to grips with formal reasoning.
+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
 >  versions of Arden's lemma, since their proofs and statement are parallel.
 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.
+explicitly a proof and his book is fairly recent.
 > - 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
 We are not 100% sure whether we are correctly interpreting your
 question: If you are after an informal "black board" calculation method
 of this regular expression in front of students, then you can use our
 algorithm. We have done this already. If you are asking whether
 our formalisation is "constructive" enough in order to directly
-extract an algorithm, then no we cannot do this. We use a theorem
+extract an algorithm, then no, we cannot do this. We use a theorem
-prover based on classical logic. We, for example, did not make
+prover based on classical logic. We did not make, for example,
 explicit how a single regular expression can be constructed from
 a set of regular expressions, still recognising the same language.
 However, we do not like to open the "can-of-worms" about constructive
 and unconstructive arguments and how to extract explicit algorithms.
 In theory we can, in practice we cannot. Unfortunately, we do not have
 a better answer for this at the moment and think this is besides
 the main point of the paper.
-> - It seems that the purpose of the tagging functions here is to build
->  right invariant equivalence relations that refines the Myhill-Nerode
->  relation (Lemma 43). Maybe you should start by that. Also, any such
->  right invariant relation naturally gives rise to an automaton, and
->  you build such later on. Maybe you could phrase it out at the very
->  beginning of this section.
-We added a long remark at the end of the section that spells
-out the automata inspiration behind the tagging functions (see p. 17).
 > - p. 13 In the definition of the tagging function for the plus case,
 >  isn't there a typo (replacing the \cdot by a comma) ?
-No. Our formalisation uses this definition.
+No. Our formalisation uses this definition generating a pair.
 > - p. 14 There is an "x" missing on the left-hand side of the definition of
 >   x tag A B.
 Yes. Corrected.
 derivatives is unfortunately not widely known, which we hope
 we can help to change with this paper.
 > - (27) are properties, not definitions, isn't it?
-Corrected.
+Yes, corrected.
 > - A question. On the one hand, Isabelle/HOL features a classical
 >   logic, with the law of the excluded middle and the Hilbert's epsilon
 >   operator. On the other hand, in Coq, it is often involved to prove
 >   decidability results, which may make it more difficult to formalize
 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
 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
+"explanation" in a constructive proof. We also leave out an explicit
-classical shortcuts in the proof. But as said before, we think opening
+choice for selecting an equation in the euqational system. But that
+can be easily patched if wanted. To sum up, there are no inherent
+classical shortcuts in the proof. But as said before, we think opening
 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?
 >   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 point is to draw
-attention to the somewhat surprising fact, namely that formalisation
+attention to the somewhat surprising fact 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

changeset 384	60bcf13adb77
parent 382	29915abff9c2