| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Tue, 03 Oct 2023 14:29:12 +0100 | |
| changeset 936 | aabd9168c7ac | 
| parent 929 | 136105292ffd | 
| child 939 | fb6ffb9b7304 | 
| permissions | -rw-r--r-- | 
| 638 | 1  | 
% !TEX program = xelatex  | 
| 743 | 2  | 
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
 | 
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
3  | 
\usepackage{../slides}
 | 
| 871 | 4  | 
\usepackage{../graphicss}
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
5  | 
\usepackage{../langs}
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
6  | 
\usepackage{../data}
 | 
| 7 | 7  | 
|
| 764 | 8  | 
\usepackage{tcolorbox}
 | 
9  | 
\newtcolorbox{mybox}{colback=red!5!white,colframe=red!75!black}
 | 
|
10  | 
\newtcolorbox{mybox2}[1]{colback=red!5!white,colframe=red!75!black,fonttitle=\bfseries,title=#1}
 | 
|
11  | 
\newtcolorbox{mybox3}[1]{colback=Cyan!5!white,colframe=Cyan!75!black,fonttitle=\bfseries,title=#1}
 | 
|
12  | 
||
13  | 
||
14  | 
||
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
15  | 
\hfuzz=220pt  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
16  | 
|
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
17  | 
\lstset{language=Scala,
 | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
18  | 
style=mystyle,  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
19  | 
numbersep=0pt,  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
20  | 
numbers=none,  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
21  | 
xleftmargin=0mm}  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
22  | 
|
| 777 | 23  | 
\pgfplotsset{compat=1.17}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
24  | 
|
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
25  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}     
 | 
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
26  | 
|
| 7 | 27  | 
% beamer stuff  | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
28  | 
\renewcommand{\slidecaption}{CFL 02, King's College London}
 | 
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
29  | 
|
| 7 | 30  | 
|
31  | 
\begin{document}
 | 
|
32  | 
||
33  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
34  | 
\begin{frame}[t]
 | 
| 7 | 35  | 
\frametitle{%
 | 
36  | 
  \begin{tabular}{@ {}c@ {}}
 | 
|
37  | 
\\[-3mm]  | 
|
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
38  | 
\LARGE Compilers and \\[-1mm]  | 
| 882 | 39  | 
\LARGE Formal Languages\\[-5mm]  | 
| 7 | 40  | 
  \end{tabular}}
 | 
41  | 
||
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
42  | 
\normalsize  | 
| 7 | 43  | 
  \begin{center}
 | 
44  | 
  \begin{tabular}{ll}
 | 
|
| 882 | 45  | 
Email: & christian.urban at kcl.ac.uk\\  | 
| 929 | 46  | 
Office Hour: & Thurdays 15 -- 16\\  | 
| 882 | 47  | 
Location: & N7.07 (North Wing, Bush House)\\  | 
48  | 
Slides \& Progs: & KEATS\\  | 
|
49  | 
  Pollev: & \texttt{\alert{https://pollev.com/cfltutoratki576}}\\  
 | 
|
| 7 | 50  | 
  \end{tabular}
 | 
51  | 
  \end{center}
 | 
|
52  | 
||
| 743 | 53  | 
  \begin{center}
 | 
54  | 
    \begin{tikzpicture}
 | 
|
55  | 
\node[drop shadow,fill=white,inner sep=0pt]  | 
|
56  | 
      {\footnotesize\rowcolors{1}{capri!10}{white}
 | 
|
57  | 
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
 | 
|
58  | 
1 Introduction, Languages & 6 While-Language \\  | 
|
59  | 
          \cellcolor{blue!50}
 | 
|
60  | 
2 Regular Expressions, Derivatives & 7 Compilation, JVM \\  | 
|
61  | 
3 Automata, Regular Languages & 8 Compiling Functional Languages \\  | 
|
62  | 
4 Lexing, Tokenising & 9 Optimisations \\  | 
|
63  | 
5 Grammars, Parsing & 10 LLVM \\ \hline  | 
|
64  | 
        \end{tabular}%
 | 
|
65  | 
};  | 
|
66  | 
    \end{tikzpicture}
 | 
|
67  | 
  \end{center}
 | 
|
68  | 
||
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
69  | 
\end{frame}
 | 
| 
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
70  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 7 | 71  | 
|
72  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 565 | 73  | 
\begin{frame}[t]
 | 
| 630 | 74  | 
  \frametitle{
 | 
| 743 | 75  | 
Let's Implement an Efficient\\[-2mm]  | 
| 565 | 76  | 
Regular Expression Matcher}  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
77  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
78  | 
\footnotesize  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
79  | 
\begin{center}
 | 
| 565 | 80  | 
  {\normalsize Graphs: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$} and strings \bl{$\underbrace{\,a\ldots a\,}_{n}$}}\medskip\\
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
81  | 
\begin{tabular}{@{}cc@{}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
82  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
83  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
84  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
85  | 
    x label style={at={(1.05,0.0)}},
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
86  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
87  | 
enlargelimits=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
88  | 
    xtick={0,5,...,30},
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
89  | 
xmax=33,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
90  | 
ymax=35,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
91  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
92  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
93  | 
axis lines=left,  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
94  | 
width=5cm,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
95  | 
height=4.5cm,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
96  | 
    legend entries={Python,Ruby},  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
97  | 
legend pos=north west,  | 
| 514 | 98  | 
legend cell align=left]  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
99  | 
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
100  | 
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
101  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
102  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
103  | 
&  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
104  | 
\begin{tikzpicture}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
105  | 
  \begin{axis}[
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
106  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
107  | 
    x label style={at={(1.1,0.05)}},
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
108  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
109  | 
enlargelimits=false,  | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
110  | 
    xtick={0,5000,...,10000},
 | 
| 
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
111  | 
xmax=11500,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
112  | 
ymax=35,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
113  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
114  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
115  | 
axis lines=left,  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
116  | 
width=5cm,  | 
| 514 | 117  | 
height=4.5cm,  | 
118  | 
    legend entries={Scala V2,Scala V3},
 | 
|
| 565 | 119  | 
legend pos=north east,  | 
| 514 | 120  | 
legend cell align=left]  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
121  | 
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
122  | 
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
123  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
124  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
125  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
126  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
127  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
128  | 
\small  | 
| 638 | 129  | 
In the handouts is a similar graph for \bl{$(a^*)^* \cdot b$} and Java 8, 
 | 
130  | 
JavaScript and Python.  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
131  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
132  | 
\end{frame}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
133  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
134  | 
|
| 512 | 135  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 638 | 136  | 
%\begin{frame}[c]
 | 
137  | 
%\frametitle{Evil Regular Expressions}
 | 
|
138  | 
%  | 
|
139  | 
%\begin{itemize}
 | 
|
140  | 
%\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip
 | 
|
141  | 
%\item Evil regular expressions\medskip  | 
|
142  | 
%\begin{itemize}
 | 
|
143  | 
%\item \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
|
144  | 
%\item \bl{$(a^*)^*$}
 | 
|
145  | 
%\item \bl{$([a$\,-\,$z]^+)^*$}
 | 
|
146  | 
%\item \bl{$(a + a \cdot a)^*$}
 | 
|
147  | 
%\item \bl{$(a + a^?)^*$}
 | 
|
148  | 
%\end{itemize}
 | 
|
149  | 
%  | 
|
150  | 
%\item sometimes also called \alert{catastrophic backtracking}\bigskip
 | 
|
151  | 
%\item \small\ldots I hope you have watched the video by the  | 
|
152  | 
% StackExchange engineer  | 
|
153  | 
%\end{itemize}
 | 
|
154  | 
%  | 
|
155  | 
%\end{frame}
 | 
|
| 512 | 156  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
157  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
158  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
159  | 
\begin{frame}[c]
 | 
| 638 | 160  | 
\frametitle{(Basic) Regular Expressions}
 | 
161  | 
||
162  | 
Their inductive definition:  | 
|
163  | 
||
164  | 
\begin{center}
 | 
|
165  | 
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
 | 
|
166  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & nothing\\
 | 
|
167  | 
         & \bl{$\mid$} & \bl{$\ONE$}       & empty string / \pcode{""} / $[]$\\
 | 
|
168  | 
         & \bl{$\mid$} & \bl{$c$}                         & character\\
 | 
|
169  | 
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
 | 
|
170  | 
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
 | 
|
171  | 
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
 | 
|
172  | 
  \end{tabular}
 | 
|
173  | 
\end{center}
 | 
|
174  | 
\vspace{\fill}
 | 
|
175  | 
||
| 743 | 176  | 
%%Q: \;What about \;\bl{$r \cdot 0$} \; ?
 | 
| 507 | 177  | 
\end{frame}
 | 
178  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
179  | 
||
| 638 | 180  | 
|
181  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
182  | 
\begin{frame}[c]
 | 
|
183  | 
  \frametitle{
 | 
|
184  | 
When Are Two Regular\\[-1mm]  | 
|
185  | 
Expressions Equivalent?}  | 
|
186  | 
||
187  | 
   \begin{bubble}[10cm]
 | 
|
188  | 
\large  | 
|
| 763 | 189  | 
    Two regular expressions \bl{$r_1$} and \bl{$r_2$} are
 | 
190  | 
    \alert{\bf{}equivalent} 
 | 
|
| 638 | 191  | 
provided:\medskip  | 
192  | 
    \begin{center}
 | 
|
193  | 
      \bl{$r_1 \equiv r_2 \;\;\dn\;\; L(r_1) = L(r_2)$}  
 | 
|
194  | 
    \end{center}\medskip
 | 
|
195  | 
    \end{bubble}
 | 
|
196  | 
||
197  | 
\end{frame}
 | 
|
198  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
199  | 
||
200  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
201  | 
\begin{frame}[c]
 | 
|
202  | 
\frametitle{Some Concrete Equivalences}
 | 
|
203  | 
||
204  | 
\begin{center}
 | 
|
205  | 
\bl{\begin{tabular}{rcl}
 | 
|
206  | 
$(a + b) + c$ & $\equiv$ & $a + (b + c)$\\  | 
|
207  | 
$a + a$ & $\equiv$ & $a$\\  | 
|
208  | 
$a + b$ & $\equiv$ & $b + a$\\  | 
|
209  | 
$(a \cdot b) \cdot c$ & $\equiv$ & $a \cdot (b \cdot c)$\\  | 
|
210  | 
$c \cdot (a + b)$ & $\equiv$ & $(c \cdot a) + (c \cdot b)$\bigskip\bigskip\\\pause  | 
|
211  | 
$a \cdot a$ & $\not\equiv$ & $a$\\  | 
|
212  | 
$a + (b \cdot c)$ & $\not\equiv$ & $(a + b) \cdot (a + c)$\\  | 
|
213  | 
\end{tabular}}
 | 
|
214  | 
\end{center}
 | 
|
215  | 
||
216  | 
\end{frame}
 | 
|
217  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
218  | 
||
219  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
220  | 
\begin{frame}[c]
 | 
|
221  | 
\frametitle{Some Corner Cases}
 | 
|
222  | 
||
223  | 
\begin{center}
 | 
|
224  | 
\bl{\begin{tabular}{rcl}
 | 
|
225  | 
$a \cdot \ZERO$ & $\not\equiv$ & $a$\\  | 
|
226  | 
$a + \ONE$ & $\not\equiv$ & $a$\\  | 
|
227  | 
$\ONE$ & $\equiv$ & $\ZERO^*$\\  | 
|
228  | 
$\ONE^*$ & $\equiv$ & $\ONE$\\  | 
|
229  | 
$\ZERO^*$ & $\not\equiv$ & $\ZERO$\\  | 
|
230  | 
\end{tabular}}
 | 
|
231  | 
\end{center}
 | 
|
232  | 
||
233  | 
\end{frame}
 | 
|
234  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
235  | 
||
236  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
237  | 
\begin{frame}[c]
 | 
|
238  | 
\frametitle{Some Simplification Rules}
 | 
|
239  | 
||
240  | 
\begin{center}
 | 
|
241  | 
\bl{\begin{tabular}{rcl}
 | 
|
242  | 
$r + \ZERO$ & $\equiv$ & $r$\\  | 
|
243  | 
$\ZERO + r$ & $\equiv$ & $r$\\  | 
|
244  | 
$r \cdot \ONE$ & $\equiv$ & $r$\\  | 
|
245  | 
$\ONE \cdot r$ & $\equiv$ & $r$\\  | 
|
246  | 
$r \cdot \ZERO$ & $\equiv$ & $\ZERO$\\  | 
|
247  | 
$\ZERO \cdot r$ & $\equiv$ & $\ZERO$\\  | 
|
248  | 
$r + r$ & $\equiv$ & $r$  | 
|
249  | 
\end{tabular}}
 | 
|
250  | 
\end{center}
 | 
|
251  | 
||
252  | 
\end{frame}
 | 
|
253  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
254  | 
||
| 764 | 255  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
256  | 
\begin{frame}[c]
 | 
|
257  | 
\frametitle{Simplification Example}
 | 
|
258  | 
||
259  | 
%%Given \bl{$r \dn ((a \cdot b) + b)^*$}, you can simplify as follows
 | 
|
260  | 
||
261  | 
\begin{center}
 | 
|
262  | 
\def\arraystretch{2}  
 | 
|
263  | 
\begin{tabular}{@{}lcl}
 | 
|
264  | 
  \bl{$((\ONE \cdot b) + \ZERO) \cdot r$}
 | 
|
265  | 
    & \bl{$\Rightarrow$} & \bl{$((\underline{\ONE \cdot b}) + \ZERO) \cdot r$}\\
 | 
|
266  | 
    & \bl{$=$} & \bl{$(\underline{b + \ZERO}) \cdot r$}\\
 | 
|
267  | 
    & \bl{$=$} & \bl{$b \cdot r$}\\
 | 
|
268  | 
\end{tabular}
 | 
|
269  | 
\end{center}
 | 
|
270  | 
||
271  | 
\end{frame}
 | 
|
272  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
273  | 
||
274  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
275  | 
\begin{frame}[c]
 | 
|
276  | 
\frametitle{Simplification Example}
 | 
|
277  | 
||
278  | 
%%Given \bl{$r \dn ((a \cdot b) + b)^*$}, you can simplify as follows
 | 
|
279  | 
||
280  | 
\begin{center}
 | 
|
281  | 
\def\arraystretch{2}  
 | 
|
282  | 
\begin{tabular}{@{}lcl}
 | 
|
283  | 
  \bl{$((\ZERO \cdot b) + \ZERO) \cdot r$}
 | 
|
284  | 
    & \bl{$\Rightarrow$} & \bl{$((\underline{\ZERO \cdot b}) + \ZERO) \cdot r$}\\
 | 
|
285  | 
    & \bl{$=$} & \bl{$(\underline{\ZERO + \ZERO}) \cdot r$}\\
 | 
|
286  | 
    & \bl{$=$} & \bl{$\ZERO \cdot r$}\\
 | 
|
287  | 
    & \bl{$=$} & \bl{$\ZERO$}\\
 | 
|
288  | 
\end{tabular}
 | 
|
289  | 
\end{center}
 | 
|
290  | 
||
291  | 
\end{frame}
 | 
|
292  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 566 | 293  | 
|
| 507 | 294  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 565 | 295  | 
\begin{frame}[t]
 | 
296  | 
\frametitle{Semantic Derivative\\[5mm]}
 | 
|
297  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
298  | 
\begin{itemize}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
299  | 
\item The \alert{\bf Semantic Derivative} of a 
 | 
| 565 | 300  | 
\underline{language}\\ w.r.t.~to a character \bl{$c$}:
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
301  | 
\bigskip  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
302  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
303  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
304  | 
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
 | 
| 565 | 305  | 
\end{center}\bigskip
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
306  | 
|
| 630 | 307  | 
For \bl{$A = \{\mathit{foo}, \mathit{bar}, \mathit{frak}\}$} then
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
308  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
309  | 
\begin{center}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
310  | 
\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
 | 
| 630 | 311  | 
$\Der\,f\,A$ & $=$ & $\{\mathit{oo}, \mathit{rak}\}$\\
 | 
312  | 
$\Der\,b\,A$ & $=$ &  $\{\mathit{ar}\}$\\  
 | 
|
| 565 | 313  | 
$\Der\,a\,A$ & $=$ & $\{\}$\pause
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
314  | 
\end{tabular}}
 | 
| 638 | 315  | 
\end{center}\medskip
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
316  | 
|
| 630 | 317  | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
318  | 
We can extend this definition to strings  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
319  | 
\[  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
320  | 
\bl{\Ders\,s\,A = \{s'\;|\;s\,@\,s' \in A\}}
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
321  | 
\]  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
322  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
323  | 
\end{itemize}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
324  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
325  | 
\end{frame}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
326  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
327  | 
|
| 763 | 328  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
329  | 
\begin{frame}[c]
 | 
|
330  | 
\frametitle{The Specification for Matching}
 | 
|
331  | 
||
332  | 
\begin{bubble}[10cm]
 | 
|
333  | 
\large  | 
|
334  | 
A regular expression \bl{$r$} matches a string~\bl{$s$} 
 | 
|
335  | 
provided:  | 
|
336  | 
\begin{center}
 | 
|
337  | 
\bl{$s \in L(r)$} 
 | 
|
338  | 
\end{center}\medskip
 | 
|
339  | 
\end{bubble}
 | 
|
340  | 
||
341  | 
\bigskip\bigskip  | 
|
342  | 
||
343  | 
\ldots and the point of the this lecture is to decide this problem as  | 
|
344  | 
fast as possible (unlike Python, Ruby, Java etc)  | 
|
345  | 
||
346  | 
\end{frame}
 | 
|
347  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 771 | 348  | 
|
349  | 
||
| 512 | 350  | 
|
351  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
352  | 
\begin{frame}[c]
 | 
|
| 573 | 353  | 
\frametitle{\mbox{Brzozowski's Algorithm (1)}}
 | 
| 11 | 354  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
355  | 
|
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
356  | 
\ldots{}whether a regular expression can match the empty string:
 | 
| 11 | 357  | 
\begin{center}
 | 
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
358  | 
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
 | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
359  | 
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
 | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
360  | 
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
361  | 
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
362  | 
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
363  | 
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
364  | 
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
 | 
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
365  | 
\end{tabular}
 | 
| 16 | 366  | 
\end{center}
 | 
367  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
368  | 
\end{frame}
 | 
| 11 | 369  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
370  | 
||
371  | 
||
372  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
373  | 
\begin{frame}[c]
 | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
374  | 
\frametitle{The Derivative of a Rexp}
 | 
| 7 | 375  | 
|
376  | 
\large  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
377  | 
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
378  | 
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
 | 
| 7 | 379  | 
|
380  | 
\small  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
381  | 
\bl{$\der\,c\,r$} gives the answer, Brzozowski 1964
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
382  | 
\end{frame}
 | 
| 7 | 383  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
384  | 
||
385  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
386  | 
\begin{frame}[c]
 | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
387  | 
\frametitle{The Derivative of a Rexp}
 | 
| 7 | 388  | 
|
389  | 
\begin{center}
 | 
|
390  | 
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
 | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
391  | 
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
392  | 
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
393  | 
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
394  | 
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
395  | 
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
396  | 
  & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\ 
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
397  | 
  & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
 | 
| 638 | 398  | 
  \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$} &\medskip\bigskip\\\pause
 | 
| 7 | 399  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
400  | 
  \bl{$\ders\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
401  | 
  \bl{$\ders\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\ders\,s\,(\der\,c\,r)$} & \\
 | 
| 7 | 402  | 
  \end{tabular}
 | 
403  | 
\end{center}
 | 
|
404  | 
||
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
405  | 
\end{frame}
 | 
| 7 | 406  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
407  | 
||
408  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
409  | 
\begin{frame}[c]
 | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
410  | 
\frametitle{Examples}
 | 
| 7 | 411  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
412  | 
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
 | 
| 7 | 413  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
414  | 
\begin{center}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
415  | 
\begin{tabular}{l}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
416  | 
\bl{$\der\,a\,r =\;?$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
417  | 
\bl{$\der\,b\,r =\;?$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
418  | 
\bl{$\der\,c\,r =\;?$}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
419  | 
\end{tabular}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
420  | 
\end{center}
 | 
| 7 | 421  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
422  | 
\end{frame}
 | 
| 7 | 423  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
424  | 
||
| 17 | 425  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 431 | 426  | 
\begin{frame}[c]
 | 
| 764 | 427  | 
\frametitle{Derivative Example}
 | 
428  | 
||
429  | 
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
 | 
|
| 431 | 430  | 
|
431  | 
\begin{center}
 | 
|
| 764 | 432  | 
\def\arraystretch{1.5}  
 | 
433  | 
\begin{tabular}{@{}lcl}
 | 
|
434  | 
  \bl{$\der\,a\,((a \cdot b) + b)^*$}
 | 
|
435  | 
    & \bl{$\Rightarrow$}& \bl{$\der\,a\, \underline{((a \cdot b) + b)^*}$}\\
 | 
|
436  | 
    & \bl{$=$} & \bl{$(der\,a\,(\underline{(a \cdot b) + b})) \cdot r$}\\
 | 
|
437  | 
    & \bl{$=$} & \bl{$((der\,a\,(\underline{a \cdot b})) + (der\,a\,b)) \cdot r$}\\
 | 
|
438  | 
    & \bl{$=$} & \bl{$(((der\,a\,\underline{a}) \cdot b) + (der\,a\,b)) \cdot r$}\\
 | 
|
439  | 
    & \bl{$=$} & \bl{$((\ONE \cdot b) + (der\,a\,\underline{b})) \cdot r$}\\
 | 
|
440  | 
    & \bl{$=$} & \bl{$((\ONE \cdot b) + \ZERO) \cdot r$}
 | 
|
| 431 | 441  | 
\end{tabular}
 | 
442  | 
\end{center}
 | 
|
443  | 
||
| 764 | 444  | 
\end{frame}
 | 
445  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
446  | 
||
447  | 
||
448  | 
||
449  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
450  | 
\begin{frame}[c]
 | 
|
451  | 
\frametitle{\mbox{The Brzozowski Algorithm}}
 | 
|
452  | 
||
453  | 
%\begin{center}
 | 
|
454  | 
%\begin{tabular}{l} 
 | 
|
455  | 
%\bl{$\textit{matcher}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}  
 | 
|
456  | 
%\end{tabular}
 | 
|
457  | 
%\end{center}
 | 
|
458  | 
||
459  | 
\begin{center}
 | 
|
460  | 
\begin{mybox3}{}
 | 
|
| 765 | 461  | 
\centering  | 
| 764 | 462  | 
\bl{$\textit{matcher}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}
 | 
463  | 
\end{mybox3}
 | 
|
464  | 
\end{center}
 | 
|
| 431 | 465  | 
|
466  | 
\end{frame}
 | 
|
467  | 
%%%%%%%%%%%%%%%%%  | 
|
468  | 
||
469  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 17 | 470  | 
\begin{frame}[t]
 | 
| 565 | 471  | 
\frametitle{Brzozowski: An Example}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
472  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
473  | 
Does \bl{$r_1$} match \bl{$abc$}?
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
474  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
475  | 
\begin{tabular}{@{}rl@{}l@{}}
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
476  | 
Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = \der\,a\,r_1)$}\smallskip\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
477  | 
Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = \der\,b\,r_2)$}\smallskip\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
478  | 
Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = \der\,c\,r_3)$}\smallskip\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
479  | 
Step 4: & the string is exhausted: & \bl{($nullable(r_4))$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
480  | 
        & test whether \bl{$r_4$} can recognise\\
 | 
| 565 | 481  | 
& the empty string\medskip\\  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
482  | 
Output: & result of the test\\  | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
483  | 
        & $\Rightarrow \bl{\textit{true}} \,\text{or}\, 
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
484  | 
                       \bl{\textit{false}}$\\        
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
485  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
486  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
487  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
488  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
489  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
490  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
491  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
492  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
493  | 
\begin{frame}[c]
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
494  | 
\frametitle{The Idea of the Algorithm}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
495  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
496  | 
If we want to recognise the string \bl{$abc$} with regular 
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
497  | 
expression \bl{$r_1$} then\medskip
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
498  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
499  | 
\begin{enumerate}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
500  | 
\item \bl{$\Der\,a\,(L(r_1))$}\pause
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
501  | 
\item \bl{$\Der\,b\,(\Der\,a\,(L(r_1)))$}\pause
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
502  | 
\item \bl{$\Der\,c\,(\Der\,b\,(\Der\,a\,(L(r_1))))$}\bigskip
 | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
503  | 
\item finally we test whether the empty string is in this  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
504  | 
set; same for  \bl{$\Ders\,abc\,(L(r_1))$}.\medskip
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
505  | 
\end{enumerate}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
506  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
507  | 
The matching algorithm works similarly, just over regular expressions instead of sets.  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
508  | 
\end{frame}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
509  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
510  | 
|
| 764 | 511  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
512  | 
\begin{frame}[c]
 | 
|
513  | 
\frametitle{The Idea with Derivatives}
 | 
|
514  | 
||
515  | 
Input: string \bl{$abc$} and regular expression \bl{$r$}\medskip 
 | 
|
516  | 
||
517  | 
\begin{enumerate}
 | 
|
518  | 
\item \bl{$der\,a\,r$}
 | 
|
519  | 
\item \bl{$der\,b\,(der\,a\,r)$}
 | 
|
520  | 
\item \bl{$der\,c\,(der\,b\,(der\,a\,r))$}\bigskip\pause
 | 
|
521  | 
\item finally check whether the last regular expression can match the empty string  | 
|
522  | 
\end{enumerate}
 | 
|
523  | 
||
524  | 
\end{frame}
 | 
|
525  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
526  | 
||
| 765 | 527  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
528  | 
\begin{frame}[c]
 | 
|
529  | 
\frametitle{\boldmath\;$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
|
530  | 
||
531  | 
\begin{center}
 | 
|
532  | 
\begin{tikzpicture}
 | 
|
533  | 
\begin{axis}[
 | 
|
534  | 
    xlabel={$n$},
 | 
|
535  | 
    x label style={at={(1.05,0.0)}},
 | 
|
536  | 
    ylabel={time in secs},
 | 
|
537  | 
enlargelimits=false,  | 
|
538  | 
    xtick={0,5,...,30},
 | 
|
539  | 
xmax=31,  | 
|
540  | 
    ytick={0,5,...,30},
 | 
|
541  | 
scaled ticks=false,  | 
|
542  | 
axis lines=left,  | 
|
543  | 
width=7cm,  | 
|
544  | 
height=7cm,  | 
|
545  | 
    legend entries={Python,Ruby},  
 | 
|
546  | 
legend pos=outer north east,  | 
|
547  | 
legend cell align=left  | 
|
548  | 
]  | 
|
549  | 
\addplot[blue,mark=*, mark options={fill=white}] 
 | 
|
550  | 
  table {re-python.data};
 | 
|
551  | 
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
 | 
|
552  | 
  table {re-ruby.data};    
 | 
|
553  | 
\end{axis}
 | 
|
554  | 
\end{tikzpicture}
 | 
|
555  | 
\end{center}
 | 
|
556  | 
||
557  | 
\end{frame}
 | 
|
558  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
559  | 
||
560  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
561  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
562  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
563  | 
\begin{frame}[c]
 | 
| 638 | 564  | 
\frametitle{Oops\ldots \boldmath\;$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
565  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
566  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
567  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
568  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
569  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
570  | 
    x label style={at={(1.05,0.0)}},
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
571  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
572  | 
enlargelimits=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
573  | 
    xtick={0,5,...,30},
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
574  | 
xmax=31,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
575  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
576  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
577  | 
axis lines=left,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
578  | 
width=7cm,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
579  | 
height=7cm,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
580  | 
    legend entries={Python,Ruby,Scala V1},  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
581  | 
legend pos=outer north east,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
582  | 
legend cell align=left  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
583  | 
]  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
584  | 
\addplot[blue,mark=*, mark options={fill=white}] 
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
585  | 
  table {re-python.data};
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
586  | 
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
587  | 
  table {re-ruby.data};  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
588  | 
\addplot[red,mark=triangle*,mark options={fill=white}] 
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
589  | 
  table {re1.data};  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
590  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
591  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
592  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
593  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
594  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
595  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
596  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
597  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 565 | 598  | 
\begin{frame}[t]
 | 
599  | 
\frametitle{A Problem\medskip}
 | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
600  | 
|
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
601  | 
We represented the ``n-times'' \bl{$a^{\{n\}}$} as a 
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
602  | 
sequence regular expression:  | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
603  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
604  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
605  | 
\begin{tabular}{rl}
 | 
| 767 | 606  | 
0: & \bl{$\ONE$}\\    
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
607  | 
1: & \bl{$a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
608  | 
2: & \bl{$a\cdot a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
609  | 
3: & \bl{$a\cdot a\cdot a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
610  | 
& \ldots\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
611  | 
13: & \bl{$a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
612  | 
& \ldots\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
613  | 
20:  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
614  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
615  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
616  | 
|
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
617  | 
This problem is aggravated with \bl{$a^?$} being represented 
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
618  | 
as \bl{$a + \ONE$}.
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
619  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
620  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
621  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
622  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
623  | 
\begin{frame}[c]
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
624  | 
\frametitle{Solving the Problem}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
625  | 
|
| 514 | 626  | 
What happens if we extend our regular expressions with explicit  | 
627  | 
constructors  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
628  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
629  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
630  | 
\begin{tabular}{rcl}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
631  | 
\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
 | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
632  | 
             & \bl{$\mid$} & \bl{$r^{\{n\}}$}\\
 | 
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
633  | 
             & \bl{$\mid$} & \bl{$r^?$} 
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
634  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
635  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
636  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
637  | 
What is their meaning?\\  | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
638  | 
What are the cases for \bl{$nullable$} and \bl{$\der$}?
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
639  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
640  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
641  | 
|
| 769 | 642  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
643  | 
\begin{frame}[c]
 | 
|
644  | 
  \frametitle{$der$ for $n$-times}
 | 
|
645  | 
||
646  | 
Case \bl{$n = 2$} and \bl{$r \cdot r$}: 
 | 
|
647  | 
||
648  | 
\begin{center}
 | 
|
649  | 
  \begin{tabular}{lcl}
 | 
|
650  | 
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
 | 
|
651  | 
                              &   & \bl{then \; \alert<3>{$(der\,c\,r)\cdot r + der\,c\,r$}}\\
 | 
|
652  | 
                              &   & \bl{else \; $(der\,c\,r)\cdot r$}\bigskip\pause\\
 | 
|
653  | 
    my claim                  &   & \bl{$\equiv\;$} \bl{$(der\,c\,r)\cdot r$}\\
 | 
|
654  | 
(in this case)  | 
|
655  | 
  \end{tabular} 
 | 
|
656  | 
\end{center}  
 | 
|
657  | 
||
658  | 
\end{frame}
 | 
|
659  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
660  | 
||
661  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
662  | 
\begin{frame}[t]
 | 
|
663  | 
||
664  | 
We know \bl{$nullable(r)$} holds!\pause 
 | 
|
665  | 
||
666  | 
\begin{center}
 | 
|
667  | 
  \begin{tabular}{@{}lcl}
 | 
|
668  | 
    \bl{$(der\,c\,r)\cdot r + der\,c\,r$}\pause
 | 
|
669  | 
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r + (der\,c\,r) \cdot \ONE$}\medskip\pause\\
 | 
|
670  | 
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot (r + \ONE)$}\medskip\pause\\
 | 
|
671  | 
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r$}\\
 | 
|
672  | 
    \multicolumn{3}{r}{\small(remember \bl{$r$} is nullable)}
 | 
|
673  | 
  \end{tabular} 
 | 
|
674  | 
\end{center}\pause
 | 
|
675  | 
||
676  | 
\rule{13cm}{0.8mm}
 | 
|
677  | 
||
678  | 
\begin{textblock}{13}(2,10)
 | 
|
679  | 
\only<6>{%
 | 
|
680  | 
  \begin{tabular}{lcl}
 | 
|
681  | 
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
 | 
|
682  | 
                          &   & \bl{then \; $(der\,c\,r)\cdot r + der\,c\,r$}\\
 | 
|
683  | 
                          &   & \bl{else \; $(der\,c\,r)\cdot r$}                                
 | 
|
684  | 
  \end{tabular}}
 | 
|
685  | 
\only<7>{%
 | 
|
686  | 
  \begin{tabular}{lcl}
 | 
|
687  | 
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
 | 
|
688  | 
                          &   & \bl{then \; $(der\,c\,r)\cdot r$}\\
 | 
|
689  | 
                          &   & \bl{else \; $(der\,c\,r)\cdot r$}                                
 | 
|
690  | 
  \end{tabular}}
 | 
|
691  | 
\only<8>{%
 | 
|
692  | 
  \begin{tabular}{lcl}
 | 
|
693  | 
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r$}                                
 | 
|
694  | 
  \end{tabular}}
 | 
|
695  | 
\end{textblock}
 | 
|
696  | 
||
697  | 
||
698  | 
\end{frame}
 | 
|
699  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
700  | 
||
701  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
702  | 
\begin{frame}[c]
 | 
|
703  | 
||
704  | 
\begin{center}
 | 
|
705  | 
\begin{tabular}{ll@{\hspace{10mm}}l}
 | 
|
706  | 
& \bl{$r\{n\}$} & \bl{$der$}\hspace{20mm}\mbox{}\\\hline\\[-4mm]    
 | 
|
707  | 
\bl{$n = 0$} : & \bl{$\ONE$}           & \bl{$\ZERO$}\\
 | 
|
708  | 
\bl{$n = 1$} : & \bl{$r$}              & \bl{$(der\,c\,r)$}\\
 | 
|
709  | 
\bl{$n = 2$} : & \bl{$r\cdot r$}       & \bl{$(der\,c\,r)\cdot r$}\\
 | 
|
710  | 
\bl{$n = 3$} : & \bl{$r\cdot r\cdot r$}& \only<1>{???}\only<2->{\bl{$(der\,c\,r)\cdot r\cdot r$}}\\
 | 
|
711  | 
\quad\vdots  | 
|
712  | 
\end{tabular} 
 | 
|
713  | 
\end{center}
 | 
|
714  | 
||
715  | 
\begin{textblock}{13}(1,11)
 | 
|
716  | 
\only<3->{%
 | 
|
717  | 
  \begin{tabular}{rcl}
 | 
|
718  | 
    \bl{$nullable(r\{n\})$} & \bl{$\dn$} &
 | 
|
719  | 
                          \bl{if\; $n = 0$\; then\; $true$\; else\; $nullable(r)$}\\
 | 
|
720  | 
    \bl{$der\,c\,(r\{n\})$} & \bl{$\dn$} &
 | 
|
721  | 
                          \bl{if\; $n = 0$\; then\; $\ZERO$\; else\; $(der\,c\,r)\cdot r\{n - 1\}$}
 | 
|
722  | 
  \end{tabular}}
 | 
|
723  | 
\end{textblock}
 | 
|
724  | 
||
725  | 
\end{frame}
 | 
|
726  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
727  | 
||
728  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
729  | 
\begin{frame}[c]
 | 
|
730  | 
||
731  | 
\begin{textblock}{13}(1.5,4)
 | 
|
732  | 
  \only<1-6>{%
 | 
|
733  | 
  \begin{tabular}{@{}lcl@{}}
 | 
|
734  | 
    \bl{$der\,c\,(r\cdot r\cdot r)$}
 | 
|
735  | 
    & \bl{$\dn$} & \bl{if $nullable(r)$}\medskip\\
 | 
|
736  | 
    & & \only<1>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + der\,c\,(r\cdot r)$}}%
 | 
|
737  | 
        \only<2>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + (der\,c\,r)\cdot r$}}%
 | 
