# HG changeset patch # User urbanc # Date 1298039183 0 # Node ID c5eb5f3065ae435ca72122871ae7f488d9b41b5f # Parent ec774952190cc0c9ee7a38367c5f9e77aca96b56 updated bib diff -r ec774952190c -r c5eb5f3065ae Paper/Paper.thy --- a/Paper/Paper.thy Fri Feb 18 12:14:07 2011 +0000 +++ b/Paper/Paper.thy Fri Feb 18 14:26:23 2011 +0000 @@ -183,7 +183,9 @@ to be no substantial formalisation of automata theory and regular languages carried out in HOL-based theorem provers. Nipkow establishes in \cite{Nipkow98} the link between regular expressions and automata in - the context of lexing. The only larger formalisations of automata theory + the context of lexing. Berghofer and Reiter formalise automata working over + bit strings in the context of Presburger arithmetic \cite{BerghoferReiter09}. + The only larger formalisations of automata theory are carried out in Nuprl \cite{Constable00} and in Coq (for example \cite{Filliatre97}). @@ -846,33 +848,31 @@ section {* Myhill-Nerode, Second Part *} text {* - TO BE DONE - \begin{theorem} Given @{text "r"} is a regular expressions, then @{thm Myhill_Nerode2}. \end{theorem} -% \begin{proof} -% By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} -% and @{const CHAR} are straightforward, because we can easily establish + \begin{proof} + By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} + and @{const CHAR} are straightforward, because we can easily establish -% \begin{center} -% \begin{tabular}{l} -% @{thm quot_null_eq}\\ -% @{thm quot_empty_subset}\\ -% @{thm quot_char_subset} -% \end{tabular} -% \end{center} -% -% \end{proof} + \begin{center} + \begin{tabular}{l} + @{thm quot_null_eq}\\ + @{thm quot_empty_subset}\\ + @{thm quot_char_subset} + \end{tabular} + \end{center} + + \end{proof} -% @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} + @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} -% @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} + @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} -% @{thm tag_str_STAR_def[where ?L1.0="A"]} + @{thm tag_str_STAR_def[where ?L1.0="A"]} *} @@ -902,9 +902,9 @@ \noindent holds for any strings @{text "s\<^isub>1"} and @{text - "s\<^isub>2"}. Therefore @{text A} and @{term "-A"} give rise to the same - partitions. - Proving the same result via automata would be quite involved. It includes the + "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same + partitions. Proving the existence of such a regular expression via automata would + be quite involved. It includes the steps: regular expression @{text "\"} non-deterministic automaton @{text "\"} deterministic automaton @{text "\"} complement automaton @{text "\"} regular expression. @@ -913,13 +913,13 @@ direction and ??? for the second. 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. This is the most + Myhill-Nerode theorem in Nuprl using automata. They write that their - four-member team needed something on the magnitute of 18 months to formalise - the Myhill-Nerode theorem. The estimate for our formalisation is that we + 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{???}, we had to find our own arguments. So for us the formalisation + \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 @@ -934,7 +934,7 @@ algebraic mehod} used to convert a finite automaton to a regular expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence classes as the states of the minimal automaton for the regular language. - However there are some subtle differences. If we identify equivalence + However there are some subtle differences. Since we identify equivalence classes with the states of the automaton, then the most natural choice is to characterise each state with the set of strings starting from the initial state leading up to that state. Usually, however, the states are characterised as the @@ -948,7 +948,7 @@ of~\cite{Brzozowski64} in order to prove the second direction of the Myhill-Nerode theorem. There he calculates the derivatives for regular expressions and shows that there can be only finitely many of them. We could - use as the tag of a string @{text s} the derivative of a regular expression + have used as the tag of a string @{text s} the derivative of a regular expression 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 diff -r ec774952190c -r c5eb5f3065ae Paper/document/root.bib --- a/Paper/document/root.bib Fri Feb 18 12:14:07 2011 +0000 +++ b/Paper/document/root.bib Fri Feb 18 14:26:23 2011 +0000 @@ -60,8 +60,8 @@ @inproceedings{Nipkow98, author={T.~Nipkow}, title={{V}erified {L}exical {A}nalysis}, - booktitle={Theorem Proving in Higher Order Logics}, - series=LNCS, + booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics}, + series={LNCS}, volume=1479, pages={1--15}, year=1998 @@ -75,4 +75,25 @@ series=LNCS, volume=2277, pages="24--40" +} + +@book{HopcroftUllman69, + author = {J.~E.~Hopcroft and + J.~D.~Ullman}, + title = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata}, + publisher = {Addison-Wesley}, + year = {1969} +} + + +@inproceedings{BerghoferReiter09, + author = {S.~Berghofer and + M.~Reiter}, + title = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection}, + booktitle = {Proc.~of the 22nd International + Conference on Theorem Proving in Higher Order Logics}, + year = {2009}, + pages = {147-163}, + series = LNCS, + volume = {5674} } \ No newline at end of file