theory Myhill

  imports Myhill_2

begin

section {* Preliminaries *}

subsection {* Finite automata and \mht  \label{sec_fa_mh} *}

text {*

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

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

\begin{enumerate}

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

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

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

           also denoted $\delta_M$.

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

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

\end{enumerate}

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

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

\begin{equation}

\begin{aligned}

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

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

\end{aligned}

\end{equation}

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

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

$L(M)$, is defined as:

\begin{equation}

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

\end{equation}

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

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

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

which is defined as:

\begin{equation}

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

\end{equation}

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

\begin{equation}\label{m_eq_def}

  L(M_p) = L(M_q)

\end{equation}

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

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

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

\begin{equation}

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

\end{equation}

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

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

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

$\approx_M$ is finite, the one induced by $\approx_{L(M)}$ must also be finite, and this is 

one of the two directions of \mht:

\begin{Lem}[\mht , Direction two]

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

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

\end{Lem}

The other direction is:

\begin{Lem}[\mht , Direction one]\label{auto_mh_d1}

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

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

\end{Lem}

The $M$ we are seeking when prove lemma \ref{auto_mh_d2} can be constructed out of $\approx_\Lang$,

denoted $M_\Lang$ and defined as the following:

\begin{subequations}

\begin{eqnarray}

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

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

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

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

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

\end{eqnarray}

\end{subequations}

It can be proved that $Q_{M_\Lang}$ is indeed finite and $\Lang = L(M_\Lang)$, so lemma \ref{auto_mh_d1} holds.

It can also be proved that $M_\Lang$ is the minimal DFA (therefore unique) which recoginzes $\Lang$.

*}

subsection {* The objective and the underlying intuition *}

text {*

  It is now obvious from section \ref{sec_fa_mh} that \mht\ can be established easily when

  {\em reglar languages} are defined as ones recognized by finite automata. 

  Under the context where the use of finite automata is forbiden, the situation is quite different.

  The theorem now has to be expressed as:

  \begin{Thm}[\mht , Regular expression version]

      A language $\Lang$ is regular (i.e. $\Lang = L(\re)$ for some {\em regular expression} $\re$)

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

  \end{Thm}

  The proof of this version consists of two directions (if the use of automata are not allowed):

  \begin{description}

    \item [Direction one:] 

      generating a regular expression $\re$ out of the finite partition induced by $\approx_\Lang$,

      such that $\Lang = L(\re)$.

    \item [Direction two:]

          showing the finiteness of the partition induced by $\approx_\Lang$, under the assmption

          that $\Lang$ is recognized by some regular expression $\re$ (i.e. $\Lang = L(\re)$).

  \end{description}

  The development of these two directions consititutes the body of this paper.

*}

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

