| author | Christian Urban <urbanc@in.tum.de> | 
| Sat, 13 Oct 2018 13:51:28 +0100 | |
| changeset 577 | 1d6043a87a3e | 
| parent 573 | f099bf6d48ee | 
| child 630 | 3cea57c5501f | 
| permissions | -rw-r--r-- | 
| 7 | 1  | 
\documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
2  | 
\usepackage{../slides}
 | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
3  | 
\usepackage{../graphics}
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
4  | 
\usepackage{../langs}
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
5  | 
\usepackage{../data}
 | 
| 7 | 6  | 
|
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
7  | 
\hfuzz=220pt  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
8  | 
|
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
9  | 
\lstset{language=Scala,
 | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
10  | 
style=mystyle,  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
11  | 
numbersep=0pt,  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
12  | 
numbers=none,  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
13  | 
xleftmargin=0mm}  | 
| 
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
14  | 
|
| 
398
 
c8ce95067c1a
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
345 
diff
changeset
 | 
15  | 
\pgfplotsset{compat=1.12}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
16  | 
|
| 
258
 
1e4da6d2490c
updated programs
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
17  | 
\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
 | 
18  | 
|
| 7 | 19  | 
% beamer stuff  | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
20  | 
\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
 | 
21  | 
|
| 7 | 22  | 
|
23  | 
\begin{document}
 | 
|
24  | 
||
25  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
26  | 
\begin{frame}[t]
 | 
| 7 | 27  | 
\frametitle{%
 | 
28  | 
  \begin{tabular}{@ {}c@ {}}
 | 
|
29  | 
\\[-3mm]  | 
|
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
30  | 
\LARGE Compilers and \\[-1mm]  | 
| 16 | 31  | 
\LARGE Formal Languages (2)\\[3mm]  | 
| 7 | 32  | 
  \end{tabular}}
 | 
33  | 
||
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
34  | 
\normalsize  | 
| 7 | 35  | 
  \begin{center}
 | 
36  | 
  \begin{tabular}{ll}
 | 
|
37  | 
Email: & christian.urban at kcl.ac.uk\\  | 
|
| 564 | 38  | 
  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
 | 
| 514 | 39  | 
Slides: & KEATS (also homework is there)  | 
| 7 | 40  | 
  \end{tabular}
 | 
41  | 
  \end{center}
 | 
|
42  | 
||
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
43  | 
\end{frame}
 | 
| 
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
44  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 7 | 45  | 
|
46  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 565 | 47  | 
\begin{frame}[t]
 | 
48  | 
  \frametitle{\Large
 | 
|
49  | 
Lets Implement an Efficient\\[-2mm]  | 
|
50  | 
Regular Expression Matcher}  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
51  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
52  | 
\footnotesize  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
53  | 
\begin{center}
 | 
| 565 | 54  | 
  {\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
 | 
55  | 
\begin{tabular}{@{}cc@{}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
56  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
57  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
58  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
59  | 
    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
 | 
60  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
61  | 
enlargelimits=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
62  | 
    xtick={0,5,...,30},
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
63  | 
xmax=33,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
64  | 
ymax=35,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
65  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
66  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
67  | 
axis lines=left,  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
68  | 
width=5cm,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
69  | 
height=4.5cm,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
70  | 
    legend entries={Python,Ruby},  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
71  | 
legend pos=north west,  | 
| 514 | 72  | 
legend cell align=left]  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
73  | 
\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
 | 
74  | 
\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
 | 
75  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
76  | 
\end{tikzpicture}
 | 
| 
 
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  | 
\begin{tikzpicture}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
79  | 
  \begin{axis}[
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
80  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
81  | 
    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
 | 
82  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
83  | 
enlargelimits=false,  | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
84  | 
    xtick={0,5000,...,10000},
 | 
| 
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
85  | 
xmax=11500,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
86  | 
ymax=35,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
87  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
88  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
89  | 
axis lines=left,  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
90  | 
width=5cm,  | 
| 514 | 91  | 
height=4.5cm,  | 
92  | 
    legend entries={Scala V2,Scala V3},
 | 
|
| 565 | 93  | 
legend pos=north east,  | 
| 514 | 94  | 
legend cell align=left]  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
95  | 
\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
 | 
96  | 
\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
 | 
97  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
98  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
99  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
100  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
101  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
102  | 
\small  | 
| 565 | 103  | 
In the handouts is a similar graph for \bl{$(a^*)^* \cdot b$} and Java 8.
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
104  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
105  | 
\end{frame}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
106  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
107  | 
|
| 512 | 108  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
109  | 
\begin{frame}[c]
 | 
|
110  | 
\frametitle{Evil Regular Expressions}
 | 
|
111  | 
||
112  | 
\begin{itemize}
 | 
|
113  | 
\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip
 | 
|
114  | 
\item Evil regular expressions\medskip  | 
|
115  | 
\begin{itemize}
 | 
|
| 565 | 116  | 
\item \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}
 | 
| 512 | 117  | 
\item \bl{$(a^*)^*$}
 | 
118  | 
\item \bl{$([a$\,-\,$z]^+)^*$}
 | 
|
119  | 
\item \bl{$(a + a \cdot a)^*$}
 | 
|
| 565 | 120  | 
\item \bl{$(a + a^?)^*$}
 | 
| 512 | 121  | 
\end{itemize}
 | 
122  | 
||
| 569 | 123  | 
\item sometimes also called \alert{catastrophic backtracking}\bigskip
 | 
124  | 
\item \small\ldots I hope you have watched the video by the  | 
|
125  | 
StackExchange engineer  | 
|
| 512 | 126  | 
\end{itemize}
 | 
127  | 
||
128  | 
\end{frame}
 | 
|
129  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
130  | 
|
| 
 
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  | 
\begin{frame}[c]
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
133  | 
\frametitle{Languages}
 | 
| 16 | 134  | 
|
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
135  | 
\begin{itemize}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
136  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
137  | 
\item A \alert{\bf Language} is a set of strings, for example\medskip
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
138  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
139  | 
\bl{$\{[], hello, \textit{foobar}, a, abc\}$}
 | 
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
140  | 
\end{center}\bigskip
 | 
