# HG changeset patch # User zhang # Date 1297084089 0 # Node ID 79de7de104c84f5d5d96b5d6a2f595278dcda9b5 # Parent e5116c2e61875d05b489fa358ccb3610b567648f More into first direction diff -r e5116c2e6187 -r 79de7de104c8 Myhill.thy --- a/Myhill.thy Mon Feb 07 11:12:36 2011 +0000 +++ b/Myhill.thy Mon Feb 07 13:08:09 2011 +0000 @@ -2,7 +2,9 @@ imports Myhill_2 begin -section {* Direction @{text "regular language \finite partition"} *} +section {* Preliminaries *} + +subsection {* Finite automata and \mht \label{sec_fa_mh} *} text {* @@ -51,19 +53,20 @@ 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. Now, we get one direction -of \mht: -\begin{Lem}[\mht , Direction one] +$\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 two]\label{auto_mh_d2} +\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} -To prove this lemma, a DFA $M_\Lang$ is constructed out of $\approx_\Lang$ with: +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^* \}\\ @@ -73,14 +76,62 @@ F_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Lang \} \end{eqnarray} \end{subequations} -From the assumption of lemma \ref{auto_mh_d2}, we have that $\{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}$ -is finite -It can be proved that $\Lang = L(M_\Lang)$. +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 \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 set aside an unknown for every DFA state and + describe the state-trasition relationship by charateristic equations. + By solving the equational system such obtained, regular expressions + characterizing DFA states are obtained. There are choices of + how DFA states can be characterized. The first is to characterize a DFA state by the set of + striings leading from the state in question into accepting states. + The other choice is to characterize a DFA state by the set of strings leading from initial state + into the state in question. For the first choice, the lauguage recognized by a DFA can + be characterized by the regular expression characterizing initial state, while + in the second choice, the languaged of the DFA can be characterized by the summation of + regular expressions of all accepting states. +*} + +text {* \begin{figure}[h!] \centering \begin{minipage}{0.5\textwidth} @@ -112,4 +163,5 @@ *} + end diff -r e5116c2e6187 -r 79de7de104c8 tphols-2011/document/root.tex --- a/tphols-2011/document/root.tex Mon Feb 07 11:12:36 2011 +0000 +++ b/tphols-2011/document/root.tex Mon Feb 07 13:08:09 2011 +0000 @@ -47,10 +47,12 @@ %\renewcommand{\isastyle}{\isastyleminor} {\theoremstyle{break} \newtheorem{Lem}{Lemma}} +{\theoremstyle{break} \newtheorem{Thm}{Theorem}} \newcommand{\dfa}[1]{\hat{\delta}_{#1}} \newcommand{\Lang}{\mathcal{L}} -\newcommand{\mht}{Myhill-Nerode Theorem} +\newcommand{\re}{e} +\newcommand{\mht}{Myhill-Nerode theorem} \newcommand{\qnt}[2]{{#1}//{#2}} \newcommand{\cls}[2]{\llbracket{#1}\rrbracket_{#2}}