850 |
850 |
851 \noindent |
851 \noindent |
852 The reason why we take the trouble of defining |
852 The reason why we take the trouble of defining |
853 two separate list rewriting definitions $\frewrite$ and $\grewrite$ |
853 two separate list rewriting definitions $\frewrite$ and $\grewrite$ |
854 is that sometimes $\grewrites$ is slightly too powerful |
854 is that sometimes $\grewrites$ is slightly too powerful |
855 that it renders certain equivalence to break after derivative: |
855 for proving equivalence. |
856 |
856 For example, when proving the closed-form for the alternative regular expression, |
857 $\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} \neq |
857 one of the rewriting steps would be: |
858 \rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing})} $ |
858 \begin{lemma} |
859 |
859 $\sum (\rDistinct \; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \; \varnothing) \sequal |
860 |
860 \sum (\rDistinct \; (\rflts \; (\map \; (\_ \backslash x) \; rs)) \; \varnothing) |
861 |
861 $ |
|
862 \end{lemma} |
|
863 \noindent |
|
864 Proving this is by first showing |
|
865 \begin{lemma} |
|
866 $\map \; (\_ \backslash x) \; (\rflts \; rs) \frewrites |
|
867 \rflts \; (\map \; (\_ \backslash x) \; rs)$ |
|
868 \end{lemma} |
|
869 \noindent |
|
870 and then using lemma |
|
871 \begin{lemma}\label{frewritesSimpeq} |
|
872 If $rs_1 \frewrites rs_2 $, then $\sum (\rDistinct \; rs_1 \; \varnothing) \sequal |
|
873 \sum (\rDistinct \; rs_2 \; {})$. |
|
874 \end{lemma} |
|
875 . But this trick will not work for $\grewrites$: |
|
876 \begin{center} |
|
877 $\map \; (\_ \backslash x) \; (\rDistinct \; rs \; rset) \grewrites \rDistinct \; (\map \; |
|
878 (\_ \backslash x) \; rs) \; (\map \; (\_ \backslash x) \; rset)$ |
|
879 \end{center} |
|
880 \noindent |
|
881 does \emph{not} hold. |
|
882 |
|
883 |
|
884 |
|
885 |
|
886 %this is for closed form for alts section, talk about that later------------------------------ |
|
887 \begin{comment} |
|
888 \begin{center} |
|
889 $\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} = |
|
890 \rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}))} $ |
|
891 \end{center} |
|
892 |
|
893 \noindent |
|
894 This is not possible to prove |
|
895 |
|
896 \end{comment} |
|
897 %this is for closed form for alts section, talk about that later------------------------------ |
862 And we define an "grewrite" relation that works on lists: |
898 And we define an "grewrite" relation that works on lists: |
863 \begin{center} |
899 \begin{center} |
864 \begin{tabular}{lcl} |
900 \begin{tabular}{lcl} |
865 $ \ZERO :: rs$ & $\rightarrow_g$ & $rs$ |
901 $ \ZERO :: rs$ & $\rightarrow_g$ & $rs$ |
866 \end{tabular} |
902 \end{tabular} |
1319 \section{A Closed Form for \textit{ALTS}} |
1355 \section{A Closed Form for \textit{ALTS}} |
1320 Now we prove that $rsimp (rders\_simp (RALTS rs) s) = rsimp (RALTS (map (\lambda r. rders\_simp r s) rs))$. |
1356 Now we prove that $rsimp (rders\_simp (RALTS rs) s) = rsimp (RALTS (map (\lambda r. rders\_simp r s) rs))$. |
1321 |
1357 |
1322 |
1358 |
1323 There are a few key steps, one of these steps is |
1359 There are a few key steps, one of these steps is |
1324 \[ |
1360 |
1325 rsimp (rsimp\_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \circ (\lambda r. rders\_simp r xs)) rs)) {}))) |
|
1326 = rsimp (rsimp\_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \circ (\lambda r. rders\_simp r xs)) rs))) {})) |
|
1327 \] |
|
1328 |
1361 |
1329 |
1362 |
1330 One might want to prove this by something a simple statement like: |
1363 One might want to prove this by something a simple statement like: |
1331 $map (rder x) (rdistinct rs rset) = rdistinct (map (rder x) rs) (rder x) ` rset)$. |
|
1332 |
1364 |
1333 For this to hold we want the $\textit{distinct}$ function to pick up |
1365 For this to hold we want the $\textit{distinct}$ function to pick up |
1334 the elements before and after derivatives correctly: |
1366 the elements before and after derivatives correctly: |
1335 $r \in rset \equiv (rder x r) \in (rder x rset)$. |
1367 $r \in rset \equiv (rder x r) \in (rder x rset)$. |
1336 which essentially requires that the function $\backslash$ is an injective mapping. |
1368 which essentially requires that the function $\backslash$ is an injective mapping. |