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, |