# HG changeset patch # User urbanc # Date 1314379426 0 # Node ID 28e98ede8599eeff2ae6545815a0b11dbe761981 # Parent 05da74214979340f14b7c43b3b3846ac4e9fa668 added a few points diff -r 05da74214979 -r 28e98ede8599 Journal/Paper.thy --- a/Journal/Paper.thy Thu Aug 25 19:33:41 2011 +0000 +++ b/Journal/Paper.thy Fri Aug 26 17:23:46 2011 +0000 @@ -359,7 +359,7 @@ lexing. Berghofer and Reiter \cite{BerghoferReiter09} formalise automata working over bit strings in the context of Presburger arithmetic. The only larger formalisations of automata theory are carried out in Nuprl - \cite{Constable00} and in Coq \cite{Filliatre97}. + \cite{Constable00} and in Coq, e.g.~\cite{Filliatre97,Almeidaetal10}. Also one might consider automata theory and regular languages as a meticulously researched subject where everything is crystal clear. However, paper proofs about @@ -474,7 +474,9 @@ always be split up into a non-empty prefix belonging to @{text "A"} and the rest being in @{term "A\"}. We omit the proofs for these properties, but invite the reader to consult our - formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}} + formalisation.\footnote{Available in the Archive of Formal Proofs at + \url{http://afp.sf.net/entries/Myhill-Nerode.shtml} + \cite{myhillnerodeafp11}.} The notation in Isabelle/HOL for the quotient of a language @{text A} according to an equivalence relation @{term REL} is @{term "A // REL"}. We @@ -1759,7 +1761,8 @@ ensuring that there are only finitely many equivalence classes. Unfortunately, this is not true in general. Sakarovitch gives an example where a regular expression has infinitely many derivatives - w.r.t.~the language \mbox{@{term "({a} \ {b})\ \ ({a} \ {b})\ \ {a}"}} + w.r.t.~the language @{text "(ab)\<^isup>\ \ (ab)\<^isup>\a"}, which is formally + written in our notation as \mbox{@{text "{[a,b]}\<^isup>\ \ ({[a,b]}\<^isup>\ \ {[a]})"}} (see \cite[Page~141]{Sakarovitch09}). @@ -2116,7 +2119,7 @@ us to use the standard operation for disjoint union whenever we need to compose two automata. Unfortunately, we cannot use such a polymorphic definition in HOL as part of the definition for regularity of a language (a predicate - over set of strings). Consider the following attempt: + over set of strings). Consider for example the following attempt: \begin{center} @{text "is_regular A \ \M(\). is_dfa (M) \ \(M) = A"} @@ -2220,15 +2223,24 @@ in the context of the work done by Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem in Nuprl using automata. They write that their four-member team needed something on the magnitude of 18 months - for their formalisation. The estimate for our formalisation is that we + for their formalisation. Also, Filli\^atre reports that his formalisation in + Coq of automata theory and Kleene's theorem is ``rather big''. + \cite{Filliatre97} More recently, Almeida et al reported about another + formalisation of regular languages in Coq \cite{Almeidaetal10}. Their + main result is the + correctness of Mirkin's construction of an automaton from a regular + expression using partial derivatives. This took approximately 10600 lines + of code. The estimate for our formalisation is that we needed approximately 3 months and this included the time to find our proof - arguments. Unlike Constable et al, who were able to follow the proofs from - \cite{HopcroftUllman69}, we had to find our own arguments. So for us the + arguments. Unlike Constable et al, who were able to follow the Myhill-Nerode + proof from \cite{HopcroftUllman69}, we had to find our own arguments. So for us the formalisation was not the bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but from what is shown in the Nuprl Math Library - about their development it seems substantially larger than ours. The code of - ours can be found in the Mercurial Repository at - \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.\medskip + about their development it seems substantially larger than ours. We attribute + this to our use of regular expressions, which meant we did not need to `fight' + the theorem prover. The code of + our formalisation can be found in the Archive of Formal Proofs at + \mbox{\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip \noindent {\bf Acknowledgements:} diff -r 05da74214979 -r 28e98ede8599 Journal/document/root.bib --- a/Journal/document/root.bib Thu Aug 25 19:33:41 2011 +0000 +++ b/Journal/document/root.bib Fri Aug 26 17:23:46 2011 +0000 @@ -1,5 +1,15 @@ - +@incollection{myhillnerodeafp11, + author = {C.~Wu and X.~Zhang and C.~Urban}, + title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, + booktitle = {The Archive of Formal Proofs}, + editor = {G.~Klein and T.~Nipkow and L.~Paulson}, + publisher = {\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}}, + month = Aug, + year = 2011, + note = {Formal proof development}, + ISSN = {2150-914x} +} @PhdThesis{Haftmann09, author = {F.~Haftmann}, @@ -63,6 +73,18 @@ } + +@InProceedings{Almeidaetal10, + author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, + title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, + booktitle = {Proc.~of the 15th International Conference on Implementation + and Application of Automata}, + pages = {59-68}, + year = {2010}, + volume = {6482}, + series = {LNCS} +} + @incollection{Constable00, author = {R.~L.~Constable and P.~B.~Jackson and diff -r 05da74214979 -r 28e98ede8599 Literature/sakarovitch-regs-chap.pdf Binary file Literature/sakarovitch-regs-chap.pdf has changed