text {*

  Although not used explicitly, the notion of finite autotmata and its relationship with 

  language partition, as outlined in section \ref{sec_fa_mh}, still servers as important intuitive 

  guides in the development of this paper.

  For example, {\em Direction one} follows the {\em Brzozowski algebraic method}

  used to convert finite autotmata to regular expressions, under the intuition that every 

  partition member $\cls{x}{\approx_\Lang}$ is a state in the DFA $M_\Lang$  constructed to prove 

  lemma \ref{auto_mh_d1} of section \ref{sec_fa_mh}.

  The basic idea of Brzozowski method is to extract an equational system out of the 

  transition relationship of the automaton in question. In the equational system, every

  automaton state is represented by an unknown, the solution of which is expected to be 

  a regular expresion characterizing the state in a certain sense. There are two choices of 

  how a automaton state can be characterized.  The first is to characterize by the set of 

  strings leading from the state in question into accepting states. 

  The other choice is to characterize by the set of strings leading from initial state 

  into the state in question. For the second choice, the language recognized the automaton 

  can be characterized by the solution of initial state, while for the second choice, 

  the language recoginzed by the automaton can be characterized by 

  combining solutions of all accepting states by @{text "+"}. Because of the automaton 

  used as our intuitive guide, the $M_\Lang$, the states of which are 

  sets of strings leading from initial state, the second choice is used in this paper.

  Supposing the automaton in Fig \ref{fig_auto_part_rel} is the $M_\Lang$ for some language $\Lang$, 

  and suppose $\Sigma = \{a, b, c, d, e\}$. Under the second choice, the equational system extracted is:

  \begin{subequations}

  \begin{eqnarray}

    X_0 & = & X_1 \cdot c + X_2 \cdot d + \lambda \label{x_0_def_o} \\

    X_1 & = & X_0 \cdot a + X_1 \cdot b + X_2 \cdot d \label{x_1_def_o} \\

    X_2 & = & X_0 \cdot b + X_1 \cdot d + X_2 \cdot a \\

    X_3 & = & \begin{aligned}

                 & X_0 \cdot (c + d + e) + X_1 \cdot (a + e) + X_2 \cdot (b + e) + \\

                 & X_3 \cdot (a + b + c + d + e)

              \end{aligned}

  \end{eqnarray}

  \end{subequations} 

\begin{figure}[h!]

\centering

\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{An example automaton}\label{fig_auto_part_rel}

\end{figure}

  Every $\cdot$-item on the right side of equations describes some state transtions, except 

  the $\lambda$ in \eqref{x_0_def_o}, which represents empty string @{text "[]"}. 

  The reason is that: every state is characterized by the

  set of incoming strings leading from initial state. For non-initial state, every such

  string can be splitted into a prefix leading into a preceding state and a single character suffix 

  transiting into from the preceding state. The exception happens at

  initial state, where the empty string is a incoming string which can not be splitted. The $\lambda$

  in \eqref{x_0_def_o} is introduce to repsent this indivisible string. There is one and only one

  $\lambda$ in every equational system such obtained, becasue $[]$ can only be contaied in one

  equivalent class (the intial state in $M_\Lang$) and equivalent classes are disjoint. 

  Suppose all unknowns ($X_0, X_1, X_2, X_3$) are  solvable, the regular expression charactering 

  laugnage $\Lang$ is $X_1 + X_2$. This paper gives a procedure

  by which arbitrarily picked unknown can be solved. The basic idea to solve $X_i$ is by 

  eliminating all variables other than $X_i$ from the equational system. If

  $X_0$ is the one picked to be solved,  variables $X_1, X_2, X_3$ have to be removed one by 

  one.  The order to remove does not matter as long as the remaing equations are kept valid.

  Suppose $X_1$ is the first one to remove, the action is to replace all occurences of $X_1$ 

  in remaining equations by the right hand side of its characterizing equation, i.e. 

  the $ X_0 \cdot a + X_1 \cdot b + X_2 \cdot d$ in \eqref{x_1_def_o}. However, because

  of the recursive occurence of $X_1$, this replacement does not really removed $X_1$. Arden's

  lemma is invoked to transform recursive equations like \eqref{x_1_def_o} into non-recursive 

  ones. For example, the recursive equation \eqref{x_1_def_o} is transformed into the follwing

  non-recursive one:

  \begin{equation}

     X_1  =  (X_0 \cdot a + X_2 \cdot d) \cdot b^*

  \end{equation}

  which, by Arden's lemma, still characterizes $X_1$ correctly. By subsitute 

  $(X_0 \cdot a + X_2 \cdot d) \cdot b^*$ for all $X_1$ and remove  \eqref{x_1_def_o},

  we get:

  \begin{subequations}

  \begin{eqnarray}

    X_0 & = & ((X_0 \cdot a + X_2 \cdot d) \cdot b^*) \cdot c + X_2 \cdot d + \lambda \label{x_0_def_1} \\

    X_2 & = & X_0 \cdot b + ((X_0 \cdot a + X_2 \cdot d) \cdot b^*) \cdot d + X_2 \cdot a \\

    X_3 & = & \begin{aligned}

                 & X_0 \cdot (c + d + e) + ((X_0 \cdot a + X_2 \cdot d) \cdot b^*) \cdot (a + e)\\

                 & + X_2 \cdot (b + e) + X_3 \cdot (a + b + c + d + e)

              \end{aligned}

  \end{eqnarray}

  \end{subequations}  

*}

end