--- a/Journal/Paper.thy Wed Aug 03 17:08:31 2011 +0000
+++ b/Journal/Paper.thy Fri Aug 05 05:34:11 2011 +0000
@@ -34,7 +34,7 @@
abbreviation "ATOM \<equiv> Atom"
abbreviation "PLUS \<equiv> Plus"
abbreviation "TIMES \<equiv> Times"
-abbreviation "TIMESS \<equiv> Times_set"
+abbreviation "TIMESS \<equiv> Timess"
abbreviation "STAR \<equiv> Star"
@@ -143,19 +143,18 @@
wide range of textbooks on this subject, many of which are aimed at students
and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97,
HopcroftUllman69}). It seems natural to exercise theorem provers by
- formalising the theorems and by verifying formally the algorithms. A
- popular choice for a theorem prover would be one based on Higher-Order Logic
- (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
+ formalising the theorems and by verifying formally the algorithms.
+
+ A popular choice for a theorem prover would be one based on Higher-Order
+ Logic (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
presented in this paper we will use the latter. HOL is a predicate calculus
that allows quantification over predicate variables. Its type system is
- based on Church's Simple Theory of Types \cite{Church40}. Although
- many mathematical concepts can be conveniently expressed in HOL, there are some
+ 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 introduce finite automata
- and then define everything in terms of them \cite{Kozen97}. For example,
- a regular language is normally defined as:
+ 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:
\begin{dfntn}\label{baddef}
A language @{text A} is \emph{regular}, provided there is a
@@ -252,7 +251,8 @@
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
the state type and there is no type quantification available in HOL (unlike
- in Coq, for example).
+ in Coq, for example).\footnote{Slind already pointed out this problem in an email
+ to the HOL4 mailing list on 21st April 2005.}
An alternative, which provides us with a single type for automata, is to give every
state node an identity, for example a natural
@@ -266,8 +266,8 @@
problems as with graphs. Composing, for example, two non-deterministic automata in parallel
requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
dismisses for this the option of using identities, because it leads according to
- him to ``messy proofs''. Since he does not need to define what a regular
- language is, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes
+ him to ``messy proofs''. Since he does not need to define what regular
+ languages are, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes
\begin{quote}
\it%
@@ -317,7 +317,7 @@
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 can be found satisfying the
+ 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.
@@ -360,11 +360,12 @@
certain tagging-functions, and another indirect proof using Antimirov's
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 recently used quite
- widely in the literature about regular expressions. However, partial
- derivatives are more suitable in the context of the Myhill-Nerode theorem,
- since it is easier to establish formally their finiteness result.
-
+ theorem. Derivatives of regular expressions have been used recently quite
+ widely in the literature; partial derivatives, in contrast, attracted 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.
*}
section {* Preliminaries *}
@@ -398,10 +399,13 @@
we will make use of the following properties of these constructions.
\begin{prpstn}\label{langprops}\mbox{}\\
- \begin{tabular}{@ {}ll}
+ \begin{tabular}{@ {}lp{10cm}}
(i) & @{thm star_unfold_left} \\
(ii) & @{thm[mode=IfThen] pow_length}\\
(iii) & @{thm conc_Union_left} \\
+ (iv) & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then
+ there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"}
+ and @{term "x\<^isub>p \<noteq> []"} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
\end{tabular}
\end{prpstn}
@@ -1167,8 +1171,8 @@
\noindent
that means we take the image of @{text f} w.r.t.~all elements in the
domain. With this we will be able to infer that the tagging-functions, seen
- as relations, give rise to finitely many equivalence classes of @{const
- UNIV}. Finally we will show that the tagging-relations are more refined than
+ as relations, give rise to finitely many equivalence classes.
+ Finally we will show that the tagging-relations are more refined than
@{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
also be finite. We formally define the notion of a \emph{tagging-relation}
as follows.
@@ -1249,7 +1253,7 @@
is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}.
This amounts to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
@{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will
- provide us just the right assumptions in order to get the proof through.
+ provide us with just the right assumptions in order to get the proof through.
\begin{proof}[@{const "PLUS"}-Case]
We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite
@@ -1264,7 +1268,7 @@
\noindent
The @{const TIMES}-case is slightly more complicated. We first prove the
- following lemma, which will aid the refinement-proofs.
+ following lemma, which will aid the proof about refinement.
\begin{lmm}\label{refinement}
The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\<approx>A"}, provided for
@@ -1274,15 +1278,21 @@
\noindent
- We therefore can clean information from how the strings @{text "x @ z"} are in @{text A}
- and construct appropriate tagging-functions to infer that @{term "y @ z \<in> A"}.
- For the @{const Times}-case we additionally need the notion of the set of all
- possible partitions of a string
+ 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
\begin{equation}
@{thm Partitions_def}
\end{equation}
+ \noindent
+ If we know that @{text "(x\<^isub>p, x\<^isub>s) \<in> 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}.
+
+
Now assuming @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split'
this string to be in @{term "A \<cdot> B"}:
%
@@ -1350,12 +1360,13 @@
(second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case
we will only go through if we know that @{term "x \<approx>A y"} holds @{text "(*)"}. Because then
we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.
- In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is a possible partition
- of the string @{text x}. So we have to know that both @{text "x\<^isub>p"} and the
+ In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is one possible partition
+ of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the
corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related'
to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
+ This will solve the second case.
Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the
- tagging-function as:
+ tagging-function in the @{const Times}-case as:
\begin{center}
@{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~
@@ -1363,27 +1374,32 @@
\end{center}
\noindent
- With this definition in place, we can discharge the @{const "Times"}-case as follows.
+ We have to make the assumption for all suffixes @{text "x\<^isub>s"}, since we do
+ not know anything about how the string @{term x} is partitioned.
+ With this definition in place, let us prove the @{const "Times"}-case.
\begin{proof}[@{const TIMES}-Case]
If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
@{term "tag_Times A B"} is a subset of this product set, and therefore finite.
- By Lemma \ref{refinement} we know
+ For the refinement of @{term "\<approx>(A \<cdot> B)"} and @{text "\<^raw:$\threesim$>\<^bsub>\<times>tag A B\<^esub>"},
+ we have by Lemma \ref{refinement}
\begin{center}
@{term "tag_Times A B x = tag_Times A B y"}
\end{center}
\noindent
- and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown
- above, there are two cases to be considered (see pictures above). First,
- there exists a @{text "z\<^isub>p"} and @{text "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}.
- By the assumption about @{term "tag_Times A B"} we have
- @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
- relation that @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"}, we can conclude in this case
- with @{term "y @ z \<in> A \<cdot> B"}.
+ and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot>
+ B"}. As shown in the pictures above, there are two cases to be
+ considered. First, there exists a @{text "z\<^isub>p"} and @{text
+ "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s
+ \<in> B"}. By the assumption about @{term "tag_Times A B"} we have @{term "\<approx>A
+ `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Hence by the Myhill-Nerode
+ relation @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"},
+ we can conclude in this case with @{term "y @ z \<in> A \<cdot> B"} (recall @{text
+ "z\<^isub>p @ z\<^isub>s = z"}).
Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with
@{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
@@ -1403,7 +1419,7 @@
This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
{y\<^isub>s}"}. Unfolding the Myhill-Nerode relation and together with the
- facts that @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}, we
+ facts that @{text "x\<^isub>p \<in> A"} and \mbox{@{text "x\<^isub>s @ z \<in> B"}}, we
obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
this case. We again can complete the @{const TIMES}-case by setting @{text
A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
@@ -1411,7 +1427,7 @@
\noindent
The case for @{const Star} is similar to @{const TIMES}, but poses a few
- extra challenges. To deal with them we define first the notion of a \emph{string
+ extra challenges. To deal with them, we define first the notion of a \emph{string
prefix} and a \emph{strict string prefix}:
\begin{center}
@@ -1421,8 +1437,7 @@
\end{tabular}
\end{center}
- \noindent
- When we analyse the case of @{text "x @ z"} being an element in @{term "A\<star>"}
+ When analysing the case of @{text "x @ z"} being an element in @{term "A\<star>"}
and @{text x} is not the empty string, we have the following picture:
\begin{center}
@@ -1466,13 +1481,13 @@
\noindent
We can find a strict prefix @{text "x\<^isub>p"} of @{text x} such that @{term "x\<^isub>p \<in> A\<star>"},
@{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string
- @{text "[]"} would do.
+ @{text "[]"} would do (recall @{term "x \<noteq> []"}).
There are potentially many such prefixes, but there can only be finitely many of them (the
string @{text x} is finite). Let us therefore choose the longest one and call it
@{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
- know it is in @{term "A\<star>"} and it is not the empty string. By Prop.~\ref{langprops}@{text "(i)"},
+ know it is in @{term "A\<star>"} and cannot be the empty string. By Prop.~\ref{langprops}@{text "(iv)"},
we can separate
- this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
+ this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<noteq> []"}, @{text "a \<in> A"}
and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
otherwise @{text "x\<^bsub>pmax\<^esub>"} is not the longest prefix. That means @{text a}
`overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
@@ -1497,8 +1512,9 @@
that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}.
We first need to consider the case that @{text x} is the empty string.
- From the assumption we can infer @{text y} is the empty string and
- clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+ From the assumption about strict prefixes in @{text "\<^raw:$\threesim$>\<^bsub>\<star>tag A\<^esub>"}, we
+ can infer @{text y} is the empty string and
+ then clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
string, we can divide the string @{text "x @ z"} as shown in the picture
above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"},
we have
@@ -1515,17 +1531,17 @@
\end{center}
\noindent
- and we know there exist partitions @{text "y\<^isub>p"} and @{text
+ From this we know there exist partitions @{text "y\<^isub>p"} and @{text
"y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
y\<^isub>s"}. Unfolding the Myhill-Nerode relation we know @{term
"y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. As the last step we have to set
- @{text "A"} to @{term "lang r"} and complete the proof.
+ @{text "A"} to @{term "lang r"} and thus complete the proof.
\end{proof}
*}
-section {* Second Part based on Partial Derivatives *}
+section {* Second Part proved using Partial Derivatives *}
text {*
\noindent
@@ -1534,10 +1550,12 @@
a more refined relation than @{term "\<approx>(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. Assume
- the following two definitions for a 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:
+ an indirect method to come up with such a refined relation based on
+ derivatives of regular expressions \cite{Brzozowski64}.
+
+ Assume the following two definitions for a \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:
\begin{center}
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
@@ -1547,6 +1565,14 @@
\end{center}
\noindent
+ In order to aid readability, we shall also make use of the following abbreviation:
+
+ \begin{center}
+ @{abbrev "Derss s A"}
+ \end{center}
+
+
+ \noindent
Clearly we have the following relation between the Myhill-Nerode relation
(Def.~\ref{myhillneroderel}) and left-quotients
@@ -1555,20 +1581,20 @@
\end{equation}
\noindent
- It is realtively easy to establish the following properties for left-quotients:
+ It is straightforward to establish the following properties for left-quotients:
\begin{equation}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
- @{thm (lhs) Der_zero} & $=$ & @{thm (rhs) Der_zero}\\
- @{thm (lhs) Der_one} & $=$ & @{thm (rhs) Der_one}\\
- @{thm (lhs) Der_atom} & $=$ & @{thm (rhs) Der_atom}\\
- @{thm (lhs) Der_union} & $=$ & @{thm (rhs) Der_union}\\
+ @{thm (lhs) Der_simps(1)} & $=$ & @{thm (rhs) Der_simps(1)}\\
+ @{thm (lhs) Der_simps(2)} & $=$ & @{thm (rhs) Der_simps(2)}\\
+ @{thm (lhs) Der_simps(3)} & $=$ & @{thm (rhs) Der_simps(3)}\\
+ @{thm (lhs) Der_simps(4)} & $=$ & @{thm (rhs) Der_simps(4)}\\
@{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
@{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\
- @{thm (lhs) Ders_nil} & $=$ & @{thm (rhs) Ders_nil}\\
- @{thm (lhs) Ders_cons} & $=$ & @{thm (rhs) Ders_cons}\\
- %@{thm (lhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
- % & @{thm (rhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+ @{thm (lhs) Ders_simps(1)} & $=$ & @{thm (rhs) Ders_simps(1)}\\
+ @{thm (lhs) Ders_simps(2)} & $=$ & @{thm (rhs) Ders_simps(2)}\\
+ %@{thm (lhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
+ % & @{thm (rhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
\end{tabular}}
\end{equation}
@@ -1603,10 +1629,10 @@
\end{center}
\noindent
- The last two lines extend @{const der} to strings (list of characters) where
- list-cons 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:
+ The last two clauses extend derivatives for characters to strings (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:
\begin{center}
\begin{tabular}{c@ {\hspace{10mm}}c}
@@ -1639,8 +1665,8 @@
\noindent
The importance in the context of the Myhill-Nerode theorem is that
- we can use \eqref{mhders} and the equations above in order to
- establish that @{term "x \<approx>(lang r) y"} if and only if
+ we can use \eqref{mhders} and \eqref{Dersders} in order to
+ establish that @{term "x \<approx>(lang r) y"} is equivalent to
@{term "lang (ders x r) = lang (ders y r)"}. From this we obtain
\begin{equation}
@@ -1649,29 +1675,35 @@
\noindent
- Consequently, we can use as the tagging relation @{text
- "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, since it refines
- @{term "\<approx>(lang r)"}. However, in order to be useful in the Myhill-Nerode
- theorem, we have to show that for a language there are only finitely many
- derivatives. Unfortunately, this is not true in general: Sakarovitch gives
- an example with infinitely many derivatives
- \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved is
- that for every language there \emph{are} 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:
+ which means the right-hand side (seen as relation) refines the
+ Myhill-Nerode relation. Consequently, we can use
+ @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a potential 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
+ 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:
- \begin{center}
- \begin{tabular}{cl}
+ \begin{equation}\label{ACI}
+ \mbox{\begin{tabular}{cl}
(@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
(@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
(@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
- Carrying this idea through menas we now have to reasoning modulo @{text "ACI"}.
- This can be done, but it is very painful in a theorem prover (since there is
- no direct characterisation of the set of dissimlar derivatives).
+ 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
+ direct characterisation of the set of dissimlar derivatives).
+
Fortunately, there is a much simpler approach using \emph{partial
derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined
@@ -1686,49 +1718,97 @@
& @{text "\<equiv>"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
@{thm (lhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
- @{term "(Times_set (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
+ @{term "(Timess (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
& & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
- @{term "Times_set (pder c r\<^isub>1) r\<^isub>2"}\\
+ @{term "Timess (pder c r\<^isub>1) r\<^isub>2"}\\
@{thm (lhs) pder.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(6)}\smallskip\\
@{thm (lhs) pders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(1)}\\
- @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+ @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
\end{tabular}
\end{center}
\noindent
- Unlike `simple' derivatives, these functions return a set of regular
- expressions. In the @{const Times} and @{const Star} cases we use
+ Again the last two clauses extend partial derivatives from characters to strings.
+ Unlike `simple' derivatives, the functions for partial derivatives return sets of regular
+ expressions. In the @{const Times} and @{const Star} cases we therefore use the
+ auxiliary definition
\begin{center}
@{text "TIMESS rs r \<equiv> {TIMES r' r | r' \<in> rs}"}
\end{center}
\noindent
- in order to `sequence' a regular expressions with respect to a set of regular
- expresions. Note that in the last case we first build the set of partial derivatives
- w.r.t~@{text c}, then build the image of this set under the function @{term "pders s"}
- and finally `union up' all resulting sets. Note also that in some sense, partial
- derivatives have the @{text "ACI"}-identities already build in. Antimirov
- \cite{Antimirov95}
- showed
+ in order to `sequence' a regular expression with a set of regular
+ 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
+
+ \begin{center}
+ @{abbrev "pderss s A"}
+ \end{center}
+
+ \noindent
+ which simplifies the last clause of @{const "pders"} to
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+ \end{tabular}
+ \end{center}
+
+ Partial derivatives can be seen as having the @{text "ACI"}-identities already built in:
+ taking the partial derivatives of the
+ regular expressions in \eqref{ACI} gives us in each case
+ equal sets. Antimirov \cite{Antimirov95} showed a similar result to
+ \eqref{Dersders} for partial derivatives:
\begin{equation}
- \mbox{\begin{tabular}{c}
- @{thm Der_pder}\\
- @{thm Ders_pders}
+ \mbox{\begin{tabular}{lc}
+ @{text "(i)"} & @{thm Der_pder}\\
+ @{text "(ii)"} & @{thm Ders_pders}
\end{tabular}}
- \end{equation}
+ \end{equation}
+
+ \begin{proof}
+ The first fact is by a simple induction on @{text r}. For the second we slightly
+ modify Antimirov's proof by performing an induction on @{text s} where we
+ genaralise over all @{text r}. That means in the @{text "cons"}-case the
+ induction hypothesis is
+
+ \begin{center}
+ @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Ders s (lang r) = \<Union> lang ` (pders s r)"}
+ \end{center}
\noindent
- and proved that for every language and regular expression there are only finitely
+ With this we can establish
+
+ \begin{center}
+ \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 (\<Union> lang ` (pder c r))"} & by @{text "(i)"}\\
+ & @{text "="} & @{term "\<Union> (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\
+ & @{text "="} & @{term "\<Union> lang ` (\<Union> pders s ` (pder c r))"} & by IH\\
+ & @{text "="} & @{term "\<Union> lang ` (pders (c # s) r)"} & by def.\\
+ \end{tabular}
+ \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.
+ \end{proof}
+
+ Antimirov also proved that for every language and regular expression there are only finitely
many partial derivatives.
*}
section {* Closure Properties *}
text {*
- The beautiful characteristics of regular languages is that they are closed
- under many operations. Closure under union, sequencencing and Kleene-star
+ \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}).
More interesting is the closure under complement, because
it seems difficult to construct a regular expression for the complement