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