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