|
1 (*<*) |
|
2 theory Slides1 |
|
3 imports "~~/src/HOL/Library/LaTeXsugar" |
|
4 begin |
|
5 |
|
6 notation (latex output) |
|
7 set ("_") and |
|
8 Cons ("_::/_" [66,65] 65) |
|
9 |
|
10 (*>*) |
|
11 |
|
12 |
|
13 text_raw {* |
|
14 %\renewcommand{\slidecaption}{Cambridge, 9 November 2010} |
|
15 \renewcommand{\slidecaption}{Nijmegen, 25 August 2011} |
|
16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
17 \mode<presentation>{ |
|
18 \begin{frame} |
|
19 \frametitle{% |
|
20 \begin{tabular}{@ {}c@ {}} |
|
21 \Large A Formalisation of the\\[-4mm] |
|
22 \Large Myhill-Nerode Theorem based on\\[-4mm] |
|
23 \Large Regular Expressions\\[-4mm] |
|
24 \Large (Proof Pearl)\\[0mm] |
|
25 \end{tabular}} |
|
26 |
|
27 \begin{center} |
|
28 \begin{tabular}{c@ {\hspace{15mm}}c} |
|
29 \includegraphics[scale=0.034]{chunhan.jpg} & |
|
30 \includegraphics[scale=0.034]{xingyuan.jpg}\\[-5mm] |
|
31 \end{tabular} |
|
32 \end{center} |
|
33 |
|
34 |
|
35 \begin{center} |
|
36 \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA |
|
37 University of Science and Technology in Nanjing |
|
38 \end{center} |
|
39 |
|
40 \begin{center} |
|
41 \small Christian Urban\\ |
|
42 TU Munich |
|
43 \end{center} |
|
44 |
|
45 |
|
46 \end{frame}} |
|
47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
48 |
|
49 *} |
|
50 |
|
51 text_raw {* |
|
52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
53 \mode<presentation>{ |
|
54 \begin{frame}[c] |
|
55 \frametitle{In Most Textbooks\ldots} |
|
56 |
|
57 \begin{itemize} |
|
58 \item A \alert{regular language} is one where there is a DFA that |
|
59 recognises it.\bigskip\pause |
|
60 \end{itemize} |
|
61 |
|
62 |
|
63 I can think of three reasons why this is a good definition:\medskip |
|
64 \begin{itemize} |
|
65 \item string matching via DFAs (yacc) |
|
66 \item pumping lemma |
|
67 \item closure properties of regular languages (closed under complement) |
|
68 \end{itemize} |
|
69 |
|
70 \end{frame}} |
|
71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
72 |
|
73 *} |
|
74 |
|
75 |
|
76 text_raw {* |
|
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
78 \mode<presentation>{ |
|
79 \begin{frame}[c] |
|
80 \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} |
|
81 |
|
82 \begin{center} |
|
83 \huge\bf\textcolor{gray}{in Nuprl} |
|
84 \end{center} |
|
85 |
|
86 \begin{itemize} |
|
87 \item Constable, Jackson, Naumov, Uribe\medskip |
|
88 \item \alert{18 months} for automata theory, Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode) |
|
89 \end{itemize} |
|
90 |
|
91 \end{frame}} |
|
92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
93 |
|
94 *} |
|
95 |
|
96 text_raw {* |
|
97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
98 \mode<presentation>{ |
|
99 \begin{frame}[c] |
|
100 \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} |
|
101 |
|
102 \begin{center} |
|
103 \huge\bf\textcolor{gray}{in Coq} |
|
104 \end{center} |
|
105 |
|
106 \begin{itemize} |
|
107 \item Filli\^atre, Briais, Braibant and others |
|
108 \item multi-year effort; a number of results in automata theory, e.g.\medskip |
|
109 \begin{itemize} |
|
110 \item Kleene's thm.~by Filli\^atre (\alert{``rather big''}) |
|
111 \item automata theory by Briais (5400 loc) |
|
112 \item Braibant ATBR library, including Myhill-Nerode ($>\!\!\!>$2000 loc) |
|
113 \item Mirkin's partial derivative automaton construction (10600 loc) |
|
114 \end{itemize} |
|
115 \end{itemize} |
|
116 |
|
117 \end{frame}} |
|
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
119 |
|
120 *} |
|
121 |
|
122 text_raw {* |
|
123 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
124 \mode<presentation>{ |
|
125 \begin{frame}[t] |
|
126 \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} |
|
127 \mbox{}\\[-10mm]\mbox{} |
|
128 |
|
129 \begin{center} |
|
130 \huge\bf\textcolor{gray}{in HOL} |
|
131 \end{center} |
|
132 |
|
133 \begin{itemize} |
|
134 \item automata @{text "\<Rightarrow>"} graphs, matrices, functions |
|
135 \item<2-> combining automata/graphs |
|
136 |
|
137 \onslide<2->{ |
|
138 \begin{center} |
|
139 \begin{tabular}{ccc} |
|
140 \begin{tikzpicture}[scale=1] |
|
141 %\draw[step=2mm] (-1,-1) grid (1,1); |
|
142 |
|
143 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); |
|
144 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3); |
|
145 |
|
146 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
147 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
148 |
|
149 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
150 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
151 |
|
152 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
153 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
154 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
155 |
|
156 \draw (-0.6,0.0) node {\small$A_1$}; |
|
157 \draw ( 0.6,0.0) node {\small$A_2$}; |
|
158 \end{tikzpicture}} |
|
159 |
|
160 & |
|
161 |
|
162 \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}} |
|
163 |
|
164 & |
|
165 |
|
166 \onslide<3->{\begin{tikzpicture}[scale=1] |
|
167 %\draw[step=2mm] (-1,-1) grid (1,1); |
|
168 |
|
169 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); |
|
170 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3); |
|
171 |
|
172 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
173 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
174 |
|
175 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
176 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
177 |
|
178 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
179 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
180 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; |
|
181 |
|
182 \draw (C) to [red, very thick, bend left=45] (B); |
|
183 \draw (D) to [red, very thick, bend right=45] (B); |
|
184 |
|
185 \draw (-0.6,0.0) node {\small$A_1$}; |
|
186 \draw ( 0.6,0.0) node {\small$A_2$}; |
|
187 \end{tikzpicture}} |
|
188 |
|
189 \end{tabular} |
|
190 \end{center}\medskip |
|
191 |
|
192 \only<4-5>{ |
|
193 \begin{tabular}{@ {}l@ {}} |
|
194 disjoint union:\\[2mm] |
|
195 \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}} |
|
196 \end{tabular}} |
|
197 \end{itemize} |
|
198 |
|
199 \only<5>{ |
|
200 \begin{textblock}{13.9}(0.7,7.7) |
|
201 \begin{block}{} |
|
202 \medskip |
|
203 \begin{minipage}{14cm}\raggedright |
|
204 Problems with definition for regularity (Slind):\bigskip\\ |
|
205 \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip |
|
206 \end{minipage} |
|
207 \end{block} |
|
208 \end{textblock}} |
|
209 \medskip |
|
210 |
|
211 \only<6->{A solution:\;\;\smath{\text{nat}} @{text "\<Rightarrow>"} state nodes} |
|
212 |
|
213 \end{frame}} |
|
214 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
215 *} |
|
216 |
|
217 text_raw {* |
|
218 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
219 \mode<presentation>{ |
|
220 \begin{frame}[t] |
|
221 \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} |
|
222 \mbox{}\\[-10mm]\mbox{} |
|
223 |
|
224 \begin{center} |
|
225 \huge\bf\textcolor{gray}{in HOL} |
|
226 \end{center} |
|
227 |
|
228 \begin{itemize} |
|
229 \item Kozen's proof of Myhill-Nerode:\\ |
|
230 \hspace{5cm}\alert{inaccessible states} |
|
231 \end{itemize}\bigskip\bigskip |
|
232 |
|
233 \begin{center} |
|
234 \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A} |
|
235 \end{center} |
|
236 |
|
237 |
|
238 \end{frame}} |
|
239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
240 *} |
|
241 |
|
242 text_raw {* |
|
243 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
244 \mode<presentation>{ |
|
245 \begin{frame}[t] |
|
246 \frametitle{Regular Expressions} |
|
247 \mbox{}\\[20mm]\mbox{} |
|
248 |
|
249 \begin{textblock}{13.9}(0.7,2.2) |
|
250 \begin{block}{} |
|
251 \begin{minipage}{13.4cm}\raggedright |
|
252 {\bf Definition:}\smallskip\\ |
|
253 |
|
254 A language \smath{A} is \alert{regular}, provided there exists a\\ |
|
255 regular expression that matches all strings of \smath{A}. |
|
256 \end{minipage} |
|
257 \end{block} |
|
258 \end{textblock}\pause |
|
259 |
|
260 {\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause |
|
261 |
|
262 What we might lose?\pause |
|
263 \begin{itemize}\renewcommand{\ULthickness}{2pt} |
|
264 \item pumping lemma\pause |
|
265 \item closure under complementation\pause |
|
266 \item \only<6>{regular expression matching}% |
|
267 \only<7>{\textcolor{red}{\sout{\textcolor{black}{regular expression matching}}}} |
|
268 \end{itemize} |
|
269 |
|
270 |
|
271 \end{frame}} |
|
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
273 |
|
274 *} |
|
275 |
|
276 text_raw {* |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 \mode<presentation>{ |
|
279 \begin{frame}[t] |
|
280 \frametitle{Regular Expressions} |
|
281 |
|
282 \end{frame}} |
|
283 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
284 |
|
285 *} |
|
286 |
|
287 |
|
288 |
|
289 text_raw {* |
|
290 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
291 \mode<presentation>{ |
|
292 \begin{frame}[c] |
|
293 \frametitle{\LARGE Regular Expression Matching} |
|
294 |
|
295 \begin{itemize} |
|
296 \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip |
|
297 \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited |
|
298 for a first-order version''\medskip |
|
299 \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''\bigskip\pause |
|
300 |
|
301 \begin{quote}\small |
|
302 ``Unfortunately, regular expression derivatives have been lost in the |
|
303 sands of time, and few computer scientists are aware of them.'' |
|
304 \end{quote} |
|
305 \end{itemize} |
|
306 |
|
307 |
|
308 \end{frame}} |
|
309 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
310 |
|
311 *} |
|
312 |
|
313 |
|
314 |
|
315 text_raw {* |
|
316 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
317 \mode<presentation>{ |
|
318 \begin{frame}[c] |
|
319 \frametitle{\LARGE The Myhill-Nerode Theorem} |
|
320 |
|
321 \begin{itemize} |
|
322 \item provides necessary and suf\!ficient conditions for a language |
|
323 being regular (pumping lemma only necessary)\medskip |
|
324 |
|
325 \item will help with closure properties of regular languages\bigskip\pause |
|
326 |
|
327 \item key is the equivalence relation:\smallskip |
|
328 \begin{center} |
|
329 \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L} |
|
330 \end{center} |
|
331 \end{itemize} |
|
332 |
|
333 \end{frame}} |
|
334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
335 |
|
336 *} |
|
337 |
|
338 text_raw {* |
|
339 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
340 \mode<presentation>{ |
|
341 \begin{frame}[c] |
|
342 \frametitle{\LARGE The Myhill-Nerode Theorem} |
|
343 |
|
344 \mbox{}\\[5cm] |
|
345 |
|
346 \begin{itemize} |
|
347 \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}} |
|
348 \end{itemize} |
|
349 |
|
350 \end{frame}} |
|
351 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
352 |
|
353 *} |
|
354 |
|
355 |
|
356 text_raw {* |
|
357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
358 \mode<presentation>{ |
|
359 \begin{frame}[c] |
|
360 \frametitle{\LARGE Equivalence Classes} |
|
361 |
|
362 \begin{itemize} |
|
363 \item \smath{L = []} |
|
364 \begin{center} |
|
365 \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}} |
|
366 \end{center}\bigskip\bigskip |
|
367 |
|
368 \item \smath{L = [c]} |
|
369 \begin{center} |
|
370 \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}} |
|
371 \end{center}\bigskip\bigskip |
|
372 |
|
373 \item \smath{L = \varnothing} |
|
374 \begin{center} |
|
375 \smath{\Big\{U\!N\!IV\Big\}} |
|
376 \end{center} |
|
377 |
|
378 \end{itemize} |
|
379 |
|
380 \end{frame}} |
|
381 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
382 |
|
383 *} |
|
384 |
|
385 |
|
386 text_raw {* |
|
387 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
388 \mode<presentation>{ |
|
389 \begin{frame}[c] |
|
390 \frametitle{\LARGE Regular Languages} |
|
391 |
|
392 \begin{itemize} |
|
393 \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} |
|
394 such that \smath{\mathbb{L}(M) = L}\\[1.5cm] |
|
395 |
|
396 \item Myhill-Nerode: |
|
397 |
|
398 \begin{center} |
|
399 \begin{tabular}{l} |
|
400 finite $\Rightarrow$ regular\\ |
|
401 \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm] |
|
402 regular $\Rightarrow$ finite\\ |
|
403 \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} |
|
404 \end{tabular} |
|
405 \end{center} |
|
406 |
|
407 \end{itemize} |
|
408 |
|
409 \end{frame}} |
|
410 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
411 |
|
412 *} |
|
413 |
|
414 |
|
415 text_raw {* |
|
416 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
417 \mode<presentation>{ |
|
418 \begin{frame}[c] |
|
419 \frametitle{\LARGE Final States} |
|
420 |
|
421 \mbox{}\\[3cm] |
|
422 |
|
423 \begin{itemize} |
|
424 \item \smath{\text{final}_L\,X \dn}\\ |
|
425 \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L} |
|
426 \smallskip |
|
427 \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}} |
|
428 |
|
429 \end{itemize} |
|
430 |
|
431 \end{frame}} |
|
432 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
433 *} |
|
434 |
|
435 |
|
436 text_raw {* |
|
437 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
438 \mode<presentation>{ |
|
439 \begin{frame}[c] |
|
440 \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes} |
|
441 |
|
442 \smath{L = \{[c]\}} |
|
443 |
|
444 \begin{tabular}{@ {\hspace{-7mm}}cc} |
|
445 \begin{tabular}{c} |
|
446 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] |
|
447 \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] |
|
448 |
|
449 %\draw[help lines] (0,0) grid (3,2); |
|
450 |
|
451 \node[state,initial] (q_0) {$R_1$}; |
|
452 \node[state,accepting] (q_1) [above right of=q_0] {$R_2$}; |
|
453 \node[state] (q_2) [below right of=q_0] {$R_3$}; |
|
454 |
|
455 \path[->] (q_0) edge node {c} (q_1) |
|
456 edge node [swap] {$\Sigma-{c}$} (q_2) |
|
457 (q_2) edge [loop below] node {$\Sigma$} () |
|
458 (q_1) edge node {$\Sigma$} (q_2); |
|
459 \end{tikzpicture} |
|
460 \end{tabular} |
|
461 & |
|
462 \begin{tabular}[t]{ll} |
|
463 \\[-20mm] |
|
464 \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm] |
|
465 |
|
466 \smath{R_1}: & \smath{\{[]\}}\\ |
|
467 \smath{R_2}: & \smath{\{[c]\}}\\ |
|
468 \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm] |
|
469 \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}} |
|
470 \end{tabular} |
|
471 |
|
472 \end{tabular} |
|
473 |
|
474 \end{frame}} |
|
475 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
476 *} |
|
477 |
|
478 |
|
479 text_raw {* |
|
480 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
481 \mode<presentation>{ |
|
482 \begin{frame}[c] |
|
483 \frametitle{\LARGE Systems of Equations} |
|
484 |
|
485 Inspired by a method of Brzozowski\;'64, we can build an equational system |
|
486 characterising the equivalence classes: |
|
487 |
|
488 \begin{center} |
|
489 \begin{tabular}{@ {\hspace{-20mm}}c} |
|
490 \\[-13mm] |
|
491 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] |
|
492 \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] |
|
493 |
|
494 %\draw[help lines] (0,0) grid (3,2); |
|
495 |
|
496 \node[state,initial] (p_0) {$R_1$}; |
|
497 \node[state,accepting] (p_1) [right of=q_0] {$R_2$}; |
|
498 |
|
499 \path[->] (p_0) edge [bend left] node {a} (p_1) |
|
500 edge [loop above] node {b} () |
|
501 (p_1) edge [loop above] node {a} () |
|
502 edge [bend left] node {b} (p_0); |
|
503 \end{tikzpicture}\\ |
|
504 \\[-13mm] |
|
505 \end{tabular} |
|
506 \end{center} |
|
507 |
|
508 \begin{center} |
|
509 \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
510 & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\ |
|
511 & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\ |
|
512 \onslide<3->{we can prove} |
|
513 & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} |
|
514 & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\ |
|
515 & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}} |
|
516 & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\ |
|
517 \end{tabular} |
|
518 \end{center} |
|
519 |
|
520 \end{frame}} |
|
521 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
522 *} |
|
523 |
|
524 text_raw {* |
|
525 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
526 \mode<presentation>{ |
|
527 \begin{frame}<1>[t] |
|
528 \small |
|
529 |
|
530 \begin{center} |
|
531 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
532 \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} |
|
533 & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
534 \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}} |
|
535 & \onslide<1->{\smath{R_1; a + R_2; a}}\\ |
|
536 |
|
537 & & & \onslide<2->{by Arden}\\ |
|
538 |
|
539 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
|
540 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
541 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
|
542 & \only<2>{\smath{R_1; a + R_2; a}}% |
|
543 \only<3->{\smath{R_1; a\cdot a^\star}}\\ |
|
544 |
|
545 & & & \onslide<4->{by Arden}\\ |
|
546 |
|
547 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
|
548 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |
|
549 \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}} |
|
550 & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\ |
|
551 |
|
552 & & & \onslide<5->{by substitution}\\ |
|
553 |
|
554 \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} |
|
555 & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ |
|
556 \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}} |
|
557 & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\ |
|
558 |
|
559 & & & \onslide<6->{by Arden}\\ |
|
560 |
|
561 \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} |
|
562 & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
563 \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}} |
|
564 & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\ |
|
565 |
|
566 & & & \onslide<7->{by substitution}\\ |
|
567 |
|
568 \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} |
|
569 & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
570 \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}} |
|
571 & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star |
|
572 \cdot a\cdot a^\star}}\\ |
|
573 \end{tabular} |
|
574 \end{center} |
|
575 |
|
576 \end{frame}} |
|
577 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
578 *} |
|
579 |
|
580 text_raw {* |
|
581 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
582 \mode<presentation>{ |
|
583 \begin{frame}[c] |
|
584 \frametitle{\LARGE A Variant of Arden's Lemma} |
|
585 |
|
586 {\bf Arden's Lemma:}\smallskip |
|
587 |
|
588 If \smath{[] \not\in A} then |
|
589 \begin{center} |
|
590 \smath{X = X; A + \text{something}} |
|
591 \end{center} |
|
592 has the (unique) solution |
|
593 \begin{center} |
|
594 \smath{X = \text{something} ; A^\star} |
|
595 \end{center} |
|
596 |
|
597 |
|
598 \end{frame}} |
|
599 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
600 *} |
|
601 |
|
602 |
|
603 text_raw {* |
|
604 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
605 \mode<presentation>{ |
|
606 \begin{frame}<1->[t] |
|
607 \small |
|
608 |
|
609 \begin{center} |
|
610 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
611 \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} |
|
612 & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
613 \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}} |
|
614 & \onslide<1->{\smath{R_1; a + R_2; a}}\\ |
|
615 |
|
616 & & & \onslide<2->{by Arden}\\ |
|
617 |
|
618 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
|
619 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
620 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
|
621 & \only<2>{\smath{R_1; a + R_2; a}}% |
|
622 \only<3->{\smath{R_1; a\cdot a^\star}}\\ |
|
623 |
|
624 & & & \onslide<4->{by Arden}\\ |
|
625 |
|
626 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
|
627 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |
|
628 \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}} |
|
629 & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\ |
|
630 |
|
631 & & & \onslide<5->{by substitution}\\ |
|
632 |
|
633 \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} |
|
634 & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ |
|
635 \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}} |
|
636 & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\ |
|
637 |
|
638 & & & \onslide<6->{by Arden}\\ |
|
639 |
|
640 \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} |
|
641 & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
642 \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}} |
|
643 & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\ |
|
644 |
|
645 & & & \onslide<7->{by substitution}\\ |
|
646 |
|
647 \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} |
|
648 & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
649 \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}} |
|
650 & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star |
|
651 \cdot a\cdot a^\star}}\\ |
|
652 \end{tabular} |
|
653 \end{center} |
|
654 |
|
655 \only<8->{ |
|
656 \begin{textblock}{6}(2.5,4) |
|
657 \begin{block}{} |
|
658 \begin{minipage}{8cm}\raggedright |
|
659 |
|
660 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm] |
|
661 \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] |
|
662 |
|
663 %\draw[help lines] (0,0) grid (3,2); |
|
664 |
|
665 \node[state,initial] (p_0) {$R_1$}; |
|
666 \node[state,accepting] (p_1) [right of=q_0] {$R_2$}; |
|
667 |
|
668 \path[->] (p_0) edge [bend left] node {a} (p_1) |
|
669 edge [loop above] node {b} () |
|
670 (p_1) edge [loop above] node {a} () |
|
671 edge [bend left] node {b} (p_0); |
|
672 \end{tikzpicture} |
|
673 |
|
674 \end{minipage} |
|
675 \end{block} |
|
676 \end{textblock}} |
|
677 |
|
678 \end{frame}} |
|
679 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
680 *} |
|
681 |
|
682 text_raw {* |
|
683 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
684 \mode<presentation>{ |
|
685 \begin{frame}[c] |
|
686 \frametitle{\LARGE The Equ's Solving Algorithm} |
|
687 |
|
688 \begin{itemize} |
|
689 \item The algorithm must terminate: Arden makes one equation smaller; |
|
690 substitution deletes one variable from the right-hand sides.\bigskip |
|
691 |
|
692 \item We need to maintain the invariant that Arden is applicable |
|
693 (if \smath{[] \not\in A} then \ldots):\medskip |
|
694 |
|
695 \begin{center}\small |
|
696 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
697 \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\ |
|
698 \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\ |
|
699 |
|
700 & & & by Arden\\ |
|
701 |
|
702 \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\ |
|
703 \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\ |
|
704 \end{tabular} |
|
705 \end{center} |
|
706 |
|
707 \end{itemize} |
|
708 |
|
709 |
|
710 \end{frame}} |
|
711 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
712 *} |
|
713 |
|
714 text_raw {* |
|
715 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
716 \mode<presentation>{ |
|
717 \begin{frame}[c] |
|
718 \frametitle{\LARGE The Equ's Solving Algorithm} |
|
719 |
|
720 \begin{itemize} |
|
721 \item The algorithm is still a bit hairy to formalise because of our set-representation |
|
722 for equations: |
|
723 |
|
724 \begin{center} |
|
725 \begin{tabular}{ll} |
|
726 \smath{\big\{ (X, \{(Y_1, r_1), (Y_2, r_2), \ldots\}),}\\ |
|
727 \mbox{}\hspace{5mm}\smath{\ldots}\\ |
|
728 & \smath{\big\}} |
|
729 \end{tabular} |
|
730 \end{center}\bigskip\pause |
|
731 |
|
732 \small |
|
733 they are generated from \smath{U\!N\!IV /\!/ \approx_L} |
|
734 |
|
735 \end{itemize} |
|
736 |
|
737 |
|
738 \end{frame}} |
|
739 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
740 *} |
|
741 |
|
742 |
|
743 |
|
744 text_raw {* |
|
745 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
746 \mode<presentation>{ |
|
747 \begin{frame}[c] |
|
748 \frametitle{\LARGE Other Direction} |
|
749 |
|
750 One has to prove |
|
751 |
|
752 \begin{center} |
|
753 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} |
|
754 \end{center} |
|
755 |
|
756 by induction on \smath{r}. Not trivial, but after a bit |
|
757 of thinking (by Chunhan), one can prove that if |
|
758 |
|
759 \begin{center} |
|
760 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm} |
|
761 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})} |
|
762 \end{center} |
|
763 |
|
764 then |
|
765 |
|
766 \begin{center} |
|
767 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})} |
|
768 \end{center} |
|
769 |
|
770 |
|
771 |
|
772 \end{frame}} |
|
773 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
774 *} |
|
775 |
|
776 text_raw {* |
|
777 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
778 \mode<presentation>{ |
|
779 \begin{frame}[c] |
|
780 \frametitle{\LARGE What Have We Achieved?} |
|
781 |
|
782 \begin{itemize} |
|
783 \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}} |
|
784 \bigskip\pause |
|
785 \item regular languages are closed under complementation; this is easy |
|
786 \begin{center} |
|
787 \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}} |
|
788 \end{center}\pause\bigskip |
|
789 |
|
790 \item if you want to do regular expression matching (see Scott's paper)\pause\bigskip |
|
791 |
|
792 \item I cannot yet give definite numbers |
|
793 \end{itemize} |
|
794 |
|
795 \only<2>{ |
|
796 \begin{textblock}{10}(4,14) |
|
797 \small |
|
798 \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L} |
|
799 \end{textblock} |
|
800 } |
|
801 |
|
802 |
|
803 |
|
804 \end{frame}} |
|
805 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
806 *} |
|
807 |
|
808 text_raw {* |
|
809 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
810 \mode<presentation>{ |
|
811 \begin{frame}[c] |
|
812 \frametitle{\LARGE Examples} |
|
813 |
|
814 \begin{itemize} |
|
815 \item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular |
|
816 \begin{quote}\small |
|
817 \begin{tabular}{lcl} |
|
818 \smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\ |
|
819 \smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\ |
|
820 \smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\ |
|
821 \smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\ |
|
822 \end{tabular} |
|
823 \end{quote} |
|
824 |
|
825 \item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular |
|
826 \begin{quote}\small |
|
827 \begin{tabular}{lcl} |
|
828 \smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\, n \ge 0\}}\\ |
|
829 \smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\ |
|
830 \smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\ |
|
831 \smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\ |
|
832 & \smath{\vdots} &\\ |
|
833 \end{tabular} |
|
834 \end{quote} |
|
835 \end{itemize} |
|
836 |
|
837 \end{frame}} |
|
838 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
839 *} |
|
840 |
|
841 |
|
842 text_raw {* |
|
843 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
844 \mode<presentation>{ |
|
845 \begin{frame}[c] |
|
846 \frametitle{\LARGE What We Have Not Achieved} |
|
847 |
|
848 \begin{itemize} |
|
849 \item regular expressions are not good if you look for a minimal |
|
850 one for a language (DFAs have this notion)\pause\bigskip |
|
851 |
|
852 \item Is there anything to be said about context free languages:\medskip |
|
853 |
|
854 \begin{quote} |
|
855 A context free language is where every string can be recognised by |
|
856 a pushdown automaton. |
|
857 \end{quote} |
|
858 \end{itemize} |
|
859 |
|
860 \end{frame}} |
|
861 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
862 *} |
|
863 |
|
864 |
|
865 text_raw {* |
|
866 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
867 \mode<presentation>{ |
|
868 \begin{frame}[c] |
|
869 \frametitle{\LARGE Conclusion} |
|
870 |
|
871 \begin{itemize} |
|
872 \item on balance regular expression are superior |
|
873 to DFAs, in my opinion\bigskip |
|
874 |
|
875 \item I cannot think of a reason to not teach regular languages |
|
876 to students this way (!?)\bigskip |
|
877 |
|
878 \item I have never ever seen a proof of Myhill-Nerode based on |
|
879 regular expressions\bigskip |
|
880 |
|
881 \item no application, but lots of fun\bigskip |
|
882 |
|
883 \item great source of examples |
|
884 |
|
885 \end{itemize} |
|
886 |
|
887 \end{frame}} |
|
888 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
889 *} |
|
890 |
|
891 (*<*) |
|
892 end |
|
893 (*>*) |