75 \end{center} |
75 \end{center} |
76 \end{frame}} |
76 \end{frame}} |
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
78 |
78 |
79 *} |
79 *} |
|
80 |
|
81 |
80 text_raw {* |
82 text_raw {* |
81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
82 \mode<presentation>{ |
84 \mode<presentation>{ |
83 \begin{frame}<1->[c] |
85 \begin{frame}<1->[c] |
84 \frametitle{My Background} |
86 \frametitle{My Background} |
85 |
87 |
86 \begin{itemize} |
88 \mbox{}\\[-10mm] |
87 \item researcher in Theoretical Computer Science\medskip |
89 \begin{itemize} |
88 |
90 \item My background is in theory and programming languages.\bigskip |
89 \item programmer on a \alert<2->{software system} with 800 kloc (though I am |
91 \pause |
90 responsible only for 35 kloc) |
92 |
91 \end{itemize} |
93 \item But I am also a programmer with a \alert<2>{software system} of around 800 kloc |
92 |
94 (though I am responsible for only appr.~35 kloc), |
93 \only<2->{ |
95 |
94 \begin{textblock}{6}(2,11) |
96 \item and I write papers. |
|
97 \end{itemize} |
|
98 |
|
99 \only<2>{ |
|
100 \begin{textblock}{6}(6.5,11.5) |
95 \begin{tikzpicture} |
101 \begin{tikzpicture} |
96 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
102 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
97 {\color{darkgray} |
103 {\color{darkgray} |
98 \begin{minipage}{4cm}\raggedright |
104 \begin{minipage}{6.5cm}\raggedright |
99 A theorem prover called {\bf Isabelle}. |
105 \begin{tabular}[b]{@ {}p{4.5cm}c@ {}} |
|
106 \raggedright |
|
107 The software is a theorem prover, called {\bf Isabelle}. |
|
108 & \mbox{}\hspace{-5mm}\raisebox{-14mm}{\includegraphics[scale=0.28]{isabelle1.png}} |
|
109 \end{tabular}% |
100 \end{minipage}}; |
110 \end{minipage}}; |
101 \end{tikzpicture} |
111 \end{tikzpicture} |
102 \end{textblock}} |
112 \end{textblock}} |
103 |
113 |
104 |
114 \only<4>{ |
105 \only<3>{ |
115 \begin{textblock}{6}(3,11.5) |
106 \begin{textblock}{6}(9,11) |
|
107 \begin{tikzpicture} |
116 \begin{tikzpicture} |
108 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
117 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
109 {\color{darkgray} |
118 {\color{darkgray} |
110 \begin{minipage}{4cm}\raggedright |
119 \begin{minipage}{9.6cm}\raggedright |
111 Like every other code, this code is very hard to |
120 So I can experience every day that writing error-free code is {\bf very, very hard} |
112 get correct. |
121 and that papers are also {\bf hard} to get correct. |
113 \end{minipage}}; |
122 \end{minipage}}; |
114 \end{tikzpicture} |
123 \end{tikzpicture} |
115 \end{textblock}} |
124 \end{textblock}} |
116 |
125 |
117 \end{frame}} |
126 \end{frame}} |
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
119 *} |
128 *} |
120 |
129 |
121 text_raw {* |
130 |
122 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
131 |
123 \mode<presentation>{ |
132 text_raw {* |
124 \begin{frame}<1->[t] |
133 |
125 \frametitle{Regular Expressions} |
134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
126 |
135 \mode<presentation>{ |
127 An example many (should) know about:\\ |
136 \begin{frame} |
128 \rd{\bf Regular Expressions:} |
137 \frametitle{Getting Papers Correct} |
129 |
138 |
130 \only<2>{ |
139 \begin{minipage}{1.1\textwidth} |
131 \begin{center} |
140 My work over the last 5 years.\\ |
132 \bl{[] $\;\;\;|\;\;\;$ c $\;\;\;|\;\;\;$ r$_1$$|$r$_2$ $\;\;\;|\;\;\;$ |
141 {\small (in the fields of programming languages, logic and lambda-calculi)} |
133 r$_1$$\cdot$r$_2$ $\;\;\;|\;\;\;$ r$^*$} |
142 \end{minipage}\bigskip |
134 \end{center}} |
143 |
135 \only<3->{ |
144 \only<1>{ |
136 \begin{center} |
145 \mbox{}\\[15mm] |
137 \begin{tabular}{@ {}rrll@ {}} |
146 \begin{center} |
138 \bl{r} & \bl{$::=$} & \bl{NULL} & \gr{(matches no string)}\\ |
147 \begin{tikzpicture}[node distance=0.5mm] |
139 & \bl{$\mid$} & \bl{EMPTY} & \gr{(matches the empty string, [])}\\ |
148 \node at (-1.0,-0.3) (proof) [double arrow, fill=gray,text=white, minimum height=2cm]{\bf Proof}; |
140 & \bl{$\mid$} & \bl{CHR c} & \gr{(matches the character c)}\\ |
149 \node [left=of proof]{\Large\bf Specification}; |
141 & \bl{$\mid$} & \bl{ALT r$_1$ r$_2$} & \gr{(alternative, r$_1 |\,$r$_2$)}\\ |
150 \node [right=of proof]{\Large\bf Code}; |
142 & \bl{$\mid$} & \bl{SEQ r$_1$ r$_2$} & \gr{(sequential, r$_1\cdot\,$r$_2$)}\\ |
|
143 & \bl{$\mid$} & \bl{STAR r} & \gr{(repeat, r$^*$)}\\ |
|
144 \end{tabular} |
|
145 \end{center}\medskip} |
|
146 |
|
147 \small |
|
148 \begin{textblock}{14.5}(1,12.5) |
|
149 \only<2->{\gr{(a$\cdot$b)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm} \{[], ab, abab, ababab, \ldots\}}\\} |
|
150 \only<2->{\gr{x$\cdot$(0 $|$ 1 $|$ 2 \ldots 8 $|$ 9)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm} |
|
151 \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}} |
|
152 \end{textblock} |
|
153 \end{frame}} |
|
154 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
155 *} |
|
156 |
|
157 text_raw {* |
|
158 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
159 \mode<presentation>{ |
|
160 \begin{frame}<1>[c] |
|
161 \frametitle{RegExp Matcher} |
|
162 |
|
163 Let's implement a regular expression matcher:\bigskip |
|
164 |
|
165 \begin{center} |
|
166 \begin{tikzpicture} |
|
167 %%\draw[help lines, black] (-3,0) grid (6,3); |
|
168 |
|
169 \draw[line width=1mm, red] (0.0,0.0) rectangle (4,2.3); |
|
170 \node[anchor=base] at (2,1) |
|
171 {\small\begin{tabular}{@ {}c@ {}}\Large\bf Regular\\ |
|
172 \Large\bf Expression \\ |
|
173 \Large\bf Matcher\end{tabular}}; |
|
174 |
|
175 \coordinate (m1) at (0,1.5); |
|
176 \draw (-2,2) node (m2) {\small\begin{tabular}{c}\bl{regular}\\[-1mm] \bl{expression}\end{tabular}}; |
|
177 \path[overlay, ->, line width = 1mm, shorten <=-3mm] (m2) edge (m1); |
|
178 |
|
179 \coordinate (s1) at (0,0.5); |
|
180 \draw (-1.8,-0) node (s2) {\small\begin{tabular}{c}\bl{string}\end{tabular}}; |
|
181 \path[overlay, ->, line width = 1mm, shorten <=-3mm] (s2) edge (s1); |
|
182 |
|
183 \coordinate (r1) at (4,1.2); |
|
184 \draw (6,1.2) node (r2) {\small\begin{tabular}{c}\bl{true}, \bl{false}\end{tabular}}; |
|
185 \path[overlay, ->, line width = 1mm, shorten >=-3mm] (r1) edge (r2); |
|
186 |
|
187 \end{tikzpicture} |
151 \end{tikzpicture} |
188 \end{center} |
152 \end{center} |
189 |
153 } |
190 |
|
191 \end{frame}} |
|
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
193 *} |
|
194 |
|
195 text_raw {* |
|
196 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
197 \mode<presentation>{ |
|
198 \begin{frame}<1->[t] |
|
199 \frametitle{RegExp Matcher} |
|
200 \small |
|
201 |
|
202 {\bf input:} a \underline{list} of RegExps and a string \hspace{6mm}{\bf output:} true or false |
|
203 |
|
204 \only<2->{ |
|
205 \begin{center} |
|
206 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
207 \bl{match [] []} & \bl{$=$} & \bl{true}\\ |
|
208 \bl{match [] \_} & \bl{$=$} & \bl{false}\\ |
|
209 \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false}\\ |
|
210 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
211 \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s}\\ |
|
212 \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false}\\ |
|
213 \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\ |
|
214 & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\ |
|
215 \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\ |
|
216 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
217 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\ |
|
218 \end{tabular} |
|
219 \end{center}} |
|
220 |
|
221 \onslide<3->{we start the program with\\ |
|
222 \hspace{6mm}\bl{matches r s $=$ match [r] s}} |
|
223 |
|
224 \end{frame}} |
|
225 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
226 *} |
|
227 |
|
228 |
|
229 text_raw {* |
|
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
231 \mode<presentation>{ |
|
232 \begin{frame}<1>[c] |
|
233 \frametitle{Program in Scala} |
|
234 |
|
235 \bl{\footnotesize |
|
236 \begin{tabular}{l} |
|
237 sealed abstract class Rexp\\ |
|
238 sealed case class Null extends Rexp\\ |
|
239 sealed case class Empty extends Rexp\\ |
|
240 sealed case class Chr(c: Char) extends Rexp\\ |
|
241 sealed case class Alt(r1 : Rexp, r2 : Rexp) extends Rexp\\ |
|
242 sealed case class Seq(r1 : Rexp, r2 : Rexp) extends Rexp\\ |
|
243 sealed case class Star(r : Rexp) extends Rexp\medskip\\ |
|
244 def match1 (rs : List[Rexp], s : List[Char]) : Boolean = rs match \{\\ |
|
245 \hspace{3mm}case Nil @{text "\<Rightarrow>"} if (s == Nil) true else false\\ |
|
246 \hspace{3mm}case (Null()::rs) @{text "\<Rightarrow>"} false\\ |
|
247 \hspace{3mm}case (Empty()::rs) @{text "\<Rightarrow>"} match1 (rs, s)\\ |
|
248 \hspace{3mm}case (Chr(c)::rs) @{text "\<Rightarrow>"} s match \\ |
|
249 \hspace{6mm}\{ case Nil @{text "\<Rightarrow>"} false\\ |
|
250 \hspace{8mm}case (d::s) @{text "\<Rightarrow>"} if (c==d) match1 (rs,s) else false \}\\ |
|
251 \hspace{3mm}case (Alt (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::rs, s) || match1 (r2::rs, s)\\ |
|
252 \hspace{3mm}case (Seq (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::r2::rs, s) \\ |
|
253 \hspace{3mm}case (Star (r)::rs) @{text "\<Rightarrow>"} match1 (r::rs, s) || match1 (r::Star (r)::rs, s)\\ |
|
254 \} |
|
255 \end{tabular}} |
|
256 |
|
257 \end{frame}} |
|
258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
259 *} |
|
260 |
|
261 |
|
262 text_raw {* |
|
263 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
264 \mode<presentation>{ |
|
265 \begin{frame}<1->[c] |
|
266 \frametitle{Testing} |
|
267 |
|
268 \small |
|
269 Every good programmer should do thourough tests: |
|
270 |
|
271 |
|
272 \begin{center} |
|
273 \begin{tabular}{@ {\hspace{-20mm}}lcl} |
|
274 \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\ |
|
275 \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\ |
|
276 \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\ |
|
277 \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ |
|
278 \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\ |
|
279 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\ |
|
280 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\ |
|
281 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}} |
|
282 \end{tabular} |
|
283 \end{center} |
|
284 |
|
285 \onslide<3-> |
|
286 {looks OK \ldots let's ship it to customers\hspace{5mm} |
|
287 \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}} |
|
288 |
|
289 \end{frame}} |
|
290 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
291 *} |
|
292 |
|
293 text_raw {* |
|
294 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
295 \mode<presentation>{ |
|
296 \begin{frame}<1->[t] |
|
297 \frametitle{Testing} |
|
298 |
|
299 \begin{itemize} |
|
300 \item While testing is an important part in the process of programming development\pause |
|
301 |
|
302 \item we can only test a {\bf finite} amount of examples\bigskip\pause |
|
303 |
|
304 \begin{center} |
|
305 \colorbox{cream} |
|
306 {\gr{\begin{minipage}{10cm} |
|
307 ``Testing can only show the presence of errors, never their |
|
308 absence'' (Edsger W.~Dijkstra) |
|
309 \end{minipage}}} |
|
310 \end{center}\bigskip\pause |
|
311 |
|
312 \item In a theorem prover we can establish properties that apply to |
|
313 {\bf all} input and {\bf all} output.\pause |
|
314 |
|
315 \item For example we can establish that the matcher terminates |
|
316 on all input. |
|
317 \end{itemize} |
|
318 |
|
319 \end{frame}} |
|
320 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
321 *} |
|
322 |
|
323 text_raw {* |
|
324 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
325 \mode<presentation>{ |
|
326 \begin{frame}<1->[t] |
|
327 \frametitle{RegExp Matcher} |
|
328 |
|
329 \small |
|
330 We need to find a measure that gets smaller in each recursive call.\bigskip |
|
331 |
|
332 \onslide<1->{ |
|
333 \begin{center} |
|
334 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-9mm}}l@ {}} |
|
335 \bl{match [] []} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\ |
|
336 \bl{match [] \_} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\ |
|
337 \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\ |
|
338 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s} & \onslide<3->{\ok}\\ |
|
339 \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s} & \onslide<4->{\ok}\\ |
|
340 \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\ |
|
341 \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s} & \onslide<5->{\ok}\\ |
|
342 & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\ |
|
343 \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s} & \onslide<6->{\ok}\\ |
|
344 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s} & \onslide<7->{\notok}\\ |
|
345 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\ |
|
346 \end{tabular} |
|
347 \end{center}} |
|
348 |
|
349 |
|
350 \begin{textblock}{5}(4,4) |
|
351 \begin{tikzpicture} |
|
352 %%\draw[help lines, black] (-3,0) grid (6,3); |
|
353 |
|
354 \coordinate (m1) at (-2,0); |
|
355 \coordinate (m2) at ( 2,0); |
|
356 \path[overlay, ->, line width = 0.6mm, color = red] (m1) edge (m2); |
|
357 \draw (0,0) node[above=-1mm] {\footnotesize\rd{needs to get smaller}}; |
|
358 \end{tikzpicture} |
|
359 \end{textblock} |
|
360 |
|
361 |
|
362 \end{frame}} |
|
363 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
364 *} |
|
365 |
|
366 text_raw {* |
|
367 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
368 \mode<presentation>{ |
|
369 \begin{frame}<1->[c] |
|
370 \frametitle{Bug Hunting} |
|
371 |
|
372 \only<1>{Several hours later\ldots}\pause |
|
373 |
|
374 |
|
375 \begin{center} |
|
376 \begin{tabular}{@ {\hspace{-20mm}}lcl} |
|
377 \bl{matches (STAR (EMPTY)) s} & \bl{$\mapsto$} & loops\\ |
|
378 \onslide<4->{\bl{matches (STAR (EMPTY $|$ \ldots)) s} & \bl{$\mapsto$} & loops\\} |
|
379 \end{tabular} |
|
380 \end{center} |
|
381 |
|
382 \small |
|
383 \onslide<3->{ |
|
384 \begin{center} |
|
385 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
386 \ldots\\ |
|
387 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
388 \ldots\\ |
|
389 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
390 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\ |
|
391 \end{tabular} |
|
392 \end{center}} |
|
393 |
|
394 |
|
395 \end{frame}} |
|
396 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
397 *} |
|
398 |
|
399 text_raw {* |
|
400 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
401 \mode<presentation>{ |
|
402 \begin{frame}<1->[c] |
|
403 \frametitle{RegExp Matcher} |
|
404 \small |
|
405 |
|
406 \begin{center} |
|
407 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
408 \bl{match [] []} & \bl{$=$} & \bl{true}\\ |
|
409 \bl{match [] \_} & \bl{$=$} & \bl{false}\\ |
|
410 \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false}\\ |
|
411 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
412 \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s}\\ |
|
413 \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false}\\ |
|
414 \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\ |
|
415 & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\ |
|
416 \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\ |
|
417 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
418 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\ |
|
419 \end{tabular} |
|
420 \end{center} |
|
421 |
|
422 \only<1>{ |
|
423 \begin{textblock}{5}(4,4) |
|
424 \largenotok |
|
425 \end{textblock}} |
|
426 |
|
427 \end{frame}} |
|
428 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
429 *} |
|
430 |
|
431 |
|
432 |
|
433 text_raw {* |
|
434 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
435 \mode<presentation>{ |
|
436 \begin{frame}<1->[t] |
|
437 \frametitle{Second Attempt} |
|
438 |
|
439 Can a regular expression match the empty string? |
|
440 |
|
441 \small |
|
442 \begin{center} |
|
443 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} |
|
444 \bl{nullable (NULL)} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\ |
|
445 \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\ |
|
446 \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\ |
|
447 \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} |
|
448 & \onslide<2->{\ok}\\ |
|
449 \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} |
|
450 & \onslide<2->{\ok}\\ |
|
451 \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\ |
|
452 \end{tabular} |
|
453 \end{center} |
|
454 |
|
455 \end{frame}} |
|
456 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
457 *} |
|
458 |
|
459 |
|
460 text_raw {* |
|
461 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
462 \mode<presentation>{ |
|
463 \begin{frame}<1->[t] |
|
464 \frametitle{RegExp Matcher 2} |
|
465 |
|
466 If \bl{r} matches \bl{c::s}, which regular expression can match the string \bl{s}? |
|
467 |
|
468 \small |
|
469 \begin{center} |
|
470 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
|
471 \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\ |
|
472 \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\ |
|
473 \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \onslide<3->{\ok}\\ |
|
474 \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \onslide<3->{\ok}\\ |
|
475 \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \onslide<3->{\ok}\\ |
|
476 & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\ |
|
477 \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} & \onslide<3->{\ok}\medskip\\ |
|
478 \pause |
154 \pause |
479 |
155 |
480 \bl{derivative r []} & \bl{$=$} & \bl{r} & \onslide<3->{\ok}\\ |
156 \begin{tabular}{c@ {\hspace{2mm}}c} |
481 \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \onslide<3->{\ok}\\ |
157 \begin{tabular}{c} |
482 \end{tabular} |
158 \includegraphics[scale=0.09]{harper.jpg}\\[-2mm] |
483 \end{center} |
159 {\footnotesize Bob Harper}\\[-2.5mm] |
484 |
160 {\footnotesize (CMU)} |
485 we call the program with\\ |
161 \end{tabular} |
486 \bl{matches r s $=$ nullable (derivative r s)} |
162 \begin{tabular}{c} |
487 |
163 \includegraphics[scale=0.31]{pfenning.jpg}\\[-2mm] |
488 |
164 {\footnotesize Frank Pfenning}\\[-2.5mm] |
489 \end{frame}} |
165 {\footnotesize (CMU)} |
490 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
166 \end{tabular} & |
491 *} |
167 |
492 |
168 \begin{tabular}{p{6cm}} |
493 text_raw {* |
169 \raggedright\small |
494 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
170 \color{gray}{published a proof in ACM Transactions on Computational Logic (2005), |
495 \mode<presentation>{ |
171 $\sim$31pp} |
496 \begin{frame}<1->[c] |
172 \end{tabular}\\ |
497 \frametitle{But Now What?} |
173 |
498 |
174 \\[-4mm] |
499 \begin{center} |
175 |
500 {\usefont{T1}{ptm}{b}{N}\VERYHuge{\rd{?}}} |
176 \begin{tabular}{c} |
501 \end{center} |
|
502 |
|
503 \end{frame}} |
|
504 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
505 *} |
|
506 |
|
507 text_raw {* |
|
508 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
509 \mode<presentation>{ |
|
510 \begin{frame}<1->[c] |
|
511 \frametitle{Testing} |
|
512 |
|
513 \small |
|
514 |
|
515 \begin{center} |
|
516 \begin{tabular}{@ {\hspace{-20mm}}lcl} |
|
517 \bl{matches []$^*$ []} & \bl{$\mapsto$} & \bl{true}\\ |
|
518 \bl{matches ([]$|$a)$^*$ a} & \bl{$\mapsto$} & \bl{true}\medskip\\ |
|
519 |
|
520 \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\ |
|
521 \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\ |
|
522 \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\ |
|
523 \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ |
|
524 \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\ |
|
525 |
|
526 \bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}\\ |
|
527 \bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}\\ |
|
528 \bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false} |
|
529 \end{tabular} |
|
530 \end{center} |
|
531 |
|
532 |
|
533 \end{frame}} |
|
534 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
535 *} |
|
536 |
|
537 text_raw {* |
|
538 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
539 \mode<presentation>{ |
|
540 \begin{frame}<1->[t] |
|
541 \frametitle{Specification} |
|
542 |
|
543 We have to specify what it means for a regular expression to match |
|
544 a string. |
|
545 % |
|
546 \only<2>{ |
|
547 \mbox{}\\[8mm] |
|
548 \bl{(a$\cdot$b)$^*$}\\ |
|
549 \hspace{7mm}\bl{$\mapsto$\hspace{3mm}\{[], ab, abab, ababab, \ldots\}}\bigskip\\ |
|
550 \bl{x$\cdot$(0 $|$ 1 $|$ 2 \ldots 8 $|$ 9 )$^*$}\\ |
|
551 \hspace{7mm}\bl{$\mapsto$\hspace{3mm} |
|
552 \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}} |
|
553 % |
|
554 \only<3->{ |
|
555 \begin{center} |
|
556 \begin{tabular}{rcl} |
|
557 \bl{\LL (NULL)} & \bl{$\dn$} & \bl{\{\}}\\ |
|
558 \bl{\LL (EMPTY)} & \bl{$\dn$} & \bl{\{[]\}}\\ |
|
559 \bl{\LL (CHR c)} & \bl{$\dn$} & \bl{\{c\}}\\ |
|
560 \bl{\LL (ALT r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<4->{\bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}}\\ |
|
561 \bl{\LL (SEQ r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<6->{\bl{\LL (r$_1$) ; \LL (r$_2$)}}\\ |
|
562 \bl{\LL (STAR r)} & \bl{$\dn$} & \onslide<8->{\bl{(\LL (r))$^\star$}}\\ |
|
563 \end{tabular} |
|
564 \end{center}} |
|
565 |
|
566 \only<5-6>{ |
|
567 \begin{textblock}{6}(2.9,13.3) |
|
568 \colorbox{cream}{\bl{S$_1$ ; S$_2$ $\;\dn\;$ \{ s$_1$@s$_2$ $|$ s$_1$$\in$S$_1$ $\wedge$ |
|
569 s$_2$$\in$S$_2$ \}}} |
|
570 \end{textblock}} |
|
571 |
|
572 \only<7->{ |
|
573 \begin{textblock}{9}(4,13) |
|
574 \colorbox{cream}{\bl{$\infer{\mbox{[]} \in \mbox{S}^\star}{}$}}\hspace{3mm} |
|
575 \colorbox{cream}{\bl{$\infer{\mbox{s}_1\mbox{@}\mbox{s}_2 \in \mbox{S}^\star} |
|
576 {\mbox{s}_1 \in \mbox{S} & \mbox{s}_2 \in \mbox{S}^\star}$}} |
|
577 \end{textblock}} |
|
578 |
|
579 \end{frame}} |
|
580 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
581 *} |
|
582 |
|
583 text_raw {* |
|
584 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
585 \mode<presentation>{ |
|
586 \begin{frame}<1->[t] |
|
587 \frametitle{Is the Matcher Error-Free?} |
|
588 |
|
589 We expect that |
|
590 |
|
591 \begin{center} |
|
592 \begin{tabular}{lcl} |
|
593 \bl{matches r s = true} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% |
|
594 \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\ |
|
595 \bl{matches r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% |
|
596 \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\ |
|
597 \end{tabular} |
|
598 \end{center} |
|
599 \pause\pause\bigskip |
|
600 By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip |
|
601 |
|
602 \begin{tabular}{lrcl} |
|
603 Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\ |
|
604 & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\ |
|
605 \end{tabular} |
|
606 |
|
607 \only<4->{ |
|
608 \begin{textblock}{3}(0.9,4.5) |
|
609 \rd{\huge$\forall$\large{}r s.} |
|
610 \end{textblock}} |
|
611 \end{frame}} |
|
612 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
613 *} |
|
614 |
|
615 text_raw {* |
|
616 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
617 \mode<presentation>{ |
|
618 \begin{frame}<1->[t] |
|
619 |
|
620 \mbox{}\\[-2mm] |
|
621 |
|
622 \small |
|
623 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} |
|
624 \bl{nullable (NULL)} & \bl{$=$} & \bl{false} &\\ |
|
625 \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} &\\ |
|
626 \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} &\\ |
|
627 \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ |
|
628 \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\ |
|
629 \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\ |
|
630 \end{tabular}\medskip |
|
631 |
|
632 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
|
633 \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \\ |
|
634 \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \\ |
|
635 \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\ |
|
636 \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\ |
|
637 \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\ |
|
638 & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\ |
|
639 \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\ |
|
640 |
|
641 \bl{derivative r []} & \bl{$=$} & \bl{r} & \\ |
|
642 \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\ |
|
643 \end{tabular}\medskip |
|
644 |
|
645 \bl{matches r s $=$ nullable (derivative r s)} |
|
646 |
|
647 \only<2>{ |
|
648 \begin{textblock}{8}(1.5,4) |
|
649 \includegraphics[scale=0.3]{approved.png} |
|
650 \end{textblock}} |
|
651 |
|
652 |
|
653 \end{frame}} |
|
654 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
655 *} |
|
656 |
|
657 |
|
658 text_raw {* |
|
659 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
660 \mode<presentation>{ |
|
661 \begin{frame}<1->[c] |
|
662 \frametitle{Interlude: TCB} |
|
663 |
|
664 \begin{itemize} |
|
665 \item The \alert{\bf Trusted Code Base} (TCB) is the code that can make your |
|
666 program behave in unintended ways (i.e.~cause bugs).\medskip |
|
667 |
|
668 \item Typically the TCB includes: CPUs, operating systems, C-libraries, |
|
669 device drivers, (J)VMs\ldots\bigskip |
|
670 \pause |
|
671 |
|
672 \item It also includes the compiler. |
|
673 \end{itemize} |
|
674 |
|
675 \end{frame}} |
|
676 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
677 *} |
|
678 |
|
679 text_raw {* |
|
680 |
|
681 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
682 \mode<presentation>{ |
|
683 \begin{frame}<1-3> |
|
684 \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers |
|
685 \end{tabular}} |
|
686 |
|
687 %Why is it so paramount to have a small trusted code base (TCB)? |
|
688 \bigskip\bigskip |
|
689 |
|
690 \begin{columns} |
|
691 \begin{column}{2.7cm} |
|
692 \begin{minipage}{2.5cm}% |
|
693 \begin{tabular}{c@ {}} |
|
694 \includegraphics[scale=0.2]{ken-thompson.jpg}\\[-1.8mm] |
|
695 \footnotesize Ken Thompson\\[-1.8mm] |
|
696 \footnotesize Turing Award, 1983\\ |
|
697 \end{tabular} |
|
698 \end{minipage} |
|
699 \end{column} |
|
700 \begin{column}{9cm} |
|
701 \begin{tabular}{l@ {\hspace{1mm}}p{8cm}} |
|
702 \myitemi |
|
703 & Ken Thompson showed how to hide a Trojan Horse in a |
|
704 compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm] |
|
705 \myitemi |
|
706 & No amount of source level verification will protect |
|
707 you from such Thompson-hacks.\\[2mm] |
|
708 |
|
709 \myitemi |
|
710 & Therefore in safety-critical systems it is important to rely |
|
711 on only a very small TCB. |
|
712 \end{tabular} |
|
713 \end{column} |
|
714 \end{columns} |
|
715 |
|
716 \only<2>{ |
|
717 \begin{textblock}{6}(4,2) |
|
718 \begin{tikzpicture} |
|
719 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
720 {\normalsize |
|
721 \begin{minipage}{8cm} |
|
722 \begin{quote} |
|
723 \includegraphics[scale=0.05]{evil.png} |
|
724 \begin{enumerate} |
|
725 \item[1)] Assume you ship the compiler as binary and also with sources. |
|
726 \item[2)] Make the compiler aware when it compiles itself. |
|
727 \item[3)] Add the Trojan horse. |
|
728 \item[4)] Compile. |
|
729 \item[5)] Delete Trojan horse from the sources of the compiler. |
|
730 \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{} |
|
731 \end{enumerate} |
|
732 \end{quote} |
|
733 \end{minipage}}; |
|
734 \end{tikzpicture} |
|
735 \end{textblock}} |
|
736 |
|
737 \end{frame}} |
|
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
739 |
|
740 *} |
|
741 |
|
742 text_raw {* |
|
743 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
744 \mode<presentation>{ |
|
745 \begin{frame} |
|
746 \frametitle{\LARGE\begin{tabular}{c}An Example: Small TCB for\\[-2mm] |
|
747 A Critical Infrastructure\end{tabular}} |
|
748 \mbox{}\\[-14mm]\mbox{} |
|
749 |
|
750 \begin{columns} |
|
751 \begin{column}{0.2\textwidth} |
|
752 \begin{tabular}{@ {} c@ {}} |
|
753 \includegraphics[scale=0.3]{appel.jpg}\\[-2mm] |
177 \includegraphics[scale=0.3]{appel.jpg}\\[-2mm] |
754 {\footnotesize Andrew Appel}\\[-2.5mm] |
178 {\footnotesize Andrew Appel}\\[-2.5mm] |
755 {\footnotesize (Princeton)} |
179 {\footnotesize (Princeton)} |
756 \end{tabular} |
180 \end{tabular} & |
757 \end{column} |
181 |
758 |
182 \begin{tabular}{p{6cm}} |
759 \begin{column}{0.8\textwidth} |
183 \raggedright\small |
760 \begin{textblock}{10}(4.5,3.95) |
184 \color{gray}{relied on their proof in a safety critical system (proof carrying code)} |
761 \begin{block}{Proof-Carrying Code} |
185 \end{tabular} |
|
186 |
|
187 \end{tabular}\medskip |
|
188 |
|
189 |
|
190 |
|
191 |
|
192 |
|
193 \end{frame}} |
|
194 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
195 |
|
196 *} |
|
197 |
|
198 text_raw {* |
|
199 |
|
200 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
201 \mode<presentation>{ |
|
202 \begin{frame} |
|
203 \frametitle{Proof-Carrying Code} |
|
204 |
|
205 \begin{textblock}{10}(2.5,2.2) |
|
206 \begin{block}{Idea:} |
762 \begin{center} |
207 \begin{center} |
763 \begin{tikzpicture} |
208 \begin{tikzpicture} |
764 \draw[help lines,cream] (0,0.2) grid (8,4); |
209 \draw[help lines,cream] (0,0.2) grid (8,4); |
765 |
210 |
766 \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4); |
211 \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4); |
910 \end{frame}} |
326 \end{frame}} |
911 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
327 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
912 |
328 |
913 *} |
329 *} |
914 |
330 |
915 text_raw {* |
331 |
916 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
332 text_raw {* |
917 \mode<presentation>{ |
333 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
918 \begin{frame}<1>[c] |
334 \mode<presentation>{ |
|
335 \begin{frame}<1->[c] |
919 \frametitle{Theorem Provers} |
336 \frametitle{Theorem Provers} |
920 |
337 |
921 \begin{itemize} |
338 \begin{itemize} |
922 \item Theorem provers help with keeping large proofs consistent; |
339 \item Theorem provers help with keeping large proofs consistent; |
923 make them modifiable.\medskip |
340 make them modifiable.\medskip |
924 |
341 |
925 \item They can ensure that all cases are covered.\medskip |
342 \item They can ensure that all cases are covered.\medskip |
926 |
343 |
927 \item Sometimes, tedious reasoning can be automated. |
344 \item Some reasoning can be automated. |
928 \end{itemize} |
345 \end{itemize}\bigskip\pause |
929 |
346 |
|
347 \begin{minipage}{1.1\textwidth} |
|
348 Formal reasoning needs to be ``smooth''.\\ |
|
349 {\small (ideally as close as possible to reasoning with ``pen-and-paper'')} |
|
350 \end{minipage} |
|
351 |
|
352 \only<2->{ |
|
353 \begin{textblock}{3}(0.1,9.9) |
|
354 \begin{tikzpicture} |
|
355 \node at (0,0) [single arrow, shape border rotate=0, fill=red,text=red]{a}; |
|
356 \end{tikzpicture} |
|
357 \end{textblock}} |
|
358 |
|
359 |
|
360 \end{frame}} |
|
361 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
362 *} |
|
363 |
|
364 |
|
365 (*<*) |
|
366 atom_decl name |
|
367 |
|
368 nominal_datatype lam = |
|
369 Var "name" |
|
370 | App "lam" "lam" |
|
371 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
|
372 |
|
373 nominal_primrec |
|
374 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]") |
|
375 where |
|
376 "(Var x)[y::=s] = (if x=y then s else (Var x))" |
|
377 | "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])" |
|
378 | "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])" |
|
379 apply(finite_guess)+ |
|
380 apply(rule TrueI)+ |
|
381 apply(simp add: abs_fresh) |
|
382 apply(fresh_guess)+ |
|
383 done |
|
384 |
|
385 lemma subst_eqvt[eqvt]: |
|
386 fixes pi::"name prm" |
|
387 shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]" |
|
388 by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct) |
|
389 (auto simp add: perm_bij fresh_atm fresh_bij) |
|
390 |
|
391 lemma fresh_fact: |
|
392 fixes z::"name" |
|
393 shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]" |
|
394 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
|
395 (auto simp add: abs_fresh fresh_prod fresh_atm) |
|
396 |
|
397 lemma forget: |
|
398 assumes asm: "x\<sharp>L" |
|
399 shows "L[x::=P] = L" |
|
400 using asm |
|
401 by (nominal_induct L avoiding: x P rule: lam.strong_induct) |
|
402 (auto simp add: abs_fresh fresh_atm) |
|
403 (*>*) |
|
404 |
|
405 text_raw {* |
|
406 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
407 \mode<presentation>{ |
|
408 \begin{frame} |
|
409 |
|
410 \begin{textblock}{16}(1,1) |
|
411 \renewcommand{\isasymbullet}{$\cdot$} |
|
412 \tiny\color{black} |
|
413 *} |
|
414 lemma substitution_lemma_not_to_be_tried_at_home: |
|
415 assumes asm: "x\<noteq>y" "x\<sharp>L" |
|
416 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
|
417 using asm |
|
418 proof (induct M arbitrary: x y N L rule: lam.induct) |
|
419 case (Lam z M1) |
|
420 have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact |
|
421 have "x\<noteq>y" by fact |
|
422 have "x\<sharp>L" by fact |
|
423 obtain z'::"name" where fc: "z'\<sharp>(x,y,z,M1,N,L)" by (rule exists_fresh) (auto simp add: fs_name1) |
|
424 have eq: "Lam [z'].([(z',z)]\<bullet>M1) = Lam [z].M1" using fc |
|
425 by (auto simp add: lam.inject alpha fresh_prod fresh_atm) |
|
426 have fc': "z'\<sharp>N[y::=L]" using fc by (simp add: fresh_fact fresh_prod) |
|
427 have "([(z',z)]\<bullet>x) \<noteq> ([(z',z)]\<bullet>y)" using `x\<noteq>y` by (auto simp add: calc_atm) |
|
428 moreover |
|
429 have "([(z',z)]\<bullet>x)\<sharp>([(z',z)]\<bullet>L)" using `x\<sharp>L` by (simp add: fresh_bij) |
|
430 ultimately |
|
431 have "M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] |
|
432 = M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]]" |
|
433 using ih by simp |
|
434 then have "[(z',z)]\<bullet>(M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] |
|
435 = M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]])" |
|
436 by (simp add: perm_bool) |
|
437 then have ih': "([(z',z)]\<bullet>M1)[x::=N][y::=L] = ([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]]" |
|
438 by (simp add: eqvts perm_swap) |
|
439 show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") |
|
440 proof - |
|
441 have "?LHS = (Lam [z'].([(z',z)]\<bullet>M1))[x::=N][y::=L]" using eq by simp |
|
442 also have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[x::=N][y::=L])" using fc by (simp add: fresh_prod) |
|
443 also from ih have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]])" sorry |
|
444 also have "\<dots> = (Lam [z'].([(z',z)]\<bullet>M1))[y::=L][x::=N[y::=L]]" using fc fc' by (simp add: fresh_prod) |
|
445 also have "\<dots> = ?RHS" using eq by simp |
|
446 finally show "?LHS = ?RHS" . |
|
447 qed |
|
448 qed (auto simp add: forget) |
|
449 text_raw {* |
|
450 \end{textblock} |
|
451 \mbox{} |
|
452 |
|
453 \only<2->{ |
|
454 \begin{textblock}{11.5}(4,2.3) |
|
455 \begin{minipage}{9.3cm} |
|
456 \begin{block}{}\footnotesize |
|
457 *} |
|
458 lemma substitution_lemma\<iota>: |
|
459 assumes asm: "x \<noteq> y" "x \<sharp> L" |
|
460 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
|
461 using asm |
|
462 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) |
|
463 (auto simp add: forget fresh_fact) |
|
464 text_raw {* |
|
465 \end{block} |
|
466 \end{minipage} |
|
467 \end{textblock}} |
930 \end{frame}} |
468 \end{frame}} |
931 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
469 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
932 *} |
470 *} |
933 |
471 |
934 text_raw {* |
472 text_raw {* |
935 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
936 \mode<presentation>{ |
474 \mode<presentation>{ |
937 \begin{frame}<1>[c] |
475 \begin{frame}<1>[c] |
938 \frametitle{Theorem Provers} |
476 \frametitle{Getting Programs Correct} |
939 |
477 |
940 \begin{itemize} |
478 \begin{center} |
941 \item You also pay a (sometimes heavy) price: reasoning can be much, much harder.\medskip |
479 \begin{tikzpicture}[node distance=0.5mm] |
942 |
480 \node at (-1.0,-0.3) (proof) [double arrow, fill=gray,text=white, minimum height=2cm]{\bf Proof}; |
943 \item Depending on your domain, suitable reasoning infrastructure |
481 \node [left=of proof]{\Large\bf Specification}; |
944 might not yet be available. |
482 \node [right=of proof]{\Large\bf Code}; |
945 \end{itemize} |
483 \end{tikzpicture} |
946 |
484 \end{center} |
947 \end{frame}} |
485 |
948 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
486 |
949 *} |
487 |
950 |
488 \end{frame}} |
951 text_raw {* |
489 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
952 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
490 *} |
953 \mode<presentation>{ |
491 |
954 \begin{frame}<1>[c] |
492 text_raw {* |
955 \frametitle{Theorem Provers} |
493 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
956 |
494 \mode<presentation>{ |
957 Recently impressive work has been accomplished proving the correctness |
495 \begin{frame}<1->[t] |
958 |
496 \frametitle{Regular Expressions} |
959 \begin{itemize} |
497 |
960 \item of a compiler for C-light (compiled code has the same observable |
498 \begin{textblock}{6}(2,4) |
961 behaviour as the original source code),\medskip |
499 \begin{tabular}{@ {}rrl} |
962 |
500 \bl{r} & \bl{$::=$} & \bl{$\varnothing$}\\ |
963 \item a mirco-kernel operating system (absence of certain |
501 & \bl{$\mid$} & \bl{[]}\\ |
964 bugs\ldots no nil pointers, no buffer overflows). |
502 & \bl{$\mid$} & \bl{c}\\ |
965 \end{itemize} |
503 & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\ |
966 |
504 & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\ |
967 \end{frame}} |
505 & \bl{$\mid$} & \bl{r$^*$}\\ |
968 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
506 \end{tabular} |
969 *} |
507 \end{textblock} |
970 |
508 |
971 |
509 \begin{textblock}{6}(8,3.5) |
972 text_raw {* |
510 \includegraphics[scale=0.35]{Screen1.png} |
973 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
511 \end{textblock} |
974 \mode<presentation>{ |
512 |
975 \begin{frame}<1>[c] |
513 \begin{textblock}{6}(10.2,2.8) |
976 \frametitle{Trust in Theorem Provers} |
514 \footnotesize Isabelle: |
977 |
515 \end{textblock} |
978 \begin{center} |
516 |
979 Why should we trust theorem provers? |
517 \only<2>{ |
980 \end{center} |
518 \begin{textblock}{9}(3.6,11.8) |
981 |
519 \bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm] |
982 \end{frame}} |
520 |
983 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
521 \hspace{10mm}\begin{tikzpicture} |
984 *} |
522 \coordinate (m1) at (0.4,1); |
985 |
523 \draw (0,0.3) node (m2) {\small\color{gray}rexp}; |
986 text_raw {* |
524 \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1); |
987 |
525 |
988 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
526 \coordinate (s1) at (0.81,1); |
989 \mode<presentation>{ |
527 \draw (1.3,0.3) node (s2) {\small\color{gray} string}; |
990 \begin{frame} |
528 \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1); |
991 \frametitle{Theorem Provers} |
529 \end{tikzpicture} |
992 |
|
993 \begin{itemize} |
|
994 \item Theorem provers are a \textcolor{red}{special kind} of software. |
|
995 |
|
996 \item We do \textcolor{red}{\bf not} need to trust them; we only need to trust: |
|
997 \end{itemize} |
|
998 |
|
999 \begin{quote} |
|
1000 \begin{itemize} |
|
1001 \item The logic they are based on \textcolor{gray}{(e.g.~HOL)}, and\smallskip |
|
1002 \item a proof checker that checks the proofs |
|
1003 \textcolor{gray}{(this can be a very small program)}.\smallskip\pause |
|
1004 \item To a little extend, we also need to trust our definitions |
|
1005 \textcolor{gray}{(this can be mitigated)}. |
|
1006 \end{itemize} |
|
1007 \end{quote} |
|
1008 |
|
1009 \end{frame}} |
|
1010 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1011 |
|
1012 *} |
|
1013 |
|
1014 text_raw {* |
|
1015 |
|
1016 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1017 \mode<presentation>{ |
|
1018 \begin{frame} |
|
1019 \frametitle{Isabelle} |
|
1020 |
|
1021 \begin{itemize} |
|
1022 \item I am using the Isabelle theorem prover (development since 1990).\bigskip\bigskip\bigskip |
|
1023 |
|
1024 \item It follows the LCF-approach: |
|
1025 |
|
1026 \begin{itemize} |
|
1027 \item Have a special abstract type \alert{\bf thm}. |
|
1028 \item Make the constructors of this abstract type the inference rules |
|
1029 of your logic. |
|
1030 \item Implement the theorem prover in a strongly-typed language (e.g.~ML). |
|
1031 \end{itemize} |
|
1032 |
|
1033 $\Rightarrow$ everything of type {\bf thm} has been proved (even if we do not |
|
1034 have to explicitly generate proofs). |
|
1035 \end{itemize} |
|
1036 |
|
1037 \only<1>{ |
|
1038 \begin{textblock}{5}(11,2.3) |
|
1039 \begin{center} |
|
1040 \includegraphics[scale=0.18]{robin-milner.jpg}\\[-0.8mm] |
|
1041 \footnotesize Robin Milner\\[-0.8mm] |
|
1042 \footnotesize Turing Award, 1991\\ |
|
1043 \end{center} |
|
1044 \end{textblock}} |
530 \end{textblock}} |
1045 |
531 |
1046 |
532 |
|
533 |
|
534 \end{frame}} |
|
535 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
536 *} |
|
537 |
|
538 text_raw {* |
|
539 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
540 \mode<presentation>{ |
|
541 \begin{frame}<1->[t] |
|
542 \frametitle{Specification} |
|
543 |
|
544 \small |
|
545 \begin{textblock}{6}(0,3.5) |
|
546 \begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} |
|
547 \multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\ |
|
548 &\bl{\LL ($\varnothing$)} & \bl{$\dn$} & \bl{$\varnothing$}\\ |
|
549 &\bl{\LL ([])} & \bl{$\dn$} & \bl{\{[]\}}\\ |
|
550 &\bl{\LL (c)} & \bl{$\dn$} & \bl{\{c\}}\\ |
|
551 &\bl{\LL (r$_1$ + r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\ |
|
552 \rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\ |
|
553 \rd{$\Rightarrow$} &\bl{\LL (r$^*$)} & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\ |
|
554 \end{tabular} |
|
555 \end{textblock} |
|
556 |
|
557 \begin{textblock}{9}(7.3,3) |
|
558 {\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip} |
|
559 \includegraphics[scale=0.325]{Screen3.png} |
|
560 \end{textblock} |
|
561 |
|
562 \end{frame}} |
|
563 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
564 *} |
|
565 |
|
566 |
|
567 text_raw {* |
|
568 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
569 \mode<presentation>{ |
|
570 \begin{frame}<1->[t] |
|
571 \frametitle{Version 1} |
|
572 \small |
|
573 \mbox{}\\[-8mm]\mbox{} |
|
574 |
|
575 \begin{center}\def\arraystretch{1.05} |
|
576 \begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}} |
|
577 \bl{match [] []} & \bl{$=$} & \bl{true}\\ |
|
578 \bl{match [] (c::s)} & \bl{$=$} & \bl{false}\\ |
|
579 \bl{match ($\varnothing$::rs) s} & \bl{$=$} & \bl{false}\\ |
|
580 \bl{match ([]::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
581 \bl{match (c::rs) []} & \bl{$=$} & \bl{false}\\ |
|
582 \bl{match (c::rs) (d::s)} & \bl{$=$} & \bl{if c = d then match rs s else false}\\ |
|
583 \bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\ |
|
584 \bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\ |
|
585 \bl{match (r$^*$::rs) s} & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\ |
|
586 \end{tabular} |
|
587 \end{center} |
|
588 |
|
589 \begin{textblock}{9}(0.2,1.6) |
|
590 \hspace{10mm}\begin{tikzpicture} |
|
591 \coordinate (m1) at (0.44,-0.5); |
|
592 \draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps}; |
|
593 \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1); |
|
594 |
|
595 \coordinate (s1) at (0.86,-0.5); |
|
596 \draw (1.5,0.3) node (s2) {\small\color{gray} string}; |
|
597 \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1); |
|
598 \end{tikzpicture} |
|
599 \end{textblock} |
|
600 |
|
601 \begin{textblock}{9}(2.8,11.8) |
|
602 \bl{matches$_1$ r s $\;=\;$ match [r] s} |
|
603 \end{textblock} |
|
604 |
|
605 \end{frame}} |
|
606 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
607 *} |
|
608 |
|
609 text_raw {* |
|
610 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
611 \mode<presentation>{ |
|
612 \begin{frame}<1->[c] |
|
613 \frametitle{Testing} |
|
614 |
|
615 \small |
|
616 Every good programmer should do thourough tests: |
|
617 |
|
618 \begin{center} |
|
619 \begin{tabular}{@ {\hspace{-20mm}}lcl} |
|
620 \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\ |
|
621 \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\ |
|
622 \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\ |
|
623 \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ |
|
624 \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\ |
|
625 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\ |
|
626 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\ |
|
627 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}} |
|
628 \end{tabular} |
|
629 \end{center} |
|
630 |
|
631 \onslide<3-> |
|
632 {looks OK \ldots let's ship it to customers\hspace{5mm} |
|
633 \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}} |
|
634 |
|
635 \end{frame}} |
|
636 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
637 *} |
|
638 |
|
639 text_raw {* |
|
640 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
641 \mode<presentation>{ |
|
642 \begin{frame}<1->[c] |
|
643 \frametitle{Version 1} |
|
644 |
|
645 \only<1->{Several hours later\ldots}\pause |
|
646 |
|
647 |
|
648 \begin{center} |
|
649 \begin{tabular}{@ {\hspace{0mm}}lcl} |
|
650 \bl{matches$_1$ []$^*$ s} & \bl{$\mapsto$} & loops\\ |
|
651 \onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s} & \bl{$\mapsto$} & loops\\} |
|
652 \end{tabular} |
|
653 \end{center} |
|
654 |
|
655 \small |
|
656 \onslide<3->{ |
|
657 \begin{center} |
|
658 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
659 \ldots\\ |
|
660 \bl{match ([]::rs) s} & \bl{$=$} & \bl{match rs s}\\ |
|
661 \ldots\\ |
|
662 \bl{match (r$^*$::rs) s} & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\ |
|
663 \end{tabular} |
|
664 \end{center}} |
|
665 |
|
666 |
|
667 \end{frame}} |
|
668 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
669 *} |
|
670 |
|
671 |
|
672 text_raw {* |
|
673 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
674 \mode<presentation>{ |
|
675 \begin{frame}<1->[t] |
|
676 \frametitle{Testing} |
|
677 |
|
678 \begin{itemize} |
|
679 \item While testing is an important part in the process of programming development\pause |
|
680 |
|
681 \item We can only test a {\bf finite} amount of examples.\bigskip\pause |
|
682 |
|
683 \begin{center} |
|
684 \colorbox{cream} |
|
685 {\gr{\begin{minipage}{10cm} |
|
686 ``Testing can only show the presence of errors, never their |
|
687 absence'' (Edsger W.~Dijkstra) |
|
688 \end{minipage}}} |
|
689 \end{center}\bigskip\pause |
|
690 |
|
691 \item In a theorem prover we can establish properties that apply to |
|
692 {\bf all} input and {\bf all} output.\pause |
|
693 |
|
694 \end{itemize} |
|
695 |
|
696 \end{frame}} |
|
697 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
698 *} |
|
699 |
|
700 |
|
701 text_raw {* |
|
702 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
703 \mode<presentation>{ |
|
704 \begin{frame}<1->[t] |
|
705 \frametitle{Version 2} |
|
706 \mbox{}\\[-14mm]\mbox{} |
|
707 |
|
708 \small |
|
709 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} |
|
710 \bl{nullable ($\varnothing$)} & \bl{$=$} & \bl{false} &\\ |
|
711 \bl{nullable ([])} & \bl{$=$} & \bl{true} &\\ |
|
712 \bl{nullable (c)} & \bl{$=$} & \bl{false} &\\ |
|
713 \bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{nullable r$_1$ $\vee$ nullable r$_2$} & \\ |
|
714 \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{nullable r$_1$ $\wedge$ nullable r$_2$} & \\ |
|
715 \bl{nullable (r$^*$)} & \bl{$=$} & \bl{true} & \\ |
|
716 \end{tabular}\medskip |
|
717 |
|
718 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
|
719 \bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\ |
|
720 \bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\ |
|
721 \bl{der c (d)} & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\ |
|
722 \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\ |
|
723 \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\ |
|
724 & & \bl{\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ |
|
725 \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\ |
|
726 |
|
727 \bl{derivative r []} & \bl{$=$} & \bl{r} & \\ |
|
728 \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\ |
|
729 \end{tabular}\medskip |
|
730 |
|
731 \bl{matches$_2$ r s $=$ nullable (derivative r s)} |
|
732 |
|
733 \begin{textblock}{6}(9.5,0.9) |
|
734 \begin{flushright} |
|
735 \color{gray}``if r matches []'' |
|
736 \end{flushright} |
|
737 \end{textblock} |
|
738 |
|
739 \begin{textblock}{6}(9.5,6.18) |
|
740 \begin{flushright} |
|
741 \color{gray}``derivative for a char'' |
|
742 \end{flushright} |
|
743 \end{textblock} |
|
744 |
|
745 \begin{textblock}{6}(9.5,12.1) |
|
746 \begin{flushright} |
|
747 \color{gray}``deriv.~for a string'' |
|
748 \end{flushright} |
|
749 \end{textblock} |
|
750 |
|
751 \begin{textblock}{6}(9.5,13.98) |
|
752 \begin{flushright} |
|
753 \color{gray}``main'' |
|
754 \end{flushright} |
|
755 \end{textblock} |
|
756 |
|
757 \end{frame}} |
|
758 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
759 *} |
|
760 |
|
761 text_raw {* |
|
762 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
763 \mode<presentation>{ |
|
764 \begin{frame}<1->[t] |
|
765 \frametitle{Is the Matcher Error-Free?} |
|
766 |
|
767 We expect that |
|
768 |
|
769 \begin{center} |
|
770 \begin{tabular}{lcl} |
|
771 \bl{matches$_2$ r s = true} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% |
|
772 \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\ |
|
773 \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% |
|
774 \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\ |
|
775 \end{tabular} |
|
776 \end{center} |
|
777 \pause\pause\bigskip |
|
778 By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip |
|
779 |
|
780 \begin{tabular}{lrcl} |
|
781 Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\ |
|
782 & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\ |
|
783 \end{tabular} |
|
784 |
|
785 \only<4->{ |
|
786 \begin{textblock}{3}(0.9,4.5) |
|
787 \rd{\huge$\forall$\large{}r s.} |
|
788 \end{textblock}} |
1047 \end{frame}} |
789 \end{frame}} |
1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
790 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1049 *} |
791 *} |
1050 |
792 |
1051 text_raw {* |
793 text_raw {* |
1064 |
806 |
1065 |
807 |
1066 text_raw {* |
808 text_raw {* |
1067 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
809 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1068 \mode<presentation>{ |
810 \mode<presentation>{ |
1069 \begin{frame}<1->[c] |
811 \begin{frame}<1->[t] |
1070 \frametitle{Future Research} |
812 |
1071 |
813 \mbox{}\\[-2mm] |
1072 \begin{itemize} |
814 |
1073 \item Make theorem provers more like a programming environment.\medskip\pause |
|
1074 |
|
1075 \item Use all the computational power we get from the hardware to |
|
1076 automate reasoning (GPUs).\medskip\pause |
|
1077 |
|
1078 \item Provide a comprehensive reasoning infrastructure for many domains and |
|
1079 design automated decision procedures. |
|
1080 \end{itemize}\pause |
|
1081 |
|
1082 |
|
1083 \begin{center} |
|
1084 \colorbox{cream}{ |
|
1085 \begin{minipage}{10cm} |
|
1086 \color{gray} |
|
1087 \small |
815 \small |
1088 ``Formal methods will never have a significant impact until |
816 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} |
1089 they can be used by people that don't understand them.''\smallskip\\ |
817 \bl{nullable (NULL)} & \bl{$=$} & \bl{false} &\\ |
1090 \mbox{}\footnotesize\hfill attributed to Tom Melham |
818 \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} &\\ |
1091 \end{minipage}} |
819 \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} &\\ |
1092 \end{center} |
820 \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ |
1093 |
821 \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\ |
1094 \end{frame}} |
822 \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\ |
1095 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
823 \end{tabular}\medskip |
1096 *} |
824 |
1097 |
825 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
1098 text_raw {* |
826 \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \\ |
1099 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
827 \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \\ |
1100 \mode<presentation>{ |
828 \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\ |
1101 \begin{frame}<1->[c] |
829 \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\ |
1102 \frametitle{Conclusion} |
830 \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\ |
1103 |
831 & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\ |
1104 \begin{itemize} |
832 \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\ |
1105 \item The plan is to make this kind of programming the ``future''.\medskip\pause |
833 |
1106 |
834 \bl{derivative r []} & \bl{$=$} & \bl{r} & \\ |
1107 \item Though the technology is already there\\ (compiler + micro-kernel os).\medskip\pause |
835 \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\ |
1108 |
836 \end{tabular}\medskip |
1109 \item Logic and reasoning (especially induction) are important skills for |
837 |
1110 Computer Scientists. |
838 \bl{matches r s $=$ nullable (derivative r s)} |
1111 \end{itemize} |
839 |
1112 |
840 \only<2>{ |
1113 \end{frame}} |
841 \begin{textblock}{8}(1.5,4) |
1114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
842 \includegraphics[scale=0.3]{approved.png} |
1115 *} |
843 \end{textblock}} |
1116 |
844 |
1117 |
845 \end{frame}} |
1118 text_raw {* |
846 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
847 *} |
1120 \mode<presentation>{ |
848 |
1121 \begin{frame}<1>[c] |
849 |
|
850 text_raw {* |
|
851 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
852 \mode<presentation>{ |
|
853 \begin{frame}[c] |
|
854 \frametitle{No Automata?} |
|
855 |
|
856 You might be wondering why I did not use any automata: |
|
857 |
|
858 \begin{itemize} |
|
859 \item A \alert{regular language} is one where there is a DFA that |
|
860 recognises it.\bigskip\pause |
|
861 \end{itemize} |
|
862 |
|
863 |
|
864 I can think of two reasons why this is a good definition:\medskip |
|
865 \begin{itemize} |
|
866 \item pumping lemma |
|
867 \item closure properties of regular languages (closed under complement) |
|
868 \end{itemize} |
|
869 |
|
870 \end{frame}} |
|
871 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
872 |
|
873 *} |
|
874 |
|
875 text_raw {* |
|
876 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
877 \mode<presentation>{ |
|
878 \begin{frame}[t] |
|
879 \frametitle{Really Bad News!} |
|
880 |
|
881 DFAs are bad news for formalisations in theorem provers. They might |
|
882 be represented as: |
|
883 |
|
884 \begin{itemize} |
|
885 \item graphs |
|
886 \item matrices |
|
887 \item partial functions |
|
888 \end{itemize} |
|
889 |
|
890 All constructions are messy to reason about.\bigskip\bigskip |
|
891 \pause |
|
892 |
|
893 \small |
|
894 \only<2>{ |
|
895 Constable et al needed (on and off) 18 months for a 3-person team |
|
896 to formalise automata theory in Nuprl including Myhill-Nerode. There is |
|
897 only very little other formalised work on regular languages I know of |
|
898 in Coq, Isabelle and HOL.} |
|
899 \only<3>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two |
|
900 automata with no inaccessible states \ldots'' |
|
901 } |
|
902 |
|
903 \end{frame}} |
|
904 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
905 |
|
906 *} |
|
907 |
|
908 text_raw {* |
|
909 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
910 \mode<presentation>{ |
|
911 \begin{frame}[c] |
|
912 \frametitle{\LARGE The Myhill-Nerode Theorem} |
|
913 |
|
914 \begin{itemize} |
|
915 \item provides necessary and suf\!ficient conditions for a language |
|
916 being regular (pumping lemma only necessary)\medskip |
|
917 |
|
918 \item will help with closure properties of regular languages\bigskip\pause |
|
919 |
|
920 \item key is the equivalence relation:\smallskip |
|
921 \begin{center} |
|
922 \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L} |
|
923 \end{center} |
|
924 \end{itemize} |
|
925 |
|
926 \end{frame}} |
|
927 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
928 |
|
929 *} |
|
930 |
|
931 text_raw {* |
|
932 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
933 \mode<presentation>{ |
|
934 \begin{frame}[c] |
|
935 \frametitle{\LARGE The Myhill-Nerode Theorem} |
|
936 |
|
937 \mbox{}\\[5cm] |
|
938 |
|
939 \begin{itemize} |
|
940 \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}} |
|
941 \end{itemize} |
|
942 |
|
943 \end{frame}} |
|
944 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
945 |
|
946 *} |
|
947 |
|
948 text_raw {* |
|
949 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
950 \mode<presentation>{ |
|
951 \begin{frame}[c] |
|
952 \frametitle{\LARGE Equivalence Classes} |
|
953 |
|
954 \begin{itemize} |
|
955 \item \smath{L = []} |
|
956 \begin{center} |
|
957 \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}} |
|
958 \end{center}\bigskip\bigskip |
|
959 |
|
960 \item \smath{L = [c]} |
|
961 \begin{center} |
|
962 \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}} |
|
963 \end{center}\bigskip\bigskip |
|
964 |
|
965 \item \smath{L = \varnothing} |
|
966 \begin{center} |
|
967 \smath{\Big\{U\!N\!IV\Big\}} |
|
968 \end{center} |
|
969 |
|
970 \end{itemize} |
|
971 |
|
972 \end{frame}} |
|
973 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
974 |
|
975 *} |
|
976 |
|
977 text_raw {* |
|
978 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
979 \mode<presentation>{ |
|
980 \begin{frame}[c] |
|
981 \frametitle{\LARGE Regular Languages} |
|
982 |
|
983 \begin{itemize} |
|
984 \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} |
|
985 such that \smath{\mathbb{L}(M) = L}\\[1.5cm] |
|
986 |
|
987 \item Myhill-Nerode: |
|
988 |
|
989 \begin{center} |
|
990 \begin{tabular}{l} |
|
991 finite $\Rightarrow$ regular\\ |
|
992 \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm] |
|
993 regular $\Rightarrow$ finite\\ |
|
994 \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} |
|
995 \end{tabular} |
|
996 \end{center} |
|
997 |
|
998 \end{itemize} |
|
999 |
|
1000 \end{frame}} |
|
1001 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1002 |
|
1003 *} |
|
1004 |
|
1005 text_raw {* |
|
1006 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1007 \mode<presentation>{ |
|
1008 \begin{frame}[c] |
|
1009 \frametitle{\LARGE Final States} |
|
1010 |
|
1011 \mbox{}\\[3cm] |
|
1012 |
|
1013 \begin{itemize} |
|
1014 \item \smath{\text{final}_L\,X \dn}\\ |
|
1015 \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L} |
|
1016 \smallskip |
|
1017 \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}} |
|
1018 |
|
1019 \end{itemize} |
|
1020 |
|
1021 \end{frame}} |
|
1022 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1023 *} |
|
1024 |
|
1025 text_raw {* |
|
1026 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1027 \mode<presentation>{ |
|
1028 \begin{frame}[c] |
|
1029 \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes} |
|
1030 |
|
1031 \smath{L = \{[c]\}} |
|
1032 |
|
1033 \begin{tabular}{@ {\hspace{-7mm}}cc} |
|
1034 \begin{tabular}{c} |
|
1035 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] |
|
1036 \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] |
|
1037 |
|
1038 %\draw[help lines] (0,0) grid (3,2); |
|
1039 |
|
1040 \node[state,initial] (q_0) {$R_1$}; |
|
1041 \node[state,accepting] (q_1) [above right of=q_0] {$R_2$}; |
|
1042 \node[state] (q_2) [below right of=q_0] {$R_3$}; |
|
1043 |
|
1044 \path[->] (q_0) edge node {c} (q_1) |
|
1045 edge node [swap] {$\Sigma-{c}$} (q_2) |
|
1046 (q_2) edge [loop below] node {$\Sigma$} () |
|
1047 (q_1) edge node {$\Sigma$} (q_2); |
|
1048 \end{tikzpicture} |
|
1049 \end{tabular} |
|
1050 & |
|
1051 \begin{tabular}[t]{ll} |
|
1052 \\[-20mm] |
|
1053 \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm] |
|
1054 |
|
1055 \smath{R_1}: & \smath{\{[]\}}\\ |
|
1056 \smath{R_2}: & \smath{\{[c]\}}\\ |
|
1057 \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm] |
|
1058 \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}} |
|
1059 \end{tabular} |
|
1060 |
|
1061 \end{tabular} |
|
1062 |
|
1063 \end{frame}} |
|
1064 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1065 *} |
|
1066 |
|
1067 |
|
1068 text_raw {* |
|
1069 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1070 \mode<presentation>{ |
|
1071 \begin{frame}[c] |
|
1072 \frametitle{\LARGE Systems of Equations} |
|
1073 |
|
1074 Inspired by a method of Brzozowski\;'64, we can build an equational system |
|
1075 characterising the equivalence classes: |
|
1076 |
|
1077 \begin{center} |
|
1078 \begin{tabular}{@ {\hspace{-20mm}}c} |
|
1079 \\[-13mm] |
|
1080 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] |
|
1081 \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] |
|
1082 |
|
1083 %\draw[help lines] (0,0) grid (3,2); |
|
1084 |
|
1085 \node[state,initial] (p_0) {$R_1$}; |
|
1086 \node[state,accepting] (p_1) [right of=q_0] {$R_2$}; |
|
1087 |
|
1088 \path[->] (p_0) edge [bend left] node {a} (p_1) |
|
1089 edge [loop above] node {b} () |
|
1090 (p_1) edge [loop above] node {a} () |
|
1091 edge [bend left] node {b} (p_0); |
|
1092 \end{tikzpicture}\\ |
|
1093 \\[-13mm] |
|
1094 \end{tabular} |
|
1095 \end{center} |
|
1096 |
|
1097 \begin{center} |
|
1098 \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
1099 & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\ |
|
1100 & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\ |
|
1101 \onslide<3->{we can prove} |
|
1102 & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} |
|
1103 & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\ |
|
1104 & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}} |
|
1105 & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\ |
|
1106 \end{tabular} |
|
1107 \end{center} |
|
1108 |
|
1109 \end{frame}} |
|
1110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1111 *} |
|
1112 |
|
1113 |
|
1114 text_raw {* |
|
1115 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1116 \mode<presentation>{ |
|
1117 \begin{frame}<1>[t] |
|
1118 \small |
|
1119 |
|
1120 \begin{center} |
|
1121 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
1122 \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} |
|
1123 & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
1124 \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}} |
|
1125 & \onslide<1->{\smath{R_1; a + R_2; a}}\\ |
|
1126 |
|
1127 & & & \onslide<2->{by Arden}\\ |
|
1128 |
|
1129 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
|
1130 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
1131 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
|
1132 & \only<2>{\smath{R_1; a + R_2; a}}% |
|
1133 \only<3->{\smath{R_1; a\cdot a^\star}}\\ |
|
1134 |
|
1135 & & & \onslide<4->{by Arden}\\ |
|
1136 |
|
1137 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
|
1138 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |
|
1139 \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}} |
|
1140 & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\ |
|
1141 |
|
1142 & & & \onslide<5->{by substitution}\\ |
|
1143 |
|
1144 \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} |
|
1145 & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ |
|
1146 \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}} |
|
1147 & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\ |
|
1148 |
|
1149 & & & \onslide<6->{by Arden}\\ |
|
1150 |
|
1151 \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} |
|
1152 & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
1153 \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}} |
|
1154 & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\ |
|
1155 |
|
1156 & & & \onslide<7->{by substitution}\\ |
|
1157 |
|
1158 \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} |
|
1159 & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
1160 \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}} |
|
1161 & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star |
|
1162 \cdot a\cdot a^\star}}\\ |
|
1163 \end{tabular} |
|
1164 \end{center} |
|
1165 |
|
1166 \end{frame}} |
|
1167 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1168 *} |
|
1169 |
|
1170 text_raw {* |
|
1171 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1172 \mode<presentation>{ |
|
1173 \begin{frame}[c] |
|
1174 \frametitle{\LARGE A Variant of Arden's Lemma} |
|
1175 |
|
1176 {\bf Arden's Lemma:}\smallskip |
|
1177 |
|
1178 If \smath{[] \not\in A} then |
|
1179 \begin{center} |
|
1180 \smath{X = X; A + \text{something}} |
|
1181 \end{center} |
|
1182 has the (unique) solution |
|
1183 \begin{center} |
|
1184 \smath{X = \text{something} ; A^\star} |
|
1185 \end{center} |
|
1186 |
|
1187 |
|
1188 \end{frame}} |
|
1189 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1190 *} |
|
1191 |
|
1192 |
|
1193 text_raw {* |
|
1194 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1195 \mode<presentation>{ |
|
1196 \begin{frame}<1->[t] |
|
1197 \small |
|
1198 |
|
1199 \begin{center} |
|
1200 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
1201 \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} |
|
1202 & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
1203 \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}} |
|
1204 & \onslide<1->{\smath{R_1; a + R_2; a}}\\ |
|
1205 |
|
1206 & & & \onslide<2->{by Arden}\\ |
|
1207 |
|
1208 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
|
1209 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
1210 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
|
1211 & \only<2>{\smath{R_1; a + R_2; a}}% |
|
1212 \only<3->{\smath{R_1; a\cdot a^\star}}\\ |
|
1213 |
|
1214 & & & \onslide<4->{by Arden}\\ |
|
1215 |
|
1216 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
|
1217 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |
|
1218 \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}} |
|
1219 & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\ |
|
1220 |
|
1221 & & & \onslide<5->{by substitution}\\ |
|
1222 |
|
1223 \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} |
|
1224 & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ |
|
1225 \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}} |
|
1226 & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\ |
|
1227 |
|
1228 & & & \onslide<6->{by Arden}\\ |
|
1229 |
|
1230 \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} |
|
1231 & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
1232 \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}} |
|
1233 & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\ |
|
1234 |
|
1235 & & & \onslide<7->{by substitution}\\ |
|
1236 |
|
1237 \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} |
|
1238 & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
1239 \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}} |
|
1240 & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star |
|
1241 \cdot a\cdot a^\star}}\\ |
|
1242 \end{tabular} |
|
1243 \end{center} |
|
1244 |
|
1245 \only<8->{ |
|
1246 \begin{textblock}{6}(2.5,4) |
|
1247 \begin{block}{} |
|
1248 \begin{minipage}{8cm}\raggedright |
|
1249 |
|
1250 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm] |
|
1251 \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] |
|
1252 |
|
1253 %\draw[help lines] (0,0) grid (3,2); |
|
1254 |
|
1255 \node[state,initial] (p_0) {$R_1$}; |
|
1256 \node[state,accepting] (p_1) [right of=q_0] {$R_2$}; |
|
1257 |
|
1258 \path[->] (p_0) edge [bend left] node {a} (p_1) |
|
1259 edge [loop above] node {b} () |
|
1260 (p_1) edge [loop above] node {a} () |
|
1261 edge [bend left] node {b} (p_0); |
|
1262 \end{tikzpicture} |
|
1263 |
|
1264 \end{minipage} |
|
1265 \end{block} |
|
1266 \end{textblock}} |
|
1267 |
|
1268 \end{frame}} |
|
1269 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1270 *} |
|
1271 |
|
1272 |
|
1273 text_raw {* |
|
1274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1275 \mode<presentation>{ |
|
1276 \begin{frame}[c] |
|
1277 \frametitle{\LARGE The Equ's Solving Algorithm} |
|
1278 |
|
1279 \begin{itemize} |
|
1280 \item The algorithm must terminate: Arden makes one equation smaller; |
|
1281 substitution deletes one variable from the right-hand sides.\bigskip |
|
1282 |
|
1283 \item We need to maintain the invariant that Arden is applicable |
|
1284 (if \smath{[] \not\in A} then \ldots):\medskip |
|
1285 |
|
1286 \begin{center}\small |
|
1287 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
1288 \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\ |
|
1289 \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\ |
|
1290 |
|
1291 & & & by Arden\\ |
|
1292 |
|
1293 \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\ |
|
1294 \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\ |
|
1295 \end{tabular} |
|
1296 \end{center} |
|
1297 |
|
1298 \end{itemize} |
|
1299 |
|
1300 |
|
1301 \end{frame}} |
|
1302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1303 *} |
|
1304 |
|
1305 |
|
1306 text_raw {* |
|
1307 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1308 \mode<presentation>{ |
|
1309 \begin{frame}[c] |
|
1310 \frametitle{\LARGE Other Direction} |
|
1311 |
|
1312 One has to prove |
|
1313 |
|
1314 \begin{center} |
|
1315 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} |
|
1316 \end{center} |
|
1317 |
|
1318 by induction on \smath{r}. Not trivial, but after a bit |
|
1319 of thinking, one can prove that if |
|
1320 |
|
1321 \begin{center} |
|
1322 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm} |
|
1323 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})} |
|
1324 \end{center} |
|
1325 |
|
1326 then |
|
1327 |
|
1328 \begin{center} |
|
1329 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})} |
|
1330 \end{center} |
|
1331 |
|
1332 |
|
1333 |
|
1334 \end{frame}} |
|
1335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1336 *} |
|
1337 |
|
1338 |
|
1339 text_raw {* |
|
1340 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1341 \mode<presentation>{ |
|
1342 \begin{frame}[c] |
|
1343 \frametitle{\LARGE What Have We Achieved?} |
|
1344 |
|
1345 \begin{itemize} |
|
1346 \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}} |
|
1347 \bigskip\pause |
|
1348 \item regular languages are closed under complementation; this is easy |
|
1349 \begin{center} |
|
1350 \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}} |
|
1351 \end{center} |
|
1352 \end{itemize} |
|
1353 |
|
1354 |
|
1355 \end{frame}} |
|
1356 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1357 *} |
|
1358 |
|
1359 text_raw {* |
|
1360 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1361 \mode<presentation>{ |
|
1362 \begin{frame}[c] |
|
1363 \frametitle{\LARGE Examples} |
|
1364 |
|
1365 \begin{itemize} |
|
1366 \item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular |
|
1367 \begin{quote}\small |
|
1368 \begin{tabular}{lcl} |
|
1369 \smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\ |
|
1370 \smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\ |
|
1371 \smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\ |
|
1372 \smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\ |
|
1373 \end{tabular} |
|
1374 \end{quote} |
|
1375 |
|
1376 \item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular |
|
1377 \begin{quote}\small |
|
1378 \begin{tabular}{lcl} |
|
1379 \smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\, n \ge 0\}}\\ |
|
1380 \smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\ |
|
1381 \smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\ |
|
1382 \smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\ |
|
1383 & \smath{\vdots} &\\ |
|
1384 \end{tabular} |
|
1385 \end{quote} |
|
1386 \end{itemize} |
|
1387 |
|
1388 \end{frame}} |
|
1389 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1390 *} |
|
1391 |
|
1392 |
|
1393 text_raw {* |
|
1394 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1395 \mode<presentation>{ |
|
1396 \begin{frame}[c] |
|
1397 \frametitle{\LARGE What We Have Not Achieved} |
|
1398 |
|
1399 \begin{itemize} |
|
1400 \item regular expressions are not good if you look for a minimal |
|
1401 one for a language (DFAs have this notion)\pause\bigskip |
|
1402 |
|
1403 \item Is there anything to be said about context free languages:\medskip |
|
1404 |
|
1405 \begin{quote} |
|
1406 A context free language is where every string can be recognised by |
|
1407 a pushdown automaton.\bigskip |
|
1408 \end{quote} |
|
1409 \end{itemize} |
|
1410 |
|
1411 \textcolor{gray}{\footnotesize Yes. Derivatives also work for c-f grammars. Ongoing work.} |
|
1412 |
|
1413 \end{frame}} |
|
1414 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1415 *} |
|
1416 |
|
1417 |
|
1418 text_raw {* |
|
1419 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1420 \mode<presentation>{ |
|
1421 \begin{frame}[c] |
|
1422 \frametitle{\LARGE Conclusion} |
|
1423 |
|
1424 \begin{itemize} |
|
1425 \item We formalised the Myhill-Nerode theorem based on |
|
1426 regular expressions (DFA are difficult to deal with in a theorem prover).\smallskip |
|
1427 |
|
1428 \item Seems to be a common theme: algorithms need to be reformulated |
|
1429 to better suit formal treatment.\smallskip |
|
1430 |
|
1431 \item The most interesting aspect is that we are able to |
|
1432 implement the matcher directly inside the theorem prover |
|
1433 (ongoing work).\smallskip |
|
1434 |
|
1435 \item Parsing is a vast field and seems to offer new results. |
|
1436 \end{itemize} |
|
1437 |
|
1438 \end{frame}} |
|
1439 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1440 *} |
|
1441 |
|
1442 text_raw {* |
|
1443 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1444 \mode<presentation>{ |
|
1445 \begin{frame}<1>[b] |
1122 \frametitle{ |
1446 \frametitle{ |
1123 \begin{tabular}{c} |
1447 \begin{tabular}{c} |
1124 \mbox{}\\[23mm] |
1448 \mbox{}\\[13mm] |
1125 \alert{\LARGE Thank you very much!}\\ |
1449 \alert{\LARGE Thank you very much!}\\ |
1126 \alert{\Large Questions?} |
1450 \alert{\Large Questions?} |
1127 \end{tabular}} |
1451 \end{tabular}} |
1128 |
1452 |
1129 \end{frame}} |
1453 %\begin{center} |
1130 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1454 %\bf \underline{Short Bio:} |
1131 *} |
1455 %\end{center} |
|
1456 %\mbox{}\\[-17mm]\mbox{}\small |
|
1457 %\begin{itemize} |
|
1458 %\item PhD in Cambridge |
|
1459 %\item Emmy-Noether Fellowship in Munich |
|
1460 %\item main results in nominal reasoning and nominal unification |
|
1461 %\end{itemize} |
|
1462 |
|
1463 \end{frame}} |
|
1464 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1465 *} |
|
1466 |
1132 |
1467 |
1133 |
1468 |
1134 |
1469 |
1135 (*<*) |
1470 (*<*) |
1136 end |
1471 end |