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 set aside an unknown for every DFA state and 
  describe the state-trasition relationship by charateristic equations. 
  By solving the equational system such obtained, regular expressions 
  characterizing DFA states are obtained. There are choices of 
  how DFA states can be characterized.  The first is to characterize a DFA state by the set of 
  striings leading from the state in question into accepting states. 
  The other choice is to characterize a DFA state by the set of strings leading from initial state 
  into the state in question. For the first choice, the lauguage recognized by a DFA can 
  be characterized by the regular expression characterizing initial state, while 
  in the second choice, the languaged of the DFA can be characterized by the summation of
  regular expressions of all accepting states.
*}

text {*
\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{The relationship between automata and finite partition}\label{fig_auto_part_rel}
\end{figure}

  *}


end