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