\documentclass[12pt]{article}+
−
\usepackage{times}+
−
\usepackage{a4}+
−
\usepackage{hyperref}+
−
\usepackage[comma,square]{natbib}+
−
\usepackage{tikz}+
−
\usetikzlibrary{automata}+
−
+
−
\begin{document}+
−
+
−
\noindent+
−
{\bf Dear Dale, dear Reviewers,}\bigskip+
−
+
−
\noindent+
−
Thank you very much for your time and effort in reviewing this paper. We really appreciate+
−
this. However we passionately believe that the most important aspect of the paper has \underline{\bf no}t been taken into account +
−
when reaching your decision, and that Referee No 3, who we assume has extensive expertise in +
−
regular languages, has proved our point in his review. He brilliantly writes:+
−
+
−
\begin{quote}\it+
−
``the Myhill-Nerode theorem admits a 15-20 lines fairly detailed proof+
−
  (e.g., see the one given on wikipedia) ; being able to formalise it+
−
  is not a real challenge from my point of view.''+
−
\end{quote}+
−
+
−
\noindent+
−
The problem is it \underline{\bf is} a challenge in theorem provers!  And the +
−
real value of the paper and its novelty is that this is a surprising fact, even for experts+
−
in regular languages, as the report of Referee No 3 shows. Because it is +
−
surprising, we really think the paper should appear in a more general journal than one+
−
specialised on theorem provers (after all, many theorem prover people already +
−
appreciate the difficulties; they +
−
just did not know of a way how to overcome them elegantly).+
−
We hope you share with us the belief that theorem prover proofs might not actually +
−
be used in all subjects, but they are +
−
the gold standard of proofs and all researchers should be aware of them.\medskip+
−
+
−
We therefore kindly ask you to reconsider the decision from this+
−
point of view and also ask you to consider the supporting +
−
numbers, which we provided in the paper in order to prove that formalising automata theory \underline{\bf is} a challenge.  +
−
We list them below again for quick reference.+
−
We are also happy to implement every improvement you suggest that make our general point+
−
and proofs clearer.\medskip+
−
+
−
We can also give one \underline{\bf new} datapoint: \citet{LammichTuerk12} took up the challenge and have formalised a library for NFAs and DFAs+
−
in approximately 7000 of lines of Isabelle code---this just sets up the framework. For proving the correctness of +
−
Hopcroft's algorithm they need an additional 7000 lines of Isabelle code. In contrast, our+
−
paper describes a formalised proof of the most central property in regular language+
−
theory taking only 1500(!) lines in Isabelle including all definitions and supporting+
−
lemmas. However, the difficulties with formalising automata theory are \underline{\bf not} restricted +
−
to Isabelle, as the Reviewers assert, and that you do not have to take+
−
our word for it, we list below numbers and comments +
−
made by researchers from \underline{\bf Coq}, \underline{\bf Isabelle} and \underline{\bf Nuprl}. We think similar comments would apply to +
−
\underline{\bf Matita}, for example,  and therefore our paper is written to be as much as possible +
−
agnostic with respect to a single theorem prover. \medskip+
−
+
−
We answer below the specific points the Reviewers raised. We also hope to surprise again+
−
 Referee No 3+
−
in that automata complementation is more tricky than it first might appear and +
−
most textbooks would suggest.\bigskip+
−
+
−
+
−
\newpage+
−
\noindent+
−
\underline{\bf Reviewer 1}\medskip+
−
+
−
\begin{itemize}+
−
\item additions with respect to ITP: section 4 gives now a more detailed proof; section 5 and 6 are+
−
new; the introduction and conclusion are extended with more numbers and comments, which should prove+
−
beyond doubt our general point that automata are difficult to reason about and regular expressions are+
−
a better substitute+
−
\item we did {\bf not} cite \citet{OwensReppyTuron09} for the comment that derivatives ``went lost in the sands of time''+
−
but that they proved with numbers and an actual implementation that in the context of lexing, derivatives are+
−
good enough in practice; we believe that this statement is still accurate and it is the only paper that we could+
−
cite for this+
−
\item we would be grateful to receive a concrete pointer to the literature: ``{\it The technique is folklore, and can be found in traditional textbooks (possibly passing through left linear +
−
grammars)}''+
−
\end{itemize}\bigskip+
−
+
−
\noindent+
−
\underline{\bf Reviewer 2}\medskip+
−
+
−
\begin{itemize}+
−
\item we hope the Reviewer agrees with us that an actual deep analysis of the technical+
−
details and a comparison with Coq/Sreflect would be a major distraction from the main+
−
point that the paper wants to convey;+
−
such an analysis would also be in violation with the editor's guidelines for ToCL+
−
\end{itemize}\bigskip+
−
+
−
\noindent+
−
\underline{\bf Reviewer 3}\medskip+
−
+
−
\noindent+
−
We honestly enjoyed the comments by Reviewer 3 very much, since they pretty much +
−
agreed with our view we helt before we started this work---automata theory is+
−
more than 50 years old, surely nothing can be challenging there. We hope, however, the+
−
following comments by independent Coq/Nuprl/Isabelle-researchers destroy this view:+
−
+
−
\begin{itemize}+
−
\item[] {\bf Numbers and comments from the literature that reasoning about automata is challenging in theorem provers+
−
(our formalisation is 1500 loc):}\medskip+
−
+
−
\item[{\bf Coq:}] \citet{Braibant12} formalises automata theory including  +
−
   Myhill-Nerode: he writes that our formalisation based on+