|
738  | 
        \only<3>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r + r)$}}%
 | 
|
739  | 
        \only<4>{\bl{then\; $(der\,c\,r)\cdot (r\cdot (r + \ONE))$}}%
 | 
|
740  | 
        \only<5>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r)$}}%
 | 
|
741  | 
        \only<6>{\bl{then\; $(der\,c\,r)\cdot r\cdot r$}}\medskip\\
 | 
|
742  | 
    & & \bl{else\; $(der\,c\,r)\cdot r\cdot r$}\\
 | 
|
743  | 
  \end{tabular}}
 | 
|
744  | 
  \only<7->{%
 | 
|
745  | 
  \begin{tabular}{@{}lcl@{}}
 | 
|
746  | 
    \bl{$der\,c\,(r\cdot r\cdot r)$}
 | 
|
747  | 
    & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r\cdot r$}%
 | 
|
748  | 
  \end{tabular}} 
 | 
|
749  | 
\end{textblock}
 | 
|
750  | 
||
751  | 
\end{frame}
 | 
|
752  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
753  | 
||
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
754  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
755  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
756  | 
\begin{frame}[t]
 | 
| 638 | 757  | 
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
758  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
759  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
760  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
761  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
762  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
763  | 
    x label style={at={(1.05,0.0)}},   
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
764  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
765  | 
enlargelimits=false,  | 
| 
434
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
766  | 
    xtick={0,200,...,1100},
 | 