| 16 | 141  | 
|
| 
332
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
142  | 
\item \alert{\bf Concatenation} of strings and languages
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
143  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
144  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
145  | 
\begin{tabular}{rcl}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
146  | 
\bl{$\textit{foo}\;@\;bar$} & \bl{$=$} & \bl{$\textit{foobar}$}\medskip\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
147  | 
\bl{$A\;@\;B$} & \bl{$\dn$} & \bl{$\{ s_1\,@\,s_2 \;\mid\; s_1 \in A \wedge s_2 \in B\}$}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
148  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
149  | 
\end{center}
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
150  | 
\bigskip  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
151  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
152  | 
\small  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
153  | 
\item [] For example \bl{$A = \{foo, bar\}$}, \bl{$B = \{a, b\}$}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
154  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
155  | 
\[  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
156  | 
\bl{A \,@\, B = \{fooa, foob, bara, barb\}}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
157  | 
\]  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
158  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
159  | 
\end{itemize}  
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
160  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
161  | 
\end{frame}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
162  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
163  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
164  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
165  | 
\begin{frame}[c]
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
166  | 
\frametitle{The Power Operation}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
167  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
168  | 
\begin{itemize}
 | 
| 512 | 169  | 
\item The \alert{\textbf{\boldmath$n$th Power}} of a language:
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
170  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
171  | 
\begin{center}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
172  | 
\begin{tabular}{lcl}
 | 
| 431 | 173  | 
\bl{$A^0$}    & \bl{$\dn$} & \bl{$\{[]\}$}\\
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
174  | 
\bl{$A^{n+1}$} & \bl{$\dn$} & \bl{$A \,@\, A^n$}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
175  | 
\end{tabular}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
176  | 
\end{center}\bigskip
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
177  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
178  | 
\item[] For example  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
179  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
180  | 
\begin{center}
 | 
| 514 | 181  | 
\begin{tabular}{lcl@{\hspace{10mm}}l}
 | 
182  | 
\bl{$A^4$} & \bl{$=$} & \bl{$A \,@\, A \,@\, A \,@\, A$} & \bl{$(@\,\{[]\})$}\\
 | 
|
183  | 
\bl{$A^1$} & \bl{$=$} & \bl{$A$} & \bl{$(@\,\{[]\})$}\\
 | 
|
| 431 | 184  | 
\bl{$A^0$} & \bl{$=$} & \bl{$\{[]\}$}\\
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
185  | 
\end{tabular}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
186  | 
\end{center}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
187  | 
|
| 
261
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
188  | 
\end{itemize}  
 | 
| 
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
189  | 
|
| 
 
24531cfaa36a
updated handouts
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
258 
diff
changeset
 | 
190  | 
\end{frame}
 | 
| 16 | 191  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
192  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
193  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
194  | 
\begin{frame}[c]
 | 
| 
336
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
195  | 
\frametitle{Homework Question}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
196  | 
|
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
197  | 
\begin{itemize}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
198  | 
\item Say \bl{$A = \{[a],[b],[c],[d]\}$}.\bigskip
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
199  | 
|
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
200  | 
\begin{center}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
201  | 
How many strings are in \bl{$A^4$}?
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
202  | 
\end{center}\bigskip\medskip\pause
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
203  | 
|
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
204  | 
|
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
205  | 
\begin{center}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
206  | 
\begin{tabular}{l}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
207  | 
What if \bl{$A = \{[a],[b],[c],[]\}$};\\ 
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
208  | 
how many strings are then in \bl{$A^4$}?
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
209  | 
\end{tabular}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
210  | 
\end{center}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
211  | 
\end{itemize}  
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
212  | 
|
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
213  | 
\end{frame}
 | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
214  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
215  | 
|
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
216  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
217  | 
\begin{frame}[c]
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
218  | 
\frametitle{The Star Operation}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
219  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
220  | 
\begin{itemize}
 | 
| 514 | 221  | 
\item The \alert{\bf Kleene Star} of a \underline{language}:
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
222  | 
\bigskip  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
223  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
224  | 
\begin{center}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
225  | 
\begin{tabular}{c}
 | 
| 431 | 226  | 
\bl{$A\star \dn \bigcup_{0\le n} A^n$}
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
227  | 
\end{tabular}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
228  | 
\end{center}\bigskip
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
229  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
230  | 
\item[] This expands to  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
231  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
232  | 
\[  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
233  | 
\bl{A^0 \cup A^1 \cup A^2 \cup A^3 \cup A^4 \cup \ldots}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
234  | 
\]  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
235  | 
|
| 565 | 236  | 
or  | 
237  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
238  | 
\small  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
239  | 
\[  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
240  | 
\bl{\{[]\} \;\cup\; A \;\cup\; A\,@\,A \;\cup\; 
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
241  | 
A\,@\,A\,@\,A \;\cup\; A\,@\,A\,@\,A\,@\,A \cup \ldots}  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
242  | 
\]  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
243  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
244  | 
\end{itemize}  
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
245  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
246  | 
\end{frame}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
247  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
248  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
249  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
250  | 
\begin{frame}[c]
 | 
| 565 | 251  | 
\frametitle{
 | 
252  | 
The Meaning of a\\[-2mm]  | 
|
253  | 
Regular Expression}  | 
|
| 507 | 254  | 
|
255  | 
\begin{textblock}{15}(1,4)
 | 
|
256  | 
 \begin{tabular}{rcl}
 | 
|
257  | 
 \bl{$L(\ZERO)$}  & \bl{$\dn$} & \bl{$\{\}$}\\
 | 
|
258  | 
 \bl{$L(\ONE)$}     & \bl{$\dn$} & \bl{$\{[]\}$}\\
 | 
|
259  | 
 \bl{$L(c)$}            & \bl{$\dn$} & \bl{$\{[c]\}$}\\
 | 
|
260  | 
 \bl{$L(r_1 + r_2)$}    & \bl{$\dn$} & \bl{$L(r_1) \cup L(r_2)$}\\
 | 
