# HG changeset patch # User Christian Urban # Date 1448626109 0 # Node ID 66f66f1710ed332c802c87e74daa523ee32cf7e4 # Parent 8aa406adfde04774f661b2ed5f8ee3e563db3d0f added diff -r 8aa406adfde0 -r 66f66f1710ed hws/proof.pdf Binary file hws/proof.pdf has changed diff -r 8aa406adfde0 -r 66f66f1710ed hws/proof.tex --- 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$. diff -r 8aa406adfde0 -r 66f66f1710ed progs/token2.scala --- 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)) diff -r 8aa406adfde0 -r 66f66f1710ed slides/slides11.pdf Binary file slides/slides11.pdf has changed diff -r 8aa406adfde0 -r 66f66f1710ed slides/slides11.tex --- /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: +