# HG changeset patch # User urbanc # Date 1297327238 0 # Node ID 2aa3756dcc9f14e86c45319994ded58dd50df6ca # Parent a9ebc410a5c876b5ce0130f9a3efd90b03352c2d more on the paper diff -r a9ebc410a5c8 -r 2aa3756dcc9f Paper/Paper.thy --- a/Paper/Paper.thy Thu Feb 10 05:57:56 2011 +0000 +++ b/Paper/Paper.thy Thu Feb 10 08:40:38 2011 +0000 @@ -146,13 +146,18 @@ Functions are much better supported in Isabelle/HOL, but they still lead to similar problems as with graphs. Composing, for example, two non-deterministic automata in parallel - poses again the problem of how to implement disjoint unions. Nipkow \cite{Nipkow98} - dismisses the option of using identities, because it leads to ``messy proofs''. He + requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} + dismisses the option of using identities, because it leads according to him to ``messy proofs''. He opts for a variant of \eqref{disjointunion} using bitlists, but writes \begin{quote} - \it ``If the reader finds the above treatment in terms of bit lists revoltingly - concrete, \phantom{``}I cannot disagree.'' + \it% + \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} + `` & If the reader finds the above treatment in terms of bit lists revoltingly + concrete, I cannot disagree.''\\ + `` & All lemmas appear obvious given a picture of the composition of automata\ldots + Yet their proofs require a painful amount of detail.'' + \end{tabular} \end{quote} \noindent @@ -160,11 +165,11 @@ upon functions in order to represent \emph{finite} automata. The best is probably to resort to more advanced reasoning frameworks, such as \emph{locales} or \emph{type classes}, - which are not avaiable in all HOL-based theorem provers. + which are not avaiable in \emph{all} HOL-based theorem provers. Because of these problems to do with representing automata, there seems to be no substantial formalisation of automata theory and regular languages - carried out in a HOL-based theorem prover. Nipkow establishes in + carried out in HOL-based theorem provers. Nipkow establishes in \cite{Nipkow98} the link between regular expressions and automata in the restricted context of lexing. The only larger formalisations of automata theory are carried out in Nuprl \cite{Constable00} and in Coq (for example @@ -210,7 +215,7 @@ are sets of strings. The language containing all strings is written in Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages is written @{term "A ;; B"} and a language raised to the power @{text n} is written - @{term "A \ n"}. Their definitions are + @{term "A \ n"}. They are defined as usual \begin{center} @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]} @@ -247,7 +252,7 @@ Central to our proof will be the solution of equational systems involving sets of languages. For this we will use Arden's lemma \cite{Brzozowski64} - which solves equations of the form @{term "X = A ;; X \ B"} in case + which solves equations of the form @{term "X = A ;; X \ B"} provided @{term "[] \ A"}. However we will need the following ``reverse'' version of Arden's lemma. @@ -325,18 +330,16 @@ Given a set of regular expressions @{text rs}, we will make use of the operation of generating a regular expression that matches all languages of @{text rs}. We only need to know the existence of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's - @{text "\"} to define @{term "\rs"}. This function, roughly speaking, folds @{const ALT} over the + @{text "\"} to define @{term "\rs"}. This operation, roughly speaking, folds @{const ALT} over the set @{text rs} with @{const NULL} for the empty set. We can prove that for finite sets @{text rs} \begin{center} - @{thm (lhs) folds_alt_simp}@{text "= \ (\ ` rs)"} + @{thm (lhs) folds_alt_simp} @{text "= \ (\ ` rs)"} \end{center} \noindent holds, whereby @{text "\ ` rs"} stands for the image of the set @{text rs} under function @{text "\"}. - - *} section {* Finite Partitions Imply Regularity of a Language *} @@ -354,7 +357,7 @@ \noindent It is easy to see that @{term "\A"} is an equivalence relation, which partitions the set of all strings, @{text "UNIV"}, into a set of disjoint - equivalence classes. An example is the regular language containing just + equivalence classes. Let us give an example: consider the regular language containing just the string @{text "[c]"}. The relation @{term "\({[c]})"} partitions @{text UNIV} into the three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"} as follows @@ -366,8 +369,8 @@ \end{center} One direction of the Myhill-Nerode theorem establishes - that if there are finitely many equivalence classes, then the language is - regular. In our setting we therefore have to show: + that if there are finitely many equivalence classes, like in the example above, then + the language is regular. In our setting we therefore have to show: \begin{theorem}\label{myhillnerodeone} @{thm[mode=IfThen] hard_direction} @@ -387,14 +390,15 @@ @{thm finals_in_partitions} hold. Therefore if we know that there exists a regular expression for every equivalence class in @{term "finals A"} (which by assumption must be - a finite set), then we can using @{text "\"} obtain a regular expression + a finite set), then we can use @{text "\"} to obtain a regular expression using that matches every string in @{text A}. Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a regular expression for \emph{every} equivalence class, not just the ones in @{term "finals A"}. We - first define the notion of \emph{one-character-transition} between equivalence classes + first define the notion of \emph{one-character-transition} between + two equivalence classes % \begin{equation} @{thm transition_def} @@ -406,7 +410,7 @@ @{text X}. Note that we do not define an automaton here, we merely relate two sets (with the help of a regular expression). In our concrete example we have @{term "X\<^isub>1 \c\ X\<^isub>2"}, @{term "X\<^isub>1 \d\ X\<^isub>3"} with @{text d} being any - other character than @{text c}, and @{term "X\<^isub>3 \d\ X\<^isub>3"} for any @{text c}. + other character than @{text c}, and @{term "X\<^isub>3 \d\ X\<^isub>3"} for any @{text d}. Next we build an equational system that contains an equation for each equivalence class. Suppose we have @@ -425,19 +429,21 @@ \noindent where the pairs @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions - @{term "Y\<^isub>i\<^isub>j \c\<^isub>i\<^isub>j\ X\<^isub>i"}. There can only be finitely many such - transitions since there are only finitely many equivalence classes - and finitely many characters. + @{term "Y\<^isub>i\<^isub>j \c\<^isub>i\<^isub>j\ X\<^isub>i"}. Our internal represeantation for the right-hand + sides are sets of terms. + There can only be finitely many such + terms since there are only finitely many equivalence classes + and only finitely many characters. The term @{text "\(EMPTY)"} in the first equation acts as a marker for the equivalence - class containing @{text "[]"}. (As an aside note that we mark, roughly speaking, the + class containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the single ``initial'' state in the equational system, which is different from - the method by Brzozowski \cite{Brzozowski64}: he marks the ``terminal'' - states. We are forced to set up the equational system in this way, because + the method by Brzozowski \cite{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 characters to the end of @{text Y}. This is also the reason why we have to use - our reverse version of Arden's lemma.) - Overloading the function @{text L} for the two kinds of terms in the + our reverse version of Arden's lemma.} + Overloading the function @{text \} for the two kinds of terms in the equational system, we have \begin{center} @@ -463,17 +469,23 @@ \noindent The reason for adding the @{text \}-marker to our equational system is to obtain this equation: it only holds in this form since none of - the other terms contain the empty string. - + the other terms contain the empty string. Since we use sets for representing + the right-hans side we can write \eqref{inv1} and \eqref{inv2} more + concisely for an equation of the form @{text "X = rhs"} as + % + \begin{equation}\label{inv} + \mbox{@{text "X = \ (\ ` rhs)"}} + \end{equation} + \noindent Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the - equational system into a \emph{solved form} maintaining the invariants - \eqref{inv1} and \eqref{inv2}. From the solved form we will be able to read + equational system into a \emph{solved form} maintaining the invariant + \eqref{inv}. From the solved form we will be able to read off the regular expressions. In order to transform an equational system into solved form, we have two main operations: one that takes an equation of the form @{text "X = rhs"} and removes - the recursive occurences of @{text X} in @{text rhs} using our variant of Arden's + the recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's Lemma. The other operation takes an equation @{text "X = rhs"} and substitutes @{text X} throughout the rest of the equational system adjusting the remaining regular expressions approriately. To define this adjustment @@ -486,12 +498,21 @@ \noindent which we also lift to entire right-hand sides of equations, written as - @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. - + @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define + the \emph{arden-operation}, which takes an equivalence class @{text X} and + a rhs of an equation. \begin{center} @{thm arden_op_def} \end{center} + + \noindent + The term left of $\triangleright$ deletes all terms of the form @{text "(X, r)"}; + the term on the right calculates first the combinded regular expressions for all + @{text r} in the @{text "(X, r)"}, forms the star and appends it to the remaining + terms in the @{text rhs}. It can be easily seen that this operation mimics Arden's + lemma on the level of equations. + *} section {* Regular Expressions Generate Finitely Many Partitions *}