# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1570700583 -3600
# Node ID 652065f55d54f0b33e60aa376ac714771f12d153
# Parent  3031e3379ea3f944e9c9188ee24a0e826a8ed4ec
updated

diff -r 3031e3379ea3 -r 652065f55d54 slides/slides03.pdf
Binary file slides/slides03.pdf has changed
diff -r 3031e3379ea3 -r 652065f55d54 slides/slides03.tex
--- a/slides/slides03.tex	Wed Oct 09 21:37:17 2019 +0100
+++ b/slides/slides03.tex	Thu Oct 10 10:43:03 2019 +0100
@@ -1,3 +1,4 @@
+% !TEX program = xelatex
 \documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{../slides}
 \usepackage{../graphics}
@@ -24,12 +25,13 @@
   \LARGE Formal Languages (3)\\[3mm] 
   \end{tabular}}
 
-\normalsize
+  \normalsize
   \begin{center}
-  \begin{tabular}{lp{8cm}}
-  Email:  & christian.urban at kcl.ac.uk\\
-  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
-  Slides: & KEATS (also homework and coursework is there)\\
+  \begin{tabular}{ll}
+    Email:  & christian.urban at kcl.ac.uk\\
+    Office Hours: & Thursdays 12 -- 14\\
+    Location: & N7.07 (North Wing, Bush House)\\
+    Slides \& Progs: & KEATS (also homework is there)\\  
   \end{tabular}
   \end{center}
 
@@ -151,7 +153,23 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+  \frametitle{Proofs about Rexp}
+  
+  \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$}.
+  \end{itemize}
+  
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
@@ -173,36 +191,6 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-
-We need to prove
-
-\begin{center}
-\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
-\end{center}
-
-also by induction on the regular expression \bl{$r$}.
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Proofs about Rexps}
-
-\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$}.
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
 \frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
 
 \begin{itemize}
@@ -220,9 +208,55 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
+  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+  \frametitle{Correctness Proof \\[-1mm]
+              for our Matcher}
+  
+  \begin{itemize}
+  \item We started from
+  
+  \begin{center}
+  \begin{tabular}{rp{4cm}}
+    & \bl{$s \in L(r)$}\medskip\\
+  \bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
+  \end{tabular}
+  \end{center}\bigskip
+  
+  \item \textbf{\alert{if}} we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
+  have\bigskip
+  
+  \begin{center}
+  \begin{tabular}{rp{4cm}}
+  \bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
+  \bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
+  \bl{$\dn$} & \bl{$matches\,s\,r$}
+  \end{tabular}
+  \end{center}
+  
+  \end{itemize}
+  
+  \end{frame}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+
+We need to prove
+
+\begin{center}
+\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
+\end{center}
+
+also by induction on the regular expression \bl{$r$}.
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
-\frametitle{Regular Expressions}
+\frametitle{(Basic) Regular Expressions}
 
 \begin{center}
    \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
@@ -243,26 +277,6 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-\frametitle{Negation of Regular Expr's}
-
-\begin{itemize}
-\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
-\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
-\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
-\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
-\end{itemize}\bigskip\pause
-
-Used often for recognising comments:
-
-\[
-\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
-\]
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
 \frametitle{Negation}
 
 Assume you have an alphabet consisting of the letters \bl{$a$}, \bl{$b$} and \bl{$c$} only.
@@ -548,7 +562,7 @@
 \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 \node[state, initial, accepting]  (Q_0)  {$\mbox{}$};
 \end{tikzpicture}\\\\
-\raisebox{2mm}{\bl{$c$}} & 
+\raisebox{5mm}{\bl{$c$}} & 
 \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 \node[state, initial]  (Q_0)  {$\mbox{}$};
 \node[state, accepting]  (Q_1)  [right=of Q_0] {$\mbox{}$};