(*<*)

theory Slides4

imports "~~/src/HOL/Library/LaTeXsugar"

begin

notation (latex output)

  set ("_") and

  Cons  ("_::/_" [66,65] 65) 

(*>*)

text_raw {*

  \renewcommand{\slidecaption}{Edinburgh, 21 February 2012}

  \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}};}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \LARGE Formalising\\[-3mm] 

  \LARGE Regular Language Theory\\[-3mm] 

  \LARGE with Regular Expressions,\\[-3mm] 

  \LARGE \alert<2>{Only}\\[0mm] 

  \end{tabular}}

  \begin{center}

   Christian Urban\\

  \small King's College London

  \end{center}\bigskip

  \begin{center}

  \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA

  University of Science and Technology in Nanjing

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1->[c]

  \frametitle{}

  \mbox{}\\[-10mm]

  \begin{itemize}

  \item My background is in 

  \begin{itemize}

  \item \normalsize theorem provers

  \item \normalsize develop Nominal Isabelle

  \end{itemize}\bigskip\bigskip  

  \item<1->to formalise and mechanically check proofs from 

  programming language research and TCS\bigskip

  \item<2->our biggest success story \ldots 

  \end{itemize}

  \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{}

  \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} &

  \begin{tabular}{p{6cm}}

  \raggedright

  \color{gray}{published a proof 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}

  \end{tabular}

  \end{tabular}

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

  \begin{frame}[c]

  \frametitle{}

  \begin{itemize}

  \item I also found fixable errors in my Ph.D.-thesis about cut-elimination

  (examined by Henk Barendregt and Andy Pitts)

  \item flaws in PIP (OS); a theorem without a shred of evidence (algorithms)

  \end{itemize}\bigskip\bigskip

  {\bf Conclusion:}\smallskip

  Pencil-and-paper proofs in TCS are not foolproof, 

  not even expertproof.

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

  \frametitle{\begin{tabular}{@ {}c@ {}}

  \large Nipkow about Teaching Proofs in TCS:\hspace{3cm}\mbox{}\\[-4mm]

  \large \textcolor{red}{``London Underground Phenomenon''}\\[-18mm]\mbox{}

  \end{tabular}}

  \begin{center}

  \begin{tabular}{ccc}

  students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs

  \end{tabular}

  \end{center}

  \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}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{}

  \begin{itemize}

  \item part of the problem is teaching the obvious\medskip

  \begin{center}

  \smath{\infer{A \vdash A}{}}

  \end{center}\bigskip\bigskip

  \item teach proofs, not logic

  \item students having too little practice and no good literature for how to do proofs\\

  \textcolor{gray}{\small(Velleman is too mathematics oriented)}

  \bigskip\bigskip\pause

  \item proof assistants lead to abundant practice because they are 

  addictive like video games (Nipkow, Pierce)\\

   \textcolor{gray}{\small(in the past they were just frustrating, but they got much better)}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1->[t]

  \frametitle{Regular Expressions}

  \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$^*$}\\

  \end{tabular}

  \end{textblock}

  \begin{textblock}{6}(8,3.5)

  \includegraphics[scale=0.35]{Screen1.png}

  \end{textblock}

  \begin{textblock}{6}(10.2,2.8)

  \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}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1->[t]

  \mbox{}\\[-2mm]

  \small

  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}

  \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\

  \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\

  \bl{nullable (CHAR c)}           & \bl{$=$} & \bl{false} &\\

  \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ 

  \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\

  \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\

  \end{tabular}\medskip\pause

  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}

  \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\

  \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\

  \bl{der c (CHAR d)}           & \bl{$=$} & \bl{if c $=$ d then EMPTY else NULL} & \\

  \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\

  \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\

       &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\

  \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\\pause

  \bl{derivative [] r}     & \bl{$=$} & \bl{r} & \\

  \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\

  \end{tabular}\medskip

  \bl{matches r s $=$ nullable (derivative s r)}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

  \mbox{}\\[-15mm]\mbox{}

  \begin{center}

  \huge\bf\textcolor{gray}{in Theorem Provers}\\

  \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

  \end{center}

  \begin{itemize}

  \item automata @{text "\<Rightarrow>"} graphs, matrices, functions

  \item<2-> combining automata / graphs

  \onslide<2->{

  \begin{center}

  \begin{tabular}{ccc}

  \begin{tikzpicture}[scale=1]

  %\draw[step=2mm] (-1,-1) grid (1,1);

  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \draw (-0.6,0.0) node {\small$A_1$};

  \draw ( 0.6,0.0) node {\small$A_2$};

  \end{tikzpicture}}

  & 

  \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}}

  &

  \onslide<3->{\begin{tikzpicture}[scale=1]

  %\draw[step=2mm] (-1,-1) grid (1,1);

  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

  \draw [very thick, red] (C) to [bend left=45] (B);

  \draw [very thick, red] (D) to [bend right=45] (B);

  \draw (-0.6,0.0) node {\small$A_1$};

  \draw ( 0.6,0.0) node {\small$A_2$};

  \end{tikzpicture}}

  \end{tabular}

  \end{center}\medskip

  \only<4-5>{

  \begin{tabular}{@ {\hspace{-5mm}}l@ {}}

  disjoint union:\\[2mm]

  \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}}

  \end{tabular}}

  \end{itemize}

  \only<5>{

  \begin{textblock}{13.9}(0.7,7.7)

  \begin{block}{}

  \medskip

  \begin{minipage}{14cm}\raggedright

  Problems with definition for regularity:\bigskip\\

  \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip

  \end{minipage}

  \end{block}

  \end{textblock}}

  \medskip

  \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}

  \only<7->{You have to \alert{rename} states!}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

  \mbox{}\\[-15mm]\mbox{}

  \begin{center}

  \huge\bf\textcolor{gray}{in Theorem Provers}\\

  \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

  \end{center}

  \begin{itemize}

  \item Kozen's paper proof of Myhill-Nerode:\\ 

  requires absence of \alert{inaccessible states}

  \item complementation of automata only works for \alert{complete} automata

  (need sink states)\medskip

  \end{itemize}\bigskip\bigskip

  \begin{center}

  \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

  \frametitle{}

  \mbox{}\\[25mm]\mbox{}

  \begin{textblock}{13.9}(0.7,1.2)

  \begin{block}{}

  \begin{minipage}{13.4cm}\raggedright

  {\bf Definition:}\smallskip\\

  A language \smath{A} is \alert{regular}, provided there exists a\\ 

  \alert{regular expression} that matches all strings of \smath{A}.

  \end{minipage}

  \end{block}

  \end{textblock}\pause

  {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause

  Infrastructure for free. But do we lose anything?\medskip\pause

  \begin{minipage}{1.1\textwidth}

  \begin{itemize}

  \item pumping lemma\pause

  \item closure under complementation\pause

  \item \only<6>{regular expression matching}%

       \only<7->{\sout{regular expression matching}

  {\footnotesize(@{text "\<Rightarrow>"}Brozowski'64, Owens et al '09)}}

  \item<8-> most textbooks are about automata

  \end{itemize}

  \end{minipage}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{\LARGE The Myhill-Nerode Theorem}

  \begin{itemize}

  \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

  \begin{center}

  \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}