−
   regular expressions ``{\it is more concise}'' than his; he also writes+
−
   there are no problems with standard textbook proofs,+
−
   except for the ``{\it {\bf intrinsic} difficulties of working with +
−
   rectangular matrices}'' in Coq ($>$10k loc)+
−
+
−
+
−
\item [{\bf Coq:}] \citet{Filliatre97} formalised automata theory using matrices+
−
   leading only to Kleene's theorem, but not +
−
   Myhill-Nerode nor closure under complementation: he +
−
   writes his formalisation based on matrices is +
−
   ``{\it rather big}'' ($>$4.5k loc)+
−
 +
−
\item[{\bf Coq:}] \citet{Almeidaetal10} verify Mirkin's partial derivatives+
−
   automata ($>$10k lines of code using matrices)+
−
+
−
\item [{\bf Nuprl:}] \citet{Constable00} estimate their 4-member team needs+
−
   11 months with Nuprl for chapters 1 - 11 from Hopcroft +
−
   \& Ullman, which includes Myhill-Nerode ($>$100k lines+
−
   of code)+
−
+
−
\item[{\bf Isabelle:}] \citet{LammichTuerk12} have in Isabelle formalised an automata +
−
   library (7k loc) and verified Hopcroft's algorithm +
−
   (additional 7k loc)+
−
+
−
\item[{\bf Isabelle:}]  +
−
 \citet{Nipkow98} formalises automata with functions but writes+
−
   ``{\it proofs require a painful amount of detail}''+
−
\end{itemize}+
−
+
−
\noindent+
−
These numbers and comments should +
−
convincingly negate the premises of the following comments from the judgement+
−
by Reviewer No 3:+
−
+
−
\begin{itemize}+
−
\item ``{\it all formalised mathematical results are well known and established+
−
  since more than fifty years''} ({\bf we do not contest this nor claim otherwise; we talk about +
−
  theorem prover proofs - there issues are interesting and we have not seen+
−
   any previous work that took our view of starting with a definition for regular expressions only})+
−
\item ``{\it the Myhill-Nerode theorem admits a 15-20 lines fairly detailed proof+
−
  (e.g., see the one given on wikipedia) ; being able to formalise it+
−
  is not a real challenge from my point of view.}'' {(\bf not true)}+
−
\item ``{\it the followed approach is highly specific to Isabelle/HOL: it is+
−
  driven by the postulate that it's hard to manipulate automata or+
−
  matrices.}'' ({\bf not true})+
−
\item ``{\it despite what the authors claim, I'm certain that a mechanised proof+
−
  of this Theorem could be straightforward in other theorem provers, +
−
  using automata for the right-to-left direction and partial+
−
  derivatives for the left-to-right direction''} {\bf (not true)}+
