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}"}

\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