# HG changeset patch # User urbanc # Date 1298153122 0 # Node ID ab6637008963d5cfcd6a5e377df69500b2fc8180 # Parent 1cf12a107b0354832f385cb72b9e9cb8d17eeae7 my latest version (SEQ and STAR still missing) diff -r 1cf12a107b03 -r ab6637008963 Paper/Paper.thy --- a/Paper/Paper.thy Sat Feb 19 21:49:11 2011 +0000 +++ b/Paper/Paper.thy Sat Feb 19 22:05:22 2011 +0000 @@ -1058,28 +1058,28 @@ regular expression. While regular expressions are convenient in formalisations, they have some - limitations. One is that there seems to be no notion of a minimal regular - expression, like there is for automata. For an implementation of a simple - regular expression matcher, whose correctness has been formally - established, we refer the reader to Owens and Slind \cite{OwensSlind08}. + limitations. One is that there seems to be no method of calculating a + minimal regular expression (for example in terms of length), like there is + for automata. For an implementation of a simple regular expression matcher, + whose correctness has been formally established, we refer the reader to + Owens and Slind \cite{OwensSlind08}. Our formalisation consists of 790 lines of Isabelle/Isar code for the first - direction and 475 for the second, plus standard material about regular languages. - While this might be seen as too large to - count as a concise proof pearl, this should be seen 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 magnitute of 18 months for their - formalisation. 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 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 + direction and 475 for the second, plus 300 lines of standard material about + regular languages. While this might be seen as too large to count as a + concise proof pearl, this should be seen 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 magnitute of 18 months for their formalisation. 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 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 \begin{center} \url{http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/regexp/} @@ -1108,7 +1108,7 @@ generated with respect to @{text s}. Using the fact that two strings are Myhill-Nerode related whenever their derivative is the same together with the fact that there are only finitely many derivatives for a regular - expression would give us the same argument as ours. However it seems not so easy to + expression would give us a similar argument as ours. However it seems not so easy to calculate the derivatives and then to count them. Therefore we preferred our direct method of using tagging-functions involving equivalence classes. This is also where our method shines, because we can completely side-step the