\documentclass[dvipsnames,14pt,t]{beamer}+
−
\usepackage{../slides}+
−
\usepackage{../langs}+
−
\usepackage{../data}+
−
\usepackage{../graphicss}+
−
\usepackage{soul}+
−
\usepackage{proof}+
−
+
−
% beamer stuff+
−
\renewcommand{\slidecaption}{CFL, King's College London}+
−
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       +
−
+
−
%\newcommand\grid[1]{%+
−
%	\begin{tikzpicture}[baseline=(char.base)]+
−
%	\path[use as bounding box]+
−
%	(0,0) rectangle (1em,1em);+
−
%	\draw[red!50, fill=red!20]+
−
%	(0,0) rectangle (1em,1em);+
−
%	\node[inner sep=1pt,anchor=base west]+
−
%	(char) at (0em,\gridraiseamount) {#1};+
−
%	\end{tikzpicture}}+
−
%\newcommand\gridraiseamount{0.12em}+
−
+
−
%\makeatletter+
−
%\newcommand\Grid[1]{%+
−
%	\@tfor\z:=#1\do{\grid{\z}}}+
−
%\makeatother	+
−
+
−
%\newcommand\Vspace[1][.3em]{%+
−
%	\mbox{\kern.06em\vrule height.3ex}%+
−
%	\vbox{\hrule width#1}%+
−
%	\hbox{\vrule height.3ex}}+
−
+
−
%\def\VS{\Vspace[0.6em]}+
−
+
−
+
−
\begin{document}+
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[t]+
−
\frametitle{%+
−
  \begin{tabular}{@ {}c@ {}}+
−
  \\[-3mm]+
−
  \LARGE Compilers and \\[-2mm] +
−
  \LARGE Formal Languages\\[3mm] +
−
  \end{tabular}}+
−
+
−
  \normalsize+
−
  \begin{center}+
−
  \begin{tabular}{ll}+
−
  Email:  & christian.urban at kcl.ac.uk\\+
−
  Office: & N7.07 (North Wing, Bush House)\\+
−
  Slides: & KEATS (also home work is there)\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\frametitle{Compilers \& Boeings 777}+
−
+
−
First flight in 1994. They want to achieve triple redundancy in hardware+
−
faults.\bigskip+
−
+
−
They compile 1 Ada program to\medskip+
−
+
−
\begin{itemize}+
−
\item Intel 80486+
−
\item Motorola 68040 (old Macintosh's)+
−
\item AMD 29050 (RISC chips used often in laser printers)+
−
\end{itemize}\medskip+
−
+
−
using 3 independent compilers.\bigskip\pause+
−
+
−
\small Airbus uses C and static analysers. Recently started using CompCert.+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\frametitle{seL4 / Isabelle}+
−
+
−
\begin{itemize}+
−
\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip+
−
\item US DoD has competitions to hack into drones; they found that the+
−
  isolation guarantees of seL4 hold up\bigskip+
−
\item CompCert and seL4 sell their code  +
−
\end{itemize}+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\frametitle{POSIX Matchers}+
−
+
−
\begin{itemize}+
−
\item Longest match rule (``maximal munch rule''): The +
−
longest initial substring matched by any regular expression +
−
is taken as the next token.+
−
+
−
\begin{center}+
−
\bl{$\texttt{\Grid{iffoo\VS bla}}$}+
−
\end{center}\medskip+
−
+
−
\item Rule priority:+
−
For a particular longest initial substring, the first regular+
−
expression that can match determines the token.+
−
+
−
\begin{center}+
−
\bl{$\texttt{\Grid{if\VS bla}}$}+
−
\end{center}+
−
\end{itemize}\bigskip\pause+
−
+
−
\small+
−
\hfill Kuklewicz: most POSIX matchers are buggy\\+
−
\footnotesize+
−
\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\mbox{}\\[-14mm]\mbox{}+
−
\small+
−
\bl{+
−
\begin{center}+
−
\begin{tabular}{lcl}+
−
$\textit{der}\;c\;(\ZERO)$ & $\dn$ & $\ZERO$\\+
−
$\textit{der}\;c\;(\ONE)$  & $\dn$ & $\ZERO$\\+
−
$\textit{der}\;c\;(d)$     & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;\ONE \; \textit{else} \;\ZERO$\\+
−
$\textit{der}\;c\;(r_1 + r_2)$ & $\dn$ & $(\textit{der}\;c\;r_1) + (\textit{der}\;c\;r_2)$\\+
−
$\textit{der}\;c\;(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\+
−
      & & $\textit{then}\;((\textit{der}\;c\;r_1)\cdot r_2) + (\textit{der}\;c\;r_2)$\\+
−
      & & $\textit{else}\;(\textit{der}\;c\;r_1)\cdot r_2$\\+
−
$\textit{der}\;c\;(r^*)$ & $\dn$ & $(\textit{der}\;c\;r)\cdot (r^*)$\\+
−
  $\textit{der}\;c\;(r^{\{n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\+
−
  & & \textit{else if} $\textit{nullable}(r)$ \textit{then} $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\+
−
  & & \textit{else} $(\textit{der}\;c\;r)\cdot (r^{\{n-1\}})$\\+
−
  $\textit{der}\;c\;(r^{\{\uparrow n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\+
−
  & & \textit{else}+
−
  $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\+
−
\end{tabular}+
−
\end{center}}+
−
  +
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[t]+
−
\frametitle{Proofs about Rexps}+
−
+
−
Remember their inductive definition:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{@ {}rrl}+
−
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\+
−
         & \bl{$\mid$} & \bl{$\ONE$}     \\+
−
         & \bl{$\mid$} & \bl{$c$}            \\+
−
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\+
−
         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\+
−
         & \bl{$\mid$} & \bl{$r^*$}          \\+
−
         & \bl{$\mid$} & \bl{$r^{\{n\}}$}     \\+
−
         & \bl{$\mid$} & \bl{$r^{\{\uparrow n\}}$}     \\+
−
  \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{$\ZERO$}, \bl{$\ONE$} 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$}.+
−
\item \ldots+
−
\end{itemize}+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\frametitle{Proofs about Strings}+
−
+
−
If we want to prove something, say a property \bl{$P(s)$}, for all+
−
strings \bl{$s$} then \ldots\bigskip+
−
+
−
\begin{itemize}+
−
\item \bl{$P$} holds for the empty string, and\medskip+
−
\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}+
−
already holds for \bl{$s$}+
−
\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{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}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\frametitle{POSIX Spec}+
−
+
−
\begin{center}+
−
\bl{\infer{[] \in \ONE \to Empty}{}}\hspace{15mm}+
−
\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip+
−
+
−
\bl{\infer{s \in r_1 + r_2 \to Left(v)}+
−
          {s \in r_1 \to v}}\hspace{10mm}+
−
\bl{\infer{s \in r_1 + r_2 \to Right(v)}+
−
          {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip+
−
+
−
\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}+
−
          {\small\begin{array}{l}+
−
           s_1 \in r_1 \to v_1 \\+
−
           s_2 \in r_2 \to v_2 \\+
−
           \neg(\exists s_3\,s_4.\; s_3 \not= []+
−
           \wedge s_3 @ s_4 = s_2 \wedge+
−
           s_1 @ s_3 \in L(r_1) \wedge+
−
           s_4 \in L(r_2))+
−
           \end{array}}}+
−
           +
−
\bl{\ldots}           +
−
\end{center}+
−
+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[t,squeeze]+
−
\frametitle{Sulzmann \& Lu Paper}+
−
+
−
\begin{itemize}+
−
\item I have no doubt the algorithm is correct --- +
−
  the problem is I do not believe their proof.+
−
+
−
  \begin{center}+
−
  \begin{bubble}[10cm]\small+
−
  ``How could I miss this? Well, I was rather careless when +
−
  stating this Lemma :)\smallskip+
−
 +
−
  Great example how formal machine checked proofs (and +
−
  proof assistants) can help to spot flawed reasoning steps.''+
−
  \end{bubble}+
−
  \end{center}\pause+
−
  +
−
  %\begin{center}+
−
  %\begin{bubble}[10cm]\small+
−
  %``Well, I don't think there's any flaw. The issue is how to +
−
  %come up with a mechanical proof. In my world mathematical +
−
  %proof $=$ mechanical proof doesn't necessarily hold.''+
−
  %\end{bubble}+
−
  %\end{center}\pause+
−
  +
−
\end{itemize}+
−
+
−
  \only<3>{%+
−
  \begin{textblock}{11}(1,4.4)+
−
  \begin{center}+
−
  \begin{bubble}[10.9cm]\small\centering+
−
  \includegraphics[scale=0.37]{../pics/msbug.png}+
−
  \end{bubble}+
−
  \end{center}+
−
  \end{textblock}}+
−
  +
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +
−
+
−
\end{document}+
−
+
−
%%% Local Variables:  +
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End: +
−
+
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\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{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}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−