Binary file hws/proof.pdf has changed

--- a/hws/proof.tex	Thu Nov 26 12:55:59 2015 +0000
+++ b/hws/proof.tex	Fri Nov 27 12:08:29 2015 +0000
@@ -188,15 +188,12 @@
 
 \end{itemize}
 
-
-
-
 Let us now analyse $Der\,c\,L(r^*)$, which is equal to $Der\,c\,((L(r))^*)$. Now $(L(r))^*$ is defined
-as $\bigcup_{n \ge 0} L(r)$. We can write this as $L(r)^0 \cup \bigcup_{n \ge 1} L(r)$, where we just 
+as $\bigcup_{n \ge 0} L(r)^n$. We can write this as $L(r)^0 \cup \bigcup_{n \ge 1} L(r)^n$, where we just 
 separated the first union and then let the ``big-union'' start from $1$. Form this we can already infer
 
 \begin{center}
-$Der\,c\,(L(r^*)) = Der\,c\,(L(r)^0 \cup \bigcup_{n \ge 1} L(r)) = (Der\,c\,L(r)^0) \cup Der\,c\,(\bigcup_{n \ge 1} L(r))$
+$Der\,c\,(L(r^*)) = Der\,c\,(L(r)^0 \cup \bigcup_{n \ge 1} L(r)^n) = (Der\,c\,L(r)^0) \cup Der\,c\,(\bigcup_{n \ge 1} L(r)^n)$
 \end{center}
 
 The first union ``disappears'' since $Der\,c\,(L(r)^0) = \varnothing$.

--- a/progs/token2.scala	Thu Nov 26 12:55:59 2015 +0000
+++ b/progs/token2.scala	Fri Nov 27 12:08:29 2015 +0000
@@ -155,6 +155,9 @@
 
 lexing(OPT("ab"), "ab")
 
+lexing(NTIMES("1", 3), "111")
+lexing(NTIMES("1" | EMPTY, 3), "11")
+
 // some "rectification" functions for simplification
 def F_ID(v: Val): Val = v
 def F_RIGHT(f: Val => Val) = (v:Val) => Right(f(v))

Binary file slides/slides11.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/slides11.tex	Fri Nov 27 12:08:29 2015 +0000
@@ -0,0 +1,317 @@
+\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: 
+