Myhill.thy
changeset 73 79de7de104c8
parent 69 ecf6c61a4541
child 78 77583805123d
equal deleted inserted replaced
72:e5116c2e6187 73:79de7de104c8
     1 theory Myhill
     1 theory Myhill
     2   imports Myhill_2
     2   imports Myhill_2
     3 begin
     3 begin
     4 
     4 
     5 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
     5 section {* Preliminaries *}
       
     6 
       
     7 subsection {* Finite automata and \mht  \label{sec_fa_mh} *}
     6 
     8 
     7 text {*
     9 text {*
     8 
    10 
     9 A {\em determinisitc finite automata (DFA)} $M$ is a 5-tuple 
    11 A {\em determinisitc finite automata (DFA)} $M$ is a 5-tuple 
    10 $(Q, \Sigma, \delta, s, F)$, where:
    12 $(Q, \Sigma, \delta, s, F)$, where:
    49   x \approx_M y ~ ~ \equiv ~ ~ \dfa{M}(x) \approx_M \dfa{M}(y)
    51   x \approx_M y ~ ~ \equiv ~ ~ \dfa{M}(x) \approx_M \dfa{M}(y)
    50 \end{equation}
    52 \end{equation}
    51 It can be proved that the the partition induced by $\approx_M$ also has $|Q_M|$ equivalent classes.
    53 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
    54 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
    55 $\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
    56 $\approx_M$ is finite, the one induced by $\approx_{L(M)}$ must also be finite, and this is 
    55 of \mht:
    57 one of the two directions of \mht:
    56 \begin{Lem}[\mht , Direction one]
    58 \begin{Lem}[\mht , Direction two]
    57   If a language $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$), then 
    59   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.
    60   the partition induced by $\approx_\Lang$ is finite.
    59 \end{Lem}
    61 \end{Lem}
    60 
    62 
    61 The other direction is:
    63 The other direction is:
    62 \begin{Lem}[\mht , Direction two]\label{auto_mh_d2}
    64 \begin{Lem}[\mht , Direction one]\label{auto_mh_d1}
    63   If  the partition induced by $\approx_\Lang$ is finite, then
    65   If  the partition induced by $\approx_\Lang$ is finite, then
    64   $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$).
    66   $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$).
    65 \end{Lem}
    67 \end{Lem}
    66 To prove this lemma, a DFA $M_\Lang$ is constructed out of $\approx_\Lang$ with:
    68 The $M$ we are seeking when prove lemma \ref{auto_mh_d2} can be constructed out of $\approx_\Lang$,
       
    69 denoted $M_\Lang$ and defined as the following:
    67 \begin{subequations}
    70 \begin{subequations}
    68 \begin{eqnarray}
    71 \begin{eqnarray}
    69   Q_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}\\
    72   Q_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}\\
    70   \Sigma_{M_\Lang} ~ & \equiv & ~ \Sigma_M \\
    73   \Sigma_{M_\Lang} ~ & \equiv & ~ \Sigma_M \\
    71   \delta_{M_\Lang} ~ & \equiv & ~ \left (\lambda (\cls{x}{\approx_\Lang}, a).  \cls{xa}{\approx_\Lang} \right) \\
    74   \delta_{M_\Lang} ~ & \equiv & ~ \left (\lambda (\cls{x}{\approx_\Lang}, a).  \cls{xa}{\approx_\Lang} \right) \\
    72   s_{M_\Lang} ~ & \equiv & ~ \cls{[]}{\approx_\Lang} \\
    75   s_{M_\Lang} ~ & \equiv & ~ \cls{[]}{\approx_\Lang} \\
    73   F_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Lang \}
    76   F_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Lang \}
    74 \end{eqnarray}
    77 \end{eqnarray}
    75 \end{subequations}
    78 \end{subequations}
    76 From the assumption of lemma \ref{auto_mh_d2}, we have that $\{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}$
    79 It can be proved that $Q_{M_\Lang}$ is indeed finite and $\Lang = L(M_\Lang)$, so lemma \ref{auto_mh_d1} holds.
    77 is finite
    80 It can also be proved that $M_\Lang$ is the minimal DFA (therefore unique) which recoginzes $\Lang$.
    78 It can be proved that $\Lang = L(M_\Lang)$.
    81 
       
    82 
    79 
    83 
    80 *}
    84 *}
    81 
    85 
       
    86 subsection {* The objective and the underlying intuition *}
       
    87 
    82 text {*
    88 text {*
       
    89   It is now obvious from section \ref{sec_fa_mh} that \mht\ can be established easily when
       
    90   {\em reglar languages} are defined as ones recognized by finite automata. 
       
    91   Under the context where the use of finite automata is forbiden, the situation is quite different.
       
    92   The theorem now has to be expressed as:
       
    93   \begin{Thm}[\mht , Regular expression version]
       
    94       A language $\Lang$ is regular (i.e. $\Lang = L(\re)$ for some {\em regular expression} $\re$)
       
    95       iff. the partition induced by $\approx_\Lang$ is finite.
       
    96   \end{Thm}
       
    97   The proof of this version consists of two directions (if the use of automata are not allowed):
       
    98   \begin{description}
       
    99     \item [Direction one:] 
       
   100       generating a regular expression $\re$ out of the finite partition induced by $\approx_\Lang$,
       
   101       such that $\Lang = L(\re)$.
       
   102     \item [Direction two:]
       
   103           showing the finiteness of the partition induced by $\approx_\Lang$, under the assmption
       
   104           that $\Lang$ is recognized by some regular expression $\re$ (i.e. $\Lang = L(\re)$).
       
   105   \end{description}
       
   106   The development of these two directions consititutes the body of this paper.
    83 
   107 
       
   108 *}
       
   109 
       
   110 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
       
   111 
       
   112 text {*
       
   113   Although not used explicitly, the notion of finite autotmata and its relationship with 
       
   114   language partition, as outlined in section \ref{sec_fa_mh}, still servers as important intuitive 
       
   115   guides in the development of this paper.
       
   116   For example, {\em Direction one} follows the {\em Brzozowski algebraic method}
       
   117   used to convert finite autotmata to regular expressions, under the intuition that every 
       
   118   partition member $\cls{x}{\approx_\Lang}$ is a state in the DFA $M_\Lang$  constructed to prove 
       
   119   lemma \ref{auto_mh_d1} of section \ref{sec_fa_mh}.
       
   120 
       
   121   The basic idea of Brzozowski method is to set aside an unknown for every DFA state and 
       
   122   describe the state-trasition relationship by charateristic equations. 
       
   123   By solving the equational system such obtained, regular expressions 
       
   124   characterizing DFA states are obtained. There are choices of 
       
   125   how DFA states can be characterized.  The first is to characterize a DFA state by the set of 
       
   126   striings leading from the state in question into accepting states. 
       
   127   The other choice is to characterize a DFA state by the set of strings leading from initial state 
       
   128   into the state in question. For the first choice, the lauguage recognized by a DFA can 
       
   129   be characterized by the regular expression characterizing initial state, while 
       
   130   in the second choice, the languaged of the DFA can be characterized by the summation of
       
   131   regular expressions of all accepting states.
       
   132 *}
       
   133 
       
   134 text {*
    84 \begin{figure}[h!]
   135 \begin{figure}[h!]
    85 \centering
   136 \centering
    86 \begin{minipage}{0.5\textwidth}
   137 \begin{minipage}{0.5\textwidth}
    87 \scalebox{0.8}{
   138 \scalebox{0.8}{
    88 \begin{tikzpicture}[ultra thick,>=latex]
   139 \begin{tikzpicture}[ultra thick,>=latex]
   110 \caption{The relationship between automata and finite partition}\label{fig_auto_part_rel}
   161 \caption{The relationship between automata and finite partition}\label{fig_auto_part_rel}
   111 \end{figure}
   162 \end{figure}
   112 
   163 
   113   *}
   164   *}
   114 
   165 
       
   166 
   115 end
   167 end