(*<*)
theory Slides6
imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
begin
declare [[show_question_marks = false]]
notation (latex output)
set ("_") and
Cons ("_::/_" [66,65] 65)
(*>*)
text_raw {*
\renewcommand{\slidecaption}{Hefei, 15.~April 2011}
\newcommand{\abst}[2]{#1.#2}% atom-abstraction
\newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
\newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
\newcommand{\unit}{\langle\rangle}% unit
\newcommand{\app}[2]{#1\,#2}% application
\newcommand{\eqprob}{\mathrel{{\approx}?}}
\newcommand{\freshprob}{\mathrel{\#?}}
\newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
\newcommand{\id}{\varepsilon}% identity substitution
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\gr}[1]{\textcolor{gray}{#1}}
\newcommand{\rd}[1]{\textcolor{red}{#1}}
\newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}
\newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}
\newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}
\renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}
\newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}
\newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}
\newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}
\newcommand{\LL}{$\mathbb{L}\,$}
\pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
{rgb(0mm)=(0,0,0.9);
rgb(0.9mm)=(0,0,0.7);
rgb(1.3mm)=(0,0,0.5);
rgb(1.4mm)=(1,1,1)}
\def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}
\usebeamercolor[fg]{subitem projected}
{\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}
\pgftext{%
\usebeamerfont*{subitem projected}}
\end{pgfpicture}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[t]
\frametitle{%
\begin{tabular}{@ {\hspace{-3mm}}c@ {}}
\\
\LARGE Verifying a Regular Expression\\[-1mm]
\LARGE Matcher and Formal Language\\[-1mm]
\LARGE Theory\\[5mm]
\end{tabular}}
\begin{center}
Christian Urban\\
\small Technical University of Munich, Germany
\end{center}
\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{My Background}
\mbox{}\\[-10mm]
\begin{itemize}
\item My background is in theory and programming languages.\bigskip
\pause
\item But I am also a programmer with a \alert<2>{software system} of around 800 kloc
(though I am responsible for only appr.~35 kloc),
\item and I write papers.
\end{itemize}
\only<2>{
\begin{textblock}{6}(6.5,11.5)
\begin{tikzpicture}
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
{\color{darkgray}
\begin{minipage}{6.5cm}\raggedright
\begin{tabular}[b]{@ {}p{4.5cm}c@ {}}
\raggedright
The software is a theorem prover, called {\bf Isabelle}.
& \mbox{}\hspace{-5mm}\raisebox{-14mm}{\includegraphics[scale=0.28]{isabelle1.png}}
\end{tabular}%
\end{minipage}};
\end{tikzpicture}
\end{textblock}}
\only<4>{
\begin{textblock}{6}(3,11.5)
\begin{tikzpicture}
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
{\color{darkgray}
\begin{minipage}{9.6cm}\raggedright
So I can experience every day that writing error-free code is {\bf very, very hard}
and that papers are also {\bf hard} to get correct.
\end{minipage}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{3 Points}
\large
\begin{itemize}
\item It is easy to make mistakes.\bigskip
\item Theorem provers can prevent mistakes, {\bf if} the problem
is formulated so that it is suitable for theorem provers.\bigskip
\item This re-formulation can be done, even in domains where
we do not expect it.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{Getting Papers Correct}
\begin{minipage}{1.1\textwidth}
My work over the last 5 years.\\
{\small (in the fields of programming languages, logic and lambda-calculi)}
\end{minipage}\bigskip
\only<1>{
\mbox{}\\[15mm]
\begin{center}
\begin{tikzpicture}[node distance=0.5mm]
\node at (-1.0,-0.3) (proof) [double arrow, fill=gray,text=white, minimum height=2cm]{\bf Proof};
\node [left=of proof]{\Large\bf Specification};
\node [right=of proof]{\Large\bf Code};
\end{tikzpicture}
\end{center}
}
\pause
\begin{tabular}{c@ {\hspace{2mm}}c}
\begin{tabular}{c}
\includegraphics[scale=0.09]{harper.jpg}\\[-2mm]
{\footnotesize Bob Harper}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular}
\begin{tabular}{c}
\includegraphics[scale=0.31]{pfenning.jpg}\\[-2mm]
{\footnotesize Frank Pfenning}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular} &
\begin{tabular}{p{6cm}}
\raggedright\small
\color{gray}{published a proof in ACM Transactions on Computational Logic (2005),
$\sim$31pp}
\end{tabular}\\
\\[-4mm]
\begin{tabular}{c}
\includegraphics[scale=0.3]{appel.jpg}\\[-2mm]
{\footnotesize Andrew Appel}\\[-2.5mm]
{\footnotesize (Princeton)}
\end{tabular} &
\begin{tabular}{p{6cm}}
\raggedright\small
\color{gray}{relied on their proof in a safety critical system (proof carrying code)}
\end{tabular}
\end{tabular}\medskip
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{Proof-Carrying Code}
\begin{textblock}{10}(2.5,2.2)
\begin{block}{Idea:}
\begin{center}
\begin{tikzpicture}
\draw[help lines,cream] (0,0.2) grid (8,4);
\draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
\node[anchor=base] at (6.5,2.8)
{\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user needs to run untrusted code\end{tabular}};
\draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
\node[anchor=base] at (1.5,2.3)
{\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering code developer/ web server/ Apple
Store\end{tabular}};
\onslide<4->{
\draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
\node[anchor=base,white] at (6.5,1.1)
{\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
\node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
\onslide<3->{
\node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};
\node at (3.8,1.9) {\small certificate};
}
\onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}
\end{tikzpicture}
\end{center}
\end{block}
\end{textblock}
\begin{textblock}{15}(2,12)
\small
\begin{itemize}
\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions;
803 loc in C including 2 library functions)\\[-3mm]
\item<5-> 167 loc in C implement a type-checker
\end{itemize}
\end{textblock}
\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{Type-Checking in LF}
\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}
\only<7->{
\begin{textblock}{14}(0.6,12.8)
\begin{block}{}
\small Each time one needs to check $\sim$31pp~of informal paper proofs.
You have to be able to keep definitions and proofs consistent.
\end{block}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{Lessons Learned}
\begin{itemize}
\item Theorem provers help with keeping large proofs consistent;
make them modifiable.\medskip
\item They can ensure that all cases are covered.\medskip
\item Some reasoning can be automated.
\end{itemize}\bigskip\pause
\begin{minipage}{1.1\textwidth}
Formal reasoning needs to be ``smooth''.\\
{\small (ideally as close as possible to reasoning with ``pen-and-paper'')}
\end{minipage}
\only<2->{
\begin{textblock}{3}(0.1,9.9)
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=0, fill=red,text=red]{a};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
atom_decl name
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
nominal_primrec
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]")
where
"(Var x)[y::=s] = (if x=y then s else (Var x))"
| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done
lemma subst_eqvt[eqvt]:
fixes pi::"name prm"
shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
(auto simp add: perm_bij fresh_atm fresh_bij)
lemma fresh_fact:
fixes z::"name"
shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_prod fresh_atm)
lemma forget:
assumes asm: "x\<sharp>L"
shows "L[x::=P] = L"
using asm
by (nominal_induct L avoiding: x P rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_atm)
(*>*)
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\begin{textblock}{16}(1,1)
\renewcommand{\isasymbullet}{$\cdot$}
\tiny\color{black}
*}
lemma substitution_lemma_not_to_be_tried_at_home:
assumes asm: "x\<noteq>y" "x\<sharp>L"
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using asm
proof (induct M arbitrary: x y N L rule: lam.induct)
case (Lam z M1)
have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
have "x\<noteq>y" by fact
have "x\<sharp>L" by fact
obtain z'::"name" where fc: "z'\<sharp>(x,y,z,M1,N,L)" by (rule exists_fresh) (auto simp add: fs_name1)
have eq: "Lam [z'].([(z',z)]\<bullet>M1) = Lam [z].M1" using fc
by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
have fc': "z'\<sharp>N[y::=L]" using fc by (simp add: fresh_fact fresh_prod)
have "([(z',z)]\<bullet>x) \<noteq> ([(z',z)]\<bullet>y)" using `x\<noteq>y` by (auto simp add: calc_atm)
moreover
have "([(z',z)]\<bullet>x)\<sharp>([(z',z)]\<bullet>L)" using `x\<sharp>L` by (simp add: fresh_bij)
ultimately
have "M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]
= M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]]"
using ih by simp
then have "[(z',z)]\<bullet>(M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]
= M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]])"
by (simp add: perm_bool)
then have ih': "([(z',z)]\<bullet>M1)[x::=N][y::=L] = ([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]]"
by (simp add: eqvts perm_swap)
show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS")
proof -
have "?LHS = (Lam [z'].([(z',z)]\<bullet>M1))[x::=N][y::=L]" using eq by simp
also have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[x::=N][y::=L])" using fc by (simp add: fresh_prod)
also from ih have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]])" sorry
also have "\<dots> = (Lam [z'].([(z',z)]\<bullet>M1))[y::=L][x::=N[y::=L]]" using fc fc' by (simp add: fresh_prod)
also have "\<dots> = ?RHS" using eq by simp
finally show "?LHS = ?RHS" .
qed
qed (auto simp add: forget)
text_raw {*
\end{textblock}
\mbox{}
\only<2->{
\begin{textblock}{11.5}(4,2.3)
\begin{minipage}{9.3cm}
\begin{block}{}\footnotesize
*}
lemma substitution_lemma\<iota>:
assumes asm: "x \<noteq> y" "x \<sharp> L"
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using asm
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
(auto simp add: forget fresh_fact)
text_raw {*
\end{block}
\end{minipage}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[c]
\frametitle{Getting Programs Correct}
\begin{center}
\begin{tikzpicture}[node distance=0.5mm]
\node at (-1.0,-0.3) (proof) [double arrow, fill=gray,text=white, minimum height=2cm]{\bf Proof};
\node [left=of proof]{\Large\bf Specification};
\node [right=of proof]{\Large\bf Code};
\end{tikzpicture}
\end{center}
\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$ + r$_2$}\\
& \bl{$\mid$} & \bl{r$_1$ $\cdot$ 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}
\only<2>{
\begin{textblock}{9}(3.6,11.8)
\bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm]
\hspace{10mm}\begin{tikzpicture}
\coordinate (m1) at (0.4,1);
\draw (0,0.3) node (m2) {\small\color{gray}rexp};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
\coordinate (s1) at (0.81,1);
\draw (1.3,0.3) node (s2) {\small\color{gray} string};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Specification}
\small
\begin{textblock}{6}(0,3.5)
\begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
\multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\
&\bl{\LL ($\varnothing$)} & \bl{$\dn$} & \bl{$\varnothing$}\\
&\bl{\LL ([])} & \bl{$\dn$} & \bl{\{[]\}}\\
&\bl{\LL (c)} & \bl{$\dn$} & \bl{\{c\}}\\
&\bl{\LL (r$_1$ + r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\
\rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\
\rd{$\Rightarrow$} &\bl{\LL (r$^*$)} & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\
\end{tabular}
\end{textblock}
\begin{textblock}{9}(7.3,3)
{\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip}
\includegraphics[scale=0.325]{Screen3.png}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Version 1}
\small
\mbox{}\\[-8mm]\mbox{}
\begin{center}\def\arraystretch{1.05}
\begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}}
\bl{match [] []} & \bl{$=$} & \bl{true}\\
\bl{match [] (c::s)} & \bl{$=$} & \bl{false}\\
\bl{match ($\varnothing$::rs) s} & \bl{$=$} & \bl{false}\\
\bl{match ([]::rs) s} & \bl{$=$} & \bl{match rs s}\\
\bl{match (c::rs) []} & \bl{$=$} & \bl{false}\\
\bl{match (c::rs) (d::s)} & \bl{$=$} & \bl{if c = d then match rs s else false}\\
\bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\
\bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
\bl{match (r$^*$::rs) s} & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
\end{tabular}
\end{center}
\begin{textblock}{9}(0.2,1.6)
\hspace{10mm}\begin{tikzpicture}
\coordinate (m1) at (0.44,-0.5);
\draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
\coordinate (s1) at (0.86,-0.5);
\draw (1.5,0.3) node (s2) {\small\color{gray} string};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
\end{tikzpicture}
\end{textblock}
\begin{textblock}{9}(2.8,11.8)
\bl{matches$_1$ r s $\;=\;$ match [r] s}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{Testing}
\small
Every good programmer should do thourough tests:
\begin{center}
\begin{tabular}{@ {\hspace{-20mm}}lcl}
\bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
\bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
\onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\
\onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\
\onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}}
\end{tabular}
\end{center}
\onslide<3->
{looks OK \ldots let's ship it to customers\hspace{5mm}
\raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{Version 1}
\only<1->{Several hours later\ldots}\pause
\begin{center}
\begin{tabular}{@ {\hspace{0mm}}lcl}
\bl{matches$_1$ []$^*$ s} & \bl{$\mapsto$} & loops\\
\onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s} & \bl{$\mapsto$} & loops\\}
\end{tabular}
\end{center}
\small
\onslide<3->{
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
\ldots\\
\bl{match ([]::rs) s} & \bl{$=$} & \bl{match rs s}\\
\ldots\\
\bl{match (r$^*$::rs) s} & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
\end{tabular}
\end{center}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Testing}
\begin{itemize}
\item While testing is an important part in the process of programming development\pause
\item We can only test a {\bf finite} amount of examples.\bigskip\pause
\begin{center}
\colorbox{cream}
{\gr{\begin{minipage}{10cm}
``Testing can only show the presence of errors, never their
absence'' (Edsger W.~Dijkstra)
\end{minipage}}}
\end{center}\bigskip\pause
\item In a theorem prover we can establish properties that apply to
{\bf all} input and {\bf all} output.\pause
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Version 2}
\mbox{}\\[-14mm]\mbox{}
\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} & \\
\end{tabular}\medskip
\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{\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
\bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
\bl{derivative r []} & \bl{$=$} & \bl{r} & \\
\bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
\end{tabular}\medskip
\bl{matches$_2$ r s $=$ nullable (derivative r s)}
\begin{textblock}{6}(9.5,0.9)
\begin{flushright}
\color{gray}``if r matches []''
\end{flushright}
\end{textblock}
\begin{textblock}{6}(9.5,6.18)
\begin{flushright}
\color{gray}``derivative w.r.t.~a char''
\end{flushright}
\end{textblock}
\begin{textblock}{6}(9.5,12.1)
\begin{flushright}
\color{gray}``deriv.~w.r.t.~a string''
\end{flushright}
\end{textblock}
\begin{textblock}{6}(9.5,13.98)
\begin{flushright}
\color{gray}``main''
\end{flushright}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Is the Matcher Error-Free?}
We expect that
\begin{center}
\begin{tabular}{lcl}
\bl{matches$_2$ r s = true} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
\only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
\bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
\only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
\end{tabular}
\end{center}
\pause\pause\bigskip
By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
\begin{tabular}{lrcl}
Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
& \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
\end{tabular}
\only<4->{
\begin{textblock}{3}(0.9,4.5)
\rd{\huge$\forall$\large{}r s.}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[c]
\frametitle{
\begin{tabular}{c}
\mbox{}\\[23mm]
\LARGE Demo
\end{tabular}}
\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 (CHR c)} & \bl{$=$} & \bl{false} &\\
\bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\
\bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
\bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\
\end{tabular}\medskip
\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 (CHR 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\\
\bl{derivative r []} & \bl{$=$} & \bl{r} & \\
\bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
\end{tabular}\medskip
\bl{matches r s $=$ nullable (derivative r s)}
\only<2>{
\begin{textblock}{8}(1.5,4)
\includegraphics[scale=0.3]{approved.png}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{No Automata?}
You might be wondering why I did not use any automata:
\begin{itemize}
\item A \alert{regular language} is one where there is a DFA that
recognises it.\bigskip\pause
\end{itemize}
There are many reasons why this is a good definition:\medskip
\begin{itemize}
\item pumping lemma
\item closure properties of regular languages\\ (e.g.~closure under complement)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{Really Bad News!}
DFAs are bad news for formalisations in theorem provers. They might
be represented as:
\begin{itemize}
\item graphs
\item matrices
\item partial functions
\end{itemize}
All constructions are messy to reason about.\bigskip\bigskip
\pause
\small
\only<2>{
Constable et al needed (on and off) 18 months for a 3-person team
to formalise automata theory in Nuprl including Myhill-Nerode. There is
only very little other formalised work on regular languages I know of
in Coq, Isabelle and HOL.}
\only<3>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
automata with no inaccessible states \ldots''
}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\large
\begin{center}
\begin{tabular}{p{9cm}}
My point:\bigskip\\
The theory about regular languages can be reformulated
to be more suitable for theorem proving.
\end{tabular}
\end{center}
\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 (pumping lemma only necessary)\medskip
\item will help with closure properties of regular languages\bigskip\pause
\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}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Myhill-Nerode Theorem}
\mbox{}\\[5cm]
\begin{itemize}
\item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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}
\item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M}
such that \smath{\mathbb{L}(M) = L}\\[1.5cm]
\item Myhill-Nerode:
\begin{center}
\begin{tabular}{l}
finite $\Rightarrow$ regular\\
\;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]
regular $\Rightarrow$ finite\\
\;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Final States}
\mbox{}\\[3cm]
\begin{itemize}
\item \smath{\text{final}_L\,X \dn}\\
\smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L}
\smallskip
\item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
\smath{L = \{[c]\}}
\begin{tabular}{@ {\hspace{-7mm}}cc}
\begin{tabular}{c}
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (q_0) {$R_1$};
\node[state,accepting] (q_1) [above right of=q_0] {$R_2$};
\node[state] (q_2) [below right of=q_0] {$R_3$};
\path[->] (q_0) edge node {c} (q_1)
edge node [swap] {$\Sigma-{c}$} (q_2)
(q_2) edge [loop below] node {$\Sigma$} ()
(q_1) edge node {$\Sigma$} (q_2);
\end{tikzpicture}
\end{tabular}
&
\begin{tabular}[t]{ll}
\\[-20mm]
\multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
\smath{R_1}: & \smath{\{[]\}}\\
\smath{R_2}: & \smath{\{[c]\}}\\
\smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
\multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}
\end{tabular}
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Systems of Equations}
Inspired by a method of Brzozowski\;'64, we can build an equational system
characterising the equivalence classes:
\begin{center}
\begin{tabular}{@ {\hspace{-20mm}}c}
\\[-13mm]
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (p_0) {$R_1$};
\node[state,accepting] (p_1) [right of=q_0] {$R_2$};
\path[->] (p_0) edge [bend left] node {a} (p_1)
edge [loop above] node {b} ()
(p_1) edge [loop above] node {a} ()
edge [bend left] node {b} (p_0);
\end{tikzpicture}\\
\\[-13mm]
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
& \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
& \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
\onslide<3->{we can prove}
& \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
& \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\
& \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
& \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[t]
\small
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; a + R_2; a}}\\
& & & \onslide<2->{by Arden}\\
\onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
& \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
& \only<2>{\smath{R_1; a + R_2; a}}%
\only<3->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<4->{by Arden}\\
\onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<5->{by substitution}\\
\onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<6->{by Arden}\\
\onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<7->{by substitution}\\
\onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
\cdot a\cdot a^\star}}\\
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE A Variant of Arden's Lemma}
{\bf Arden's Lemma:}\smallskip
If \smath{[] \not\in A} then
\begin{center}
\smath{X = X; A + \text{something}}
\end{center}
has the (unique) solution
\begin{center}
\smath{X = \text{something} ; A^\star}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\small
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; a + R_2; a}}\\
& & & \onslide<2->{by Arden}\\
\onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
& \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
& \only<2>{\smath{R_1; a + R_2; a}}%
\only<3->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<4->{by Arden}\\
\onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<5->{by substitution}\\
\onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<6->{by Arden}\\
\onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<7->{by substitution}\\
\onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
\cdot a\cdot a^\star}}\\
\end{tabular}
\end{center}
\only<8->{
\begin{textblock}{6}(2.5,4)
\begin{block}{}
\begin{minipage}{8cm}\raggedright
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (p_0) {$R_1$};
\node[state,accepting] (p_1) [right of=q_0] {$R_2$};
\path[->] (p_0) edge [bend left] node {a} (p_1)
edge [loop above] node {b} ()
(p_1) edge [loop above] node {a} ()
edge [bend left] node {b} (p_0);
\end{tikzpicture}
\end{minipage}
\end{block}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Equ's Solving Algorithm}
\begin{itemize}
\item The algorithm must terminate: Arden makes one equation smaller;
substitution deletes one variable from the right-hand sides.\bigskip
\item We need to maintain the invariant that Arden is applicable
(if \smath{[] \not\in A} then \ldots):\medskip
\begin{center}\small
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
\smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\
& & & by Arden\\
\smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
\smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Other Direction}
One has to prove
\begin{center}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
\end{center}
by induction on \smath{r}. Not trivial, but after a bit
of thinking, one can prove that if
\begin{center}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
\end{center}
then
\begin{center}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE What Have We Achieved?}
\begin{itemize}
\item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
\bigskip\pause
\item regular languages are closed under complementation; this is now easy\medskip
\begin{center}
\smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
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 {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE What We Have Not Achieved}
\begin{itemize}
\item regular expressions are not good if you look for a minimal
one for a language (DFAs have this notion)\pause\bigskip
\item Is there anything to be said about context free languages:\medskip
\begin{quote}
A context free language is where every string can be recognised by
a pushdown automaton.\bigskip
\end{quote}
\end{itemize}
\textcolor{gray}{\footnotesize Yes. Derivatives also work for c-f grammars. Ongoing work.}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Conclusion}
\begin{itemize}
\item We formalised the Myhill-Nerode theorem based on
regular expressions only (DFAs are difficult to deal with in a theorem prover).\smallskip
\item Seems to be a common theme: algorithms need to be reformulated
to better suit formal treatment.\smallskip
\item The most interesting aspect is that we are able to
implement the matcher directly inside the theorem prover
(ongoing work).\smallskip
\item Parsing is a vast field which seem to offer new results.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[b]
\frametitle{
\begin{tabular}{c}
\mbox{}\\[13mm]
\alert{\LARGE Thank you very much!}\\
\alert{\Large Questions?}
\end{tabular}}
\begin{center}
\bf \underline{Short Bio:}
\end{center}
\mbox{}\\[-17mm]\mbox{}\small
\begin{itemize}
\item PhD in Cambridge
\item Emmy-Noether Research Fellowship at the TU Munich
\item talks at: CMU, Yale, Princeton, MIT,$\ldots$
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Future Research}
My existing strengths:\bigskip
\begin{itemize}
\item Isabelle (implementation)\bigskip
\item background in logic, programming languages, formal methods
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Future Research}
I want to have a single logic framework in which I can
write programs and prove their correctness.\bigskip
\begin{itemize}
\item extensions of HOL (IO, modules, advanced types)
\item high-level programming languages
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Future Research}
Compilers\bigskip
\begin{itemize}
\item the high-level language needs to be compiled to correct machine
code
\item compiler verification, machine code verification
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Future Research}
Stronger type-systems\bigskip
\begin{itemize}
\item ``correct by construction''
\item GADTs, dependent types
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Future Research}
Proof automation\bigskip
\begin{itemize}
\item external tools generate ``proof-certificates''
\item certificates are imported into Isabelle
\item GPU based external provers
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Future Research}
Large-scale applications\bigskip
\begin{itemize}
\item verification of Java-Script, Scala,$\ldots$
\item interesting code (INTEL in Shanghai)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)