# HG changeset patch # User urbanc # Date 1303387631 0 # Node ID fd39492b187c19b32ccc862f111224514b940b4f # Parent d8d1e1f53d6e4c76ce5565f254dc0aafc40acd74 a few more changes diff -r d8d1e1f53d6e -r fd39492b187c Paper/Paper.thy --- a/Paper/Paper.thy Tue Apr 19 02:25:21 2011 +0000 +++ b/Paper/Paper.thy Thu Apr 21 12:07:11 2011 +0000 @@ -265,7 +265,7 @@ \noindent In @{text "(ii)"} we use the notation @{term "length s"} for the length of a - string; this property states that if @{term "[] \ A"} then the lengths of + string; this property states that if \mbox{@{term "[] \ A"}} then the lengths of the strings in @{term "A \ (Suc n)"} must be longer than @{text n}. 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}} @@ -273,14 +273,14 @@ 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 will write @{text "\x\\<^isub>\"} for the equivalence class defined - as @{text "{y | y \ x}"}. + as \mbox{@{text "{y | y \ x}"}}. Central to our proof will be the solution of equational systems - involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64}, + involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64}, 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 (`reverse' in the sense of changing the order of @{term "A ;; X"} to + version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to \mbox{@{term "X ;; A"}}). \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\ @@ -446,8 +446,9 @@ @{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 d}. - Next we build an \emph{initial equational system} that - contains an equation for each equivalence class. Suppose we have + Next we construct an \emph{initial equational system} that + contains an equation for each equivalence class. We first give + an informal description of this construction. Suppose we have the equivalence classes @{text "X\<^isub>1,\,X\<^isub>n"}, there must be one and only one that contains the empty string @{text "[]"} (since equivalence classes are disjoint). Let us assume @{text "[] \ X\<^isub>1"}. We build the following equational system @@ -464,9 +465,13 @@ \noindent where the terms @{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 terms in a right-hand side since by assumption there are only finitely many - equivalence classes and only finitely many characters. The term @{text + X\<^isub>i"}. In terms of finite automata, every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system + corresponds very roughly to a state whose name is @{text X\<^isub>i} and its predecessor states + are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these + predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be + finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side + since by assumption 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 "[]"}.\footnote{Note that we mark, roughly speaking, the single `initial' state in the equational system, which is different from @@ -475,7 +480,7 @@ 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 reverse version of Arden's lemma.} + reason why we have to use our reverse version of Arden's Lemma.} Overloading the function @{text \} for the two kinds of terms in the equational system, we have @@ -571,8 +576,8 @@ then we calculate the combined regular expressions for all @{text r} coming from the deleted @{text "(X, r)"}, and take the @{const STAR} of it; finally we append this regular expression to @{text rhs'}. It can be easily seen - that this operation mimics Arden's lemma on the level of equations. To ensure - the non-emptiness condition of Arden's lemma we say that a right-hand side is + that this operation mimics Arden's Lemma on the level of equations. To ensure + the non-emptiness condition of Arden's Lemma we say that a right-hand side is @{text ardenable} provided \begin{center} @@ -580,7 +585,7 @@ \end{center} \noindent - This allows us to prove a version of Arden's lemma on the level of equations. + This allows us to prove a version of Arden's Lemma on the level of equations. \begin{lemma}\label{ardenable} Given an equation @{text "X = rhs"}. @@ -591,7 +596,9 @@ \end{lemma} \noindent - The \emph{substitution-operation} takes an equation + Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma, + but we can still ensure that it holds troughout our algorithm of transforming equations + into solved form. The \emph{substitution-operation} takes an equation of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}. \begin{center} @@ -710,7 +717,7 @@ equations is preserved under our transformations. The other properties are a bit more technical, but are needed to get our proof through. Distinctness states that every equation in the system is distinct. @{text Ardenable} ensures that we can always - apply the arden operation. + apply the @{text Arden} operation. The last property states that every @{text rhs} can only contain equivalence classes for which there is an equation. Therefore @{text lhss} is just the set containing the first components of an equational system, @@ -742,7 +749,7 @@ \end{lemma} \begin{proof} - This boils down to choosing an equation @{text "Y = yrhs"} to be eliminated + The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"} preserves the invariant. We prove this as follows: @@ -753,7 +760,7 @@ \end{center} \noindent - Finiteness is straightforward, as @{const Subst} and @{const Arden} operations + Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations keep the equational system finite. These operations also preserve soundness and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}). The property @{text ardenable} is clearly preserved because the append-operation @@ -829,7 +836,7 @@ know @{text "X = \\ ` rhs"}. We further know that this is equal to \mbox{@{text "\\ ` (Arden X rhs)"}} using the properties of the invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"}, - we can infer that @{term "rhss rhs \ {X}"} and because the arden operation + we can infer that @{term "rhss rhs \ {X}"} and because the @{text Arden} operation removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}. This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}. So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\rs)"}. @@ -1104,8 +1111,8 @@ \end{center} % \noindent - Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B}, - or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}. + Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture), + or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture). In both cases we have to show that @{term "y @ z \ A ;; B"}. For this we use the following tagging-function % @@ -1347,19 +1354,19 @@ choice has consequences about how the initial equational system is set up. We have the $\lambda$-term on our `initial state', while Brzozowski has it on the terminal states. This means we also need to reverse the direction of Arden's - lemma. + Lemma. We briefly considered using the method Brzozowski presented in the Appendix 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 (if regarded equal - modulo ACI). We could - 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 + expressions and shows that there can be only finitely many of them with + respect to a language (if regarded equal modulo ACI). We could + have used as the tag of a string @{text s} the set of derivatives of a regular expression + generated by a language. 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 a similar argument as ours. However it seems not so easy to - calculate the derivatives and then to count them. Therefore we preferred our + the fact that there are only finitely such derivatives + would give us a similar argument as ours. However it seems not so easy to + calculate the set of derivatives modulo ACI and then to count them. Therefore we preferred our direct method of using tagging-functions. This is also where our method shines, because we can completely side-step the standard argument \cite{Kozen97} where automata need to be composed, which