|
261  | 
 \bl{$L(r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$\{ s_1 \,@\, s_2 \;|\; s_1 \in L(r_1) \wedge s_2 \in L(r_2) \}$}\\
 | 
|
262  | 
 \bl{$L(r^*)$}           & \bl{$\dn$} & \bl{$(L(r))\star \quad\dn \bigcup_{0 \le n} L(r)^n$}\\
 | 
|
263  | 
  \end{tabular}
 | 
|
264  | 
\end{textblock}
 | 
|
265  | 
||
| 514 | 266  | 
\begin{textblock}{9}(6,12)\small
 | 
| 507 | 267  | 
\bl{$L$} is a function from regular expressions to 
 | 
| 514 | 268  | 
sets of strings (languages):\smallskip\\  | 
| 507 | 269  | 
\bl{$L$ : Rexp $\Rightarrow$ Set$[$String$]$}
 | 
270  | 
\end{textblock}
 | 
|
271  | 
||
272  | 
\end{frame}
 | 
|
273  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
274  | 
||
| 566 | 275  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
276  | 
\begin{frame}[c]
 | 
|
277  | 
\frametitle{\begin{tabular}{c}\\[3cm]\huge\alert{Questions?}\end{tabular}}
 | 
|
278  | 
||
279  | 
\bigskip  | 
|
280  | 
homework (written exam 80\%)\\  | 
|
281  | 
coursework (20\%; first one today)\\  | 
|
| 567 | 282  | 
submission Fridays @ 18:00 -- accepted until Mondays  | 
| 566 | 283  | 
\mbox{}
 | 
284  | 
\end{frame}
 | 
|
285  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
286  | 
||
287  | 
||
| 507 | 288  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 565 | 289  | 
\begin{frame}[t]
 | 
290  | 
\frametitle{Semantic Derivative\\[5mm]}
 | 
|
291  | 
||
292  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
293  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
294  | 
\begin{itemize}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
295  | 
\item The \alert{\bf Semantic Derivative} of a 
 | 
| 565 | 296  | 
\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
 | 
297  | 
\bigskip  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
298  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
299  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
300  | 
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
 | 
| 565 | 301  | 
\end{center}\bigskip
 | 
| 
335
 
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  | 
For \bl{$A = \{\textit{foo}, \textit{bar}, \textit{frak}\}$} then
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
304  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
305  | 
\begin{center}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
306  | 
\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
307  | 
$\Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
308  | 
$\Der\,b\,A$ & $=$ &  $\{\textit{ar}\}$\\  
 | 
| 565 | 309  | 
$\Der\,a\,A$ & $=$ & $\{\}$\pause
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
310  | 
\end{tabular}}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
311  | 
\end{center}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
312  | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
313  | 
\small  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
314  | 
We can extend this definition to strings  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
315  | 
\[  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
316  | 
\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
 | 
317  | 
\]  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
318  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
319  | 
\end{itemize}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
320  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
321  | 
\end{frame}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
322  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
323  | 
|
| 512 | 324  | 
|
325  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
326  | 
\begin{frame}[c]
 | 
|
| 565 | 327  | 
\frametitle{The Specification\\ for Matching}
 | 
| 512 | 328  | 
|
329  | 
\begin{bubble}[10cm]
 | 
|
330  | 
\large  | 
|
331  | 
A regular expression \bl{$r$} matches a string~\bl{$s$} 
 | 
|
332  | 
provided  | 
|
333  | 
||
334  | 
\begin{center}
 | 
|
335  | 
\bl{$s \in L(r)$}\\ 
 | 
|
336  | 
\end{center}
 | 
|
337  | 
\end{bubble}\bigskip\bigskip
 | 
|
338  | 
||
339  | 
\ldots and the point of the this lecture is  | 
|
340  | 
to decide this problem as fast as possible  | 
|
341  | 
(unlike Python, Ruby, Java etc)  | 
|
342  | 
||
343  | 
\end{frame}
 | 
|
344  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
345  | 
||
346  | 
||
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
347  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
348  | 
\begin{frame}[t]
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
349  | 
\frametitle{Regular Expressions}
 | 
| 7 | 350  | 
|
| 15 | 351  | 
Their inductive definition:  | 
352  | 
||
353  | 
||
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
354  | 
\begin{textblock}{6}(2,7.5)
 | 
| 7 | 355  | 
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
 | 
| 514 | 356  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & nothing\\
 | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
357  | 
         & \bl{$\mid$} & \bl{$\ONE$}       & empty string / \pcode{""} / $[]$\\
 | 
| 514 | 358  | 
         & \bl{$\mid$} & \bl{$c$}              & single character\\
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
359  | 
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}  & sequence\\
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
360  | 
         & \bl{$\mid$} & \bl{$r_1 + r_2$}      & alternative / choice\\
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
361  | 
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
 | 
| 7 | 362  | 
  \end{tabular}
 | 
| 
336
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
363  | 
\end{textblock}
 | 
| 7 | 364  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
365  | 
\only<2->{\footnotesize
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
366  | 
\begin{textblock}{9}(2,0.5)
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
367  | 
\begin{bubble}[9.8cm]
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
368  | 
\lstinputlisting{../progs/app01.scala}
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
369  | 
\end{bubble}
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
370  | 
\end{textblock}}  
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
371  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
372  | 
\end{frame}
 | 
| 16 | 373  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
374  | 
||
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
375  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
332
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
376  | 
\begin{frame}[c]
 | 
| 565 | 377  | 
\frametitle{
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
378  | 
When Are Two Regular\\[-1mm]  | 
| 565 | 379  | 
Expressions Equivalent?}  | 
380  | 
||
| 
332
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
381  | 
\large  | 
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
382  | 
\begin{center}
 | 
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
383  | 
\bl{$r_1 \equiv r_2 \;\;\dn\;\; L(r_1) = L(r_2)$}
 | 
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
384  | 
\end{center}  
 | 
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
385  | 
|
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
386  | 
\end{frame}
 | 
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
387  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
388  | 
|
| 
 
4755ad4b457b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
changeset
 | 
389  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
390  | 
\begin{frame}[t]
 | 
| 
336
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
391  | 
\frametitle{Concrete Equivalences}
 | 
