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