# HG changeset patch # User Christian Urban # Date 1379164099 -3600 # Node ID 288637d9dcdee727e8434393ed92bc6010c6a9f5 # Parent 92ca56c1a1992933a2609858d0393eeaa073bb65 more changes for final submission diff -r 92ca56c1a199 -r 288637d9dcde Journal/JAR-review2 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Journal/JAR-review2 Sat Sep 14 14:08:19 2013 +0100 @@ -0,0 +1,156 @@ + +Reviewer #1: This paper demonstrates that a) the Myhill-Nerode theorem can be +proved without relying on the notion of automata and b) argues +shallowly thorough the paper that not having to formalize the notion +of automata is easier. + +While I do agree that point a) is a an interesting theoretical +contribution that deserves publication, I disagree with the second +argument. + +It should be noted that the handling of the notion of automata has +been difficult historically for two reasons. On the one hand, giving +an identifier to every state of an automata indeed yields proofs that +may be characterized as "clunky" (even if the wording is a bit +strong), but is a necessary condition for efficient implementation of +automata algorithms. This yields sizable formalizations as is +demonstrated by the Lammich and Tuerk's work or Braibant and Pous's +work [1]. On the other hand, it seems to be the case that the +"principle of definition" in HOL makes it impossible to use parametric +definitions of automata (but there is no problem with such a +definition in Coq). + +But, the startup cost of a formalization depends on the scope of what +one intends to formalize. Perhaps Braibant concedes that your +development is more concise that his, yet Braibant's work dealt with +the formalization of an _efficient_ decision procedure for Kleene +algebras that required _two_ formalizations of automata (the matrices +are only used in the proof of correctness of this decision procedure, +while the computational part uses efficient representations for DAGs +-- see for instance [1] p. 21 or Braibant's thesis p. 49). I am only +adding emphasis here to demonstrate that this does not compare easily +with the formalization of the proof of Myhill-Nerode by itself. + +(At this point, let me comment on your answer: "As far as we know +Braibant also uses ssreflect". It is not the case. One may wonder to +what extent the use of ssreflect there could have alleviated the +"intrinsic difficulties of working with rectangular matrices".) + +In the same fashion, Lammich and Tuerk's work uses efficient +data-structures (.e.g, for collections, automatas), and some amount of +data-refinement to link various representations together. + +My most stringent remark about the paper is that it should make clear +from the beginning whether or not the algorithms are computational, +and if they are executable, how efficient. Then, comparing with the +two aforementioned work will make sense. + +In fact, I have been made aware of the following work [2] that do +formalize automata and regular language theory without using explicit +identifiers for state numbers in automata. The upside is that it +yields much smoother proofs than previous works in Coq. The downside +is that this formalization strategy does not yield efficient algorithm +for automata constructions. I reckon that this is a technical report +that should be taken with a grain of salt in the context of this +review, but I think that it gives evidence that it is not always the +case that the startup cost is higher with automata rather than with +regular expressions: they formalize the Myhill-Nerode theorem, +Kleene's theorem, the relationships between various representations of +regular languages in around 1500 lines of ssreflect/Coq. (Again, let +me emphasize that this is not a computational representation of +automata, and thus, it does not easily compare in terms of size with +Lammich and Tuerk's work or Braibant and Pous's work.) I think this +work would make for a much more relevant comparison with your work. + +I agree that comparing with related work is hard, and that the authors +have already been careful in their comparison with the formalization +sizes from other works. Yet, I am afraid an uninformed outsider would +miss the distinction between related work that are executable and +efficient and this formalization. + + +Minor comments about the paper +============================== + +- I am still confused about the explanation about the way the +equational system is set up (your comment in the conclusion does not +help me to pinpoint why you have to do that): I understand that +Brzozowski annotates the final states with lambdas, and propagates +them to the unique initial state. On the other hand you start with a +set of equivalence classes, and you want to compute a regular +expression for all classes that are in finals. In other words, I still +fail to see why the following system does not suit your needs + +X1 = a,X2 + b,X4 +X2 = b,X3 + a,X4 + lambda(ONE) +X3 = a,X4 + b,X4 + lambda(ONE) +X4 = a,X4 + b,X4 + +with L(r,X) = L(r) \cdot X + +and then propagate the equation to compute to compute a value for +X1. (And, you could draw the automata underlying the transitions at +the top of p. 7 to help the reader understand what is going on, and +the relationship with the current equational system.) + +Maybe it is simply that you could have done it, but that it would have +been less pleasant to work with in the context of a Myhill-Nerode +relation? + +- I really appreciate the rephrasing of section 4, especially the +final remark. I think it clearly helps the reader to understand the +proof arguments, and the relationship with automata. + +- I concur with the second reviewer to say that the executability of +the first half of the M-N theorem should be discussed in the +conclusion. Moreover, I am puzzled by your comments in the response to +reviewers: to what extent does your formalization need to be +_modified_ to make it executable? Do you need to change the code, or +to add more things? (More precisely, you discuss the executability of +the second half of the M-N theorem -- that constructs a partition of +the set of strings -- in the conclusion, in the context of Haftmann +executable sets; you should do the same for the first-half---that +constructs a regular expression). I am not sure I am happy with the +things you wrote about executable sets, because it is not clear from +my point of view if you need to modify the code, or add things. + +- More generally, it should be made clear that when you say algorithm, +the reader should not understand it as something that is computable as +it is. In particular, I think that the following sentence is +misleading: "our algorithm for solving equational systems actually +calculates a regular expression for the complement language." You +actually define such an expression, but it seems not possible, as it +is, to open the box to see what is inside. + +- You answered: + +> In our opinion, Coquand and Siles' development strongly justifies our +> comment about formalisation of Brzozowski's argument being painful. +> If you like to have this reference added in the paper, we are happy +> to do so. + +I think that it is worth adding a comment like this one either in +section 5 (at the beginning of p. 20) or in the conclusion. + +- There are still some spell-checking mistakes in the paper, e.g., + "refular" p. 26, and + +- The authors provide a detailed figure for the number of line of code + of Almeida et al's implementation of Mirkin construction, but there + is no such figure for some of other works that are cited. Maybe this + number could be dropped, or similar figures could be given for other + works, in order to give a more accurate picture. + +- I wonder if you have direction for future works, that would satisfy + your predicate "results from regular language theory, not results + from automata theory". It would be nice to give a few examples if + you have some in mind. + + + +[1] Deciding Kleene algebras in Coq, Thomas Braibant, Damien Pous +http://dx.doi.org/10.2168/LMCS-8(1:16)2012 + +[2] A Constructive Theory of Regular Languages in Coq, Christian +Doczkal and Jan-Oliver Kaiser and Gert Smolka +http://www.ps.uni-saarland.de/Publications/details/DoczkalEtAl:2013:A-Constructive.html diff -r 92ca56c1a199 -r 288637d9dcde Journal/Paper.thy --- a/Journal/Paper.thy Thu Sep 12 17:20:48 2013 +0100 +++ b/Journal/Paper.thy Sat Sep 14 14:08:19 2013 +0100 @@ -341,10 +341,10 @@ not in the predicate for regularity; and there is no type quantification available in HOL.\footnote{Slind already pointed out this problem in an email to the HOL4 mailing list on 21st April - 2005.} Coq, for example, has quantification over types and thus can - state such a definition. This has been recently exploited in a - slick formalisation of the Myhill-Nerode theorem in Coq by - \citeN{XXX}. + 2005.} Systems such as Coq permit quantification over types and thus can + state such a definition. This has been recently exploited in an + elegant and short formalisation of the Myhill-Nerode theorem in Coq by + \citeN{Smolka13}, but as said this is not avaible to us working in Isabelle/HOL. An alternative, which provides us with a single type for states of automata, is to give every state node an identity, for example a natural number, and @@ -470,6 +470,9 @@ ``{\it \ldots [b]ut is there a rigorous way to even state that?}'' \end{quote} + \noindent + We shall give an answer to these questions with our paper. + %Moreover, no side-conditions will be needed for regular expressions, %like we need for automata. @@ -773,14 +776,7 @@ equivalence classes and only finitely many characters. The term @{text "\(ONE)"} in the first equation acts as a marker for the initial state, that is the equivalence class - containing the empty string @{text "[]"}.\footnote{Note that we mark, roughly speaking, the - single `initial' state in the equational system, which is different from - the method by \citeN{Brzozowski64}, where he marks the - `terminal' states. We are forced to set up the equational system in our - way, because the Myhill-Nerode Relation determines the `direction' of the - transitions---the successor `state' of an equivalence class @{text Y} can - be reached by adding a character to the end of @{text Y}. This is also the - reason why we have to use our reversed version of Arden's Lemma.} + containing the empty string @{text "[]"}. In our running example we have the initial equational system % \begin{equation}\label{exmpcs} @@ -793,7 +789,17 @@ \end{tabular}} \end{equation} - \noindent + Note that we mark, roughly speaking, the + single `initial' state in the equational system, which is different from + the method by \citeN{Brzozowski64}, where he marks the + `terminal' states. We are forced to set up the equational system in our + way, because the Myhill-Nerode Relation determines the `direction' of the + transitions---the successor `state' of an equivalence class @{text Y} can + be reached by adding a character to the end of @{text Y}. If we had defined + our equations the `Brzozowski-way', then our variables do not correspond to + the equivalence classes generated by the Myhill-Nerode relation. This need of reverse marking is also the + reason why we have to use our reversed version of Arden's Lemma. + Overloading the function @{text \} for the two kinds of terms in the equational system, we have @@ -818,10 +824,12 @@ \end{equation} \noindent - holds. The reason for adding the @{text \}-marker to our initial equational system is + holds. Again note that the reason for adding the @{text \}-marker to our initial equational system is to obtain this equation: it only holds with the marker, since none of - the other terms contain the empty string. The point of the initial equational system is - that solving it means we will be able to extract a regular expression for every equivalence class. + the other terms contain the empty string. + The point of the initial equational system is + that solving it means we will be able to extract a regular expression for every equivalence class + generated by the Myhill-Nerode relation. Our representation for the equations in Isabelle/HOL are pairs, where the first component is an equivalence class (a set of strings) @@ -1958,8 +1966,11 @@ \noindent Carrying this idea through, we must not consider the set of all derivatives, but the one modulo @{text "ACI"}. In principle, this can be done formally, - but it is very painful in a theorem prover (since there is no - direct characterisation of the set of dissimilar derivatives). + but it is very painful in a theorem prover---since there is no + direct characterisation of the set of dissimilar derivatives. Therefore + \citeN{CoquandSiles12} who follow through this idea had to `stand on their heads' and + first formalise the quite intricate notion of \emph{inductively finite sets} in + order to formalise this property. Fortunately, there is a much simpler approach using \emph{partial @@ -2668,7 +2679,8 @@ Our future work will focus on formalising the regular expression matchers developed by \citeN{Sulzmann12} which generate variable assignments for - regular expression submatching.\smallskip + regular expression sub-matching. For this they use both, derivatives and + partial derivatives of regular expressions.\smallskip \noindent {\bf Acknowledgements:} diff -r 92ca56c1a199 -r 288637d9dcde Journal/document/root.bib --- a/Journal/document/root.bib Thu Sep 12 17:20:48 2013 +0100 +++ b/Journal/document/root.bib Sat Sep 14 14:08:19 2013 +0100 @@ -426,10 +426,22 @@ year = "2002", } -@InProceedings{Sulzmann12, - title = "M.~Sulzmann and K.~Z.~M.~Lu", - author = "XXX", - booktitle = "Proc. of XXX", - year = "2012", - pages = "XXX" +@inproceedings{Sulzmann12, + author = {M.~Sulzmann and K.~Z.~M.~Lu}, + title = {{R}egular {E}xpression {S}ub-{M}atching using {P}artial {D}erivatives}, + booktitle = {Proc.~of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP)}, + year = {2012}, + pages = {79--90}, + publisher = {ACM} } + + + +@Unpublished{Smolka13, + author = {C.~Doczkal and J.~O.~Kaiser and G.~Smolka}, + title = {{A} {C}onstructive {T}heory of {R}egular {L}anguages in {C}oq}, + note = {Accepted for publication in {\it Proc.~of the 3rd International Conference on + Certified Programs and Proofs}}, + year = {2013} +} + diff -r 92ca56c1a199 -r 288637d9dcde journal.pdf Binary file journal.pdf has changed