--- a/Journal/JAR-response Thu Jul 11 12:07:11 2013 +0100
+++ b/Journal/JAR-response Thu Jul 11 16:46:05 2013 +0100
@@ -22,7 +22,7 @@
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
@@ -44,14 +44,14 @@
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
-one clearly has to use the usual notion of the automata somewhere, even
-might have to start from it.
+NFA-to-DFA conversion, which are all based on "concrete" notions of
+automata, then yes one clearly has to use the usual notion of the
+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
@@ -137,7 +137,7 @@
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
@@ -150,9 +150,10 @@
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"
-that many structural inductions over regular expressions are good learning
-tools for students in order to come to grips with formal reasoning.
+in regular language theory. We have already found as one successful
+"application" 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
@@ -163,7 +164,7 @@
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
@@ -250,8 +251,8 @@
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
-prover based on classical logic. We, for example, did not make
+extract an algorithm, then no, we cannot do this. We use a theorem
+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
@@ -260,20 +261,10 @@
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.
@@ -344,7 +335,7 @@
> - (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
@@ -360,8 +351,10 @@
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, we think opening
+"explanation" in a constructive proof. We also leave out an explicit
+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.
@@ -387,7 +380,7 @@
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