# HG changeset patch # User urbanc # Date 1313104299 0 # Node ID 2a5ac68db24b5f843663e15b86238a2f8db19587 # Parent ce24ed955cca0fb827110910ea9b49453b934a96 finished section about derivatives and closure properties diff -r ce24ed955cca -r 2a5ac68db24b Closures.thy --- a/Closures.thy Thu Aug 11 16:55:41 2011 +0000 +++ b/Closures.thy Thu Aug 11 23:11:39 2011 +0000 @@ -143,7 +143,7 @@ subsection {* Closure under left-quotients *} abbreviation - "Ders_lang A B \ \s \ A. Ders s B" + "Ders_lang A B \ \x \ A. Ders x B" lemma closure_left_quotient: assumes "regular A" diff -r ce24ed955cca -r 2a5ac68db24b Derivatives.thy --- a/Derivatives.thy Thu Aug 11 16:55:41 2011 +0000 +++ b/Derivatives.thy Thu Aug 11 23:11:39 2011 +0000 @@ -115,12 +115,12 @@ fun pder :: "'a \ 'a rexp \ ('a rexp) set" where - "pder c Zero = {Zero}" -| "pder c One = {Zero}" -| "pder c (Atom c') = (if c = c' then {One} else {Zero})" + "pder c Zero = {}" +| "pder c One = {}" +| "pder c (Atom c') = (if c = c' then {One} else {})" | "pder c (Plus r1 r2) = (pder c r1) \ (pder c r2)" | "pder c (Times r1 r2) = - (if nullable r1 then Timess (pder c r1) r2 \ pder c r2 else Timess (pder c r1) r2)" + (if nullable r1 then Timess (pder c r1) r2 \ pder c r2 else Timess (pder c r1) r2)" | "pder c (Star r) = Timess (pder c r) (Star r)" abbreviation @@ -144,11 +144,14 @@ by (simp add: pders_append) lemma pders_simps [simp]: - shows "pders s Zero = {Zero}" - and "pders s One = (if s = [] then {One} else {Zero})" - and "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" + shows "pders s Zero = (if s= [] then {Zero} else {})" + and "pders s One = (if s = [] then {One} else {})" and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \ (pders s r2))" -by (induct s) (auto) +by (induct s) (simp_all) + +lemma pders_Atom [intro]: + shows "pders s (Atom c) \ {Atom c, One}" +by (induct s) (simp_all) subsection {* Relating left-quotients and partial derivatives *} @@ -185,7 +188,7 @@ subsection {* There are only finitely many partial derivatives for a language *} definition - "pders_lang A r \ \s \ A. pders s r" + "pders_lang A r \ \x \ A. pders x r" lemma pders_lang_subsetI [intro]: assumes "\s. s \ A \ pders s r \ C" @@ -196,20 +199,31 @@ shows "pders_lang (A \ B) r = (pders_lang A r \ pders_lang B r)" by (simp add: pders_lang_def) +lemma pders_lang_subset: + shows "A \ B \ pders_lang A r \ pders_lang B r" +by (auto simp add: pders_lang_def) + definition "UNIV1 \ UNIV - {[]}" lemma pders_lang_Zero [simp]: - shows "pders_lang UNIV1 Zero = {Zero}" + shows "pders_lang UNIV1 Zero = {}" unfolding UNIV1_def pders_lang_def by auto lemma pders_lang_One [simp]: - shows "pders_lang UNIV1 One = {Zero}" + shows "pders_lang UNIV1 One = {}" unfolding UNIV1_def pders_lang_def by (auto split: if_splits) -lemma pders_lang_Atom: - shows "pders_lang UNIV1 (Atom c) \ {One, Zero}" -unfolding UNIV1_def pders_lang_def by (auto split: if_splits) +lemma pders_lang_Atom [simp]: + shows "pders_lang UNIV1 (Atom c) = {One}" +unfolding UNIV1_def pders_lang_def +apply(auto) +apply(frule rev_subsetD) +apply(rule pders_Atom) +apply(simp) +apply(case_tac xa) +apply(auto split: if_splits) +done lemma pders_lang_Plus [simp]: shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \ pders_lang UNIV1 r2" @@ -328,15 +342,9 @@ lemma finite_pders_lang_UNIV1: shows "finite (pders_lang UNIV1 r)" apply(induct r) -apply(simp) -apply(simp) -apply(rule finite_subset[OF pders_lang_Atom]) -apply(simp) -apply(simp) -apply(rule finite_subset[OF pders_lang_Times]) -apply(simp) -apply(rule finite_subset[OF pders_lang_Star]) -apply(simp) +apply(simp_all add: + finite_subset[OF pders_lang_Times] + finite_subset[OF pders_lang_Star]) done lemma pders_lang_UNIV: @@ -351,9 +359,9 @@ lemma finite_pders_lang: shows "finite (pders_lang A r)" -apply(rule rev_finite_subset) -apply(rule_tac r="r" in finite_pders_lang_UNIV) -apply(auto simp add: pders_lang_def) +apply(rule rev_finite_subset[OF finite_pders_lang_UNIV]) +apply(rule pders_lang_subset) +apply(simp) done text {* Relating the Myhill-Nerode relation with left-quotients. *} diff -r ce24ed955cca -r 2a5ac68db24b Journal/Paper.thy --- a/Journal/Paper.thy Thu Aug 11 16:55:41 2011 +0000 +++ b/Journal/Paper.thy Thu Aug 11 23:11:39 2011 +0000 @@ -42,7 +42,7 @@ str_eq ("\\<^bsub>_\<^esub>") and str_eq_applied ("_ \\<^bsub>_\<^esub> _") and conc (infixr "\" 100) and - star ("_\<^bsup>\\<^esup>") and + star ("_\<^bsup>\\<^esup>" [101] 200) and pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and Suc ("_+1" [100] 100) and quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and @@ -66,14 +66,17 @@ tag_Times ("\tag _ _ _" [100, 100, 100] 100) and tag_Star ("\tag _" [100] 100) and tag_Star ("\tag _ _" [100, 100] 100) and - tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and + tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>" [100] 100) and Delta ("\'(_')") and nullable ("\'(_')") and Cons ("_ :: _" [100, 100] 100) and Rev ("Rev _" [1000] 100) and Der ("Der _ _" [1000, 1000] 100) and ONE ("ONE" 999) and - ZERO ("ZERO" 999) + ZERO ("ZERO" 999) and + pders_lang ("pderl") and + UNIV1 ("UNIV\<^isup>+") and + Ders_lang ("Derl") lemma meta_eq_app: shows "f \ \x. g x \ f x \ g x" @@ -152,7 +155,9 @@ based on Church's Simple Theory of Types \cite{Church40}. Although many mathematical concepts can be conveniently expressed in HOL, there are some limitations that hurt badly, if one attempts a simple-minded formalisation - of regular languages in it. The typical approach to regular languages is to + of regular languages in it. + + The typical approach to regular languages is to introduce finite automata and then define everything in terms of them \cite{Kozen97}. For example, a regular language is normally defined as: @@ -204,7 +209,7 @@ & - \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$} + \raisebox{2.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$} & @@ -316,7 +321,7 @@ (Brzozowski mentions this side-condition in the context of state complexity of automata \cite{Brzozowski10}). Such side-conditions mean that if we define a regular language as one for which there exists \emph{a} finite - automaton that recognises all its strings (see Def.~\ref{baddef}), then we + automaton that recognises all its strings (see Definition~\ref{baddef}), then we need a lemma which ensures that another equivalent one can be found satisfying the side-condition. Unfortunately, such `little' and `obvious' lemmas make a formalisation of automata theory a hair-pulling experience. @@ -1095,7 +1100,7 @@ In this section we will give a proof for establishing the second part of the Myhill-Nerode theorem. It can be formulated in our setting as follows: - \begin{thrm} + \begin{thrm}\label{myhillnerodetwo} Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}. \end{thrm} @@ -1560,13 +1565,13 @@ the second direction of the Myhill-Nerode theorem, we need to find a more refined relation than @{term "\(lang r)"} for which we can show that there are only finitely many equivalence classes. So far we - showed this by induction on @{text "r"}. However, there is also - an indirect method to come up with such a refined relation by using - derivatives of regular expressions \cite{Brzozowski64}. + showed this directly by induction on @{text "r"} using tagging-functions. + However, there is also an indirect method to come up with such a refined + relation by using derivatives of regular expressions \cite{Brzozowski64}. - Assume the following two definitions for a \emph{left-quotient} of a language, + Assume the following two definitions for the \emph{left-quotient} of a language, which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c} - is a character and @{text s} a string: + is a character and @{text s} a string, respectively: \begin{center} \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l} @@ -1576,7 +1581,7 @@ \end{center} \noindent - In order to aid readability, we shall also make use of the following abbreviation + In order to aid readability, we shall make use of the following abbreviation \begin{center} @{abbrev "Derss s As"} @@ -1584,15 +1589,15 @@ \noindent where we apply the left-quotient to a set of languages and then combine the results. - Clearly we have the following relation between the Myhill-Nerode relation - (Def.~\ref{myhillneroderel}) and left-quotients + Clearly we have the following equivalence between the Myhill-Nerode relation + (Definition~\ref{myhillneroderel}) and left-quotients \begin{equation}\label{mhders} @{term "x \A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"} \end{equation} \noindent - It is also straightforward to establish the following properties for left-quotients: + It is also straightforward to establish the following properties of left-quotients \begin{equation} \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l} @@ -1610,16 +1615,16 @@ \end{equation} \noindent - where @{text "\"} is a function that tests whether the empty string + where @{text "\"} in the fifth line is a function that tests whether the empty string is in the language and returns @{term "{[]}"} or @{term "{}"}, accordingly. The only interesting case above is the last one where we use Prop.~\ref{langprops}@{text "(i)"} in order to infer that @{term "Der c (A\) = Der c (A \ A\)"}. We can - then complete the proof by observing that @{term "Delta A \ Der c (A\) \ (Der c A) \ A\"}. + then complete the proof by noting that @{term "Delta A \ Der c (A\) \ (Der c A) \ A\"}. Brzozowski observed that the left-quotients for languages of regular - expressions can be calculated directly via the notion of \emph{derivatives - of a regular expression} \cite{Brzozowski64}, which we define in Isabelle/HOL as - follows: + expressions can be calculated directly using the notion of \emph{derivatives + of a regular expression} \cite{Brzozowski64}. We define this notion in + Isabelle/HOL as follows: \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}} @@ -1642,7 +1647,7 @@ \noindent The last two clauses extend derivatives from characters to strings---i.e.~list of characters. The list-cons operator is written \mbox{@{text "_ :: _"}}. The - function @{term "nullable r"} needed in the @{const Times}-case tests + boolean function @{term "nullable r"} needed in the @{const Times}-case tests whether a regular expression can recognise the empty string: \begin{center} @@ -1687,19 +1692,22 @@ \noindent which means the right-hand side (seen as relation) refines the - Myhill-Nerode relation. Consequently, we can use + Myhill-Nerode relation. Consequently, we can use @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as a tagging-relation for the regular expression @{text r}. However, in - order to be useful for teh second part of the Myhill-Nerode theorem, we also have to show that + order to be useful for the second part of the Myhill-Nerode theorem, we also have to show that for the corresponding language there are only finitely many derivatives---thus 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.~a language - \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved - is that for every language there \emph{are} only finitely `dissimilar' - derivatives for a regular expression. Two regular expressions are said to be - \emph{similar} provided they can be identified using the using the @{text - "ACI"}-identities: + expression has infinitely many derivatives w.r.t.~the language + \mbox{@{term "({a} \ {b})\ \ ({a} \ {b})\ \ {a}"}} + \cite[Page~141]{Sakarovitch09}. + + What Brzozowski \cite{Brzozowski64} established is that for every language there + \emph{are} only finitely `dissimilar' derivatives for a regular + expression. Two regular expressions are said to be \emph{similar} provided + they can be identified using the using the @{text "ACI"}-identities: + \begin{equation}\label{ACI} \mbox{\begin{tabular}{cl} @@ -1756,7 +1764,7 @@ convenient to introduce for this the following abbreviation \begin{center} - @{abbrev "pderss s A"} + @{abbrev "pderss s rs"} \end{center} \noindent @@ -1824,11 +1832,88 @@ \noindent These two properties confirm the observation made earlier - that by using sets, partial derivatives have the @{text "ACI"}-identidies + that by using sets, partial derivatives have the @{text "ACI"}-identities of derivatives already built in. Antimirov also proved that for every language and regular expression - there are only finitely many partial derivatives. + there are only finitely many partial derivatives, whereby the partial + derivatives of @{text r} w.r.t.~a language @{text A} is defined as + + \begin{equation}\label{Pdersdef} + @{thm pders_lang_def} + \end{equation} + + \begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov} + For every language @{text A} and every regular expression @{text r}, + \mbox{@{thm finite_pders_lang}}. + \end{thrm} + + \noindent + Antimirov's argument first shows this theorem for the language @{term UNIV1}, + which is the set of all non-empty strings. For this he proves: + + \begin{equation} + \mbox{\begin{tabular}{l} + @{thm pders_lang_Zero}\\ + @{thm pders_lang_One}\\ + @{thm pders_lang_Atom}\\ + @{thm pders_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ + @{thm pders_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ + @{thm pders_lang_Star}\\ + \end{tabular}} + \end{equation} + + \noindent + from which one can deduce by induction on @{text r} that + + \begin{center} + @{thm finite_pders_lang_UNIV1} + \end{center} + + \noindent + holds. Now Antimirov's theorem follows because + + \begin{center} + @{thm pders_lang_UNIV}\\ + \end{center} + + \noindent + and for all languages @{text "A"}, @{thm pders_lang_subset[where B="UNIV", + simplified]} holds. Since we follow Antimirov's proof quite closely in our + formalisation, we omit the details. + + + Let us return to our proof of the second direction in the Myhill-Nerode + theorem. The point of the above calculations is to use + @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as tagging-relation. + + + \begin{proof}[Proof of Theorem~\ref{myhillnerodetwo}] + Using \eqref{mhders} + and \eqref{Derspders} we can easily infer that + + \begin{center} + @{term "x \(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pders x r = pders y r"} + \end{center} + + \noindent + which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} refines @{term "\(lang r)"}. + So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\(lang r)))"}} + holds if @{term "finite (UNIV // (=(\x. pders x r)=))"}. In order to establish + the latter, we can use Lemma~\ref{finone} and show that the range of the + tagging-function \mbox{@{term "\x. pders x r"}} is finite. For this recall Definition + \ref{Pdersdef}, which gives us that + + \begin{center} + @{thm pders_lang_def[where A="UNIV", simplified]} + \end{center} + + \noindent + Now the range of @{term "\x. pders x r"} is a subset of @{term "Pow (pders_lang UNIV r)"}, + which we know is finite by Theorem~\ref{antimirov}. This means there + are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"}, + and we can again conclude the second part of the Myhill-Nerode theorem. + \end{proof} *} section {* Closure Properties *} @@ -1837,7 +1922,7 @@ \noindent The real beauty of regular languages is that they are closed under almost all set operations. Closure under union, concatenation and Kleene-star - are trivial to establish given our definition of regularity (Def.~\ref{regular}). + are trivial to establish given our definition of regularity (Definition~\ref{regular}). More interesting is the closure under complement, because it seems difficult to construct a regular expression for the complement language by direct means. However the existence of such a regular expression @@ -1850,7 +1935,8 @@ \noindent holds for any strings @{text "s\<^isub>1"} and @{text "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} - give rise to the same partitions. + give rise to the same partitions. So if one is finite, the other is too and the + other way around. Once closure under complement is established, closure under intersection and set difference is also easy, because @@ -1886,11 +1972,39 @@ \end{tabular} \end{center} + \noindent + For this operation we can so - In connection with left-quotient, the perhaps surprising fact is that - regular languages are closed under any left-quotient. + \begin{center} + @{text "(\(r))\<^bsup>-1\<^esup>"}~@{text "="}~@{thm (rhs) rev_lang} + \end{center} + + \noindent + from which closure under reversal follows. + + The perhaps the most surprising fact is that regular languages are closed under any + left-quotient. Define + + \begin{center} + @{abbrev "Ders_lang B A"} + \end{center} + \noindent + and assume @{text A} is regular. From this we know there exists a regular + expression @{text r} such that @{term "A = lang r"}. We also know that + @{term "pders_lang B r"} is finite. By definition and Lemma~\ref{Derspders} + \begin{equation}\label{eqq} + @{term "Ders_lang B (lang r) = (\ lang ` (pders_lang B r))"} + \end{equation} + + \noindent + Since there are only finitely many regular expressions in @{term "pders_lang B r"} + by Theorem~\ref{antimirov}, we know that the right-hand side of \eqref{eqq}, is + equal to @{term "lang (\(pders_lang B r))"} using \eqref{uplus}. Hence + the regular expression @{term "pders_lang B r"} verifies that @{term "Ders_lang B A"} + is regular. + *} diff -r ce24ed955cca -r 2a5ac68db24b Mirkin.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Mirkin.thy Thu Aug 11 23:11:39 2011 +0000 @@ -0,0 +1,56 @@ +theory Mirkin +imports Derivatives +begin + +fun + pbase :: "'a rexp \ 'a rexp set" +where + "pbase (Zero) = {}" +| "pbase (One) = {}" +| "pbase (Atom a) = {One}" +| "pbase (Plus r1 r2) = pbase r1 \ pbase r2" +| "pbase (Times r1 r2) = Timess (pbase r1) r2 \ pbase r2" +| "pbase (Star r) = Timess (pbase r) (Star r)" + + +lemma a: "A \ B \ Timess A r \ Timess B r" +apply(auto) +done + +lemma b: "pders_lang UNIV1 r \ pbase r" +apply(induct r) +apply(simp) +apply(simp) +apply(simp) +apply(simp) +apply(auto)[1] +apply(simp) +apply(rule subset_trans) +apply(rule pders_lang_Times) +apply(simp) +apply(rule conjI) +apply(drule_tac r="r2" in a) +apply(auto)[1] +apply(auto)[1] +apply(rule subset_trans) +apply(rule pders_lang_Star) +apply(simp) +apply(rule a) +apply(simp) +done + +lemma c: "pders_lang UNIV r \ pbase r \ {r}" +using b +apply(auto simp add: pders_lang_UNIV) +done + +lemma d: "finite (pbase r)" +apply(induct r) +apply(auto) +done + +lemma e: "pder c r \ pbase r" +by (induct r) (auto) + + +end \ No newline at end of file