
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<presentation>{
   \begin{frame}
@@ -52,19 +53,25 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \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 "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman
   \end{itemize}
 
   \end{frame}}
@@ -208,7 +215,9 @@
   \end{textblock}}
   \medskip
 
-  \only<6->{A solution:\;\;\smath{\text{nat}} @{text "\<Rightarrow>"} state nodes}
+  \only<6->{A solution:\;\;\smath{\text{nat}} \;@{text "\<Rightarrow>"}\; 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<presentation>{
   \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<presentation>{
-  \begin{frame}[t]
-  \frametitle{Regular Expressions}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \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<presentation>{
   \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<presentation>{
-  \begin{frame}[c]
   \frametitle{\LARGE Regular Languages}
 
   \begin{itemize}
@@ -711,35 +653,6 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \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<presentation>{
-  \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 {*




