theory Myhill
  imports Myhill_2
begin

section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}

text {*

The intuition behind our treatment is still automata. Taking the automaton in 
Fig.\ref{fig_origin_auto} as an example, like any automaton, it
represents the vehicle used to recognize a certain regular language.
For any given string, the process starts from the left most and proceed 
character by character to the right, driving the state transtion of automaton 
starting from the initial state (the one marked by an short arrow). There could
be three outcomes:
  \begin{enumerate}
   \item The process finally reaches the end of the string and the automaton is at an accepting
        state, in which case the string is considered a member of the language.
         For the automaton in Fig.\ref{fig_origin_auto}, @{text "a, ab, abb, abc, abbcc, b, baa"}
         are such kind of strings.
   \item The process finally reaches the end of the string but the automaton is at an non-accepting
         state, in which case, the string is considered a non-member of the language. For the automaton 
         in Fig.\ref{fig_origin_auto}, @{text "ad, abbd, adbd, bdabbccd"}
         are such kind of strings. \label{case_end_reject}
   \item \label{case_stuck}
     The process get stuck at the middle of the string, in which case, the string is considered
           a non-member of the lauguage.  For the automaton in Fig.\ref{fig_origin_auto}, 
           @{text "c, acb, bbacd, aaccd"} 
           are such kind of strings.
  \end{enumerate}
To avoid the situation \ref{case_stuck} above, we can augment a normal automaton with a ``absorbing state'',
as the state $X_3$ in Fig.\ref{fig_extended_auto}. In an auguments automaton, the process of strings never
get stuck: whenever a string is recognized as not belonging to the language, the augmented automaton
is transfered into the ``absorbing state'' and kept there until the process reaches the end of the string, 
in which case, the string is rejected by situation \ref{case_end_reject} above.

Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}
corresponds to the state reached by processing @{text "x"} with the augmented automaton. 

\begin{figure}[h!]
\centering
\subfigure[Original automaton]{\label{fig_origin_auto}
\begin{minipage}{0.4\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$};

  \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);
\end{tikzpicture}}
\end{minipage}
}
\subfigure[Extended automaton]{\label{fig_extended_auto}
\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