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