--- a/Myhill.thy Thu Feb 03 12:44:46 2011 +0000
+++ b/Myhill.thy Fri Feb 04 13:02:00 2011 +0000
@@ -5,7 +5,88 @@
section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
text {*
- It is now the time for use to discuss further about the way.
+
+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