diff -r cf0e1fc65876 -r 69c22ded2f49 Slides/Slides1.thy --- a/Slides/Slides1.thy Tue Aug 23 00:33:12 2011 +0000 +++ b/Slides/Slides1.thy Tue Aug 23 08:11:25 2011 +0000 @@ -13,6 +13,7 @@ text_raw {* %\renewcommand{\slidecaption}{Cambridge, 9 November 2010} \renewcommand{\slidecaption}{Nijmegen, 25 August 2011} + \renewcommand{\ULthickness}{2pt} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame} @@ -52,19 +53,25 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{In Most Textbooks\ldots} + \frametitle{} + + \begin{textblock}{12.9}(1.5,3.2) + \begin{block}{} + \begin{minipage}{12.4cm}\raggedright + \large I want to teach \alert{students}\\ + with theorem provers (induction). + \end{minipage} + \end{block} + \end{textblock}\pause + + \mbox{}\\[35mm]\mbox{} \begin{itemize} - \item A \alert{regular language} is one where there is a DFA that - recognises it.\bigskip\pause - \end{itemize} - - - I can think of three reasons why this is a good definition:\medskip - \begin{itemize} - \item string matching via DFAs (yacc) - \item pumping lemma - \item closure properties of regular languages (closed under complement) + \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}% + \only<3->{\textcolor{red}{\sout{\textcolor{black}% + {\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}}}\medskip + \item<3-> formal language theory \\ + \mbox{}\;\;@{text "\"} nice textbooks: Kozen, Hopcroft \& Ullman \end{itemize} \end{frame}} @@ -208,7 +215,9 @@ \end{textblock}} \medskip - \only<6->{A solution:\;\;\smath{\text{nat}} @{text "\"} state nodes} + \only<6->{A solution:\;\;\smath{\text{nat}} \;@{text "\"}\; state nodes\medskip} + + \only<7->{You have to \alert{\uline{rename}} states!} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -226,8 +235,8 @@ \end{center} \begin{itemize} - \item Kozen's proof of Myhill-Nerode:\\ - \hspace{5cm}\alert{inaccessible states} + \item Kozen's paper proof of Myhill-Nerode:\\ + \hspace{2cm}requires absence of \alert{inaccessible states} \end{itemize}\bigskip\bigskip \begin{center} @@ -243,10 +252,10 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[t] - \frametitle{Regular Expressions} - \mbox{}\\[20mm]\mbox{} + \frametitle{} + \mbox{}\\[25mm]\mbox{} - \begin{textblock}{13.9}(0.7,2.2) + \begin{textblock}{13.9}(0.7,1.2) \begin{block}{} \begin{minipage}{13.4cm}\raggedright {\bf Definition:}\smallskip\\ @@ -257,14 +266,15 @@ \end{block} \end{textblock}\pause - {\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause + {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause - What we might lose?\pause - \begin{itemize}\renewcommand{\ULthickness}{2pt} + Do we lose anything?\pause + \begin{itemize} \item pumping lemma\pause \item closure under complementation\pause \item \only<6>{regular expression matching}% - \only<7>{\textcolor{red}{\sout{\textcolor{black}{regular expression matching}}}} + \only<7->{\textcolor{red}{\sout{\textcolor{black}{regular expression matching}}}} + \item<8-> most textbooks are about automata \end{itemize} @@ -273,44 +283,6 @@ *} -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Regular Expressions} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\LARGE Regular Expression Matching} - - \begin{itemize} - \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip - \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited - for a first-order version''\medskip - \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''\bigskip\pause - - \begin{quote}\small - ``Unfortunately, regular expression derivatives have been lost in the - sands of time, and few computer scientists are aware of them.'' - \end{quote} - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -326,7 +298,7 @@ \item key is the equivalence relation:\smallskip \begin{center} - \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L} + \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} \end{center} \end{itemize} @@ -357,36 +329,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{\LARGE Equivalence Classes} - - \begin{itemize} - \item \smath{L = []} - \begin{center} - \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}} - \end{center}\bigskip\bigskip - - \item \smath{L = [c]} - \begin{center} - \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}} - \end{center}\bigskip\bigskip - - \item \smath{L = \varnothing} - \begin{center} - \smath{\Big\{U\!N\!IV\Big\}} - \end{center} - - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] \frametitle{\LARGE Regular Languages} \begin{itemize} @@ -711,35 +653,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\LARGE The Equ's Solving Algorithm} - - \begin{itemize} - \item The algorithm is still a bit hairy to formalise because of our set-representation - for equations: - - \begin{center} - \begin{tabular}{ll} - \smath{\big\{ (X, \{(Y_1, r_1), (Y_2, r_2), \ldots\}),}\\ - \mbox{}\hspace{5mm}\smath{\ldots}\\ - & \smath{\big\}} - \end{tabular} - \end{center}\bigskip\pause - - \small - they are generated from \smath{U\!N\!IV /\!/ \approx_L} - - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -805,38 +718,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\LARGE Examples} - - \begin{itemize} - \item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular - \begin{quote}\small - \begin{tabular}{lcl} - \smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\ - \smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\ - \smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\ - \smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\ - \end{tabular} - \end{quote} - - \item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular - \begin{quote}\small - \begin{tabular}{lcl} - \smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\, n \ge 0\}}\\ - \smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\ - \smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\ - \smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\ - & \smath{\vdots} &\\ - \end{tabular} - \end{quote} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} text_raw {*