9 The intuition behind our treatment is still automata. Taking the automaton in 

     9 A {\em determinisitc finite automata (DFA)} $M$ is a 5-tuple 

    10 Fig.\ref{fig_origin_auto} as an example, like any automaton, it

    10 $(Q, \Sigma, \delta, s, F)$, where:

    11 represents the vehicle used to recognize a certain regular language.

    11 \begin{enumerate}

    12 For any given string, the process starts from the left most and proceed 

    12   \item $Q$ is a finite set of {\em states}, also denoted $Q_M$.

    13 character by character to the right, driving the state transtion of automaton 

    13   \item $\Sigma$ is a finite set of {\em alphabets}, also denoted $\Sigma_M$.

    14 starting from the initial state (the one marked by an short arrow). There could

    14   \item $\delta$ is a {\em transition function} of type @{text "Q \<times> \<Sigma> \<Rightarrow> Q"} (a total function),

    15 be three outcomes:

    15            also denoted $\delta_M$.

    16   \begin{enumerate}

    16   \item @{text "s \<in> Q"} is a state called {\em initial state}, also denoted $s_M$.

    17    \item The process finally reaches the end of the string and the automaton is at an accepting

    17   \item @{text "F \<subseteq> Q"} is a set of states named {\em accepting states}, also denoted $F_M$.

    18         state, in which case the string is considered a member of the language.

    18 \end{enumerate}

    19          For the automaton in Fig.\ref{fig_origin_auto}, @{text "a, ab, abb, abc, abbcc, b, baa"}

    19 Therefore, we have $M = (Q_M, \Sigma_M, \delta_M, s_M, F_M)$. Every DFA $M$ can be interpreted as 

    20          are such kind of strings.

    20 a function assigning states to strings, denoted $\dfa{M}$, the  definition of which is as the following:

    21    \item The process finally reaches the end of the string but the automaton is at an non-accepting

    21 \begin{equation}

    22          state, in which case, the string is considered a non-member of the language. For the automaton 

    22 \begin{aligned}

    23          in Fig.\ref{fig_origin_auto}, @{text "ad, abbd, adbd, bdabbccd"}

    23   \dfa{M}([]) &\equiv s_M \\

    24          are such kind of strings. \label{case_end_reject}

    24    \dfa{M}(xa) &\equiv  \delta_M(\dfa{M}(x), a)

    25    \item \label{case_stuck}

    25 \end{aligned}

    26      The process get stuck at the middle of the string, in which case, the string is considered

    26 \end{equation}

    27            a non-member of the lauguage.  For the automaton in Fig.\ref{fig_origin_auto}, 

    27 A string @{text "x"} is said to be {\em accepted} (or {\em recognized}) by a DFA $M$ if 

    28            @{text "c, acb, bbacd, aaccd"} 

    28 $\dfa{M}(x) \in F_M$. The language recoginzed by DFA $M$, denoted

    29            are such kind of strings.

    29 $L(M)$, is defined as:

    30   \end{enumerate}

    30 \begin{equation}

    31 To avoid the situation \ref{case_stuck} above, we can augment a normal automaton with a ``absorbing state'',

    31   L(M) \equiv \{x~|~\dfa{M}(x) \in F_M\}

    32 as the state $X_3$ in Fig.\ref{fig_extended_auto}. In an auguments automaton, the process of strings never

    32 \end{equation}

    33 get stuck: whenever a string is recognized as not belonging to the language, the augmented automaton

    33 The standard way of specifying a laugage $\Lang$ as {\em regular} is by stipulating that:

    34 is transfered into the ``absorbing state'' and kept there until the process reaches the end of the string, 

    34 $\Lang = L(M)$ for some DFA $M$.

    35 in which case, the string is rejected by situation \ref{case_end_reject} above.

    37 Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}

    36 For any DFA $M$, the DFA obtained by changing initial state to another $p \in Q_M$ is denoted $M_p$, 

    38 corresponds to the state reached by processing @{text "x"} with the augmented automaton. Since  

    37 which is defined as:

    39 @{text "\<approx>Lang `` {x}"} is defined for every @{text "x"}, it corresponds to the fact that 

    38 \begin{equation}

    40 the processing of @{text "x"} will never get stuck.

    39     M_p \ \equiv\ (Q_M, \Sigma_M, \delta_M, p, F_M) 

    40 \end{equation}

    41 Two states $p, q \in Q_M$ are said to be {\em equivalent}, denoted $p \approx_M q$, iff.

    42 \begin{equation}\label{m_eq_def}

    43   L(M_p) = L(M_q)

    44 \end{equation}

    45 It is obvious that $\approx_M$ is an equivalent relation over $Q_M$. and 

    46 the partition induced by $\approx_M$ has $|Q_M|$ equivalent classes.

    47 By overloading $\approx_M$,  an equivalent relation over strings can be defined:

    48 \begin{equation}

    49   x \approx_M y ~ ~ \equiv ~ ~ \dfa{M}(x) \approx_M \dfa{M}(y)

    50 \end{equation}

    51 It can be proved that the the partition induced by $\approx_M$ also has $|Q_M|$ equivalent classes.

    52 It is also easy to show that: if $x \approx_M y$, then $x \approx_{L(M)} y$, and this means

    53 $\approx_M$ is a more refined equivalent relation than $\approx_{L(M)}$. Since partition induced by

    54 $\approx_M$ is finite, the one induced by $\approx_{L(M)}$ must also be finite. Now, we get one direction

    55 of \mht:

    56 \begin{Lem}[\mht , Direction one]

    57   If a language $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$), then 

    58   the partition induced by $\approx_\Lang$ is finite.

    59 \end{Lem}

    42 The most acquainted way to define a regular language @{text "Lang"} is by giving an automaton which

    61 The other direction is:

    43 recorgizes every string in @{text "Lang"}. Fig.\ref{fig_origin_auto} gives such a automaton, which 

    62 \begin{Lem}[\mht , Direction two]\label{auto_mh_d2}

    44 can be viewed as a way of assigning status to strings: for any given string @{text "x"}:

    63   If  the partition induced by $\approx_\Lang$ is finite, then

    64   $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$).

    65 \end{Lem}

    66 To prove this lemma, a DFA $M_\Lang$ is constructed out of $\approx_\Lang$ with:

    67 \begin{subequations}

    68 \begin{eqnarray}

    69   Q_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}\\

    70   \Sigma_{M_\Lang} ~ & \equiv & ~ \Sigma_M \\

    71   \delta_{M_\Lang} ~ & \equiv & ~ \left (\lambda (\cls{x}{\approx_\Lang}, a).  \cls{xa}{\approx_\Lang} \right) \\

    72   s_{M_\Lang} ~ & \equiv & ~ \cls{[]}{\approx_\Lang} \\

    73   F_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Lang \}

    74 \end{eqnarray}

    75 \end{subequations}

    76 From the assumption of lemma \ref{auto_mh_d2}, we have that $\{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}$

    77 is finite

    78 It can be proved that $\Lang = L(M_\Lang)$.