| 16 | 392  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
393  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
394  | 
\bl{\begin{tabular}{rcl}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
395  | 
$(a + b) + c$ & $\equiv$ & $a + (b + c)$\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
396  | 
$a + a$ & $\equiv$ & $a$\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
397  | 
$a + b$ & $\equiv$ & $b + a$\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
398  | 
$(a \cdot b) \cdot c$ & $\equiv$ & $a \cdot (b \cdot c)$\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
399  | 
$c \cdot (a + b)$ & $\equiv$ & $(c \cdot a) + (c \cdot b)$\bigskip\bigskip\\\pause  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
400  | 
$a \cdot a$ & $\not\equiv$ & $a$\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
401  | 
$a + (b \cdot c)$ & $\not\equiv$ & $(a + b) \cdot (a + c)$\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
402  | 
\end{tabular}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
403  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
404  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
405  | 
\end{frame}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
406  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
407  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
408  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
409  | 
\begin{frame}[t]
 | 
| 
336
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
410  | 
\frametitle{Corner Cases}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
411  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
412  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
413  | 
\bl{\begin{tabular}{rcl}
 | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
414  | 
$a \cdot \ZERO$ & $\not\equiv$ & $a$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
415  | 
$a + \ONE$ & $\not\equiv$ & $a$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
416  | 
$\ONE$ & $\equiv$ & $\ZERO^*$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
417  | 
$\ONE^*$ & $\equiv$ & $\ONE$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
418  | 
$\ZERO^*$ & $\not\equiv$ & $\ZERO$\\  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
419  | 
\end{tabular}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
420  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
421  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
422  | 
\end{frame}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
423  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
424  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
425  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
426  | 
\begin{frame}[t]
 | 
| 
336
 
7c80b9b6f713
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
335 
diff
changeset
 | 
427  | 
\frametitle{Simplification Rules}
 | 
| 565 | 428  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
429  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
430  | 
\bl{\begin{tabular}{rcl}
 | 
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
431  | 
$r + \ZERO$ & $\equiv$ & $r$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
432  | 
$\ZERO + r$ & $\equiv$ & $r$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
433  | 
$r \cdot \ONE$ & $\equiv$ & $r$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
434  | 
$\ONE \cdot r$ & $\equiv$ & $r$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
435  | 
$r \cdot \ZERO$ & $\equiv$ & $\ZERO$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
436  | 
$\ZERO \cdot r$ & $\equiv$ & $\ZERO$\\  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
437  | 
$r + r$ & $\equiv$ & $r$  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
438  | 
\end{tabular}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
439  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
440  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
441  | 
\end{frame}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
442  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 16 | 443  | 
|
| 568 | 444  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
445  | 
\begin{frame}[c]
 | 
|
446  | 
\frametitle{Another Homework\\[-2mm] Question}
 | 
|
447  | 
||
448  | 
\begin{itemize}
 | 
|
449  | 
\item How many basic regular expressions are there to match  | 
|
450  | 
  the string \bl{$abcd$}\,?\pause
 | 
|
451  | 
\item How many if they cannot include  | 
|
452  | 
  \bl{$\ONE$} and \bl{$\ZERO$}\/?\pause
 | 
|
453  | 
\item How many if they are also not  | 
|
454  | 
allowed to contain stars?\pause  | 
|
455  | 
\item How many if they are also  | 
|
456  | 
      not allowed to contain \bl{$\_ + \_$}\/? 
 | 
|
457  | 
\end{itemize}  
 | 
|
458  | 
||
459  | 
\end{frame}
 | 
|
460  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
118
 
6a5b59690f7d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
117 
diff
changeset
 | 
461  | 
|
| 
 
6a5b59690f7d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
117 
diff
changeset
 | 
462  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 573 | 463  | 
\begin{frame}[c]
 | 
464  | 
\frametitle{\mbox{Brzozowski's Algorithm (1)}}
 | 
|
| 11 | 465  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
466  | 
|
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
467  | 
\ldots{}whether a regular expression can match the empty string:
 | 
| 11 | 468  | 
\begin{center}
 | 
| 
117
 
25999de692b2
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
469  | 
\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
 | 
470  | 
\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
 | 
471  | 
\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
 | 
472  | 
\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
 | 
473  | 
\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
 | 
474  | 
\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
 | 
475  | 
\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
 | 
476  | 
\end{tabular}
 | 
| 16 | 477  | 
\end{center}
 | 
478  | 
||
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
479  | 
\end{frame}
 | 
| 11 | 480  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
481  | 
||
482  | 
||
483  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
484  | 
\begin{frame}[c]
 | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
485  | 
\frametitle{The Derivative of a Rexp}
 | 
| 7 | 486  | 
|
487  | 
\large  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
488  | 
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
 | 
489  | 
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
 | 
| 7 | 490  | 
|
491  | 
\small  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
492  | 
\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
 | 
493  | 
\end{frame}
 | 
| 7 | 494  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
495  | 
||
496  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
497  | 
\begin{frame}[c]
 | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
498  | 
\frametitle{The Derivative of a Rexp}
 | 
| 7 | 499  | 
|
500  | 
\begin{center}
 | 
|
501  | 
\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
 | 
502  | 
  \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
 | 
503  | 
  \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
 | 
504  | 
  \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
 | 
505  | 
  \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
 | 
506  | 
  \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
 | 
507  | 
  & & \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
 | 
508  | 
  & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
509  | 
  \bl{$\der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$} &\bigskip\\\pause
 | 
| 7 | 510  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
511  | 
  \bl{$\ders\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
512  | 
  \bl{$\ders\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\ders\,s\,(\der\,c\,r)$} & \\
 | 
| 7 | 513  | 
  \end{tabular}
 | 
514  | 
\end{center}
 | 
|
515  | 
||
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
516  | 
\end{frame}
 | 
| 7 | 517  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
518  | 
||
519  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
520  | 
\begin{frame}[c]
 | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
521  | 
\frametitle{Examples}
 | 
| 7 | 522  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
523  | 
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
 | 
| 7 | 524  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
525  | 
\begin{center}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
526  | 
\begin{tabular}{l}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
527  | 
\bl{$\der\,a\,r =\;?$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
528  | 
\bl{$\der\,b\,r =\;?$}\\
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
529  | 
\bl{$\der\,c\,r =\;?$}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
530  | 
\end{tabular}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
531  | 
\end{center}
 | 
| 7 | 532  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
533  | 
\end{frame}
 | 
| 7 | 534  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
535  | 
||
| 17 | 536  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 431 | 537  | 
\begin{frame}[c]
 | 
| 565 | 538  | 
\frametitle{\mbox{The Brzozowski Algorithm}}
 | 
| 431 | 539  | 
|
540  | 
\begin{center}
 | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
541  | 
\begin{tabular}{l} 
 | 
| 565 | 542  | 
\bl{$\textit{matches}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}  
 | 
| 431 | 543  | 
\end{tabular}
 | 
544  | 
\end{center}
 | 
|
545  | 
||
546  | 
||
547  | 
\end{frame}
 | 
|
548  | 
%%%%%%%%%%%%%%%%%  | 
|
549  | 
||
550  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 17 | 551  | 
\begin{frame}[t]
 | 
| 565 | 552  | 
\frametitle{Brzozowski: An Example}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
553  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
554  | 
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
 | 
555  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
556  | 
\begin{tabular}{@{}rl@{}l@{}}
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
557  | 
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
 | 
558  | 
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
 | 
559  | 
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
 | 
560  | 
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
 | 
561  | 
        & test whether \bl{$r_4$} can recognise\\
 | 
| 565 | 562  | 
& the empty string\medskip\\  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
563  | 
Output: & result of the test\\  | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
564  | 
        & $\Rightarrow \bl{\textit{true}} \,\text{or}\, 
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
565  | 
                       \bl{\textit{false}}$\\        
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
566  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
567  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
568  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
569  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
570  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
571  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
572  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
573  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
574  | 
\begin{frame}[c]
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
575  | 
\frametitle{The Idea of the Algorithm}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
576  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
577  | 
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
 | 
578  | 
expression \bl{$r_1$} then\medskip
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
579  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
580  | 
\begin{enumerate}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
581  | 
\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
 | 
582  | 
\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
 | 
583  | 
\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
 | 
584  | 
\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
 | 
585  | 
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
 | 
586  | 
\end{enumerate}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
587  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
588  | 
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
 | 
589  | 
\end{frame}
 | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
590  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
591  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
592  | 
|
| 
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
593  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
594  | 
\begin{frame}[c]
 | 
| 565 | 595  | 
\frametitle{Oops\ldots \;\bl{$a^{?\{n\}} \cdot a^{\{n\}}$}}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
596  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
597  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
598  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
599  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
600  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
601  | 
    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
 | 
602  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
603  | 
enlargelimits=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
604  | 
    xtick={0,5,...,30},
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
605  | 
xmax=31,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
606  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
607  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
608  | 
axis lines=left,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
609  | 
width=7cm,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
610  | 
height=7cm,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
611  | 
    legend entries={Python,Ruby,Scala V1},  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
612  | 
legend pos=outer north east,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
613  | 
legend cell align=left  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
614  | 
]  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
615  | 
\addplot[blue,mark=*, mark options={fill=white}] 
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
616  | 
  table {re-python.data};
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
617  | 
\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
 | 
618  | 
  table {re-ruby.data};  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
619  | 
\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
 | 
620  | 
  table {re1.data};  
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
621  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
622  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
623  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
624  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
625  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
626  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
627  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
628  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 565 | 629  | 
\begin{frame}[t]
 | 
630  | 
\frametitle{A Problem\medskip}
 | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
631  | 
|
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
632  | 
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
 | 
633  | 
sequence regular expression:  | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
634  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
635  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
636  | 
\begin{tabular}{rl}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
637  | 
1: & \bl{$a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
638  | 
2: & \bl{$a\cdot a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
639  | 
3: & \bl{$a\cdot a\cdot a$}\\
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
640  | 
& \ldots\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
641  | 
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
 | 
642  | 
& \ldots\\  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
643  | 
20:  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
644  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
645  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
646  | 
|
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
647  | 
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
 | 
648  | 
as \bl{$a + \ONE$}.
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
649  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
650  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
651  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
652  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
653  | 
\begin{frame}[c]
 | 
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
654  | 
\frametitle{Solving the Problem}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
655  | 
|
| 514 | 656  | 
What happens if we extend our regular expressions with explicit  | 
657  | 
constructors  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
658  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
659  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
660  | 
\begin{tabular}{rcl}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
661  | 
\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
 | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
662  | 
             & \bl{$\mid$} & \bl{$r^{\{n\}}$}\\
 | 
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
663  | 
             & \bl{$\mid$} & \bl{$r^?$} 
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
664  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
665  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
666  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
667  | 
What is their meaning?\\  | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
668  | 
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
 | 
669  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
670  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
671  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
672  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
673  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
674  | 
\begin{frame}[t]
 | 
| 565 | 675  | 
\frametitle{Brzozowski: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
676  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
677  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
678  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
679  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
680  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
681  | 
    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
 | 
682  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
683  | 
enlargelimits=false,  | 
| 
434
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
684  | 
    xtick={0,200,...,1100},
 | 
| 
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
685  | 
xmax=1200,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
686  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
687  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
688  | 
axis lines=left,  | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
689  | 
width=8cm,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
690  | 
height=6.5cm,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
691  | 
    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
 | 
692  | 
legend pos=outer north east,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
693  | 
legend cell align=left  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
694  | 
]  | 
| 
434
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
695  | 
\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
 | 
696  | 
\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
 | 
697  | 
\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
 | 
698  | 
\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
 | 
699  | 
\end{axis}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
700  | 
\end{tikzpicture}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
701  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
702  | 
|
| 
335
 
2d112a7b29eb
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
332 
diff
changeset
 | 
703  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
704  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
705  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
706  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
707  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
708  | 
\begin{frame}[c]
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
709  | 
\frametitle{Examples}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
710  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
711  | 
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
 | 
712  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
713  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
714  | 
\begin{tabular}{l}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
715  | 
\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
 | 
716  | 
\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
 | 
717  | 
\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
 | 
718  | 
\end{tabular}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
719  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
720  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
721  | 
What are these regular expressions equivalent to?  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
722  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
723  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
724  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
725  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
726  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
727  | 
\begin{frame}[c]
 | 
| 565 | 728  | 
\frametitle{Simplification Rules}
 | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
729  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
730  | 
\begin{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
731  | 
\bl{\begin{tabular}{rcl}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
732  | 
$r + \ZERO$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
733  | 
$\ZERO + r$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
734  | 
$r \cdot \ONE$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
735  | 
$\ONE \cdot r$ & $\Rightarrow$ & $r$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
736  | 
$r \cdot \ZERO$ & $\Rightarrow$ & $\ZERO$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
737  | 
$\ZERO \cdot r$ & $\Rightarrow$ & $\ZERO$\\  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
738  | 
$r + r$ & $\Rightarrow$ & $r$  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
739  | 
\end{tabular}}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
740  | 
\end{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
741  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
742  | 
\footnotesize  | 
| 565 | 743  | 
\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
 | 
744  | 
\end{frame}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
745  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
746  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
747  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
748  | 
\begin{frame}[c]
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
749  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
750  | 
\footnotesize  | 
| 565 | 751  | 
\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
 | 
752  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
753  | 
\end{frame}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
754  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
755  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
756  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
757  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
758  | 
\begin{frame}[t]
 | 
| 565 | 759  | 
\frametitle{Brzozowski: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
760  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
761  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
762  | 
\begin{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
763  | 
\begin{axis}[
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
764  | 
    xlabel={$n$},
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
765  | 
    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
 | 
766  | 
    ylabel={time in secs},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
767  | 
enlargelimits=false,  | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
768  | 
    xtick={0,5000,...,10000},
 | 
| 
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
769  | 
xmax=11000,  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
770  | 
ymax=35,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
771  | 
    ytick={0,5,...,30},
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
772  | 
scaled ticks=false,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
773  | 
axis lines=left,  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
774  | 
width=9cm,  | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
775  | 
height=7cm,  | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
776  | 
    legend entries={Scala V2,Scala V3},  
 | 
| 
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
777  | 
legend pos=north east  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
778  | 
]  | 
| 
434
 
8664ff87cd77
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
433 
diff
changeset
 | 
779  | 
\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
 | 
780  | 
\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
 | 
781  | 
\end{axis}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
782  | 
\end{tikzpicture}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
783  | 
\end{center}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
784  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
785  | 
\end{frame}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
786  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
787  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
788  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
789  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
790  | 
\begin{frame}[c]
 | 
| 565 | 791  | 
  \frametitle{
 | 
792  | 
Another Example\\[-1mm]  | 
|
793  | 
    in Java \liningnums{8} and Python}
 | 
|
794  | 
||
795  | 
\begin{center}
 | 
|
796  | 
\begin{tikzpicture}
 | 
|
797  | 
  \begin{axis}[
 | 
|
798  | 
    xlabel={$n$},
 | 
|
799  | 
    x label style={at={(1.05,0.0)}},
 | 
|
800  | 
    ylabel={time in secs},
 | 
|
801  | 
enlargelimits=false,  | 
|
802  | 
    xtick={0,5,...,30},
 | 
|
803  | 
xmax=33,  | 
|
804  | 
ymax=35,  | 
|
805  | 
    ytick={0,10,...,30},
 | 
|
806  | 
scaled ticks=false,  | 
|
807  | 
axis lines=left,  | 
|
808  | 
width=9cm,  | 
|
809  | 
height=5cm,  | 
|
810  | 
    legend entries={Java 8, Python},  
 | 
|
811  | 
legend pos=north west,  | 
|
812  | 
legend cell align=left]  | 
|
813  | 
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
 | 
|
814  | 
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
 | 
|
815  | 
\end{axis}
 | 
|
816  | 
\end{tikzpicture}
 | 
|
817  | 
\end{center}
 | 
|
818  | 
||
819  | 
Regex: \bl{$(a^*)^* \cdot b$}
 | 
|
820  | 
||
821  | 
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
 | 
|
822  | 
||
823  | 
\end{frame}
 | 
|
824  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
825  | 
||
826  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
827  | 
\begin{frame}[c]
 | 
|
828  | 
\frametitle{Same Example in Java \liningnums{9}+}
 | 
|
829  | 
||
830  | 
\begin{center}
 | 
|
831  | 
\begin{tikzpicture}
 | 
|
832  | 
  \begin{axis}[
 | 
|
833  | 
    xlabel={$n$},
 | 
|
834  | 
    x label style={at={(1.09,-0.15)}},
 | 
|
835  | 
    ylabel={time in secs},
 | 
|
836  | 
scaled x ticks=false,  | 
|
837  | 
enlargelimits=false,  | 
|
838  | 
xtick distance=10000,  | 
|
839  | 
xmax=44000,  | 
|
840  | 
    ytick={0,10,...,30}, 
 | 
|
841  | 
ymax=35,  | 
|
842  | 
axis lines=left,  | 
|
843  | 
width=9cm,  | 
|
844  | 
height=5cm,  | 
|
845  | 
    legend entries={Java \liningnums{9}+},
 | 
|
846  | 
legend pos=north west,  | 
|
847  | 
legend cell align=left]  | 
|
848  | 
\addplot[blue,mark=square*,mark options={fill=white}] table {re-java9.data};
 | 
|
849  | 
\end{axis}
 | 
|
850  | 
\end{tikzpicture}
 | 
|
851  | 
\end{center}
 | 
|
852  | 
||
853  | 
Regex: \bl{$(a^*)^* \cdot b$}
 | 
|
854  | 
||
855  | 
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
 | 
|
856  | 
||
857  | 
\end{frame}
 | 
|
858  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
859  | 
||
860  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
861  | 
\begin{frame}[c]
 | 
|
862  | 
\frametitle{and with Brzozowski}
 | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
863  | 
|
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
864  | 
\begin{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
865  | 
\begin{tikzpicture}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
866  | 
  \begin{axis}[
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
867  | 
    xlabel={$n$},
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
868  | 
    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
 | 
869  | 
    ylabel={time in secs},
 | 
| 565 | 870  | 
scaled x ticks=false,  | 
871  | 
xtick distance=2000000,  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
872  | 
enlargelimits=false,  | 
| 565 | 873  | 
xmax=6400000,  | 
| 514 | 874  | 
    ytick={0,10,...,30},
 | 
875  | 
ymax=35,  | 
|
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
876  | 
axis lines=left,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
877  | 
width=9cm,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
878  | 
height=5cm,  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
879  | 
    legend entries={Scala V3},
 | 
| 565 | 880  | 
legend pos=north west,  | 
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
881  | 
legend cell align=left]  | 
| 514 | 882  | 
%\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
 | 
883  | 
\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
 | 
884  | 
\end{axis}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
885  | 
\end{tikzpicture}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
886  | 
\end{center}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
887  | 
|
| 565 | 888  | 
Regex: \bl{$(a^*)^* \cdot b$}
 | 
889  | 
||
890  | 
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
 | 
|
891  | 
||
| 
435
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
892  | 
\end{frame}
 | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
893  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
e08431a78f66
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
434 
diff
changeset
 | 
894  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
895  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 573 | 896  | 
\begin{frame}[c]
 | 
897  | 
\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
 | 
898  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
899  | 
\begin{itemize}
 | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
900  | 
\item extends to most regular expressions, for example  | 
| 573 | 901  | 
\bl{$\sim r$} (next slide)
 | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
902  | 
|
| 573 | 903  | 
\item is easy to implement in a functional language (slide after)  | 
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
904  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
905  | 
\item the algorithm is already quite old; there is still  | 
| 514 | 906  | 
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
 | 
907  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
908  | 
\item we can prove its correctness\ldots  | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
909  | 
\end{itemize}
 | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
910  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
911  | 
\end{frame}
 | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
912  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
913  | 
|
| 
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
914  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 566 | 915  | 
\begin{frame}[c]
 | 
916  | 
\frametitle{Negation of Regular Expr's}
 | 
|
917  | 
||
918  | 
\begin{itemize}
 | 
|
919  | 
\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
 | 
|
920  | 
\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
 | 
|
921  | 
\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
 | 
|
922  | 
\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
 | 
|
923  | 
\end{itemize}\bigskip\pause
 | 
|
924  | 
||
925  | 
Used often for recognising comments:  | 
|
926  | 
||
927  | 
\[  | 
|
928  | 
\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
 | 
|
929  | 
\]  | 
|
930  | 
||
931  | 
\end{frame}
 | 
|
932  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
933  | 
||
934  | 
||
935  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
936  | 
\begin{frame}[c]
 | 
|
937  | 
\frametitle{Coursework}
 | 
|
938  | 
||
939  | 
\underline{Strand 1:}
 | 
|
940  | 
||
941  | 
\begin{itemize}
 | 
|
942  | 
\item Submission on Friday 12 October\\accepted until Monday 15 @ 18:00\medskip  | 
|
943  | 
\item source code needs to be submitted as well\medskip  | 
|
944  | 
\item you can re-use my Scala code from KEATS \\  | 
|
945  | 
or use any programming language you like\medskip  | 
|
946  | 
\item \small https://nms.kcl.ac.uk/christian.urban/ProgInScala2ed.pdf\normalsize  | 
|
947  | 
\end{itemize}  
 | 
|
948  | 
||
949  | 
\end{frame}
 | 
|
950  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
951  | 
||
952  | 
||
953  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
342
 
c235e0aeb8df
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
338 
diff
changeset
 | 
954  | 
\begin{frame}[t]
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
955  | 
\frametitle{Proofs about Rexps}
 | 
| 17 | 956  | 
|
957  | 
Remember their inductive definition:\\[5cm]  | 
|
958  | 
||
959  | 
\begin{textblock}{6}(5,5)
 | 
|
960  | 
  \begin{tabular}{@ {}rrl}
 | 
|
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
961  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
 | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
962  | 
         & \bl{$\mid$} & \bl{$\ONE$}     \\
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
963  | 
         & \bl{$\mid$} & \bl{$c$}            \\
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
964  | 
         & \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
 | 
965  | 
         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\
 | 
| 
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
966  | 
         & \bl{$\mid$} & \bl{$r^*$}          \\
 | 
| 17 | 967  | 
  \end{tabular}
 | 
968  | 
  \end{textblock}
 | 
|
969  | 
||
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
970  | 
If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
 | 
| 17 | 971  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
972  | 
\end{frame}
 | 
| 17 | 973  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
974  | 
||
975  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
976  | 
\begin{frame}[c]
 | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
977  | 
\frametitle{Proofs about Rexp (2)}
 | 
| 17 | 978  | 
|
979  | 
\begin{itemize}
 | 
|
| 
429
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
980  | 
\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
 | 
981  | 
\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
 | 
982  | 
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
 | 
983  | 
\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
 | 
984  | 
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
 | 
985  | 
\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
 | 
986  | 
holds for \bl{$r$}.
 | 
| 17 | 987  | 
\end{itemize}
 | 
988  | 
||
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
989  | 
\end{frame}
 | 
| 17 | 990  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
991  | 
||
992  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
993  | 
\begin{frame}[c]
 | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
994  | 
\frametitle{Proofs about Rexp (3)}
 | 
| 17 | 995  | 
|
996  | 
Assume \bl{$P(r)$} is the property:
 | 
|
997  | 
||
998  | 
\begin{center}
 | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
999  | 
\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
 | 
| 17 | 1000  | 
\end{center}
 | 
1001  | 
||
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1002  | 
\end{frame}
 | 
| 17 | 1003  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1004  | 
||
1005  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1006  | 
\begin{frame}[c]
 | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1007  | 
\frametitle{Proofs about Rexp (4)}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1008  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1009  | 
\begin{center}
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1010  | 
\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
 | 
1011  | 
$rev(\ZERO)$ & $\dn$ & $\ZERO$\\  | 
| 
 
7e71c947ec69
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
398 
diff
changeset
 | 
1012  | 
$rev(\ONE)$ & $\dn$ & $\ONE$\\  | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1013  | 
$rev(c)$ & $\dn$ & $c$\\  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1014  | 
$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
 | 
1015  | 
$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
 | 
1016  | 
$rev(r^*)$ & $\dn$ & $rev(r)^*$\\  | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1017  | 
\end{tabular}}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1018  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1019  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1020  | 
We can prove  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1021  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1022  | 
\begin{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1023  | 
\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
 | 
1024  | 
\end{center}
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1025  | 
|
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1026  | 
by induction on \bl{$r$}.
 | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1027  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1028  | 
\end{frame}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1029  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1030  | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1031  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1032  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1033  | 
\begin{frame}[c]
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1034  | 
\frametitle{\begin{tabular}{c}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1035  | 
  Correctness Proof\\[-1mm] for our Matcher\end{tabular}}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1036  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1037  | 
\begin{itemize}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1038  | 
\item We started from  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1039  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1040  | 
\begin{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1041  | 
\begin{tabular}{rp{4cm}}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1042  | 
  & \bl{$s \in L(r)$}\medskip\\
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1043  | 
\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
 | 
1044  | 
\end{tabular}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1045  | 
\end{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1046  | 
|
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1047  | 
\item if we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1048  | 
have  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1049  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1050  | 
\begin{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1051  | 
\begin{tabular}{rp{4cm}}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1052  | 
\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
 | 
1053  | 
\bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1054  | 
\bl{$\dn$} & \bl{$matches\,s\,r$}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1055  | 
\end{tabular}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1056  | 
\end{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1057  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1058  | 
\end{itemize}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1059  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1060  | 
\end{frame}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1061  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1062  | 
|
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1063  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1064  | 
\begin{frame}[c]
 | 
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1065  | 
\frametitle{Proofs about Rexp (5)}
 | 
| 
263
 
92e6985018ae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
261 
diff
changeset
 | 
1066  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1067  | 
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
 | 
1068  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1069  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1070  | 
\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
 | 
1071  | 
\end{center}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1072  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1073  | 
We can prove  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1074  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1075  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1076  | 
\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
 | 
1077  | 
\end{center}
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1078  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1079  | 
by induction on \bl{$r$}.
 | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1080  | 
|
| 
337
 
885ac2b6c27d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
336 
diff
changeset
 | 
1081  | 
\end{frame}
 | 
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1082  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1083  | 
|
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1084  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1085  | 
\begin{frame}[c]
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1086  | 
\frametitle{Proofs about Strings}
 | 
| 17 | 1087  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1088  | 
If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip
 | 
| 17 | 1089  | 
|
1090  | 
\begin{itemize}
 | 
|
1091  | 
\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
 | 
1092  | 
\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
 | 
1093  | 
already holds for \bl{$s$}
 | 
| 17 | 1094  | 
\end{itemize}
 | 
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1095  | 
\end{frame}
 | 
| 17 | 1096  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1097  | 
||
| 19 | 1098  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1099  | 
\begin{frame}[c]
 | 
|
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1100  | 
\frametitle{Proofs about Strings (2)}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1101  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1102  | 
We can then prove  | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1103  | 
|
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1104  | 
\begin{center}
 | 
| 
433
 
c08290ee4f1f
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
431 
diff
changeset
 | 
1105  | 
\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
 | 
1106  | 
\end{center}
 | 
| 
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1107  | 
|
| 19 | 1108  | 
|
| 
119
 
a6684e8961d0
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
118 
diff
changeset
 | 
1109  | 
We can finally prove  | 
| 19 | 1110  | 
|
1111  | 
\begin{center}
 | 
|
| 
345
 
0922b3e01289
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
342 
diff
changeset
 | 
1112  | 
\bl{$matches\,s\,r$}  if and only if  \bl{$s \in L(r)$} 
 | 
| 19 | 1113  | 
\end{center}
 | 
1114  | 
||
1115  | 
||
| 
338
 
f16120cb4e19
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
337 
diff
changeset
 | 
1116  | 
\end{frame}
 | 
| 19 | 1117  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 17 | 1118  | 
|
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1119  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1120  | 
\begin{frame}[c]
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1121  | 
\frametitle{Epilogue}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1122  | 
|
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1123  | 
\footnotesize  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1124  | 
\begin{center}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1125  | 
\begin{tabular}{cc}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1126  | 
\begin{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1127  | 
\begin{axis}[
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1128  | 
    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
 | 
1129  | 
    xlabel={$n$},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1130  | 
    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
 | 
1131  | 
    ylabel={time in secs},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1132  | 
enlargelimits=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1133  | 
xmax=7100000,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1134  | 
    ytick={0,5,...,30},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1135  | 
ymax=33,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1136  | 
%scaled ticks=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1137  | 
axis lines=left,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1138  | 
width=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1139  | 
height=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1140  | 
    legend entries={Scala V3, Scala V4},
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1141  | 
    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
 | 
1142  | 
\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
 | 
1143  | 
\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
 | 
1144  | 
\end{axis}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1145  | 
\end{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1146  | 
&  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1147  | 
\begin{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1148  | 
\begin{axis}[
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1149  | 
    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
 | 
1150  | 
    xlabel={$n$},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1151  | 
    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
 | 
1152  | 
    ylabel={time in secs},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1153  | 
enlargelimits=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1154  | 
xmax=8100000,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1155  | 
    ytick={0,5,...,30},
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1156  | 
ymax=33,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1157  | 
%scaled ticks=false,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1158  | 
axis lines=left,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1159  | 
width=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1160  | 
height=5cm,  | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1161  | 
    legend entries={Scala V3, Scala V4},
 | 
| 
442
 
84d6714840c9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
436 
diff
changeset
 | 
1162  | 
    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
 | 
1163  | 
\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
 | 
1164  | 
\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
 | 
1165  | 
\end{axis}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1166  | 
\end{tikzpicture}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1167  | 
\end{tabular}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1168  | 
\end{center}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1169  | 
|
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1170  | 
\only<2->{\footnotesize
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1171  | 
\begin{textblock}{9}(0.5,8)
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1172  | 
\begin{bubble}[11.8cm]
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1173  | 
\lstinputlisting[numbers=none]{../progs/app52.scala}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1174  | 
\end{bubble}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1175  | 
\end{textblock}} 
 | 
| 510 | 1176  | 
|
| 
436
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1177  | 
|
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1178  | 
\end{frame}
 | 
| 
 
9213b8298ca9
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
435 
diff
changeset
 | 
1179  | 
|
| 7 | 1180  | 
\end{document}
 | 
1181  | 
||
1182  | 
%%% Local Variables:  | 
|
1183  | 
%%% mode: latex  | 
|
1184  | 
%%% TeX-master: t  | 
|
1185  | 
%%% End:  | 
|
1186  |