--- a/Slides/Slides6.thy Wed Oct 02 13:17:32 2013 +0100
+++ b/Slides/Slides6.thy Thu Oct 03 15:29:03 2013 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory Slides5
+theory Slides6
imports "~~/src/HOL/Library/LaTeXsugar"
begin
@@ -11,7 +11,7 @@
text_raw {*
- \renewcommand{\slidecaption}{London, 29 August 2012}
+ \renewcommand{\slidecaption}{London, 3 October 2013}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]
\node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
@@ -21,8 +21,9 @@
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\\[-3mm]
- \LARGE The Myhill-Nerode Theorem\\[-3mm]
- \LARGE in a Theorem Prover\\[0mm]
+ \Large A Formalisation of the\\[-1mm]
+ \Large Myhill-Nerode Theorem using\\[-1mm]
+ \Large Regular Expressions only
\end{tabular}}
\begin{center}
@@ -35,11 +36,6 @@
University of Science and Technology in Nanjing
\end{center}
- \only<2->{
- \begin{textblock}{6}(9,5.3)
- \alert{\bf Isabelle/HOL}
- \end{textblock}}
-
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -52,20 +48,15 @@
\mbox{}\\[2mm]
\begin{itemize}
- \item my background is in
- \begin{itemize}
- \item \normalsize programming languages and theorem provers
- \item \normalsize develop Nominal Isabelle
- \end{itemize}\bigskip\bigskip\bigskip\bigskip\bigskip
+ \item my background is in:
+ \begin{itemize}
+ \item \normalsize programming languages and
+ \item \normalsize theorem provers
+ \end{itemize}\medskip
- \item<1->to formalise and mechanically check proofs from
- programming language research, TCS \textcolor{gray}{and OS}\bigskip
-
- \item<2->we found out that the variable convention can lead to
- faulty proofs\ldots
+ \item \normalsize develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
\end{itemize}
- \onslide<2->{
\begin{center}
\begin{block}{}
\color{gray}
@@ -73,145 +64,22 @@
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm]
If $M_1,\ldots,M_n$ occur in a certain mathematical context
(e.g. definition, proof), then in these terms all bound variables
- are chosen to be different from the free variables.\hfill Henk Barendregt
+ are chosen to be different from the free variables.\hfill ---Henk Barendregt
\end{block}
- \end{center}}
-
-
- \only<1->{
- \begin{textblock}{6}(10.9,3.5)
- \includegraphics[scale=0.23]{isabelle1.png}
- \end{textblock}}
-
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{}
+ \end{center}\pause
- \begin{tabular}{c@ {\hspace{2mm}}c}
- \\[6mm]
- \begin{tabular}{c}
- \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
- {\footnotesize Bob Harper}\\[-2.5mm]
- {\footnotesize (CMU)}
- \end{tabular}
- \begin{tabular}{c}
- \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
- {\footnotesize Frank Pfenning}\\[-2.5mm]
- {\footnotesize (CMU)}
- \end{tabular} &
+ \mbox{}\\[-19mm]\mbox{}
- \begin{tabular}{p{6cm}}
- \raggedright
- \color{gray}{published a proof on LF in\\ {\bf ACM Transactions on Computational Logic}, 2005,
- $\sim$31pp}
- \end{tabular}\\
-
- \pause
- \\[0mm]
-
- \begin{tabular}{c}
- \includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
- {\footnotesize Andrew Appel}\\[-2.5mm]
- {\footnotesize (Princeton)}
- \end{tabular} &
-
- \begin{tabular}{p{6cm}}
- \raggedright
- \color{gray}{relied on their proof in a\\ {\bf security} critical application\\ (proof-carrying code)}
- \end{tabular}
- \end{tabular}
-
-
+ \begin{itemize}
+ \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning
+ about LF (and fixed it in three ways)
+ \end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
-
-text {*
- \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
- \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
- draw=black!50, top color=white, bottom color=black!20]
- \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
- draw=red!70, top color=white, bottom color=red!50!black!20]
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<2->[squeeze]
- \frametitle{}
-
- \begin{columns}
-
- \begin{column}{0.8\textwidth}
- \begin{textblock}{0}(1,2)
-
- \begin{tikzpicture}
- \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
- { \&[-10mm]
- \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
- \node (proof1) [node1] {\large Proof}; \&
- \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
-
- \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
- \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
- \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
- \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
-
- \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
- \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
- \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
- \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
-
- \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
- \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
- \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
- \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
- };
-
- \draw[->,black!50,line width=2mm] (proof1) -- (def1);
- \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
-
- \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
- \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
-
- \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
- \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
-
- \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
- \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
-
- \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
- \end{tikzpicture}
-
- \end{textblock}
- \end{column}
- \end{columns}
-
-
- \begin{textblock}{3}(12,3.6)
- \onslide<4->{
- \begin{tikzpicture}
- \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
- \end{tikzpicture}}
- \end{textblock}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -219,54 +87,18 @@
\frametitle{}
\begin{itemize}
- \item I also found fixable errors in my Ph.D.-thesis about cut-elimination
+ \item found also fixable errors in my Ph.D.-thesis about cut-elimination
(examined by Henk Barendregt and Andy Pitts)\bigskip
- \item found flaws in a proof about a classic OS scheduling algorithm
- --- helped us to implement\\ it correctly and ef$\!$ficiently\\
- {\small\textcolor{gray}{(the existing literature ``proved''
- correct an incorrect algorithm; used in the Mars Pathfinder mission)}}
- \end{itemize}\bigskip\bigskip\pause
-
-
- {\bf Conclusion:}\smallskip
-
- Pencil-and-paper proofs in TCS are not foolproof,
- not even expertproof.
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{}
- \begin{center}
- \begin{block}{}
- \color{gray}
- \small
- ``I still remember having to grade hundreds of exams where the
- students started out by assuming what had to be proved, or filled
- page after page with gibberish in the hope that, somewhere in the
- mess, they might accidentally have said something
- correct. \ldots{}innumerable examples of ``parrot proofs'' ---
- NP-completeness reductions done in the wrong direction, arguments
- that look more like LSD trips than coherent chains of logic \ldots{}''
- \end{block}
- \end{center}\pause
+ \item formalised a classic OS scheduling algorithm (priority inversion
+ protocol)
+ \begin{itemize}
+ \item original algorithm was incorrect even being proved correct (with `pencil-and-paper')
+ \item helped us to implement this algorithm correctly and efficiently\\
+ \end{itemize}\bigskip\pause
- \begin{tabular}{@ {}c@ {}}
- Tobias Nipkow calls this the ``London Underground Phenomenon'':
- \end{tabular}
-
- \begin{center}
- \begin{tabular}{ccc}
- students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs
- \end{tabular}
- \end{center}
+ \item used Isabelle to prove properties about access controls and OSes
+ \end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -281,7 +113,7 @@
\begin{textblock}{12.9}(1.5,2.0)
\begin{block}{}
\begin{minipage}{12.4cm}\raggedright
- \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with
+ \large {\bf Motivation:}\\[2mm]I want to teach \alert{students}
theorem\\ provers (especially for inductions).
\end{minipage}
\end{block}
@@ -310,12 +142,12 @@
\begin{textblock}{6}(2,4)
\begin{tabular}{@ {}rrl}
- \bl{r} & \bl{$::=$} & \bl{$\varnothing$}\\
- & \bl{$\mid$} & \bl{[]}\\
- & \bl{$\mid$} & \bl{c}\\
- & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\
- & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\
- & \bl{$\mid$} & \bl{r$^*$}\\
+ \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\
+ & \bl{$\mid$} & \bl{$[]$}\\
+ & \bl{$\mid$} & \bl{$c$}\\
+ & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
+ & \bl{$\mid$} & \bl{$r_1 + r_2$}\\
+ & \bl{$\mid$} & \bl{$r^*$}\\
\end{tabular}
\end{textblock}
@@ -327,75 +159,226 @@
\footnotesize Isabelle:
\end{textblock}
- \begin{textblock}{6}(7,12)
- \footnotesize\textcolor{gray}{students have seen them and can be motivated about them}
- \end{textblock}
-
- \end{frame}}
+ \end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1->[t]
+ \begin{frame}<1-5>[t]
\mbox{}\\[-2mm]
\small
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
- \bl{nullable ($\varnothing$)} & \bl{$=$} & \bl{false} &\\
- \bl{nullable ([])} & \bl{$=$} & \bl{true} &\\
- \bl{nullable (c)} & \bl{$=$} & \bl{false} &\\
- \bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\
- \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\
- \bl{nullable (r$^*$)} & \bl{$=$} & \bl{true} & \\
+ \bl{$nullable(\varnothing)$} & \bl{$=$} & \bl{false} &\\
+ \bl{$nullable([])$} & \bl{$=$} & \bl{true} &\\
+ \bl{$nullable(c)$} & \bl{$=$} & \bl{false} &\\
+ \bl{$nullable(r_1 + r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \vee nullable(r_2)$} & \\
+ \bl{$nullable(r_1 \cdot r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} & \\
+ \bl{$nullable(r^*)$} & \bl{$=$} & \bl{true} & \\
\end{tabular}\medskip\pause
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
- \bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\
- \bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\
- \bl{der c (d)} & \bl{$=$} & \bl{if c $=$ d then [] else $\varnothing$} & \\
- \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
- \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$) + } & \\
- & & \bl{\hspace{3mm}(if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
- \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ (r$^*$)} &\smallskip\\\pause
+ \bl{$der\,c\,(\varnothing)$} & \bl{$=$} & \bl{$\varnothing$} & \\
+ \bl{$der\,c\,([])$} & \bl{$=$} & \bl{$\varnothing$} & \\
+ \bl{$der\,c\,(d)$} & \bl{$=$} & \bl{if $c = d$ then $[]$ else $\varnothing$} & \\
+ \bl{$der\,c\,(r_1 + r_2)$} & \bl{$=$} & \bl{$der\,c\,r_1 + der\,c\,r_2$} & \\
+ \bl{$der\,c\,(r_1 \cdot r_2)$} & \bl{$=$} & \bl{if $nullable(r_1)$}\\
+ & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\
+ & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
+ \bl{$der\,c\,(r^*)$} & \bl{$=$} & \bl{$(der\,c\,r) \cdot r^*$} &\smallskip\\\pause
- \bl{derivative [] r} & \bl{$=$} & \bl{r} & \\
- \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\
+ \bl{$deriv\,[]\,r$} & \bl{$=$} & \bl{$r$} & \\
+ \bl{$deriv\,(c::s)\,r$} & \bl{$=$} & \bl{$deriv\,s\,(der\,c\,r)$} & \\
\end{tabular}\medskip
- \bl{matches r s $=$ nullable (derivative s r)}
+ \bl{$match\,r\,s = nullable (deriv\,s\,r)$}
+
+ \only<4>{
+ \begin{textblock}{10.5}(2,5)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+{\normalsize\color{darkgray}
+ \begin{minipage}{10.5cm}
+ \begin{center}
+ a)\;\; \bl{$nullable(r) \Leftrightarrow ""\in {\cal L}(r)$}\medskip
+ \end{center}
+
+ \begin{center}
+ b)\;\; \bl{${\cal L}(der\,c\,r) = Der\,c\,({\cal L}(r))$}
+ \end{center}
+
+ where
+ \begin{center}
+ \bl{$Der\,c\,A \dn \{s\,|\, c\!::\!s \in A\}$}
+ \end{center}\medskip\pause
+
+ \begin{center}
+ c)\;\; \bl{$match\,r\,s \Leftrightarrow s\in{\cal L}(r)$}
+ \end{center}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Regular Expression Matching\\[-2mm] in Education}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
+
+\mbox{}\\[-13mm]
+
+\begin{tikzpicture}[y=.2cm, x=.3cm]
+ %axis
+ \draw (0,0) -- coordinate (x axis mid) (30,0);
+ \draw (0,0) -- coordinate (y axis mid) (0,30);
+ %ticks
+ \foreach \x in {0,5,...,30}
+ \draw (\x,1pt) -- (\x,-3pt)
+ node[anchor=north] {\x};
+ \foreach \y in {0,5,...,30}
+ \draw (1pt,\y) -- (-3pt,\y)
+ node[anchor=east] {\y};
+ %labels
+ \node[below=0.6cm] at (x axis mid) {\bl{a}s};
+ \node[rotate=90, left=1.2cm] at (y axis mid) {secs};
- \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\bigskip\bigskip\pause
- \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''
- \bigskip
+ %plots
+ \draw[color=blue] plot[mark=*, mark options={fill=white}]
+ file {re-python.data};
+ \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ]
+ file {re-ruby.data};
+
+ %legend
+ \begin{scope}[shift={(4,20)}]
+ \draw[color=blue] (0,0) --
+ plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0)
+ node[right]{\small Python};
+ \draw[yshift=-\baselineskip, color=brown] (0,0) --
+ plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0)
+ node[right]{\small Ruby};
+ \end{scope}
+\end{tikzpicture}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
+
+\mbox{}\\[-13mm]
+
+\begin{tabular}{@ {\hspace{-5mm}}l}
+\begin{tikzpicture}[y=.2cm, x=.01cm]
+ %axis
+ \draw (0,0) -- coordinate (x axis mid) (1000,0);
+ \draw (0,0) -- coordinate (y axis mid) (0,30);
+ %ticks
+ \foreach \x in {0,200,...,1000}
+ \draw (\x,1pt) -- (\x,-3pt)
+ node[anchor=north] {\x};
+ \foreach \y in {0,5,...,30}
+ \draw (1pt,\y) -- (-3pt,\y)
+ node[anchor=east] {\y};
+ %labels
+ \node[below=0.6cm] at (x axis mid) {\bl{a}s};
+ \node[rotate=90, left=1.2cm] at (y axis mid) {secs};
- \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}
-
+ %plots
+ \draw[color=blue] plot[mark=*, mark options={fill=white}]
+ file {re-python.data};
+ \draw[color=green] plot[mark=square*, mark options={fill=white} ]
+ file {re2c.data};
+ \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ]
+ file {re-ruby.data};
+
+ %legend
+ \begin{scope}[shift={(100,20)}]
+ \draw[color=blue] (0,0) --
+ plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small Python};
+ \draw[yshift=-13, color=brown] (0,0) --
+ plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small Ruby};
+ \draw[yshift=13, color=green] (0,0) --
+ plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small nullable + der};
+ \end{scope}
+\end{tikzpicture}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw{*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
+
+\mbox{}\\[-9mm]
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{tabular}{@ {\hspace{-5mm}}l}
+\begin{tikzpicture}[y=.2cm, x=.0008cm]
+ %axis
+ \draw (0,0) -- coordinate (x axis mid) (12000,0);
+ \draw (0,0) -- coordinate (y axis mid) (0,30);
+ %ticks
+ \foreach \x in {0,2000,...,12000}
+ \draw (\x,1pt) -- (\x,-3pt)
+ node[anchor=north] {\x};
+ \foreach \y in {0,5,...,30}
+ \draw (1pt,\y) -- (-3pt,\y)
+ node[anchor=east] {\y};
+ %labels
+ \node[below=0.6cm] at (x axis mid) {\bl{a}s};
+ \node[rotate=90, left=1.2cm] at (y axis mid) {secs};
+ %plots
+ \draw[color=green] plot[mark=square*, mark options={fill=white} ]
+ file {re2b.data};
+ \draw[color=black] plot[mark=square*, mark options={fill=white} ]
+ file {re3.data};
+ \draw[color=blue] plot[mark=*, mark options={fill=white}]
+ file {re-python.data};
+ \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ]
+ file {re-ruby.data};
+
+ %legend
+ \begin{scope}[shift={(2000,20)}]
+ \draw[color=blue] (0,0) --
+ plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small Python};
+ \draw[yshift=-13, color=brown] (0,0) --
+ plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small Ruby};
+ \draw[yshift=13, color=green] (0,0) --
+ plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small nullable + der};
+ \draw[yshift=26, color=black] (0,0) --
+ plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
+ node[right]{\small nullable + der + simplification};
+ \end{scope}
+\end{tikzpicture}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -479,7 +462,7 @@
\begin{block}{}
\medskip
\begin{minipage}{14cm}\raggedright
- Problems with definition for regularity:\bigskip\\
+ Already problems with defining regularity:\bigskip\\
\smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip
\end{minipage}
\end{block}
@@ -488,7 +471,7 @@
\only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}
- \only<7->{You have to \alert{rename} states!}
+ \only<7->{You have to \alert{rename} states apart!}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -542,7 +525,7 @@
{\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
- Infrastructure for free. But do we lose anything?\medskip\pause
+ Reasoning infrastructure is for free. But do we lose anything?\medskip\pause
\begin{minipage}{1.1\textwidth}
\begin{itemize}
@@ -572,7 +555,7 @@
\item provides necessary and suf\!ficient conditions\\ for a language
being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip
- \item key is the equivalence relation:\medskip
+ \item the key notion is the equivalence relation:\medskip
\begin{center}
\smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
\end{center}
@@ -620,7 +603,7 @@
\begin{tikzpicture}
\node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
{@{text "\<lbrakk>s\<rbrakk>"}$_{\approx_{A}}$};
- \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};
+ \draw (0.9,-1.1) node {\begin{tabular}{l}\;\;an equivalence class\end{tabular}};
\end{tikzpicture}
\end{textblock}}
@@ -702,7 +685,7 @@
\mode<presentation>{
\begin{frame}<-1>[c]
\frametitle{\begin{tabular}{@ {}l}\LARGE%
- Transitions between Eq-Classes\end{tabular}}
+ Transitions\end{tabular}}
\begin{center}
\begin{tikzpicture}[scale=3]
@@ -1147,30 +1130,31 @@
\textcolor{blue}{%
\begin{center}
\begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}}
- der c $\varnothing$ & $\dn$ & $\varnothing$\\
- der c [] & $\dn$ & $\varnothing$\\
- der c d & $\dn$ & if c $=$ d then [] else $\varnothing$\\
- der c ($r_1 + r_2$) & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\
- der c ($r^*$) & $\dn$ & (der c $r$) $\cdot$ ($r^*$)\\
- der c ($r_1 \cdot r_2$) & $\dn$ & ((der c $r_1$) $\cdot$ $r_2$) +\\
- & & \hspace{-3mm}(if nullable $r_1$ then der c $r_2$ else $\varnothing$)\\
+ $der\,c\,\varnothing$ & $\dn$ & $\varnothing$\\
+ $der\,c\,[]$ & $\dn$ & $\varnothing$\\
+ $der\,c\,d$ & $\dn$ & if $c = d$ then $[]$ else $\varnothing$\\
+ $der\,c\,(r_1 + r_2)$ & $\dn$ & $der\,c\,r_1 + der\,c\,r_2$\\
+ $der\,c\,(r^*)$ & $\dn$ & $(der\,c\,r) \cdot r^*$\\
+ $der\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\
+ & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\
+ & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
\end{tabular}
\end{center}}}
\only<2->{
- \begin{textblock}{13}(1.5,5.7)
+ \begin{textblock}{14.1}(1.5,5.7)
\begin{block}{}
\begin{quote}
- \begin{minipage}{13cm}\raggedright
+ \begin{minipage}{14.1cm}\raggedright\rm
derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip
\begin{center}
- \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(\text{ders}~x~r) = {\cal{L}}(\text{ders}~y~r)
+ \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(deriv~x~r) = {\cal{L}}(deriv~y~r)
\Longleftrightarrow x \approx_{{\cal{L}}(r)} y}}
- \only<3>{\mbox{\hspace{-22mm}}\smath{\text{ders}~x~r = \text{ders}~y~r
+ \only<3>{\mbox{\hspace{-22mm}}\smath{deriv~x~r = deriv~y~r
\Longrightarrow x \approx_{{\cal{L}}(r)} y}}
\end{center}\bigskip
\
- \smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI
+ \smath{\text{finite}(deriv~A~r)}, but only modulo ACI
\begin{center}
\begin{tabular}{@ {\hspace{-10mm}}rcl}
@@ -1192,20 +1176,21 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<2>[t]
- \frametitle{\LARGE\begin{tabular}{c}Partial Derivatives of RExps\end{tabular}}
+ \frametitle{\LARGE\begin{tabular}{c}Partial Derivatives\end{tabular}}
\only<2>{%
\textcolor{blue}{%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
- pder c $\varnothing$ & $\dn$ & \alert{$\{\}$}\\
- pder c [] & $\dn$ & \alert{$\{\}$}\\
- pder c d & $\dn$ & if c $=$ d then $\{$[]$\}$ else $\{\}$\\
- pder c ($r_1 + r_2$) & $\dn$ & (pder c $r_1$) \alert{$\cup$} (der c $r_2$)\\
- pder c ($r^\star$) & $\dn$ & (pder c $r$) $\cdot$ $r^\star$\\
- pder c ($r_1 \cdot r_2$) & $\dn$ & (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$}\\
- & & \hspace{-4mm}if nullable $r_1$ then (pder c $r_2$) else $\varnothing$\\
+ $pder\,c\,\varnothing$ & $\dn$ & \alert{$\{\}$}\\
+ $pder\,c\,[]$ & $\dn$ & \alert{$\{\}$}\\
+ $pder\,c\,d$ & $\dn$ & if $c = d$ then $\{[]\}$ else $\{\}$\\
+ $pder\,c\,(r_1 + r_2)$ & $\dn$ & $pder\,c\,r_1 \alert{\cup} pder\,c\,r_2$\\
+ $pder\,c\,(r^\star)$ & $\dn$ & $(pder\,c\,r) \cdot r^\star$\\
+ $pder\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\
+ & & \bl{then $(pder\,c\,r_1) \cdot r_2 \alert{\cup} pder\, c\, r_2$}\\
+ & & \bl{else $(pder\, c\, r_1) \cdot r_2$}\\
\end{tabular}
\end{center}}}
@@ -1213,7 +1198,7 @@
\begin{textblock}{6}(8.5,2.7)
\begin{block}{}
\begin{quote}
- \begin{minipage}{6cm}\raggedright
+ \begin{minipage}{6cm}\rm\raggedright
\begin{itemize}
\item partial derivatives
\item by Antimirov~'95
@@ -1237,11 +1222,13 @@
\begin{itemize}
- \item \alt<1>{\smath{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}}
- {\smath{\underbrace{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}_{R}}}
+ \item \alt<1>{\smath{\text{$pderiv\,x\,r = pderiv\,y\,r$}}}
+ {\smath{\underbrace{\text{$pderiv\,x\,r = pderiv\,y\,r$}}_{R}}}
refines \textcolor{blue}{$x$ $\approx_{{\cal L}(r)}$ $y$}\\[16mm]\pause
\item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause
- \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.
+ \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.\bigskip\pause
+
+ \item We also gave a direct proof, but not as beautiful.
\end{itemize}
\only<2->{%
@@ -1310,51 +1297,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
-
- \begin{center}
- \huge\bf\textcolor{gray}{in Nuprl}
- \end{center}
-
- \begin{itemize}
- \item Constable, Jackson, Naumov, Uribe\medskip
- \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode)
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
-
- \begin{center}
- \huge\bf\textcolor{gray}{in Coq}
- \end{center}
-
- \begin{itemize}
- \item Filli\^atre, Briais, Braibant and others
- \item multi-year effort; a number of results in automata theory, e.g.\medskip
- \begin{itemize}
- \item Kleene's thm.~by Filli\^atre (\alert{``rather big''})
- \item automata theory by Briais (5400 loc)
- \item Braibant ATBR library, including Myhill-Nerode\\ ($>$7000 loc)
- \item Mirkin's partial derivative automaton construction (10600 loc)
- \end{itemize}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1364,7 +1306,7 @@
\begin{itemize}
\item we have never seen a proof of Myhill-Nerode based on
- regular expressions only\smallskip\pause
+ regular expressions\smallskip\pause
\item great source of examples (inductions)\smallskip\pause
@@ -1374,9 +1316,24 @@
\item second direction (400 / 390 loc)
\end{itemize}
- \item I am not saying automata are bad; just formal proofs about
- them are quite dif$\!$ficult\pause\bigskip\medskip
+ \item I am not saying automata are bad; just proofs about
+ them are quite difficult in theorem provers\bigskip
+
+ \item \small our journal paper has just been accepted in JAR (see webpage)
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Future Work}
+
+ \begin{itemize}
+ \item regular expression sub-matching with derivatives (Martin Sulzmann PPDP'12)\bigskip
\item parsing with derivatives of grammars\\ (Matt Might ICFP'11)
\end{itemize}
@@ -1387,43 +1344,8 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE An Apology}
-
- \begin{itemize}
- \item This should all of course be done co-inductively
- \end{itemize}
-
- \footnotesize
- \begin{tabular}{@ {\hspace{4mm}}l}
- From: Jasmin Christian Blanchette\\
- To: isabelle-dev@mailbroy.informatik.tu-muenchen.de\\
- Subject: [isabelle-dev] NEWS\\
- Date: \alert{\bf Tue, 28 Aug 2012} 17:40:55 +0200\\
- \\
- * {\bf HOL/Codatatype}: New (co)datatype package with support for mixed,\\
- nested recursion and interesting non-free datatypes.\\
- \\
- * HOL/Ordinals\_and\_Cardinals: Theories of ordinals and cardinals\\
- (supersedes the AFP entry of the same name).\\[2mm]
- Kudos to Andrei and Dmitriy!\\
- \\
- Jasmin\\[-1mm]
- ------------------------------------\\
- isabelle-dev mailing list\\
- isabelle-dev@in.tum.de\\
- \end{tabular}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
\begin{frame}[b]
- \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}}
+ \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much\\ for listening!\\[5mm]Questions?}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%