ChengsongTanPhdThesis/Chapters/Bitcoded2.tex
changeset 586 826af400b068
parent 585 4969ef817d92
child 588 80e1114d6421
equal deleted inserted replaced
585:4969ef817d92 586:826af400b068
   611 which will be needed later.\\
   611 which will be needed later.\\
   612 The inference rules (\ref{rrewriteRules}) we 
   612 The inference rules (\ref{rrewriteRules}) we 
   613 gave in the previous section 
   613 gave in the previous section 
   614 have their ``many-steps version'':
   614 have their ``many-steps version'':
   615 
   615 
   616 \begin{lemma}
   616 \begin{lemma}\label{squig1}
   617 	\hspace{0em}
   617 	\hspace{0em}
   618 	\begin{itemize}
   618 	\begin{itemize}
   619 		\item
   619 		\item
   620 			$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies _{bs} \sum rs_1 \stackrel{*}{\rightsquigarrow} _{bs} \sum rs_2$
   620 			$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies _{bs} \sum rs_1 \stackrel{*}{\rightsquigarrow} _{bs} \sum rs_2$
   621 		\item
   621 		\item
   622 			$r \stackrel{*}{\rightsquigarrow} r' \implies _{bs} \sum r :: rs \stackrel{*}{\rightsquigarrow}  _{bs} \sum r' :: rs$
   622 			$r \rightsquigarrow^* r' \implies _{bs} \sum (r :: rs)\; \rightsquigarrow^*\;  _{bs} \sum (r' :: rs)$
       
   623 
       
   624 		\item
       
   625 			The rewriting in many steps property is composible 
       
   626 			in terms of the sequence constructor:\\
       
   627 			$r_1 \rightsquigarrow^* r_2 
       
   628 			\implies _{bs} r_1 \cdot r_3 \rightsquigarrow^* \;  
       
   629 			_{bs} r_2 \cdot r_3 \quad $ 
       
   630 			and 
       
   631 			$\quad r_3 \rightsquigarrow^* r_4 
       
   632 			\implies _{bs} r_1 \cdot r_3 \rightsquigarrow^* _{bs} \; r_1 \cdot r_4$
       
   633 		\item
       
   634 			The rewriting in many steps properties 
       
   635 			$\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ 
       
   636 			is preserved under the function $\fuse$:\\
       
   637 				$r_1 \rightsquigarrow^* r_2 
       
   638 				\implies \fuse \; bs \; r_1 \rightsquigarrow^* \; 
       
   639 				\fuse \; bs \; r_2 \quad  $ and 
       
   640 				$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 
       
   641 				\implies \map \; (\fuse \; bs) \; rs_1 
       
   642 				\stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs) \; rs_2$
   623 	\end{itemize}
   643 	\end{itemize}
   624 \end{lemma}
   644 \end{lemma}
   625 \begin{proof}
   645 \begin{proof}
   626 	By an induction on 
   646 	By an induction on 
   627 	the inductive cases of $\stackrel{s*}{\rightsquigarrow}$ and $\rightsquigarrow^*$ respectively.
   647 	the inductive cases of $\stackrel{s*}{\rightsquigarrow}$ and $\rightsquigarrow^*$ respectively.
       
   648 	The third and fourth points are 
       
   649 	by the properties $r_1 \rightsquigarrow r_2 \implies \fuse \; bs \; r_1 \implies \fuse \; bs \; r_2$ and
       
   650 	$rs_2 \stackrel{s}{\rightsquigarrow} rs_3 
       
   651 	\implies \map \; (\fuse \; bs) rs_2 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs)\; rs_3$,
       
   652 	which can be indutively proven by the inductive cases of $\rightsquigarrow$ and 
       
   653 	$\stackrel{s}{\rightsquigarrow}$.
   628 \end{proof}
   654 \end{proof}
   629 \noindent
   655 \noindent
   630 The inference rules of $\stackrel{s}{\rightsquigarrow}$
   656 The inference rules of $\stackrel{s}{\rightsquigarrow}$
   631 are defined in terms of list cons operation, here
   657 are defined in terms of list cons operation, here
   632 we establish that the 
   658 we establish that the 
   633 $\stackrel{s}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ 
   659 $\stackrel{s}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ 
   634 relation is also preserved w.r.t appending and prepending of a list:
   660 relation is also preserved w.r.t appending and prepending of a list.
       
   661 In addition, we
       
   662 also prove some relations 
       
   663 between $\rightsquigarrow^*$ and $\stackrel{s*}{\rightsquigarrow}$.
   635 \begin{lemma}\label{ssgqTossgs}
   664 \begin{lemma}\label{ssgqTossgs}
   636 	\hspace{0em}
   665 	\hspace{0em}
   637 	\begin{itemize}
   666 	\begin{itemize}
   638 		\item
   667 		\item
   639 			$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies rs @ rs_1 \stackrel{s}{\rightsquigarrow} rs @ rs_2$
   668 			$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies rs @ rs_1 \stackrel{s}{\rightsquigarrow} rs @ rs_2$
   640 
   669 
   641 		\item
   670 		\item
   642 			$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies 
   671 			$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies 
   643 			rs @ rs_1 \stackrel{s*}{\rightsquigarrow} rs @ rs_2$
   672 			rs @ rs_1 \stackrel{s*}{\rightsquigarrow} rs @ rs_2 \; \;
       
   673 			\textit{and} \; \;
       
   674 			rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
       
   675 			
   644 		\item
   676 		\item
   645 			The $\stackrel{s}{\rightsquigarrow} $ relation after appending 
   677 			The $\stackrel{s}{\rightsquigarrow} $ relation after appending 
   646 			a list becomes $\stackrel{s*}{\rightsquigarrow}$:\\
   678 			a list becomes $\stackrel{s*}{\rightsquigarrow}$:\\
   647 			$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
   679 			$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 
   648 
   680 			\implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
       
   681 		\item
       
   682 		
       
   683 			$r_1 \rightsquigarrow^* r_2 \implies [r_1] \stackrel{s*}{\rightsquigarrow} [r_2]$
       
   684 		\item
       
   685 		
       
   686 			$rs_3 \stackrel{s*}{\rightsquigarrow} rs_4 \land r_1 \rightsquigarrow^* r_2 \implies
       
   687 			r_2 :: rs_3 \stackrel{s*}{\rightsquigarrow} r_2 :: rs_4$
       
   688 		\item			
       
   689 			If we could rewrite a regular expression 
       
   690 			in many steps to $\ZERO$, then 
       
   691 			we could also rewrite any sequence containing it to $\ZERO$:\\
       
   692 			$r_1 \rightsquigarrow^* \ZERO 
       
   693 			\implies _{bs}r_1\cdot r_2 \rightsquigarrow^* \ZERO$
   649 	\end{itemize}
   694 	\end{itemize}
   650 \end{lemma}
   695 \end{lemma}
   651 \begin{proof}
   696 \begin{proof}
   652 	The first part is by induction on the list $rs$.
   697 	The first part is by induction on the list $rs$.
   653 	The second part is by induction on the inductive cases of $\stackrel{s*}{\rightsquigarrow}$.
   698 	The second part is by induction on the inductive cases of $\stackrel{s*}{\rightsquigarrow}$.
   654 	The third part is 
   699 	The third part is 
   655 	by rule induction of $\stackrel{s}{\rightsquigarrow}$.
   700 	by rule induction of $\stackrel{s}{\rightsquigarrow}$.
   656 \end{proof}
   701 	The fourth sub-lemma is 
   657 \begin{lemma}
   702 	by rule induction of 
   658 	$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
   703 	$\stackrel{s*}{\rightsquigarrow}$ and using part one to three. 
   659 \end{lemma}
   704 	The fifth part is a corollary of part four.
   660 \begin{proof}
   705 	The last part is proven by rule induction again on $\rightsquigarrow^*$.
   661 	By rule induction of $\stackrel{s*}{\rightsquigarrow}$ and using \ref{ssgqTossgs}.
   706 \end{proof}
   662 \end{proof}
   707 \noindent
   663 Here are two lemmas relating $\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$:
   708 Now we are ready to give the proofs of the below properties:
   664 \begin{lemma}\label{singleton}
       
   665 	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies [r_1] \stackrel{s*}{\rightsquigarrow} [r_2]$
       
   666 \end{lemma}
       
   667 \begin{proof}
       
   668 	By rule induction of $ \stackrel{*}{\rightsquigarrow} $.
       
   669 \end{proof}
       
   670 \begin{lemma}
       
   671 	$rs_3 \stackrel{s*}{\rightsquigarrow} rs_4 \land r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies
       
   672 	r_2 :: rs_3 \stackrel{s*}{\rightsquigarrow} r_2 :: rs_4$
       
   673 \end{lemma}
       
   674 \begin{proof}
       
   675 	By using \ref{singleton}.
       
   676 \end{proof}
       
   677 In this section we give details for the proofs of the below properties:
       
   678 \begin{itemize}
   709 \begin{itemize}
   679 	\item
   710 	\item
   680 		$(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) 
   711 		$(r \rightsquigarrow^* r'\land \bnullable \; r_1) 
   681 		\implies \bmkeps \; r = \bmkeps \; r'$. \\
   712 		\implies \bmkeps \; r = \bmkeps \; r'$. \\
   682 		If we can rewrite 
       
   683 		in many steps from $r$ to $r'$, then they  
       
   684 		will produce the same bitcodes 
       
   685 		under $\bmkeps$. 
       
   686 	\item
   713 	\item
   687 		$r \rightsquigarrow^* \textit{bsimp} \;r$.\\
   714 		$r \rightsquigarrow^* \textit{bsimp} \;r$.\\
   688 		The simplification function
       
   689 		$\textit{bsimp}$ only transforms the regex $r$ using steps specified by 
       
   690 		$\rightsquigarrow^*$ and nothing else.
       
   691 	\item
   715 	\item
   692 		$r \rightsquigarrow r' \implies r \backslash c \rightsquigarrow^* r'\backslash c$.\\
   716 		$r \rightsquigarrow r' \implies r \backslash c \rightsquigarrow^* r'\backslash c$.\\
   693 		The rewritability relation $\rightsquigarrow$ is preserved under derivatives--
       
   694 		it is just that we might need more steps.
       
   695 \end{itemize}
   717 \end{itemize}
   696 These properties would work together towards the correctness theorem.
   718 These properties would work together towards the correctness theorem.
   697 We start proving each of these lemmas below.
   719 \subsubsection{Property 1: $(r \rightsquigarrow^* r'\land \bnullable \; r_1) 
   698 \subsubsection{Property 1: $(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) \implies \bmkeps \; r = \bmkeps \; r'$}
   720 		\implies \bmkeps \; r = \bmkeps \; r'$}
   699 Intuitively this property says we can 
   721 Intuitively, this property says we can 
   700 extract the same bitcodes from the nullable
   722 extract the same bitcodes using $\bmkeps$ from the nullable
   701 components of two regular expressions
   723 components of two regular expressions $r$ and $r'$,
   702 if we can rewrite from one to the other.
   724 if we can rewrite from one to the other in finitely
   703 
   725 many steps.\\
   704 
   726 For convenience, 
   705 
   727 we define a predicate for a list of regular expressions
   706 
   728 having at least one nullable regular expressions:
   707 Now we get to the "meaty" part of the proof, which relates the relations $\stackrel{s*}{\rightsquigarrow}$ and 
   729 \begin{center}
   708 $\stackrel{*}{\rightsquigarrow} $ with our simplification components such $\distinctBy$ and $\flts$.
   730 	$\textit{bnullables} \; rs \quad \dn \quad \exists r \in rs. \;\; \bnullable \; r$
   709 The first lemma below says that for a list made of two parts $rs_1 @ rs_2$, one can throw away the duplicate
   731 \end{center}
   710 elements in $rs_2$, as well as those that have appeared in $rs_1$:
   732 \noindent
       
   733 The rewriting relation $\rightsquigarrow$ preserves nullability:
       
   734 \begin{lemma}\label{rewritesBnullable}
       
   735 	\hspace{0em}
       
   736 	\begin{itemize}
       
   737 		\item
       
   738 			$\text{If} \; r_1 \rightsquigarrow r_2, \; 
       
   739 			\text{then} \; \bnullable \; r_1 = \bnullable \; r_2$
       
   740 		\item 	
       
   741 			$\text{If} \; rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \;
       
   742 			\text{then} \; \textit{bnullables} \; rs_1 = \textit{bnullables} \; rs_2$
       
   743 		\item
       
   744 			$r_1 \rightsquigarrow^* r_2 
       
   745 			\implies \bnullable \; r_1 = \bnullable \; r_2$
       
   746 	\end{itemize}
       
   747 \end{lemma}
       
   748 \begin{proof}
       
   749 	By rule induction of $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$.
       
   750 	The third point is a corollary of the second.
       
   751 \end{proof}
       
   752 \noindent
       
   753 For convenience again,
       
   754 we define $\bmkepss$ on a list $rs$,
       
   755 which extracts the bit-codes on the first $\bnullable$ element in $rs$:
       
   756 \begin{center}
       
   757 	\begin{tabular}{lcl}
       
   758 		$\bmkepss \; [] $ & $\dn$ & $[]$\\
       
   759 		$\bmkepss \; r :: rs$ & $\dn$ & $\textit{if} \;(\bnullable \; r) \;\; 
       
   760 		\textit{then} \;\; \bmkeps \; r \; \textit{else} \;\; \bmkepss \; rs$
       
   761 	\end{tabular}
       
   762 \end{center}
       
   763 \noindent
       
   764 If both regular expressions in a rewriting relation are nullable, then they 
       
   765 produce the same bitcodes:
       
   766 \begin{lemma}\label{rewriteBmkepsAux}
       
   767 	\hspace{0em}
       
   768 	\begin{itemize}
       
   769 		\item
       
   770 			$r_1 \rightsquigarrow r_2 \implies 
       
   771 			(\bnullable \; r_1 \land \bnullable \; r_2 \implies \bmkeps \; r_1 = 
       
   772 			\bmkeps \; r_2)$ 
       
   773 		\item
       
   774 			and
       
   775 			$rs_ 1 \stackrel{s}{\rightsquigarrow} rs_2 
       
   776 			\implies (\bnullables \; rs_1 \land \bnullables \; rs_2 \implies 
       
   777 			\bmkepss \; rs_1 = \bmkepss \; rs2)$
       
   778 	\end{itemize}
       
   779 \end{lemma}
       
   780 \begin{proof}
       
   781 	By rule induction over the cases that lead to $r_1 \rightsquigarrow r_2$.
       
   782 \end{proof}
       
   783 \noindent
       
   784 With lemma \ref{rewriteBmkepsAux} we are ready to prove its
       
   785 many-step version: 
   711 \begin{lemma}
   786 \begin{lemma}
   712 	$rs_1 @ rs_2 \stackrel{s*}{\rightsquigarrow} (rs_1 @ (\distinctBy \; rs_2 \; \; \rerase{\_}\;  \; (\map\;\; \rerase{\_}\; \; rs_1)))$
   787 	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r' \;\; \text{and} \;\; \bnullable \; r, \;\;\; \text{then} \;\; \bmkeps \; r = \bmkeps \; r'$
   713 \end{lemma}
   788 \end{lemma}
       
   789 \begin{proof}
       
   790 	By rule induction of $\stackrel{*}{\rightsquigarrow} $.
       
   791 	$\ref{rewritesBnullable}$ tells us both $r$ and $r'$ are nullable.
       
   792 	\ref{rewriteBmkepsAux} solves the inductive case.
       
   793 \end{proof}
       
   794 
       
   795 \subsubsection{Property 2: $r \stackrel{*}{\rightsquigarrow} \bsimp{r}$}
       
   796 Now we get to the ``meaty'' part of the proof, 
       
   797 which says that our simplification's helper functions 
       
   798 such as $\distinctBy$ and $\flts$ conform to 
       
   799 the $\stackrel{s*}{\rightsquigarrow}$ and 
       
   800 $\rightsquigarrow^* $ rewriting relations.\\
       
   801 The first lemma to prove is a more general version of 
       
   802 $rs_ 1 \rightsquigarrow^* \distinctBy \; rs_1 \; \phi$:
       
   803 \begin{lemma}
       
   804 	$rs_1 @ rs_2 \stackrel{s*}{\rightsquigarrow} 
       
   805 	(rs_1 @ (\distinctBy \; rs_2 \; \; \rerases \;\; (\map\;\; \rerases \; \; rs_1)))$
       
   806 \end{lemma}
       
   807 \noindent
       
   808 It says that that for a list made of two parts $rs_1 @ rs_2$, 
       
   809 one can throw away the duplicate
       
   810 elements in $rs_2$, as well as those that have appeared in $rs_1$.
   714 \begin{proof}
   811 \begin{proof}
   715 	By induction on $rs_2$, where $rs_1$ is allowed to be arbitrary.
   812 	By induction on $rs_2$, where $rs_1$ is allowed to be arbitrary.
   716 \end{proof}
   813 \end{proof}
   717 The above h as the corollary that is suitable for the actual way $\distinctBy$ is called in $\bsimp$:
   814 \noindent
   718 \begin{lemma}\label{dBPreserves}
   815 Setting $rs_2$ to be empty,
   719 	$rs_ 1 \rightarrow \distinctBy \; rs_1 \; \phi$
   816 we get the corollary
   720 \end{lemma}
   817 \begin{corollary}\label{dBPreserves}
   721 
   818 	$rs_1 \stackrel{s*}{\rightsquigarrow} \distinctBy \; rs_1 \; \phi$.
   722 
   819 \end{corollary}
   723 
   820 \noindent
   724 The flatten function $\flts$ works within the $\rightsquigarrow$ relation:
   821 The flatten function $\flts$ conforms to
       
   822 $\stackrel{s*}{\rightsquigarrow}$ as well:
       
   823 
   725 \begin{lemma}\label{fltsPreserves}
   824 \begin{lemma}\label{fltsPreserves}
   726 	$rs \stackrel{s*}{\rightsquigarrow} \flts \; rs$
   825 	$rs \stackrel{s*}{\rightsquigarrow} \flts \; rs$
   727 \end{lemma}
   826 \end{lemma}
   728 
   827 \begin{proof}
   729 The rewriting in many steps property is composible in terms of regular expression constructors:
   828 	By an induction on $rs$.
   730 \begin{lemma}
   829 \end{proof}
   731 	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies _{bs} r_1 \cdot r_3 \stackrel{*}{\rightsquigarrow} \;  _{bs} r_2 \cdot r_3 \quad $ and 
       
   732 $r_3 \stackrel{*}{\rightsquigarrow} r_4 \implies _{bs} r_1 \cdot r_3 \stackrel{*}{\rightsquigarrow} _{bs} \; r_1 \cdot r_4$
       
   733 \end{lemma}
       
   734 
       
   735 The rewriting in many steps properties $\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ is preserved under the function $\fuse$:
       
   736 \begin{lemma}
       
   737 	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies \fuse \; bs \; r_1 \stackrel{*}{\rightsquigarrow} \; \fuse \; bs \; r_2 \quad $ and 
       
   738 	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \map \; (\fuse \; bs) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs) \; rs_2$
       
   739 \end{lemma}
       
   740 \begin{proof}
       
   741 	By the properties $r_1 \rightsquigarrow r_2 \implies \fuse \; bs \; r_1 \implies \fuse \; bs \; r_2$ and
       
   742 	$rs_2 \stackrel{s}{\rightsquigarrow} rs_3 \implies \map \; (\fuse \; bs) rs_2 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs)\; rs_3$.
       
   743 \end{proof}
       
   744 \noindent
       
   745 If we could rewrite a regular expression in many steps to $\ZERO$, then 
       
   746 we could also rewrite any sequence containing it to $\ZERO$:
       
   747 \begin{lemma}
       
   748 	$r_1 \stackrel{*}{\rightsquigarrow} \ZERO \implies _{bs}r_1\cdot r_2 \stackrel{*}{\rightsquigarrow} \ZERO$
       
   749 \end{lemma}
       
   750 \begin{lemma}
       
   751 	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$
       
   752 \end{lemma}
       
   753 \noindent
   830 \noindent
   754 The function $\bsimpalts$ preserves rewritability:
   831 The function $\bsimpalts$ preserves rewritability:
   755 \begin{lemma}\label{bsimpaltsPreserves}
   832 \begin{lemma}\label{bsimpaltsPreserves}
   756 	$_{bs} \sum rs \stackrel{*}{\rightsquigarrow} \bsimpalts \; _{bs} \; rs$
   833 	$_{bs} \sum rs \stackrel{*}{\rightsquigarrow} \bsimpalts \; _{bs} \; rs$
   757 \end{lemma}
   834 \end{lemma}
   758 \noindent
   835 \noindent
   759 Before we give out the next lemmas, we define a predicate for a list of regular expressions
   836 The simplification function
   760 having at least one nullable regular expressions:
   837 $\textit{bsimp}$ only transforms the regex $r$ using steps specified by 
   761 \begin{definition}
   838 $\rightsquigarrow^*$ and nothing else.
   762 	$\textit{bnullables} \; rs \dn  \exists r \in rs. \bnullable r$
       
   763 \end{definition}
       
   764 The rewriting relation $\rightsquigarrow$ preserves nullability:
       
   765 \begin{lemma}
       
   766 	$r_1 \rightsquigarrow r_2 \implies  \bnullable \; r_1 = \bnullable \; r_2$ and
       
   767 	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \textit{bnullables} \; rs_1 = \textit{bnullables} \; rs_2$
       
   768 \end{lemma}
       
   769 \begin{proof}
       
   770 	By rule induction of $\rightarrow$ and $\stackrel{s}{\rightsquigarrow}$.
       
   771 \end{proof}
       
   772 So does the many steps rewriting:
       
   773 \begin{lemma}\label{rewritesBnullable}
       
   774 	$r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies \bnullable \; r_1 = \bnullable \; r_2$
       
   775 \end{lemma}
       
   776 \begin{proof}
       
   777 	By rule induction of $\stackrel{*}{\rightsquigarrow} $.
       
   778 \end{proof}
       
   779 \noindent
       
   780 And if both regular expressions in a rewriting relation are nullable, then they 
       
   781 produce the same bit-codes:
       
   782 
       
   783 \begin{lemma}\label{rewriteBmkepsAux}
       
   784 	$r_1 \rightsquigarrow r_2 \implies (\bnullable \; r_1 \land \bnullable \; r_2 \implies \bmkeps \; r_1 = 
       
   785 	\bmkeps \; r_2)$ and
       
   786 	$rs_ 1 \stackrel{s}{\rightsquigarrow} rs_2 \implies (\bnullables \; rs_1 \land \bnullables \; rs_2 \implies 
       
   787 	\bmkepss \; rs_1 = \bmkepss \; rs2)$
       
   788 \end{lemma}
       
   789 \noindent
       
   790 The definition of $\bmkepss$ on list $rs$ is just to extract the bit-codes on the first element in $rs$ that 
       
   791 is $bnullable$:
       
   792 \begin{center}
       
   793 	\begin{tabular}{lcl}
       
   794 		$\bmkepss \; [] $ & $\dn$ & $[]$\\
       
   795 		$\bmkepss \; r :: rs$ & $\dn$ & $\textit{if} \; \bnullable \; r then \; (\bmkeps \; r) \; \textit{else} \; \bmkepss \; rs$
       
   796 	\end{tabular}
       
   797 \end{center}
       
   798 \noindent
       
   799 And now we are ready to prove the key property that if you 
       
   800 have two regular expressions, one rewritable in many steps to the other,
       
   801 and one of them is $\bnullable$, then they will both yield the same bits under $\bmkeps$:
       
   802 \begin{lemma}
       
   803 	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r' \;\; \text{and} \;\; \bnullable \; r_1 \;\; \text{then} \;\; \bmkeps \; r = \bmkeps \; r'$
       
   804 \end{lemma}
       
   805 \begin{proof}
       
   806 	By rule induction of $\stackrel{*}{\rightsquigarrow} $, using \ref{rewriteBmkepsAux} and $\ref{rewritesBnullable}$.
       
   807 \end{proof}
       
   808 \noindent
       
   809 \subsubsection{Property 2: $r \stackrel{*}{\rightsquigarrow} \bsimp{r}$}
       
   810 the other property is also ready:
       
   811 \begin{lemma}
   839 \begin{lemma}
   812 	$r \stackrel{*}{\rightsquigarrow} \bsimp{r}$
   840 	$r \stackrel{*}{\rightsquigarrow} \bsimp{r}$
   813 \end{lemma}
   841 \end{lemma}
   814 \begin{proof}
   842 \begin{proof}
   815 	By an induction on $r$.
   843 	By an induction on $r$.
   816 The most difficult case would be the alternative case, where we using properties such as \ref{bsimpaltsPreserves} and \ref{fltsPreserves} and \ref{dBPreserves}, we could continuously rewrite a list like:\\
   844 	The most involved case would be the alternative, 
   817 	$rs \stackrel{s*}{\rightsquigarrow} \map \; \textit{bsimp} \; rs$\\
   845 	where we use lemmas \ref{bsimpaltsPreserves},
   818 	$\ldots \stackrel{s*}{\rightsquigarrow} \flts \; (\map \; \textit{bsimp} \; rs)$\\
   846 	\ref{fltsPreserves} and \ref{dBPreserves} to do a series of rewriting:\\
   819 	$\ldots \;\stackrel{s*}{\rightsquigarrow} \distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerase \; \phi$\\
   847 	\begin{center}
   820 	Then we could do the following regular expresssion many steps rewrite:\\
   848 		\begin{tabular}{lcl}
   821 	$ _{bs} \sum \distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerase \; \phi \stackrel{*}{\rightsquigarrow} \bsimpalts \; bs \; (\distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerase \; \phi)$
   849 			$rs$ &  $\stackrel{s*}{\rightsquigarrow}$ & $ \map \; \textit{bsimp} \; rs$\\
   822 	\\
   850 			     &  $\stackrel{s*}{\rightsquigarrow}$ & $ \flts \; (\map \; \textit{bsimp} \; rs)$\\
   823 	
   851 			     &  $\stackrel{s*}{\rightsquigarrow}$ & $ \distinctBy \; 
       
   852 			(\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerases \; \phi$\\
       
   853 		\end{tabular}
       
   854 	\end{center}
       
   855 	Using this we derive the following rewrite relation:\\
       
   856 	\begin{center}
       
   857 		\begin{tabular}{lcl}
       
   858 			$r$ & $=$ & $_{bs}\sum rs$\\[1.5ex]
       
   859 			    & $\rightsquigarrow^*$ & $\bsimpalts \; bs \; rs$ \\[1.5ex]
       
   860 			    & $\rightsquigarrow^*$ & $\ldots$ \\ [1.5ex]
       
   861 			    & $\rightsquigarrow^*$ & $\bsimpalts \; bs \; 
       
   862 			    (\distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) 
       
   863 			    \; \rerases \; \phi)$\\[1.5ex]
       
   864 			    %& $\rightsquigarrow^*$ & $ _{bs} \sum (\distinctBy \; 
       
   865 				%(\flts \; (\map \; \textit{bsimp}\; rs)) \; \;
       
   866 				%\rerases \; \;\phi) $\\[1.5ex]
       
   867 			    & $\rightsquigarrow^*$ & $\textit{bsimp} \; r$\\[1.5ex]
       
   868 		\end{tabular}
       
   869 	\end{center}	
   824 \end{proof}
   870 \end{proof}
   825 \subsubsection{Property 3: $r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow} r_2 \backslash c$}
   871 \subsubsection{Property 3: $r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow} r_2 \backslash c$}
   826 The first thing we prove is that if we could rewrite in one step, then after derivative
   872 The rewritability relation 
   827 we could rewrite in many steps:
   873 $\rightsquigarrow$ is preserved under derivatives--
       
   874 it is just that we might need multiple steps 
       
   875 where originally only one step was needed.
   828 \begin{lemma}\label{rewriteBder}
   876 \begin{lemma}\label{rewriteBder}
   829 	$r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$ and
   877 	$r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$ 
   830 	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$
   878 	and
       
   879 	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies 
       
   880 	\map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$
   831 \end{lemma}
   881 \end{lemma}
   832 \begin{proof}
   882 \begin{proof}
   833 	By induction on $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.
   883 	By induction on $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.
   834 \end{proof}
   884 \end{proof}
   835 Now we can prove that once we could rewrite from one expression to another in many steps,
   885 Now we can prove that once we could rewrite from one expression to another in many steps,
   866 	lexer with simplification applied:
   916 	lexer with simplification applied:
   867 	$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.
   917 	$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.
   868 	If two regular expressions are rewritable, then they produce the same bits.
   918 	If two regular expressions are rewritable, then they produce the same bits.
   869 	Under the condition that $ r_1$ is nullable, we have
   919 	Under the condition that $ r_1$ is nullable, we have
   870 	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$.
   920 	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$.
   871 	This proves the \emph{if} (interesting) branch of
   921 	We have that 
       
   922 	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$ holds.
       
   923 	This proves the \emph{if}  branch of
   872 	$\blexer \; r \; s = \blexersimp{r}{s}$.
   924 	$\blexer \; r \; s = \blexersimp{r}{s}$.
   873 
   925 
   874 \end{proof}
   926 \end{proof}
   875 \noindent
   927 \noindent
   876 As a corollary,
   928 As a corollary,