--- 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 {*