(*<*)
theory Slides8
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}{Copenhagen, 23rd~May 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}[c]
\frametitle{This Talk: 4 Points}
\large
\begin{itemize}
\item It is easy to make mistakes.\medskip
\item Theorem provers can prevent mistakes, {\bf if} the problem
is formulated so that it is suitable for theorem provers.\medskip
\item This re-formulation can be done, even in domains where
we least expect it.\medskip
\item Where theorem provers are superior to the {\color{gray}{(best)}} human reasoners. ;o)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{tabular}{c@ {\hspace{2mm}}c}
\\[6mm]
\begin{tabular}{c}
\includegraphics[scale=0.12]{harper.jpg}\\[-2mm]
{\footnotesize Bob Harper}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular}
\begin{tabular}{c}
\includegraphics[scale=0.36]{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_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: 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 developer ---\\ web server\end{tabular}};
\onslide<3->{
\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<2->{
\node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};
\node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof in LF}};
}
\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{}
\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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
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{Lesson Learned}
\begin{textblock}{11.5}(1.2,5)
\begin{minipage}{10.5cm}
\begin{block}{}
Theorem provers can keep large proofs and definitions consistent and
make them modifiable.
\end{block}
\end{minipage}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{}
\begin{textblock}{11.5}(0.8,2.3)
\begin{minipage}{11.2cm}
In most papers/books:
\begin{block}{}
\color{darkgray}
``\ldots this necessary hygienic discipline is somewhat swept under the carpet via
the so-called `{\bf variable convention}' \ldots
The {\color{black}{\bf belief}} that this is {\bf sound} came from the calculus
with nameless binders in de Bruijn''
\end{block}\medskip
\end{minipage}
\end{textblock}
\begin{textblock}{11.5}(0.8,10)
\includegraphics[scale=0.25]{LambdaBook.jpg}\hspace{-3mm}\includegraphics[scale=0.3]{barendregt.jpg}
\end{textblock}
\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$_1$ (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
\onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\
\onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\
\onslide<2->{\bl{matches$_1$ 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->[c]
\frametitle{Testing}
\begin{itemize}
\item We can only test a {\bf finite} amount of examples:\bigskip
\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.
\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 {\bf Def.:} 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 Equiv.~Classes}
\mbox{}\\[3cm]
\begin{itemize}
\item \smath{\text{finals}\,L \dn
\{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\
\medskip
\item we can prove: \smath{L = \bigcup (\text{finals}\,L)}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Transitions between ECs}
\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}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)