234 |
234 |
235 \begin{center} |
235 \begin{center} |
236 \bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l} |
236 \bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l} |
237 $Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\ |
237 $Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\ |
238 $Der\,b\,A$ & $=$ & $\{\textit{ar}\}$\\ |
238 $Der\,b\,A$ & $=$ & $\{\textit{ar}\}$\\ |
239 $Der\,a\,A$ & $=$ & $\varnothing$\\ |
239 $Der\,a\,A$ & $=$ & $\varnothing$\\\pause |
240 \end{tabular}} |
240 \end{tabular}} |
241 \end{center} |
241 \end{center} |
|
242 |
|
243 \small |
|
244 We can extend this definition to strings |
|
245 \[ |
|
246 \bl{Ders\,s\,A = \{s'\;|\;s\,@\,s' \in A\}} |
|
247 \] |
242 |
248 |
243 \end{itemize} |
249 \end{itemize} |
244 |
250 |
245 \end{frame} |
251 \end{frame} |
246 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
252 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
781 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
787 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
782 \begin{frame}[c] |
788 \begin{frame}[c] |
783 \frametitle{Proofs about Rexp (4)} |
789 \frametitle{Proofs about Rexp (4)} |
784 |
790 |
785 \begin{center} |
791 \begin{center} |
786 \bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l} |
792 \bl{\begin{tabular}{r@{\hspace{2mm}}c@{\hspace{2mm}}l} |
787 $rev(\varnothing)$ & $\dn$ & $\varnothing$\\ |
793 $rev(\varnothing)$ & $\dn$ & $\varnothing$\\ |
788 $rev(\epsilon)$ & $\dn$ & $\epsilon$\\ |
794 $rev(\epsilon)$ & $\dn$ & $\epsilon$\\ |
789 $rev(c)$ & $\dn$ & $c$\\ |
795 $rev(c)$ & $\dn$ & $c$\\ |
790 $rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\ |
796 $rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\ |
791 $rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\ |
797 $rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\ |
792 $rev(r^*)$ & $\dn$ & $rev(r)^*$\\ |
798 $rev(r^*)$ & $\dn$ & $rev(r)^*$\\ |
793 \end{tabular}} |
799 \end{tabular}} |
794 \end{center} |
800 \end{center} |
795 |
801 |
796 |
|
797 We can prove |
802 We can prove |
798 |
803 |
799 \begin{center} |
804 \begin{center} |
800 \bl{$L(rev(r)) = \{s^{-1} \;|\; s \in L(r)\}$} |
805 \bl{$L(rev(r)) = \{s^{-1} \;|\; s \in L(r)\}$} |
801 \end{center} |
806 \end{center} |
803 by induction on \bl{$r$}. |
808 by induction on \bl{$r$}. |
804 |
809 |
805 \end{frame} |
810 \end{frame} |
806 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
811 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
807 |
812 |
|
813 |
|
814 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
815 \begin{frame}[c] |
|
816 \frametitle{\begin{tabular}{c} |
|
817 Correctness Proof\\[-1mm] for our Matcher\end{tabular}} |
|
818 |
|
819 \begin{itemize} |
|
820 \item We started from |
|
821 |
|
822 \begin{center} |
|
823 \begin{tabular}{rp{4cm}} |
|
824 & \bl{$s \in L(r)$}\medskip\\ |
|
825 \bl{$\Leftrightarrow$} & \bl{$[] \in Ders\,s\,(L(r))$}\pause |
|
826 \end{tabular} |
|
827 \end{center} |
|
828 |
|
829 \item if we can show \bl{$Ders\, s\,(L(r)) = L(ders\,s\,r)$} we |
|
830 have |
|
831 |
|
832 \begin{center} |
|
833 \begin{tabular}{rp{4cm}} |
|
834 \bl{$\Leftrightarrow$} & \bl{$[] \in L(ders\,s\,r)$}\medskip\\ |
|
835 \bl{$\Leftrightarrow$} & \bl{$nullable(ders\,s\,r)$}\medskip\\ |
|
836 \bl{$\dn$} & \bl{$matches\,s\,r$} |
|
837 \end{tabular} |
|
838 \end{center} |
|
839 |
|
840 \end{itemize} |
|
841 |
|
842 \end{frame} |
|
843 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
844 |
808 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
845 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
809 \begin{frame}[c] |
846 \begin{frame}[c] |
810 \frametitle{Proofs about Rexp (5)} |
847 \frametitle{Proofs about Rexp (5)} |
811 |
848 |
812 Let \bl{$Der\,c\,A$} be the set defined as |
849 Let \bl{$Der\,c\,A$} be the set defined as |
824 by induction on \bl{$r$}. |
861 by induction on \bl{$r$}. |
825 |
862 |
826 \end{frame} |
863 \end{frame} |
827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
864 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
828 |
865 |
829 |
866 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
830 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
867 \begin{frame}[c] |
831 \mode<presentation>{ |
868 \frametitle{Proofs about Strings} |
832 \begin{frame}[c] |
|
833 \frametitle{\begin{tabular}{c}Proofs about Strings\end{tabular}} |
|
834 |
869 |
835 If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip |
870 If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip |
836 |
871 |
837 \begin{itemize} |
872 \begin{itemize} |
838 \item \bl{$P$} holds for the empty string, and\medskip |
873 \item \bl{$P$} holds for the empty string, and\medskip |
839 \item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$} |
874 \item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$} |
840 already holds for \bl{$s$} |
875 already holds for \bl{$s$} |
841 \end{itemize} |
876 \end{itemize} |
842 \end{frame}} |
877 \end{frame} |
843 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
878 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
844 |
879 |
845 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
880 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
846 \mode<presentation>{ |
881 \begin{frame}[c] |
847 \begin{frame}[c] |
882 \frametitle{Proofs about Strings (2)} |
848 \frametitle{\begin{tabular}{c}Proofs about Strings (2)\end{tabular}} |
883 |
|
884 We can then prove |
|
885 |
|
886 \begin{center} |
|
887 \bl{$Ders\,s\,(L(r)) = L(ders\,s\,r)$} |
|
888 \end{center} |
|
889 |
849 |
890 |
850 We can finally prove |
891 We can finally prove |
851 |
892 |
852 \begin{center} |
893 \begin{center} |
853 \bl{$matches(r, s)$} if and only if \bl{$s \in L(r)$} |
894 \bl{$matches(r, s)$} if and only if \bl{$s \in L(r)$} |
854 \end{center} |
895 \end{center} |
855 |
896 |
856 |
897 |
857 \end{frame}} |
898 \end{frame} |
858 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
899 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
859 |
900 |
860 \end{document} |
901 \end{document} |
861 |
902 |
862 %%% Local Variables: |
903 %%% Local Variables: |