
diff -r b794db0b79db -r b1258b7d2789 Attic/Myhill.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Myhill.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -0,0 +1,331 @@
+theory Myhill
+  imports Myhill_2
+begin
+
+section {* Preliminaries \label{sec_prelim}*}
+
+subsection {* Finite automata and \mht  \label{sec_fa_mh} *}
+
+text {*
+
+A {\em determinisitc finite automata (DFA)} $M$ is a 5-tuple 
+$(Q, \Sigma, \delta, s, F)$, where:
+\begin{enumerate}
+  \item $Q$ is a finite set of {\em states}, also denoted $Q_M$.
+  \item $\Sigma$ is a finite set of {\em alphabets}, also denoted $\Sigma_M$.
+  \item $\delta$ is a {\em transition function} of type @{text "Q \<times> \<Sigma> \<Rightarrow> Q"} (a total function),
+           also denoted $\delta_M$.
+  \item @{text "s \<in> Q"} is a state called {\em initial state}, also denoted $s_M$.
+  \item @{text "F \<subseteq> Q"} is a set of states named {\em accepting states}, also denoted $F_M$.
+\end{enumerate}
+Therefore, we have $M = (Q_M, \Sigma_M, \delta_M, s_M, F_M)$. Every DFA $M$ can be interpreted as 
+a function assigning states to strings, denoted $\dfa{M}$, the  definition of which is as the following:
+\begin{equation}
+\begin{aligned}
+  \dfa{M}([]) &\equiv s_M \\
+   \dfa{M}(xa) &\equiv  \delta_M(\dfa{M}(x), a)
+\end{aligned}
+\end{equation}
+A string @{text "x"} is said to be {\em accepted} (or {\em recognized}) by a DFA $M$ if 
+$\dfa{M}(x) \in F_M$. The language recoginzed by DFA $M$, denoted
+$L(M)$, is defined as:
+\begin{equation}
+  L(M) \equiv \{x~|~\dfa{M}(x) \in F_M\}
+\end{equation}
+The standard way of specifying a laugage $\Lang$ as {\em regular} is by stipulating that:
+$\Lang = L(M)$ for some DFA $M$.
+
+For any DFA $M$, the DFA obtained by changing initial state to another $p \in Q_M$ is denoted $M_p$, 
+which is defined as:
+\begin{equation}
+    M_p \ \equiv\ (Q_M, \Sigma_M, \delta_M, p, F_M) 
+\end{equation}
+Two states $p, q \in Q_M$ are said to be {\em equivalent}, denoted $p \approx_M q$, iff.
+\begin{equation}\label{m_eq_def}
+  L(M_p) = L(M_q)
+\end{equation}
+It is obvious that $\approx_M$ is an equivalent relation over $Q_M$. and 
+the partition induced by $\approx_M$ has $|Q_M|$ equivalent classes.
+By overloading $\approx_M$,  an equivalent relation over strings can be defined:
+\begin{equation}
+  x \approx_M y ~ ~ \equiv ~ ~ \dfa{M}(x) \approx_M \dfa{M}(y)
+\end{equation}
+It can be proved that the the partition induced by $\approx_M$ also has $|Q_M|$ equivalent classes.
+It is also easy to show that: if $x \approx_M y$, then $x \approx_{L(M)} y$, and this means
+$\approx_M$ is a more refined equivalent relation than $\approx_{L(M)}$. Since partition induced by
+$\approx_M$ is finite, the one induced by $\approx_{L(M)}$ must also be finite, and this is 
+one of the two directions of \mht:
+\begin{Lem}[\mht , Direction two]
+  If a language $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$), then 
+  the partition induced by $\approx_\Lang$ is finite.
+\end{Lem}
+
+The other direction is:
+\begin{Lem}[\mht , Direction one]\label{auto_mh_d1}
+  If  the partition induced by $\approx_\Lang$ is finite, then
+  $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$).
+\end{Lem}
+The $M$ we are seeking when prove lemma \ref{auto_mh_d2} can be constructed out of $\approx_\Lang$,
+denoted $M_\Lang$ and defined as the following:
+\begin{subequations}
+\begin{eqnarray}
+  Q_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}\\
+  \Sigma_{M_\Lang} ~ & \equiv & ~ \Sigma_M \\
+  \delta_{M_\Lang} ~ & \equiv & ~ \left (\lambda (\cls{x}{\approx_\Lang}, a).  \cls{xa}{\approx_\Lang} \right) \\
+  s_{M_\Lang} ~ & \equiv & ~ \cls{[]}{\approx_\Lang} \\
+  F_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Lang \}
+\end{eqnarray}
+\end{subequations}
+It can be proved that $Q_{M_\Lang}$ is indeed finite and $\Lang = L(M_\Lang)$, so lemma \ref{auto_mh_d1} holds.
+It can also be proved that $M_\Lang$ is the minimal DFA (therefore unique) which recoginzes $\Lang$.
+
+
+
+*}
+
+subsection {* The objective and the underlying intuition *}
+
+text {*
+  It is now obvious from section \ref{sec_fa_mh} that \mht\ can be established easily when
+  {\em reglar languages} are defined as ones recognized by finite automata. 
+  Under the context where the use of finite automata is forbiden, the situation is quite different.
+  The theorem now has to be expressed as:
+  \begin{Thm}[\mht , Regular expression version]
+      A language $\Lang$ is regular (i.e. $\Lang = L(\re)$ for some {\em regular expression} $\re$)
+      iff. the partition induced by $\approx_\Lang$ is finite.
+  \end{Thm}
+  The proof of this version consists of two directions (if the use of automata are not allowed):
+  \begin{description}
+    \item [Direction one:] 
+      generating a regular expression $\re$ out of the finite partition induced by $\approx_\Lang$,
+      such that $\Lang = L(\re)$.
+    \item [Direction two:]
+          showing the finiteness of the partition induced by $\approx_\Lang$, under the assmption
+          that $\Lang$ is recognized by some regular expression $\re$ (i.e. $\Lang = L(\re)$).
+  \end{description}
+  The development of these two directions consititutes the body of this paper.
+
+*}
+
+section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
+
+text {*
+  Although not used explicitly, the notion of finite autotmata and its relationship with 
+  language partition, as outlined in section \ref{sec_fa_mh}, still servers as important intuitive 
+  guides in the development of this paper.
+  For example, {\em Direction one} follows the {\em Brzozowski algebraic method}
+  used to convert finite autotmata to regular expressions, under the intuition that every 
+  partition member $\cls{x}{\approx_\Lang}$ is a state in the DFA $M_\Lang$  constructed to prove 
+  lemma \ref{auto_mh_d1} of section \ref{sec_fa_mh}.
+
+  The basic idea of Brzozowski method is to extract an equational system out of the 
+  transition relationship of the automaton in question. In the equational system, every
+  automaton state is represented by an unknown, the solution of which is expected to be 
+  a regular expresion characterizing the state in a certain sense. There are two choices of 
+  how a automaton state can be characterized.  The first is to characterize by the set of 
+  strings leading from the state in question into accepting states. 
+  The other choice is to characterize by the set of strings leading from initial state 
+  into the state in question. For the second choice, the language recognized the automaton 
+  can be characterized by the solution of initial state, while for the second choice, 
+  the language recoginzed by the automaton can be characterized by 
+  combining solutions of all accepting states by @{text "+"}. Because of the automaton 
+  used as our intuitive guide, the $M_\Lang$, the states of which are 
+  sets of strings leading from initial state, the second choice is used in this paper.
+
+  Supposing the automaton in Fig \ref{fig_auto_part_rel} is the $M_\Lang$ for some language $\Lang$, 
+  and suppose $\Sigma = \{a, b, c, d, e\}$. Under the second choice, the equational system extracted is:
+  \begin{subequations}
+  \begin{eqnarray}
+    X_0 & = & X_1 \cdot c + X_2 \cdot d + \lambda \label{x_0_def_o} \\
+    X_1 & = & X_0 \cdot a + X_1 \cdot b + X_2 \cdot d \label{x_1_def_o} \\
+    X_2 & = & X_0 \cdot b + X_1 \cdot d + X_2 \cdot a \\
+    X_3 & = & \begin{aligned}
+                 & X_0 \cdot (c + d + e) + X_1 \cdot (a + e) + X_2 \cdot (b + e) + \\
+                 & X_3 \cdot (a + b + c + d + e)
+              \end{aligned}
+  \end{eqnarray}
+  \end{subequations} 
+
+\begin{figure}[h!]
+\centering
+\begin{minipage}{0.5\textwidth}
+\scalebox{0.8}{
+\begin{tikzpicture}[ultra thick,>=latex]
+  \node[draw,circle,initial] (start) {$X_0$};
+  \node[draw,circle,accepting] at ($(start) + (3.5cm,2cm)$) (ac1) {$X_1$};
+  \node[draw,circle,accepting] at ($(start) + (3.5cm,-2cm)$) (ac2) {$X_2$};
+  \node[draw,circle] at ($(start) + (6.5cm,0cm)$) (ab) {$X_3$};
+
+  \path[->] (start) edge [bend left] node [midway, above] {$a$} (ac1);
+  \path[->] (start) edge [bend right] node [midway, below] {$b$} (ac2);
+  \path[->] (ac1) edge [loop above] node [midway, above] {$b$} (ac1);
+  \path[->] (ac2) edge [loop below] node [midway, below] {$a$} (ac2);
+  \path[->] (ac1) edge [bend right] node [midway, left] {$c$} (ac2);
+  \path[->] (ac2) edge [bend right] node [midway, right] {$c$} (ac1);
+  \path[->] (ac1) edge node [midway, sloped, above] {$d$} (start);
+  \path[->] (ac2) edge node [midway, sloped, above] {$d$} (start);
+
+  \path [draw, rounded corners,->,dashed] (start) -- ($(start) + (0cm, 3.7cm)$)
+         -- ($(ab) + (0cm, 3.7cm)$)  node[midway,above,sloped]{$\Sigma - \{a, b\}$} -- (ab);
+  \path[->,dashed] (ac1) edge node [midway, above, sloped] {$\Sigma - \{b,c,d\}$} (ab);
+  \path[->,dashed] (ac2) edge node [midway, below, sloped] {$\Sigma - \{a,c,d\}$} (ab);
+  \path[->,dashed] (ab) edge [loop right] node [midway, right] {$\Sigma$} (ab);
+\end{tikzpicture}}
+\end{minipage}
+\caption{An example automaton}\label{fig_auto_part_rel}
+\end{figure}
+
+  Every $\cdot$-item on the right side of equations describes some state transtions, except 
+  the $\lambda$ in \eqref{x_0_def_o}, which represents empty string @{text "[]"}. 
+  The reason is that: every state is characterized by the
+  set of incoming strings leading from initial state. For non-initial state, every such
+  string can be splitted into a prefix leading into a preceding state and a single character suffix 
+  transiting into from the preceding state. The exception happens at
+  initial state, where the empty string is a incoming string which can not be splitted. The $\lambda$
+  in \eqref{x_0_def_o} is introduce to repsent this indivisible string. There is one and only one
+  $\lambda$ in every equational system such obtained, becasue $[]$ can only be contaied in one
+  equivalent class (the intial state in $M_\Lang$) and equivalent classes are disjoint. 
+  
+  Suppose all unknowns ($X_0, X_1, X_2, X_3$) are  solvable, the regular expression charactering 
+  laugnage $\Lang$ is $X_1 + X_2$. This paper gives a procedure
+  by which arbitrarily picked unknown can be solved. The basic idea to solve $X_i$ is by 
+  eliminating all variables other than $X_i$ from the equational system. If
+  $X_0$ is the one picked to be solved,  variables $X_1, X_2, X_3$ have to be removed one by 
+  one.  The order to remove does not matter as long as the remaing equations are kept valid.
+  Suppose $X_1$ is the first one to remove, the action is to replace all occurences of $X_1$ 
+  in remaining equations by the right hand side of its characterizing equation, i.e. 
+  the $ X_0 \cdot a + X_1 \cdot b + X_2 \cdot d$ in \eqref{x_1_def_o}. However, because
+  of the recursive occurence of $X_1$, this replacement does not really removed $X_1$. Arden's
+  lemma is invoked to transform recursive equations like \eqref{x_1_def_o} into non-recursive 
+  ones. For example, the recursive equation \eqref{x_1_def_o} is transformed into the follwing
+  non-recursive one:
+  \begin{equation}
+     X_1  =  (X_0 \cdot a + X_2 \cdot d) \cdot b^* = X_0 \cdot (a \cdot b^*) + X_2 \cdot (d \cdot b^*)
+  \end{equation}
+  which, by Arden's lemma, still characterizes $X_1$ correctly. By subsituting
+  $(X_0 \cdot a + X_2 \cdot d) \cdot b^*$ for all $X_1$ and removing  \eqref{x_1_def_o},
+  we get:
+  \begin{subequations}
+  \begin{eqnarray}
+    X_0 & = & \begin{aligned}
+              & (X_0 \cdot (a \cdot b^*) + X_2 \cdot (d \cdot b^*)) \cdot c + 
+                X_2 \cdot d + \lambda = \\
+              & X_0 \cdot (a \cdot b^* \cdot c) + X_2 \cdot (d \cdot b^* \cdot c) + 
+                X_2 \cdot d + \lambda = \\
+              &  X_0 \cdot (a \cdot b^* \cdot c) + X_2 \cdot (d \cdot b^* \cdot c + d) + \lambda 
+              \end{aligned} \label{x_0_def_1} \\
+    X_2 & = & \begin{aligned}
+                 & X_0 \cdot b + (X_0 \cdot (a \cdot b^*) + X_2 \cdot (d \cdot b^*)) \cdot d + X_2 \cdot a = \\
+                 & X_0 \cdot b + X_0 \cdot (a \cdot b^* \cdot d) + X_2 \cdot (d \cdot b^* \cdot d) + X_2 \cdot a = \\
+                 & X_0 \cdot (b + a \cdot b^* \cdot d) + X_2 \cdot (d \cdot b^* \cdot d + a)
+              \end{aligned} \\
+    X_3 & = & \begin{aligned}
+                 & X_0 \cdot (c + d + e) + ((X_0 \cdot a + X_2 \cdot d) \cdot b^*) \cdot (a + e)\\
+                 & + X_2 \cdot (b + e) + X_3 \cdot (a + b + c + d + e) \label{x_3_def_1}
+              \end{aligned}
+  \end{eqnarray}
+  \end{subequations}  
+Suppose $X_3$ is the one to remove next, since $X_3$ dose not appear in either $X_0$ or $X_2$, 
+the removal of equation \eqref{x_3_def_1} changes nothing in the rest equations. Therefore, we get:
+ \begin{subequations}
+  \begin{eqnarray}
+    X_0 & = & X_0 \cdot (a \cdot b^* \cdot c) + X_2 \cdot (d \cdot b^* \cdot c + d) + \lambda  \label{x_0_def_2} \\
+    X_2 & = & X_0 \cdot (b + a \cdot b^* \cdot d) + X_2 \cdot (d \cdot b^* \cdot d + a) \label{x_2_def_2}
+  \end{eqnarray}
+  \end{subequations}  
+Actually, since absorbing state like $X_3$ contributes nothing to the language $\Lang$, it could have been removed
+at the very beginning of this precedure without affecting the final result. Now, the last unknown to remove 
+is $X_2$ and the Arden's transformaton of \eqref{x_2_def_2} is:
+\begin{equation} \label{x_2_ardened}
+   X_2 ~ = ~  (X_0 \cdot (b + a \cdot b^* \cdot d)) \cdot (d \cdot b^* \cdot d + a)^* =
+              X_0 \cdot ((b + a \cdot b^* \cdot d) \cdot (d \cdot b^* \cdot d + a)^*)
+\end{equation}
+By substituting the right hand side of \eqref{x_2_ardened} into \eqref{x_0_def_2}, we get:
+\begin{equation}
+\begin{aligned}
+  X_0  & = && X_0 \cdot (a \cdot b^* \cdot c) + \\
+       &   && X_0 \cdot ((b + a \cdot b^* \cdot d) \cdot (d \cdot b^* \cdot d + a)^*) \cdot 
+           (d \cdot b^* \cdot c + d) + \lambda \\
+       & =  && X_0 \cdot ((a \cdot b^* \cdot c) + \\
+       &   && \hspace{3em} ((b + a \cdot b^* \cdot d) \cdot (d \cdot b^* \cdot d + a)^*) \cdot 
+           (d \cdot b^* \cdot c + d)) + \lambda 
+\end{aligned}
+\end{equation}
+By applying Arden's transformation to this, we get the solution of $X_0$ as:
+\begin{equation}
+\begin{aligned}
+  X_0  =  ((a \cdot b^* \cdot c) + 
+                ((b + a \cdot b^* \cdot d) \cdot (d \cdot b^* \cdot d + a)^*) \cdot 
+                        (d \cdot b^* \cdot c + d))^*
+\end{aligned}
+\end{equation}
+Using the same method, solutions for $X_1$ and $X_2$ can be obtained as well and the
+regular expressoin for $\Lang$ is just $X_1 + X_2$. The formalization of this procedure
+consititues the first direction of the {\em regular expression} verion of
+\mht. Detailed explaination are given in {\bf paper.pdf} and more details and comments
+can be found in the formal scripts.
+*}
+
+section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
+
+text {*
+  It is well known in the theory of regular languages that
+  the existence of finite  language partition amounts to the existence of 
+  a minimal automaton, i.e. the $M_\Lang$ constructed in section \ref{sec_prelim}, which recoginzes the 
+  same language $\Lang$. The standard way to prove the existence of finite language partition 
+  is to construct a automaton out of the regular expression which recoginzes the same language, from
+  which the existence of finite language partition follows immediately. As discussed in the introducton of 
+  {\bf paper.pdf} as well as in [5], the problem for this approach happens when automata 
+  of sub regular expressions are combined to form the automaton of the mother regular expression, 
+  no matter what kind of representation is used, the formalization is cubersome, as said 
+  by Nipkow in [5]: `{\em a more abstract mathod is clearly desirable}'. In this section, 
+  an {\em intrinsically abstract} method is given, which completely avoid the mentioning of automata,
+  let along any particular representations.
+  *}
+
+text {*
+  The main proof structure is a structural induction on regular expressions,
+  where base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
+  proof. Real difficulty lies in inductive cases.  By inductive hypothesis, languages defined by
+  sub-expressions induce finite partitiions. Under such hypothsis, we need to prove that the language 
+  defined by the composite regular expression gives rise to finite partion.  
+  The basic idea is to attach a tag @{text "tag(x)"} to every string 
+  @{text "x"}. The tagging fuction @{text "tag"} is carefully devised, which returns tags 
+  made of equivalent classes of the partitions induced by subexpressoins, and therefore has a finite
+  range. Let @{text "Lang"} be the composite language, it is proved that:
+  \begin{quote}
+  If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
+  \[
+  @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
+  \]
+  then the partition induced by @{text "Lang"} must be finite.
+  \end{quote}
+  There are two arguments for this. The first goes as the following:
+  \begin{enumerate}
+    \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} 
+          (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).
+    \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, 
+           the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).
+           Since tags are made from equivalent classes from component partitions, and the inductive
+           hypothesis ensures the finiteness of these partitions, it is not difficult to prove
+           the finiteness of @{text "range(tag)"}.
+    \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"}
+           (expressed as @{text "R1 \<subseteq> R2"}),
+           and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"}
+           is finite as well (lemma @{text "refined_partition_finite"}).
+    \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that
+            @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}.
+    \item Combining the points above, we have: the partition induced by language @{text "Lang"}
+          is finite (lemma @{text "tag_finite_imageD"}).
+  \end{enumerate}
+
+We could have followed another approach given in  appendix II of Brzozowski's paper [?], where
+the set of derivatives of any regular expression can be proved to be finite. 
+Since it is easy to show that strings with same derivative are equivalent with respect to the 
+language, then the second direction follows. We believe that our
+apporoach is easy to formalize, with no need to do complicated derivation calculations
+and countings as in [???].
+*}
+
+
+end