−
\end{itemize}+
−
+
−
\noindent+
−
Reviewer 3 also raised the following criticisms in his judgement:+
−
+
−
\begin{itemize}+
−
\item ``{\it Moreover, the authors insist on the fact that they don't want to use+
−
automata, while they actually just rephrase automata-based proofs,+
−
without using the word `automaton'}''+
−
+
−
We did not deliberately avoid the word ``automaton'', but the {\bf definition} of what an automaton+
−
is. As soon as we start with such a definition, be it in terms of functions, matrices or graphs, we would be in trouble +
−
with formalised proofs as the loc-numbers above show in comparison to ours.+
−
+
−
\item ``{\it All in all, the paper should be presented as `here is a way of doing+
−
automata in HOL'. I'm sure this would make it much clearer and more+
−
interesting, notably since doing automata is supposed to be difficult+
−
in HOL.}''+
−
+
−
The fundamental difference is that it is easier in {\bf every} theorem prover to +
−
reason about inductive datatypes in comparison with non-inductively defined structures+
−
(graphs, functions, matrices). The specific problem the paper addresses is that+
−
all textbook proofs of Myhill-Nerode start with a definition of automata leading +
−
to cumbersome theorem prover proofs in {\bf all} theorem provers we are aware of.+
−
\end{itemize}\bigskip+
−
+
−
\subsection*{Complementation of Automata}+
−
+
−
Finally, we like to comment on the difficulty about complementation of automata, which+
−
on {\bf paper} looks trivial and which highlights the differences between pencil-and-paper textbook +
−
reasoning and formal proofs in a theorem prover:+
−
+
−
\begin{quote}\it +
−
``if we take the definition `a language is regular if recognised by+
−
    a finite deterministic automaton (DFA)' then closure under +
−
    complementation is **trivial** (revert the accepting status of +
−
    states, that's it)''+
−
\end{quote}    +
−
    +
−
\noindent+
−
Given a representation of automata as graphs or+
−
matrices, then the following +
−
+
−
\begin{center}+
−
\begin{tikzpicture}[scale=3, line width=0.7mm]+
−
  \node[state, initial]        (q0) at ( 0,1) {$q_0$};+
−
  \node[state, accepting]  (q1) at ( 1,1) {$q_1$};+
−
  \path[->] (q0) edge node[above] {$a$} (q1)+
−
                   (q1) edge [loop right] node {$b$} ()+
−
                  ;+
−
\end{tikzpicture}+
−
\end{center}+
−
+
−
\noindent+
−
fits the definition as a graph or matrix of nodes. However interchanging the terminal and+
−
non-terminal states gives the {\bf incorrect} result. What is needed is the+
−
notion of a {\bf completed} automaton, such as+
−
 +
−
\begin{center}+
−
\begin{tikzpicture}[scale=3, line width=0.7mm]+
−
  \node[state, initial]        (q0) at ( 0,1) {$q_0$};+
−
  \node[state, accepting]  (q1) at ( 1,1) {$q_1$};+
−
  \node[state]        (q3) at (0.5, 1.5) {$q_{sink}$};+
−
+
−
  \path[->] (q0) edge node[above] {$a$} (q1)+
−
                   (q1) edge [loop right] node {$b$} ()+
−
                   (q0) edge node[above] {$b$} (q3) +
−
                   (q1) edge node[above] {$a$} (q3) +
−
                    (q3) edge [loop above] node {$a, b$} ()+
−
                  ;+
−
\end{tikzpicture}+
−
\end{center}+
−
    +
−
\noindent+
−
This additional restriction unfortunately percolates  through formalised proofs.  In the work by+
−
\citet{LammichTuerk12}, for example, this completeness constrain is  mentioned in 160 places+
−
out of almost 600 lemmas. Since, their representation is based on graphs (sets of nodes and edges), the restriction+
−
about finitely many nodes is mentioned in another 108 places. Similarly, badly fare the definitions+
−
based on matrices in Coq: they need to formalise the shape of matrices and carry around+
−
this baggage in their proofs and operations (which {\bf all} authors of formalised automata theory in+
−
Coq point out as clunky).  Also, attempting to imitate the textbook definition of a finite+
−
function of type state $\times$ letter $\rightarrow$ state, which by the way has not been +
−
used by anybody who formalised automata theory in Coq, does not solve the difficulties: since+
−
no theorem prover has a finite-function type built in, the additional constraint about finite+
−
domains need to be carried around, again making proofs clunky.+
−
 +
−
Regular expressions really solve all the problems mentioned above: they are inductive+
−
datatypes in all theorem provers, they come with simple structural induction principles +
−
for free and operations can be easily defined without any restrictions.  The concrete question+
−
the paper answers is whether regular expressions are enough to obtain the central result in+
−
regular language theory side-stepping the definition of automata which, according to+
−
all previous work,  leads to cumbersome reasoning in all theorem provers. The answer we give is yes:+
−
If you are in the business of verifying Hopcroft's algorithm there is no way around automata.+
−
But for Myhill-Nerode there is, and the work involved is reduced by roughly a {\bf factor of 5}.+
−
We have not found this answer in any of the textbooks or papers available to us. We are happy to+
−
be proved otherwise.+
−
+
−
    +
−
\bibliographystyle{apa}+
−
\bibliography{root}+
−
+
−
\end{document}+
−