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+ −