\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../data}
\usepackage{../graphics}
\usepackage{soul}


% beamer stuff
\renewcommand{\slidecaption}{AFL, King's College London}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       


\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[-3mm]
  \LARGE Automata and \\[-2mm] 
  \LARGE Formal Languages\\[3mm] 
  \end{tabular}}

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Office: & S1.27 (1st floor Strand Building)\\
  Slides: & KEATS (also home work is there)\\
  \end{tabular}
  \end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{2nd CW}

Remember we showed that\\

\begin{center}
\bl{$der\;c\;(r^+) = (der\;c\;r)\cdot r^*$}
\end{center}\bigskip\pause


Does the same hold for \bl{$r^{\{n\}}$} with \bl{$n > 0$}

\begin{center}
\bl{$der\;c\;(r^{\{n\}}) = (der\;c\;r)\cdot r^{\{n-1\}}$} ?
\end{center}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{2nd CW}

\begin{itemize}
\item \bl{$der$}

\begin{center}
\bl{$der\;c\;(r^{\{n\}}) \dn 
\begin{cases}
\varnothing & \text{\textcolor{black}{if}}\; n = 0\\
der\;c\;(r\cdot r^{\{n-1\}}) & \text{\textcolor{black}{o'wise}}
\end{cases}$} 
\end{center}

\item \bl{$mkeps$}

\begin{center}
\bl{$mkeps(r^{\{n\}}) \dn
[\underbrace{mkeps(r),\ldots,mkeps(r)}_{n\;times}]$} 
\end{center}

\item \bl{$inj$}

\begin{center}
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
\bl{$inj\;r^{\{n\}}\;c\;(v_1, [vs])$}     & \bl{$\dn$} &
\bl{$[inj\;r\;c\;v_1::vs]$}\\
\bl{$inj\;r^{\{n\}}\;c\;Left(v_1, [vs])$} & \bl{$\dn$} &
\bl{$[inj\;r\;c\;v_1::vs]$}\\
\bl{$inj\;r^{\{n\}}\;c\;Right([v::vs])$}  & \bl{$\dn$} &
\bl{$[mkeps(r)::inj\;r\;c\;v::vs]$}\\
\end{tabular}
\end{center}

\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Compilers in Boeings 777}

They want to achieve triple redundancy in hardware
faults.\bigskip

They compile 1 Ada program to

\begin{itemize}
\item Intel 80486
\item Motorola 68040 (old Macintosh's)
\item AMD 29050 (RISC chips used often in laser printers)
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Proofs about Rexps}

Remember their inductive definition:

  \begin{center}
  \begin{tabular}{@ {}rrl}
  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\
         & \bl{$\mid$} & \bl{$\epsilon$}     \\
         & \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{center}

If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Rexp (2)}

\begin{itemize}
\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
holds for \bl{$r$}.
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\bl{\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
$zeroable(\varnothing)$      & $\dn$ & \textit{true}\\
$zeroable(\epsilon)$         & $\dn$ &  \textit{false}\\
$zeroable (c)$               & $\dn$ &  \textit{false}\\
$zeroable (r_1 + r_2)$       & $\dn$ &  $zeroable(r_1) \wedge zeroable(r_2)$ \\ 
$zeroable (r_1 \cdot r_2)$   & $\dn$ &  $zeroable(r_1) \vee zeroable(r_2)$ \\
$zeroable (r^*)$             & $\dn$ & \textit{false}\\
\end{tabular}
\end{center}}

\begin{center}
\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Correctness of the Matcher}

\begin{itemize}
\item We want to prove\medskip
\begin{center}
\bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$}
\end{center}\bigskip

where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$}
\bigskip\pause

\item We can do this, if we know\medskip
\begin{center}
\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}
\end{center}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Induction over Strings}

\begin{itemize}
\item case \bl{$[]$}:\bigskip

We need to prove 

\begin{center}
  \bl{$\forall r.\;\;nullable(ders\;[]\;r) \;\Leftrightarrow\; [] \in L(r)$}
\end{center}\bigskip  
  
\begin{center}
  \bl{$nullable(ders\;[]\;r) \;\dn\; nullable\;r \;\Leftrightarrow\ldots$}
\end{center} 
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Induction over Strings}

\begin{itemize}
\item case \bl{$c::s$}\bigskip

We need to prove 

\begin{center}
  \bl{$\forall r.\;\;nullable(ders\;(c::s)\;r) \;\Leftrightarrow\; (c::s) \in L(r)$}
\end{center} 

We have by IH

\begin{center}
  \bl{$\forall r.\;\;nullable(ders\;s\;r) \;\Leftrightarrow\; s \in L(r)$}
\end{center}\bigskip 

\begin{center}
\bl{$ders\;(c::s)\;r \dn ders\;s\;(der\;c\;r)$}
\end{center}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Induction over Regexps}

\begin{itemize}
\item The proof hinges on the fact that we can prove\bigskip

\begin{center}
  \Large\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}
\end{center} 
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Some Lemmas}

\begin{itemize}
\item \bl{$Der\;c\;(A\cup B) = 
(Der\;c\;A)\cup(Der\;c\;B)$}\bigskip
\item If \bl{$[] \in A$} then
\begin{center}
\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$}
\end{center}\bigskip
\item If \bl{$[] \not\in A$} then
\begin{center}
\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$}
\end{center}\bigskip
\item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\
\small\mbox{}\hfill (interesting case)\\
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Why?}

Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold?
\bigskip


\begin{center}
\begin{tabular}{lcl}
\bl{$Der\;c\;(A^*)$} & \bl{$=$} &  \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\
& \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\
& \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\
& \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\
\end{tabular}
\end{center}\bigskip\bigskip

\small
using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\
\mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   



\end{document}

%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: