theory Myhill
  imports Myhill_2
begin

section {* Preliminaries *}

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^*
  \end{equation}
  which, by Arden's lemma, still characterizes $X_1$ correctly. By subsitute 
  $(X_0 \cdot a + X_2 \cdot d) \cdot b^*$ for all $X_1$ and remove  \eqref{x_1_def_o},
  we get:

  \begin{subequations}
  \begin{eqnarray}
    X_0 & = & ((X_0 \cdot a + X_2 \cdot d) \cdot b^*) \cdot c + X_2 \cdot d + \lambda \label{x_0_def_1} \\
    X_2 & = & X_0 \cdot b + ((X_0 \cdot a + X_2 \cdot d) \cdot b^*) \cdot d + X_2 \cdot a \\
    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)
              \end{aligned}
  \end{eqnarray}
  \end{subequations}  
 
*}

end