# HG changeset patch # User urbanc # Date 1312928111 0 # Node ID b73478aaf33e178eeac057865d3b89ebc8dfa6e7 # Parent 48b452a2d4dfe30e4a7f9c3d3aba14d48e5ab360 more on paper diff -r 48b452a2d4df -r b73478aaf33e Closures.thy --- a/Closures.thy Tue Aug 09 22:14:41 2011 +0000 +++ b/Closures.thy Tue Aug 09 22:15:11 2011 +0000 @@ -143,21 +143,21 @@ subsection {* Closure under left-quotients *} abbreviation - "Ders_set A B \ \s \ A. Ders s B" + "Ders_lang A B \ \s \ A. Ders s B" lemma closure_left_quotient: assumes "regular A" - shows "regular (Ders_set B A)" + shows "regular (Ders_lang B A)" proof - from assms obtain r::"'a rexp" where eq: "lang r = A" by auto - have fin: "finite (pders_set B r)" by (rule finite_pders_set) + have fin: "finite (pders_lang B r)" by (rule finite_pders_lang) - have "Ders_set B (lang r) = (\ lang ` (pders_set B r))" + have "Ders_lang B (lang r) = (\ lang ` (pders_lang B r))" by (simp add: Ders_pders) - also have "\ = lang (\(pders_set B r))" using fin by simp - finally have "Ders_set B A = lang (\(pders_set B r))" using eq + also have "\ = lang (\(pders_lang B r))" using fin by simp + finally have "Ders_lang B A = lang (\(pders_lang B r))" using eq by simp - then show "regular (Ders_set B A)" by auto + then show "regular (Ders_lang B A)" by auto qed diff -r 48b452a2d4df -r b73478aaf33e Derivatives.thy --- a/Derivatives.thy Tue Aug 09 22:14:41 2011 +0000 +++ b/Derivatives.thy Tue Aug 09 22:15:11 2011 +0000 @@ -173,11 +173,11 @@ subsection {* Relating derivatives and partial derivatives *} -lemma +lemma der_pder: shows "(\ lang ` (pder c r)) = lang (der c r)" unfolding Der_der[symmetric] Der_pder by simp -lemma +lemma ders_pders: shows "(\ lang ` (pders s r)) = lang (ders s r)" unfolding Ders_ders[symmetric] Ders_pders by simp @@ -185,7 +185,7 @@ subsection {* There are only finitely many partial derivatives for a language *} abbreviation - "pders_set A r \ \s \ A. pders s r" + "pders_lang A r \ \s \ A. pders s r" text {* Non-empty suffixes of a string *} @@ -201,61 +201,61 @@ shows "(\v \ Suf s \ {[c]}. f v) = (\v \ Suf s. f (v @ [c]))" by (auto simp add: conc_def) -lemma pders_set_snoc: - shows "pders_set (Suf s \ {[c]}) r = (pder_set c (pders_set (Suf s) r))" +lemma pders_lang_snoc: + shows "pders_lang (Suf s \ {[c]}) r = (pder_set c (pders_lang (Suf s) r))" by (simp add: Suf_Union pders_snoc) lemma pders_Times: - shows "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_set (Suf s) r2)" + shows "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_lang (Suf s) r2)" proof (induct s rule: rev_induct) case (snoc c s) - have ih: "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_set (Suf s) r2)" + have ih: "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_lang (Suf s) r2)" by fact have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by (simp add: pders_snoc) - also have "\ \ pder_set c (Timess (pders s r1) r2 \ (pders_set (Suf s) r2))" + also have "\ \ pder_set c (Timess (pders s r1) r2 \ (pders_lang (Suf s) r2))" using ih by (auto) (blast) - also have "\ = pder_set c (Timess (pders s r1) r2) \ pder_set c (pders_set (Suf s) r2)" + also have "\ = pder_set c (Timess (pders s r1) r2) \ pder_set c (pders_lang (Suf s) r2)" by (simp) - also have "\ = pder_set c (Timess (pders s r1) r2) \ pders_set (Suf s \ {[c]}) r2" - by (simp add: pders_set_snoc) - also have "\ \ pder_set c (Timess (pders s r1) r2) \ pder c r2 \ pders_set (Suf s \ {[c]}) r2" + also have "\ = pder_set c (Timess (pders s r1) r2) \ pders_lang (Suf s \ {[c]}) r2" + by (simp add: pders_lang_snoc) + also have "\ \ pder_set c (Timess (pders s r1) r2) \ pder c r2 \ pders_lang (Suf s \ {[c]}) r2" by auto - also have "\ \ Timess (pders (s @ [c]) r1) r2 \ pder c r2 \ pders_set (Suf s \ {[c]}) r2" - by (auto simp add: if_splits pders_snoc) (blast) - also have "\ = Timess (pders (s @ [c]) r1) r2 \ pders_set (Suf (s @ [c])) r2" + also have "\ \ Timess (pder_set c (pders s r1)) r2 \ pder c r2 \ pders_lang (Suf s \ {[c]}) r2" + by (auto simp add: if_splits) (blast) + also have "\ = Timess (pders (s @ [c]) r1) r2 \ pder c r2 \ pders_lang (Suf s \ {[c]}) r2" + by (simp add: pders_snoc) + also have "\ \ Timess (pders (s @ [c]) r1) r2 \ pders_lang (Suf (s @ [c])) r2" by (auto simp add: Suf_snoc) finally show ?case . qed (simp) - lemma pders_Star: assumes a: "s \ []" - shows "pders s (Star r) \ (\v \ Suf s. Timess (pders v r) (Star r))" + shows "pders s (Star r) \ Timess (pders_lang (Suf s) r) (Star r)" using a proof (induct s rule: rev_induct) case (snoc c s) - have ih: "s \ [] \ pders s (Star r) \ (\v\Suf s. Timess (pders v r) (Star r))" by fact + have ih: "s \ [] \ pders s (Star r) \ Timess (pders_lang (Suf s) r) (Star r)" by fact { assume asm: "s \ []" have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) - also have "\ \ (pder_set c (\v\Suf s. Timess (pders v r) (Star r)))" + also have "\ \ pder_set c (Timess (pders_lang (Suf s) r) (Star r))" using ih[OF asm] by (auto) (blast) - also have "\ = (\v\Suf s. pder_set c (Timess (pders v r) (Star r)))" - by simp - also have "\ \ (\v\Suf s. (Timess (pder_set c (pders v r)) (Star r) \ pder c (Star r)))" - by (auto split: if_splits) - also have "\ = (\v\Suf s. (Timess (pder_set c (pders v r)) (Star r))) \ pder c (Star r)" - using asm by (auto simp add: Suf_def) - also have "\ = (\v\Suf s. (Timess (pders (v @ [c]) r) (Star r))) \ (Timess (pder c r) (Star r))" - by (simp add: pders_snoc) - also have "\ = (\v\Suf (s @ [c]). (Timess (pders v r) (Star r)))" + also have "\ \ Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \ pder c (Star r)" + by (auto split: if_splits) (blast)+ + also have "\ \ Timess (pders_lang (Suf (s @ [c])) r) (Star r) \ (Timess (pder c r) (Star r))" + by (auto simp add: Suf_snoc pders_lang_snoc) + also have "\ = Timess (pders_lang (Suf (s @ [c])) r) (Star r)" by (auto simp add: Suf_snoc Suf_Union pders_snoc) finally have ?case . } moreover { assume asm: "s = []" then have ?case - by (auto simp add: pders_snoc Suf_def) + apply (auto simp add: pders_snoc Suf_def) + apply(rule_tac x = "[c]" in exI) + apply(auto) + done } ultimately show ?case by blast qed (simp) @@ -263,29 +263,29 @@ definition "UNIV1 \ UNIV - {[]}" -lemma pders_set_Zero: - shows "pders_set UNIV1 Zero = {Zero}" +lemma pders_lang_Zero [simp]: + shows "pders_lang UNIV1 Zero = {Zero}" unfolding UNIV1_def by auto -lemma pders_set_One: - shows "pders_set UNIV1 One = {Zero}" +lemma pders_lang_One [simp]: + shows "pders_lang UNIV1 One = {Zero}" unfolding UNIV1_def by (auto split: if_splits) -lemma pders_set_Atom: - shows "pders_set UNIV1 (Atom c) \ {One, Zero}" +lemma pders_lang_Atom: + shows "pders_lang UNIV1 (Atom c) \ {One, Zero}" unfolding UNIV1_def by (auto split: if_splits) -lemma pders_set_Plus: - shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \ pders_set UNIV1 r2" +lemma pders_lang_Plus: + shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \ pders_lang UNIV1 r2" unfolding UNIV1_def by auto -lemma pders_set_Times_aux: +lemma pders_lang_Times_aux: assumes a: "s \ UNIV1" - shows "pders_set (Suf s) r2 \ pders_set UNIV1 r2" -using a unfolding UNIV1_def Suf_def by (auto) + shows "pders_lang (Suf s) r \ pders_lang UNIV1 r" +using a unfolding UNIV1_def Suf_def by auto -lemma pders_set_Times: - shows "pders_set UNIV1 (Times r1 r2) \ Timess (pders_set UNIV1 r1) r2 \ pders_set UNIV1 r2" +lemma pders_lang_Times [intro]: + shows "pders_lang UNIV1 (Times r1 r2) \ Timess (pders_lang UNIV1 r1) r2 \ pders_lang UNIV1 r2" unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) @@ -294,12 +294,12 @@ apply(rule conjI) apply(auto)[1] apply(rule subset_trans) -apply(rule pders_set_Times_aux) +apply(rule pders_lang_Times_aux) apply(auto simp add: UNIV1_def) done -lemma pders_set_Star: - shows "pders_set UNIV1 (Star r) \ Timess (pders_set UNIV1 r) (Star r)" +lemma pders_lang_Star [intro]: + shows "pders_lang UNIV1 (Star r) \ Timess (pders_lang UNIV1 r) (Star r)" unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) @@ -312,60 +312,60 @@ lemma finite_Timess: assumes a: "finite A" shows "finite (Timess A r)" -using a by (auto) +using a by auto -lemma finite_pders_set_UNIV1: - shows "finite (pders_set UNIV1 r)" +lemma finite_pders_lang_UNIV1: + shows "finite (pders_lang UNIV1 r)" apply(induct r) apply(simp) -apply(simp only: pders_set_One) +apply(simp only: pders_lang_One) apply(simp) apply(rule finite_subset) -apply(rule pders_set_Atom) +apply(rule pders_lang_Atom) apply(simp) -apply(simp only: pders_set_Plus) +apply(simp only: pders_lang_Plus) apply(simp) apply(rule finite_subset) -apply(rule pders_set_Times) +apply(rule pders_lang_Times) apply(simp only: finite_Timess finite_Un) apply(simp) apply(rule finite_subset) -apply(rule pders_set_Star) +apply(rule pders_lang_Star) apply(simp only: finite_Timess) done -lemma pders_set_UNIV_UNIV1: - shows "pders_set UNIV r = pders [] r \ pders_set UNIV1 r" +lemma pders_lang_UNIV_UNIV1: + shows "pders_lang UNIV r = pders [] r \ pders_lang UNIV1 r" unfolding UNIV1_def apply(auto) apply(rule_tac x="[]" in exI) apply(simp) done -lemma finite_pders_set_UNIV: - shows "finite (pders_set UNIV r)" -unfolding pders_set_UNIV_UNIV1 -by (simp add: finite_pders_set_UNIV1) +lemma finite_pders_lang_UNIV: + shows "finite (pders_lang UNIV r)" +unfolding pders_lang_UNIV_UNIV1 +by (simp add: finite_pders_lang_UNIV1) -lemma finite_pders_set: - shows "finite (pders_set A r)" +lemma finite_pders_lang: + shows "finite (pders_lang A r)" apply(rule rev_finite_subset) -apply(rule_tac r="r" in finite_pders_set_UNIV) +apply(rule_tac r="r" in finite_pders_lang_UNIV) apply(auto) done lemma finite_pders: shows "finite (pders s r)" -using finite_pders_set[where A="{s}" and r="r"] +using finite_pders_lang[where A="{s}" and r="r"] by simp lemma finite_pders2: shows "finite {pders s r | s. s \ A}" proof - - have "{pders s r | s. s \ A} \ Pow (pders_set A r)" by auto + have "{pders s r | s. s \ A} \ Pow (pders_lang A r)" by auto moreover - have "finite (Pow (pders_set A r))" - using finite_pders_set by simp + have "finite (Pow (pders_lang A r))" + using finite_pders_lang by simp ultimately show "finite {pders s r | s. s \ A}" by(rule finite_subset) @@ -405,13 +405,9 @@ by (auto simp add: MN_Rel_Ders Ders_pders) moreover have "equiv UNIV =(\x. pders x r)=" + and "equiv UNIV (\(lang r))" unfolding equiv_def refl_on_def sym_def trans_def - unfolding tag_eq_def - by auto - moreover - have "equiv UNIV (\(lang r))" - unfolding equiv_def refl_on_def sym_def trans_def - unfolding str_eq_def + unfolding tag_eq_def str_eq_def by auto ultimately show "finite (UNIV // \(lang r))" by (rule refined_partition_finite) diff -r 48b452a2d4df -r b73478aaf33e Journal/Paper.thy --- a/Journal/Paper.thy Tue Aug 09 22:14:41 2011 +0000 +++ b/Journal/Paper.thy Tue Aug 09 22:15:11 2011 +0000 @@ -249,7 +249,7 @@ pairs. Using this definition for disjoint union means we do not have a single type for automata. As a result we will not be able to define a regular language as one for which there exists an automaton that recognises all its - strings. This is because we cannot make a definition in HOL that is polymorphic in + strings (Definition~\ref{baddef}). This is because we cannot make a definition in HOL that is polymorphic in the state type and there is no type quantification available in HOL (unlike in Coq, for example).\footnote{Slind already pointed out this problem in an email to the HOL4 mailing list on 21st April 2005.} @@ -305,21 +305,21 @@ larger formalisations of automata theory are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}. - Also one might consider automata theory as a well-worn stock subject where - everything is crystal clear. However, paper proofs about automata often - involve subtle side-conditions which are easily overlooked, but which make - formal reasoning rather painful. For example Kozen's proof of the - Myhill-Nerode theorem requires that automata do not have inaccessible + Also one might consider automata theory and regular languages as a well-worn + stock subject where everything is crystal clear. However, paper proofs about + automata often involve subtle side-conditions which are easily overlooked, + but which make formal reasoning rather painful. For example Kozen's proof of + the Myhill-Nerode theorem requires that automata do not have inaccessible states \cite{Kozen97}. Another subtle side-condition is completeness of - automata, that is automata need to have total transition functions and at most one - `sink' state from which there is no connection to a final state (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 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. + automata, that is automata need to have total transition functions and at + most one `sink' state from which there is no connection to a final state + (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 + 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. In this paper, we will not attempt to formalise automata theory in @@ -361,11 +361,11 @@ partial derivatives \cite{Antimirov95}. Again to our best knowledge, the tagging-functions have not been used before to establish the Myhill-Nerode theorem. Derivatives of regular expressions have been used recently quite - widely in the literature; partial derivatives, in contrast, attracted much + widely in the literature; partial derivatives, in contrast, attract much less attention. However, partial derivatives are more suitable in the context of the Myhill-Nerode theorem, since it is easier to establish - formally their finiteness result. We have not found any proof that uses - either of them in order to prove the Myhill-Nerode theorem. + formally their finiteness result. We are not aware of any proof that uses + either of them for proving the Myhill-Nerode theorem. *} section {* Preliminaries *} @@ -412,7 +412,10 @@ \noindent In @{text "(ii)"} we use the notation @{term "length s"} for the length of a 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 strings in @{term "A \ (Suc n)"} must be longer than @{text n}. + Property @{text "(iv)"} states that a non-empty string in @{term "A\"} can + always be split up into a non-empty prefix belonging to @{text "A"} and the + rest being in @{term "A\"}. 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}} @@ -511,7 +514,15 @@ \noindent holds, whereby @{text "\ ` rs"} stands for the - image of the set @{text rs} under function @{text "\"}. + image of the set @{text rs} under function @{text "\"} defined as + + \begin{center} + @{term "lang ` rs \ {lang r | r. r \ rs}"} + \end{center} + + \noindent + In what follows we shall use this convenient short-hand notation for images of sets + also with other functions. *} @@ -1147,7 +1158,7 @@ \end{equation} \noindent - The relation @{term "\(lang r)"} partitions the set of all strings into some + The relation @{term "\(lang r)"} partitions the set of all strings, @{term UNIV}, into some equivalence classes. To show that there are only finitely many of them, it suffices to show in each induction step that another relation, say @{text R}, has finitely many equivalence classes and refines @{term "\(lang r)"}. @@ -1272,7 +1283,7 @@ \begin{lmm}\label{refinement} The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\A"}, provided for - all strings @{text x}, @{text y} and @{text z} we have \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}} + all strings @{text x}, @{text y} and @{text z} we have that \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}} and @{term "x @ z \ A"} imply @{text "y @ z \ A"}. \end{lmm} @@ -1280,8 +1291,8 @@ \noindent We therefore can analyse how the strings @{text "x @ z"} are in the language @{text A} and then construct an appropriate tagging-function to infer that - @{term "y @ z"} are also in @{text A}. For this we sill need the notion of - the set of all possible \emph{partitions} of a string + @{term "y @ z"} are also in @{text A}. For this we will use the notion of + the set of all possible \emph{partitions} of a string: \begin{equation} @{thm Partitions_def} @@ -1290,7 +1301,7 @@ \noindent If we know that @{text "(x\<^isub>p, x\<^isub>s) \ Partitions x"}, we will refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x}, - respectively to @{text "x\<^isub>s"} as the \emph{suffix}. + and respectively to @{text "x\<^isub>s"} as the \emph{suffix}. Now assuming @{term "x @ z \ A \ B"} there are only two possible ways of how to `split' @@ -1531,12 +1542,12 @@ \end{center} \noindent - From this we know there exist partitions @{text "y\<^isub>p"} and @{text + From this we know there exist a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"} with @{term "y\<^isub>p \ A\"} and also @{term "x\<^isub>s \A y\<^isub>s"}. Unfolding the Myhill-Nerode relation we know @{term "y\<^isub>s @ z\<^isub>a \ A"}. We also know that @{term "z\<^isub>b \ A\"}. Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \ - A\"}, which means @{term "y @ z \ A\"}. As the last step we have to set + A\"}, which means @{term "y @ z \ A\"}. The last step is to set @{text "A"} to @{term "lang r"} and thus complete the proof. \end{proof} *} @@ -1550,7 +1561,7 @@ 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 based on + 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, @@ -1565,14 +1576,14 @@ \end{center} \noindent - In order to aid readability, we shall also make use of the following abbreviation: + In order to aid readability, we shall also make use of the following abbreviation \begin{center} - @{abbrev "Derss s A"} + @{abbrev "Derss s As"} \end{center} - \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 @@ -1581,7 +1592,7 @@ \end{equation} \noindent - It is straightforward to establish the following properties for left-quotients: + It is also straightforward to establish the following properties for left-quotients: \begin{equation} \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l} @@ -1600,8 +1611,8 @@ \noindent where @{text "\"} is a function that tests whether the empty string - is in the language and returns @{term "{[]}"} or @{term "{}"}, respectively. - The only interesting case above is the last one where we use Prop.~\ref{langprops} + 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\"}. @@ -1629,8 +1640,8 @@ \end{center} \noindent - The last two clauses extend derivatives for characters to strings (list of - characters). The list-cons operator is written \mbox{@{text "_ :: _"}}. The + 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 whether a regular expression can recognise the empty string: @@ -1652,7 +1663,7 @@ \end{center} \noindent - By induction on the regular expression @{text r}, respectively the string @{text s}, + By induction on the regular expression @{text r}, respectively on the string @{text s}, one can easily show that left-quotients and derivatives relate as follows \cite{Sakarovitch09}: @@ -1667,7 +1678,7 @@ The importance in the context of the Myhill-Nerode theorem is that we can use \eqref{mhders} and \eqref{Dersders} in order to establish that @{term "x \(lang r) y"} is equivalent to - @{term "lang (ders x r) = lang (ders y r)"}. From this we obtain + @{term "lang (ders x r) = lang (ders y r)"}. Hence \begin{equation} @{term "x \(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"} @@ -1677,10 +1688,10 @@ \noindent which means the right-hand side (seen as relation) refines the Myhill-Nerode relation. Consequently, we can use - @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as a potential tagging-relation + @{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 in the Myhill-Nerode theorem, we also have to show that - for the corresponding language there are only finitely many derivatives---ensuring + order to be useful for teh 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 @@ -1700,8 +1711,8 @@ \noindent Carrying this idea through, we must not consider the set of all derivatives, - but the ones modulo @{text "ACI"}. In principle, this can be formally - defined, but it is very painful in a theorem prover (since there is no + but the ones modulo @{text "ACI"}. In principle, this can be done formally, + but it is very painful in a theorem prover (since there is no direct characterisation of the set of dissimlar derivatives). @@ -1742,7 +1753,7 @@ expressions. Note that in the last clause we first build the set of partial derivatives w.r.t~the character @{text c}, then build the image of this set under the function @{term "pders s"} and finally `union up' all resulting sets. It will be - convenient to introduce the following abbreviation + convenient to introduce for this the following abbreviation \begin{center} @{abbrev "pderss s A"} @@ -1763,7 +1774,7 @@ equal sets. Antimirov \cite{Antimirov95} showed a similar result to \eqref{Dersders} for partial derivatives: - \begin{equation} + \begin{equation}\label{Derspders} \mbox{\begin{tabular}{lc} @{text "(i)"} & @{thm Der_pder}\\ @{text "(ii)"} & @{thm Ders_pders} @@ -1787,7 +1798,7 @@ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll} @{term "Ders (c # s) (lang r)"} & @{text "="} & @{term "Ders s (Der c (lang r))"} & by def.\\ - & @{text "="} & @{term "Ders s (\ lang ` (pder c r))"} & by @{text "(i)"}\\ + & @{text "="} & @{term "Ders s (\ lang ` (pder c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\ & @{text "="} & @{term "\ (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\ & @{text "="} & @{term "\ lang ` (\ pders s ` (pder c r))"} & by IH\\ & @{text "="} & @{term "\ lang ` (pders (c # s) r)"} & by def.\\ @@ -1795,12 +1806,29 @@ \end{center} \noindent - In order to apply the induction hypothesis in the fourth step, we need the generalisation - over all regular expressions @{text r}. The case for the empty string is routine and omitted. + Note that in order to apply the induction hypothesis in the fourth equation, we + need the generalisation over all regular expressions @{text r}. The case for + the empty string is routine and omitted. \end{proof} - Antimirov also proved that for every language and regular expression there are only finitely - many partial derivatives. + \noindent + Taking \eqref{Dersders} and \eqref{Derspders} together gives the relationship + between languages of derivatives and partial derivatives + + \begin{equation} + \mbox{\begin{tabular}{lc} + @{text "(i)"} & @{thm der_pder[symmetric]}\\ + @{text "(ii)"} & @{thm ders_pders[symmetric]} + \end{tabular}} + \end{equation} + + \noindent + These two properties confirm the observation made earlier + that by using sets, partial derivatives have the @{text "ACI"}-identidies + of derivatives already built in. + + Antimirov also proved that for every language and regular expression + there are only finitely many partial derivatives. *} section {* Closure Properties *}