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