| 
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
767  | 
xmax=1200,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
768  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
769  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
770  | 
axis lines=left,  | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
771  | 
width=8cm,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
772  | 
height=6.5cm,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
773  | 
    legend entries={Python,Ruby,Scala V1,Scala V2},  
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
774  | 
legend pos=outer north east,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
775  | 
legend cell align=left  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
776  | 
]  | 
| 
434
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
777  | 
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
 | 
| 
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
778  | 
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
 | 
| 
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
779  | 
\addplot[red,mark=triangle*,mark options={fill=white}] table {re1.data};  
 | 
| 
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
780  | 
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
781  | 
\end{axis}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
782  | 
\end{tikzpicture}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
783  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
784  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
785  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
786  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
787  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
788  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
789  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
790  | 
\begin{frame}[c]
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
791  | 
\frametitle{Examples}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
792  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
793  | 
Recall the example of \bl{$r \dn ((a \cdot b) + b)^*$} with
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
794  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
795  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
796  | 
\begin{tabular}{l}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
797  | 
\bl{$\der\,a\,r = ((\ONE \cdot b) + \ZERO) \cdot r$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
798  | 
\bl{$\der\,b\,r = ((\ZERO \cdot b) + \ONE)\cdot r$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
799  | 
\bl{$\der\,c\,r = ((\ZERO \cdot b) + \ZERO)\cdot r$}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
800  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
801  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
802  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
803  | 
What are these regular expressions equivalent to?  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
804  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
805  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
806  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
807  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
808  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
809  | 
\begin{frame}[c]
 | 
| 565 | 810  | 
\frametitle{Simplification Rules}
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
811  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
812  | 
\begin{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
813  | 
\bl{\begin{tabular}{rcl}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
814  | 
$r + \ZERO$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
815  | 
$\ZERO + r$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
816  | 
$r \cdot \ONE$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
817  | 
$\ONE \cdot r$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
818  | 
$r \cdot \ZERO$ & $\Rightarrow$ & $\ZERO$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
819  | 
$\ZERO \cdot r$ & $\Rightarrow$ & $\ZERO$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
820  | 
$r + r$ & $\Rightarrow$ & $r$  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
821  | 
\end{tabular}}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
822  | 
\end{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
823  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
824  | 
\footnotesize  | 
| 565 | 825  | 
\lstinputlisting[firstline=22,lastline=26]{../progs/app6.scala}
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
826  | 
\end{frame}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
827  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
828  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
829  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
830  | 
\begin{frame}[c]
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
831  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
832  | 
\footnotesize  | 
| 565 | 833  | 
\lstinputlisting[firstline=1,lastline=21]{../progs/app6.scala}
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
834  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
835  | 
\end{frame}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
836  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
837  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
838  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
839  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
840  | 
\begin{frame}[t]
 | 
| 638 | 841  | 
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
842  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
843  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
844  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
845  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
846  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
847  | 
    x label style={at={(1.05,0.0)}},     
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
848  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
849  | 
enlargelimits=false,  | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
850  | 
    xtick={0,5000,...,10000},
 | 
| 
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
851  | 
xmax=11000,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
852  | 
ymax=35,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
853  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
854  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
855  | 
axis lines=left,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
856  | 
width=9cm,  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
857  | 
height=7cm,  | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
858  | 
    legend entries={Scala V2,Scala V3},  
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
859  | 
legend pos=north east  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
860  | 
]  | 
| 
434
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
861  | 
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
862  | 
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
863  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
864  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
865  | 
\end{center}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
866  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
867  | 
\end{frame}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
868  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
869  | 
|
| 778 | 870  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
871  | 
\begin{frame}[t]
 | 
|
872  | 
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
|
873  | 
||
874  | 
\begin{center}
 | 
|
875  | 
\begin{tikzpicture}
 | 
|
876  | 
\begin{axis}[
 | 
|
877  | 
    xlabel={$n$},
 | 
|
878  | 
    x label style={at={(1.05,0.0)}},     
 | 
|
879  | 
    ylabel={time in secs},
 | 
|
880  | 
enlargelimits=false,  | 
|
881  | 
    xtick={0,5000,...,10000},
 | 
|
882  | 
xmax=11000,  | 
|
883  | 
ymax=35,  | 
|
884  | 
    ytick={0,5,...,30},
 | 
|
885  | 
scaled ticks=false,  | 
|
886  | 
axis lines=left,  | 
|
887  | 
width=9cm,  | 
|
888  | 
height=7cm,  | 
|
889  | 
    legend entries={Scala V2,Scala V3,Rust},  
 | 
|
890  | 
legend pos=north east  | 
|
891  | 
]  | 
|
892  | 
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
 | 
|
893  | 
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
 | 
|
894  | 
\addplot[pink,mark=triangle,mark options={fill=pink}] table {re-rust.data};
 | 
|
895  | 
\end{axis}
 | 
|
896  | 
\end{tikzpicture}
 | 
|
897  | 
\end{center}
 | 
|
898  | 
||
| 782 | 899  | 
code by Archie Collard  | 
900  | 
||
| 778 | 901  | 
\end{frame}
 | 
902  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
903  | 
||
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
904  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
905  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
906  | 
\begin{frame}[c]
 | 
| 743 | 907  | 
  \frametitle{Another Example \boldmath$(a^*)^* \cdot b$}
 | 
| 565 | 908  | 
|
| 638 | 909  | 
\bigskip  | 
| 565 | 910  | 
\begin{center}
 | 
911  | 
\begin{tikzpicture}
 | 
|
912  | 
  \begin{axis}[
 | 
|
913  | 
    xlabel={$n$},
 | 
|
914  | 
    x label style={at={(1.05,0.0)}},
 | 
|
915  | 
    ylabel={time in secs},
 | 
|
916  | 
enlargelimits=false,  | 
|
917  | 
    xtick={0,5,...,30},
 | 
|
918  | 
xmax=33,  | 
|
919  | 
ymax=35,  | 
|
920  | 
    ytick={0,10,...,30},
 | 
|
921  | 
scaled ticks=false,  | 
|
922  | 
axis lines=left,  | 
|
923  | 
width=9cm,  | 
|
| 638 | 924  | 
height=5.5cm,  | 
| 777 | 925  | 
    legend entries={Java 8,Python,JavaScript,Swift,Dart},  
 | 
| 778 | 926  | 
legend pos=outer north east,  | 
| 565 | 927  | 
legend cell align=left]  | 
928  | 
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
 | 
|
929  | 
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
 | 
|
| 638 | 930  | 
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
 | 
| 767 | 931  | 
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
 | 
| 777 | 932  | 
\addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data};
 | 
| 565 | 933  | 
\end{axis}
 | 
934  | 
\end{tikzpicture}
 | 
|
935  | 
\end{center}
 | 
|
936  | 
||
937  | 
Regex: \bl{$(a^*)^* \cdot b$}
 | 
|
938  | 
||
939  | 
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
 | 
|
940  | 
||
941  | 
\end{frame}
 | 
|
942  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
943  | 
||
944  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
945  | 
\begin{frame}[c]
 | 
|
| 638 | 946  | 
\frametitle{Same Example in Java 9+}
 | 
| 565 | 947  | 
|
948  | 
\begin{center}
 | 
|
949  | 
\begin{tikzpicture}
 | 
|
950  | 
  \begin{axis}[
 | 
|
951  | 
    xlabel={$n$},
 | 
|
952  | 
    x label style={at={(1.09,-0.15)}},
 | 
|
953  | 
    ylabel={time in secs},
 | 
|
954  | 
scaled x ticks=false,  | 
|
955  | 
enlargelimits=false,  | 
|
956  | 
xtick distance=10000,  | 
|
957  | 
xmax=44000,  | 
|
958  | 
    ytick={0,10,...,30}, 
 | 
|
959  | 
ymax=35,  | 
|
960  | 
axis lines=left,  | 
|
961  | 
width=9cm,  | 
|
962  | 
height=5cm,  | 
|
963  | 
    legend entries={Java \liningnums{9}+},
 | 
|
964  | 
legend pos=north west,  | 
|
965  | 
legend cell align=left]  | 
|
966  | 
\addplot[blue,mark=square*,mark options={fill=white}] table {re-java9.data};
 | 
|
967  | 
\end{axis}
 | 
|
968  | 
\end{tikzpicture}
 | 
|
969  | 
\end{center}
 | 
|
970  | 
||
971  | 
Regex: \bl{$(a^*)^* \cdot b$}
 | 
|
972  | 
||
973  | 
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
 | 
|
974  | 
||
975  | 
\end{frame}
 | 
|
976  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
977  | 
||
978  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
979  | 
\begin{frame}[c]
 | 
|
| 646 | 980  | 
\frametitle{\ldots{}and with Brzozowski}
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
981  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
982  | 
\begin{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
983  | 
\begin{tikzpicture}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
984  | 
  \begin{axis}[
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
985  | 
    xlabel={$n$},
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
986  | 
    x label style={at={(1.09,0.0)}},
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
987  | 
    ylabel={time in secs},
 | 
| 565 | 988  | 
scaled x ticks=false,  | 
989  | 
xtick distance=2000000,  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
990  | 
enlargelimits=false,  | 
| 565 | 991  | 
xmax=6400000,  | 
| 514 | 992  | 
    ytick={0,10,...,30},
 | 
993  | 
ymax=35,  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
994  | 
axis lines=left,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
995  | 
width=9cm,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
996  | 
height=5cm,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
997  | 
    legend entries={Scala V3},
 | 
| 565 | 998  | 
legend pos=north west,  | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
999  | 
legend cell align=left]  | 
| 514 | 1000  | 
%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1001  | 
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1002  | 
\end{axis}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1003  | 
\end{tikzpicture}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1004  | 
\end{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1005  | 
|
| 565 | 1006  | 
Regex: \bl{$(a^*)^* \cdot b$}
 | 
1007  | 
||
1008  | 
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
 | 
|
1009  | 
||
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1010  | 
\end{frame}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1011  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
1012  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1013  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 573 | 1014  | 
\begin{frame}[c]
 | 
1015  | 
\frametitle{\mbox{What is good about this Alg.}}
 | 
|
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1016  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1017  | 
\begin{itemize}
 | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1018  | 
\item extends to most regular expressions, for example  | 
| 573 | 1019  | 
\bl{$\sim r$} (next slide)
 | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1020  | 
|
| 769 | 1021  | 
\item is easy to implement in a functional language  | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1022  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1023  | 
\item the algorithm is already quite old; there is still  | 
| 514 | 1024  | 
work to be done to use it as a tokenizer (that is relatively new work)  | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1025  | 
|
| 769 | 1026  | 
\item we can prove its correctness\ldots (another video)  | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1027  | 
\end{itemize}
 | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1028  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1029  | 
\end{frame}
 | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1030  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1031  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1032  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 566 | 1033  | 
\begin{frame}[c]
 | 
1034  | 
\frametitle{Negation of Regular Expr's}
 | 
|
1035  | 
||
1036  | 
\begin{itemize}
 | 
|
1037  | 
\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
 | 
|
1038  | 
\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
 | 
|
1039  | 
\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
 | 
|
1040  | 
\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
 | 
|
| 769 | 1041  | 
\end{itemize}\bigskip\bigskip\medskip\pause
 | 
| 566 | 1042  | 
|
1043  | 
Used often for recognising comments:  | 
|
1044  | 
\[  | 
|
1045  | 
\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
 | 
|
1046  | 
\]  | 
|
1047  | 
||
1048  | 
\end{frame}
 | 
|
1049  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1050  | 
||
| 771 | 1051  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1052  | 
\begin{frame}[c]
 | 
|
1053  | 
\frametitle{The Specification for Matching}
 | 
|
| 566 | 1054  | 
|
| 771 | 1055  | 
\begin{bubble}[10cm]
 | 
1056  | 
\large  | 
|
1057  | 
A regular expression \bl{$r$} matches a string~\bl{$s$} 
 | 
|
1058  | 
provided:  | 
|
1059  | 
\begin{center}
 | 
|
1060  | 
\bl{$s \in L(r)$} 
 | 
|
1061  | 
\end{center}\medskip
 | 
|
1062  | 
\end{bubble}
 | 
|
1063  | 
||
1064  | 
||
1065  | 
\begin{center}
 | 
|
1066  | 
\onslide<2>{\bl{\large$\forall\,r\,s.\;$}}
 | 
|
1067  | 
\bl{$matcher\,s\,r$}  \;if and only if\  \bl{$s \in L(r)$} 
 | 
|
1068  | 
\end{center}
 | 
|
1069  | 
||
1070  | 
||
1071  | 
\end{frame}
 | 
|
1072  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1073  | 
||
1074  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1075  | 
\begin{frame}[c]
 | 
|
1076  | 
\frametitle{nullable and \boldmath$der$}
 | 
|
1077  | 
||
1078  | 
The central properties:\bigskip\bigskip  | 
|
1079  | 
||
1080  | 
\large  | 
|
1081  | 
\begin{quote}
 | 
|
1082  | 
  \onslide<3>{\bl{$\forall r.\phantom{\,c}\;$}}%
 | 
|
1083  | 
  \bl{$nullable(r)$} \;if and only if\; \bl{$[] \in L(r)$}
 | 
|
1084  | 
\end{quote}\bigskip\bigskip\pause
 | 
|
1085  | 
||
1086  | 
\begin{quote}
 | 
|
1087  | 
  \onslide<3>{\bl{$\forall r\,c.\;$}}%
 | 
|
1088  | 
  \bl{$L(der\,c\,r) \;=\; Der\,c\,(L(r))$}
 | 
|
1089  | 
\end{quote}
 | 
|
1090  | 
||
1091  | 
\end{frame}
 | 
|
1092  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 770 | 1093  | 
|
| 566 | 1094  | 
|
1095  | 
||
| 764 | 1096  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
1097  | 
\begin{frame}[t]
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1098  | 
\frametitle{Proofs about Rexps}
 | 
| 17 | 1099  | 
|
1100  | 
Remember their inductive definition:\\[5cm]  | 
|
1101  | 
||
1102  | 
\begin{textblock}{6}(5,5)
 | 
|
1103  | 
  \begin{tabular}{@ {}rrl}
 | 
|
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
1104  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
 | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
1105  | 
         & \bl{$\mid$} & \bl{$\ONE$}     \\
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1106  | 
         & \bl{$\mid$} & \bl{$c$}            \\
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1107  | 
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1108  | 
         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1109  | 
         & \bl{$\mid$} & \bl{$r^*$}          \\
 | 
| 17 | 1110  | 
  \end{tabular}
 | 
1111  | 
  \end{textblock}
 | 
|
1112  | 
||
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1113  | 
If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
 | 
| 17 | 1114  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1115  | 
\end{frame}
 | 
| 17 | 1116  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1117  | 
||
1118  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1119  | 
\begin{frame}[c]
 | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1120  | 
\frametitle{Proofs about Rexp (2)}
 | 
| 17 | 1121  | 
|
1122  | 
\begin{itemize}
 | 
|
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
1123  | 
\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1124  | 
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1125  | 
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1126  | 
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1127  | 
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1128  | 
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1129  | 
holds for \bl{$r$}.
 | 
| 17 | 1130  | 
\end{itemize}
 | 
1131  | 
||
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1132  | 
\end{frame}
 | 
| 17 | 1133  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1134  | 
||
1135  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1136  | 
\begin{frame}[c]
 | 
|
| 771 | 1137  | 
\frametitle{Proofs about Rexp}
 | 
| 17 | 1138  | 
|
1139  | 
Assume \bl{$P(r)$} is the property:
 | 
|
1140  | 
||
1141  | 
\begin{center}
 | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1142  | 
\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
 | 
| 17 | 1143  | 
\end{center}
 | 
1144  | 
||
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1145  | 
\end{frame}
 | 
| 17 | 1146  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1147  | 
||
| 778 | 1148  | 
\begin{frame}[c]
 | 
1149  | 
\begin{mybox3}{}
 | 
|
1150  | 
der c (r*) def = (der c r) $\cdot$ (r*)\smallskip\\  | 
|
1151  | 
Why in the example (slide 19) the first step is:  | 
|
1152  | 
der a ((a $\cdot$ b) + b)* = (der a ((a $\cdot$ b) + b)) $\cdot$ r\smallskip\\  | 
|
1153  | 
and not\smallskip\\  | 
|
1154  | 
der a ((a $\cdot$ b) + b) = (der a ((a $\cdot$ b) + b)) · (r*)  | 
|
1155  | 
\end{mybox3}
 | 
|
1156  | 
\end{frame}
 | 
|
1157  | 
||
1158  | 
\begin{frame}[c]
 | 
|
1159  | 
\begin{mybox3}{}
 | 
|
1160  | 
Would it be possible to find and go over a few examples from the  | 
|
1161  | 
Brzozowski Algorithm, as it doesn't seem to be as simple as it  | 
|
1162  | 
sounds?  | 
|
1163  | 
\end{mybox3}
 | 
|
1164  | 
\end{frame}
 | 
|
1165  | 
||
1166  | 
\begin{frame}[c]
 | 
|
1167  | 
\begin{mybox3}{}
 | 
|
1168  | 
Is it possible to make a visual example of how using simp() function  | 
|
1169  | 
on a (a*)*.b regular expression reduces its runtime? If not it's  | 
|
1170  | 
fine. I am just very surprised that it is so efficient.  | 
|
1171  | 
\end{mybox3}
 | 
|
1172  | 
\end{frame}
 | 
|
1173  | 
||
1174  | 
\begin{frame}[c]
 | 
|
1175  | 
\begin{mybox3}{}
 | 
|
1176  | 
Do you think the algorithm can be still improved (made faster)?  | 
|
1177  | 
\end{mybox3}
 | 
|
1178  | 
\end{frame}
 | 
|
1179  | 
||
1180  | 
\begin{frame}[c]
 | 
|
1181  | 
\begin{mybox3}{}
 | 
|
1182  | 
Do the regular expression matchers in Python and Java 8 have more  | 
|
1183  | 
features than the one implemented in this module? Or is there  | 
|
1184  | 
another reason for their inefficiency?  | 
|
1185  | 
\end{mybox3}
 | 
|
1186  | 
\end{frame}
 | 
|
1187  | 
||
1188  | 
\begin{frame}[c]
 | 
|
1189  | 
\begin{mybox3}{}
 | 
|
1190  | 
Will we discuss the broader Chomsky hierarchy of languages at some  | 
|
1191  | 
point?  | 
|
1192  | 
\end{mybox3}
 | 
|
1193  | 
\end{frame}
 | 
|
1194  | 
||
1195  | 
\begin{frame}<1-8>[c]
 | 
|
1196  | 
\end{frame}
 | 
|
1197  | 
||
| 842 | 1198  | 
\begin{frame}[c]
 | 
1199  | 
\end{frame}
 | 
|
1200  | 
||
1201  | 
\begin{frame}[c]
 | 
|
1202  | 
\end{frame}
 | 
|
1203  | 
||
1204  | 
\begin{frame}[c]
 | 
|
1205  | 
\end{frame}
 | 
|
1206  | 
||
1207  | 
\begin{frame}<1-10>[c]
 | 
|
1208  | 
\end{frame}
 | 
|
1209  | 
||
1210  | 
||
1211  | 
||
| 771 | 1212  | 
\end{document}
 | 
1213  | 
% below are slides for proving.  | 
|
1214  | 
||
| 17 | 1215  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1216  | 
\begin{frame}[c]
 | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1217  | 
\frametitle{Proofs about Rexp (4)}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1218  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1219  | 
\begin{center}
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1220  | 
\bl{\begin{tabular}{r@{\hspace{2mm}}c@{\hspace{2mm}}l}
 | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
1221  | 
$rev(\ZERO)$ & $\dn$ & $\ZERO$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
1222  | 
$rev(\ONE)$ & $\dn$ & $\ONE$\\  | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1223  | 
$rev(c)$ & $\dn$ & $c$\\  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1224  | 
$rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1225  | 
$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1226  | 
$rev(r^*)$ & $\dn$ & $rev(r)^*$\\  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1227  | 
\end{tabular}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1228  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1229  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1230  | 
We can prove  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1231  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1232  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1233  | 
\bl{$L(rev(r)) = \{s^{-1} \;|\; s \in L(r)\}$}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1234  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1235  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1236  | 
by induction on \bl{$r$}.
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1237  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1238  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1239  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1240  | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1241  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1242  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1243  | 
\begin{frame}[c]
 | 
| 638 | 1244  | 
\frametitle{Correctness Proof \\[-1mm]
 | 
1245  | 
for our Matcher}  | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1246  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1247  | 
\begin{itemize}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1248  | 
\item We started from  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1249  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1250  | 
\begin{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1251  | 
\begin{tabular}{rp{4cm}}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1252  | 
  & \bl{$s \in L(r)$}\medskip\\
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1253  | 
\bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1254  | 
\end{tabular}
 | 
| 638 | 1255  | 
\end{center}\bigskip
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1256  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1257  | 
\item if we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
 | 
| 638 | 1258  | 
have\bigskip  | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1259  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1260  | 
\begin{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1261  | 
\begin{tabular}{rp{4cm}}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1262  | 
\bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1263  | 
\bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
 | 
| 764 | 1264  | 
\bl{$\dn$} & \bl{$matcher\,s\,r$}
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1265  | 
\end{tabular}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1266  | 
\end{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1267  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1268  | 
\end{itemize}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1269  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1270  | 
\end{frame}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1271  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1272  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1273  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1274  | 
\begin{frame}[c]
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1275  | 
\frametitle{Proofs about Rexp (5)}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1276  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1277  | 
Let \bl{$Der\,c\,A$} be the set defined as
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1278  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1279  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1280  | 
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1281  | 
\end{center}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1282  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1283  | 
We can prove  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1284  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1285  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1286  | 
\bl{$L(\der\,c\,r) = \Der\,c\,(L(r))$}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1287  | 
\end{center}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1288  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1289  | 
by induction on \bl{$r$}.
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1290  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1291  | 
\end{frame}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1292  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1293  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1294  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1295  | 
\begin{frame}[c]
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1296  | 
\frametitle{Proofs about Strings}
 | 
| 17 | 1297  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1298  | 
If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip
 | 
| 17 | 1299  | 
|
1300  | 
\begin{itemize}
 | 
|
1301  | 
\item \bl{$P$} holds for the empty string, and\medskip
 | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1302  | 
\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1303  | 
already holds for \bl{$s$}
 | 
| 17 | 1304  | 
\end{itemize}
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1305  | 
\end{frame}
 | 
| 17 | 1306  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1307  | 
||
| 19 | 1308  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1309  | 
\begin{frame}[c]
 | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1310  | 
\frametitle{Proofs about Strings (2)}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1311  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1312  | 
We can then prove  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1313  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1314  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1315  | 
\bl{$\Ders\,s\,(L(r)) = L(\ders\,s\,r)$}  
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1316  | 
\end{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1317  | 
|
| 19 | 1318  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1319  | 
We can finally prove  | 
| 19 | 1320  | 
|
1321  | 
\begin{center}
 | 
|
| 764 | 1322  | 
\bl{$matcher\,s\,r$}  if and only if  \bl{$s \in L(r)$} 
 | 
| 19 | 1323  | 
\end{center}
 | 
1324  | 
||
1325  | 
||
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1326  | 
\end{frame}
 | 
| 19 | 1327  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 17 | 1328  | 
|
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1329  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1330  | 
\begin{frame}[c]
 | 
| 770 | 1331  | 
\frametitle{Coursework 1}
 | 
1332  | 
||
1333  | 
%%\underline{Strand 1:}
 | 
|
1334  | 
||
1335  | 
\begin{itemize}
 | 
|
1336  | 
\item Submission on Friday 16 October @ 18:00\medskip  | 
|
1337  | 
\item source code needs to be submitted as well\medskip  | 
|
1338  | 
\item you can re-use my Scala code from KEATS \\  | 
|
1339  | 
and use any programming language you like\medskip  | 
|
1340  | 
\item \small https://nms.kcl.ac.uk/christian.urban/ProgInScala2ed.pdf\normalsize  | 
|
1341  | 
\end{itemize}  
 | 
|
1342  | 
||
1343  | 
\end{frame}
 | 
|
1344  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1345  | 
||
1346  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1347  | 
\begin{frame}[c]
 | 
|
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1348  | 
\frametitle{Epilogue}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1349  | 
|
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1350  | 
\footnotesize  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1351  | 
\begin{center}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1352  | 
\begin{tabular}{cc}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1353  | 
\begin{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1354  | 
\begin{axis}[
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1355  | 
    title={\small{}Graph: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}},
 | 
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1356  | 
    xlabel={$n$},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1357  | 
    x label style={at={(1.04,0.0)}},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1358  | 
    ylabel={time in secs},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1359  | 
enlargelimits=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1360  | 
xmax=7100000,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1361  | 
    ytick={0,5,...,30},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1362  | 
ymax=33,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1363  | 
%scaled ticks=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1364  | 
axis lines=left,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1365  | 
width=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1366  | 
height=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1367  | 
    legend entries={Scala V3, Scala V4},
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1368  | 
    legend style={at={(0.1,-0.2)},anchor=north}]
 | 
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1369  | 
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1370  | 
\addplot[purple,mark=square*,mark options={fill=white}] table {re4.data};
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1371  | 
\end{axis}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1372  | 
\end{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1373  | 
&  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1374  | 
\begin{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1375  | 
\begin{axis}[
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1376  | 
    title={\small{}Graph: \bl{$(a^*)^* \cdot b$}},
 | 
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1377  | 
    xlabel={$n$},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1378  | 
    x label style={at={(1.09,0.0)}},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1379  | 
    ylabel={time in secs},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1380  | 
enlargelimits=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1381  | 
xmax=8100000,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1382  | 
    ytick={0,5,...,30},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1383  | 
ymax=33,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1384  | 
%scaled ticks=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1385  | 
axis lines=left,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1386  | 
width=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1387  | 
height=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1388  | 
    legend entries={Scala V3, Scala V4},
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1389  | 
    legend style={at={(0.1,-0.2)},anchor=north}]
 | 
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1390  | 
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1391  | 
\addplot[purple,mark=square*,mark options={fill=white}] table {re4a.data};
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1392  | 
\end{axis}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1393  | 
\end{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1394  | 
\end{tabular}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1395  | 
\end{center}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1396  | 
|
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1397  | 
\only<2->{\footnotesize
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1398  | 
\begin{textblock}{9}(0.5,8)
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1399  | 
\begin{bubble}[11.8cm]
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1400  | 
\lstinputlisting[numbers=none]{../progs/app52.scala}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1401  | 
\end{bubble}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1402  | 
\end{textblock}} 
 | 
| 510 | 1403  | 
|
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1404  | 
|
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1405  | 
\end{frame}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1406  | 
|
| 638 | 1407  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1408  | 
\begin{frame}[c]
 | 
|
1409  | 
  \frametitle{Another Homework Question}
 | 
|
1410  | 
||
1411  | 
  \begin{itemize}
 | 
|
1412  | 
\item How many basic regular expressions are there to match  | 
|
1413  | 
    the string \bl{$abcd$}\,?\pause
 | 
|
1414  | 
\item How many if they cannot include  | 
|
1415  | 
    \bl{$\ONE$} and \bl{$\ZERO$}\/?\pause
 | 
|
1416  | 
\item How many if they are also not  | 
|
1417  | 
allowed to contain stars?\pause  | 
|
1418  | 
\item How many if they are also  | 
|
1419  | 
        not allowed to contain \bl{$\_ + \_$}\/? 
 | 
|
1420  | 
  \end{itemize}  
 | 
|
1421  | 
||
1422  | 
  \end{frame}
 | 
|
1423  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 743 | 1424  | 
|
1425  | 
||
1426  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1427  | 
\begin{frame}[c]
 | 
|
1428  | 
\frametitle{\begin{tabular}{c}\\[3cm]\huge\alert{Questions?}\end{tabular}}
 | 
|
1429  | 
||
| 764 | 1430  | 
%\bigskip  | 
1431  | 
%homework (written exam 80\%)\\  | 
|
1432  | 
%coursework (20\%; first one today)\\  | 
|
1433  | 
%submission Fridays @ 18:00 -- accepted until Mondays  | 
|
| 743 | 1434  | 
\mbox{}
 | 
1435  | 
\end{frame}
 | 
|
1436  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1437  | 
||
1438  | 
||
1439  | 
||
1440  | 
||
1441  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1442  | 
\begin{frame}[c]
 | 
|
1443  | 
\frametitle{Last Week}
 | 
|
1444  | 
||
1445  | 
Last week I showed you a regular expression matcher  | 
|
1446  | 
that works provably correct in all cases (we only  | 
|
1447  | 
started with the proving part though)  | 
|
1448  | 
||
1449  | 
\begin{center}
 | 
|
| 764 | 1450  | 
\bl{$matcher\,s\,r$} \;\;if and only if \;\; \bl{$s \in L(r)$}
 | 
| 743 | 1451  | 
\end{center}\bigskip\bigskip 
 | 
1452  | 
||
1453  | 
\small  | 
|
1454  | 
\textcolor{gray}{\mbox{}\hfill{}by Janusz Brzozowski (1964)}
 | 
|
1455  | 
||
1456  | 
\end{frame}
 | 
|
1457  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1458  | 
||
1459  | 
||
1460  | 
||
1461  | 
||
1462  | 
||
| 764 | 1463  | 
|
| 743 | 1464  | 
|
1465  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1466  | 
\begin{frame}[c]
 | 
|
1467  | 
  \frametitle{Proofs about Rexp}
 | 
|
1468  | 
||
1469  | 
  \begin{itemize}
 | 
|
1470  | 
  \item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
 | 
|
1471  | 
  \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
 | 
|
1472  | 
  holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
|
1473  | 
  \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
 | 
|
1474  | 
  holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
|
1475  | 
  \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
 | 
|
1476  | 
  holds for \bl{$r$}.
 | 
|
1477  | 
  \end{itemize}
 | 
|
1478  | 
||
1479  | 
\end{frame}
 | 
|
1480  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1481  | 
||
1482  | 
||
1483  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1484  | 
\begin{frame}[c]
 | 
|
1485  | 
||
1486  | 
We proved  | 
|
1487  | 
||
1488  | 
\begin{center}
 | 
|
1489  | 
\bl{$nullable(r)$} \;if and only if\;  \bl{$[] \in L(r)$}
 | 
|
1490  | 
\end{center}
 | 
|
1491  | 
||
1492  | 
by induction on the regular expression \bl{$r$}.\bigskip\pause
 | 
|
1493  | 
||
1494  | 
\begin{center}
 | 
|
1495  | 
{\huge\bf\alert{Any Questions?}}
 | 
|
1496  | 
\end{center}
 | 
|
1497  | 
||
1498  | 
\end{frame}
 | 
|
1499  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1500  | 
||
1501  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1502  | 
\begin{frame}[c]
 | 
|
1503  | 
\frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
 | 
|
1504  | 
||
1505  | 
\begin{itemize}
 | 
|
1506  | 
\item \bl{$P$} holds for \bl{$0$} and
 | 
|
1507  | 
\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
 | 
|
1508  | 
holds for \bl{$n$}
 | 
|
1509  | 
\end{itemize}\bigskip
 | 
|
1510  | 
||
1511  | 
\begin{itemize}
 | 
|
1512  | 
\item \bl{$P$} holds for \bl{$[]$} and
 | 
|
1513  | 
\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
 | 
|
1514  | 
holds for \bl{$s$}
 | 
|
1515  | 
\end{itemize}
 | 
|
1516  | 
||
1517  | 
\end{frame}
 | 
|
1518  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1519  | 
||
1520  | 
||
1521  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1522  | 
\begin{frame}[c]
 | 
|
1523  | 
  \frametitle{Correctness Proof \\[-1mm]
 | 
|
1524  | 
for our Matcher}  | 
|
1525  | 
||
1526  | 
  \begin{itemize}
 | 
|
1527  | 
\item We started from  | 
|
1528  | 
||
1529  | 
  \begin{center}
 | 
|
1530  | 
  \begin{tabular}{rp{4cm}}
 | 
|
1531  | 
    & \bl{$s \in L(r)$}\medskip\\
 | 
|
1532  | 
  \bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
 | 
|
1533  | 
  \end{tabular}
 | 
|
1534  | 
  \end{center}\bigskip
 | 
|
1535  | 
||
1536  | 
  \item \textbf{\alert{if}} we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
 | 
|
1537  | 
have\bigskip  | 
|
1538  | 
||
1539  | 
  \begin{center}
 | 
|
1540  | 
  \begin{tabular}{rp{4cm}}
 | 
|
1541  | 
  \bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
 | 
|
1542  | 
  \bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
 | 
|
| 764 | 1543  | 
  \bl{$\dn$} & \bl{$matcher\,s\,r$}
 | 
| 743 | 1544  | 
  \end{tabular}
 | 
1545  | 
  \end{center}
 | 
|
1546  | 
||
1547  | 
  \end{itemize}
 | 
|
1548  | 
||
1549  | 
  \end{frame}
 | 
|
1550  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1551  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1552  | 
\begin{frame}[c]
 | 
|
1553  | 
||
1554  | 
We need to prove  | 
|
1555  | 
||
1556  | 
\begin{center}
 | 
|
1557  | 
\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
 | 
|
1558  | 
\end{center}
 | 
|
1559  | 
||
1560  | 
also by induction on the regular expression \bl{$r$}.
 | 
|
1561  | 
\end{frame}
 | 
|
1562  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1563  | 
||
1564  | 
||
1565  | 
||
| 638 | 1566  | 
|
| 7 | 1567  | 
\end{document}
 | 
1568  | 
||
1569  | 
%%% Local Variables:  | 
|
1570  | 
%%% mode: latex  | 
|
1571  | 
%%% TeX-master: t  | 
|
1572  | 
%%% End:  | 
|
1573  |