11 |
11 |
12 |
12 |
13 text_raw {* |
13 text_raw {* |
14 %\renewcommand{\slidecaption}{Cambridge, 9 November 2010} |
14 %\renewcommand{\slidecaption}{Cambridge, 9 November 2010} |
15 \renewcommand{\slidecaption}{Nijmegen, 25 August 2011} |
15 \renewcommand{\slidecaption}{Nijmegen, 25 August 2011} |
|
16 \renewcommand{\ULthickness}{2pt} |
16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
17 \mode<presentation>{ |
18 \mode<presentation>{ |
18 \begin{frame} |
19 \begin{frame} |
19 \frametitle{% |
20 \frametitle{% |
20 \begin{tabular}{@ {}c@ {}} |
21 \begin{tabular}{@ {}c@ {}} |
50 |
51 |
51 text_raw {* |
52 text_raw {* |
52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
53 \mode<presentation>{ |
54 \mode<presentation>{ |
54 \begin{frame}[c] |
55 \begin{frame}[c] |
55 \frametitle{In Most Textbooks\ldots} |
56 \frametitle{} |
56 |
57 |
57 \begin{itemize} |
58 \begin{textblock}{12.9}(1.5,3.2) |
58 \item A \alert{regular language} is one where there is a DFA that |
59 \begin{block}{} |
59 recognises it.\bigskip\pause |
60 \begin{minipage}{12.4cm}\raggedright |
60 \end{itemize} |
61 \large I want to teach \alert{students}\\ |
61 |
62 with theorem provers (induction). |
62 |
63 \end{minipage} |
63 I can think of three reasons why this is a good definition:\medskip |
64 \end{block} |
64 \begin{itemize} |
65 \end{textblock}\pause |
65 \item string matching via DFAs (yacc) |
66 |
66 \item pumping lemma |
67 \mbox{}\\[35mm]\mbox{} |
67 \item closure properties of regular languages (closed under complement) |
68 |
|
69 \begin{itemize} |
|
70 \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}% |
|
71 \only<3->{\textcolor{red}{\sout{\textcolor{black}% |
|
72 {\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}}}\medskip |
|
73 \item<3-> formal language theory \\ |
|
74 \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman |
68 \end{itemize} |
75 \end{itemize} |
69 |
76 |
70 \end{frame}} |
77 \end{frame}} |
71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
72 |
79 |
224 \begin{center} |
233 \begin{center} |
225 \huge\bf\textcolor{gray}{in HOL} |
234 \huge\bf\textcolor{gray}{in HOL} |
226 \end{center} |
235 \end{center} |
227 |
236 |
228 \begin{itemize} |
237 \begin{itemize} |
229 \item Kozen's proof of Myhill-Nerode:\\ |
238 \item Kozen's paper proof of Myhill-Nerode:\\ |
230 \hspace{5cm}\alert{inaccessible states} |
239 \hspace{2cm}requires absence of \alert{inaccessible states} |
231 \end{itemize}\bigskip\bigskip |
240 \end{itemize}\bigskip\bigskip |
232 |
241 |
233 \begin{center} |
242 \begin{center} |
234 \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A} |
243 \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A} |
235 \end{center} |
244 \end{center} |
241 |
250 |
242 text_raw {* |
251 text_raw {* |
243 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
252 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
244 \mode<presentation>{ |
253 \mode<presentation>{ |
245 \begin{frame}[t] |
254 \begin{frame}[t] |
246 \frametitle{Regular Expressions} |
255 \frametitle{} |
247 \mbox{}\\[20mm]\mbox{} |
256 \mbox{}\\[25mm]\mbox{} |
248 |
257 |
249 \begin{textblock}{13.9}(0.7,2.2) |
258 \begin{textblock}{13.9}(0.7,1.2) |
250 \begin{block}{} |
259 \begin{block}{} |
251 \begin{minipage}{13.4cm}\raggedright |
260 \begin{minipage}{13.4cm}\raggedright |
252 {\bf Definition:}\smallskip\\ |
261 {\bf Definition:}\smallskip\\ |
253 |
262 |
254 A language \smath{A} is \alert{regular}, provided there exists a\\ |
263 A language \smath{A} is \alert{regular}, provided there exists a\\ |
255 regular expression that matches all strings of \smath{A}. |
264 regular expression that matches all strings of \smath{A}. |
256 \end{minipage} |
265 \end{minipage} |
257 \end{block} |
266 \end{block} |
258 \end{textblock}\pause |
267 \end{textblock}\pause |
259 |
268 |
260 {\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause |
269 {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause |
261 |
270 |
262 What we might lose?\pause |
271 Do we lose anything?\pause |
263 \begin{itemize}\renewcommand{\ULthickness}{2pt} |
272 \begin{itemize} |
264 \item pumping lemma\pause |
273 \item pumping lemma\pause |
265 \item closure under complementation\pause |
274 \item closure under complementation\pause |
266 \item \only<6>{regular expression matching}% |
275 \item \only<6>{regular expression matching}% |
267 \only<7>{\textcolor{red}{\sout{\textcolor{black}{regular expression matching}}}} |
276 \only<7->{\textcolor{red}{\sout{\textcolor{black}{regular expression matching}}}} |
268 \end{itemize} |
277 \item<8-> most textbooks are about automata |
269 |
278 \end{itemize} |
270 |
279 |
271 \end{frame}} |
280 |
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
281 \end{frame}} |
273 |
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
274 *} |
283 |
275 |
284 *} |
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 |
285 |
314 |
286 |
315 text_raw {* |
287 text_raw {* |
316 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
288 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
317 \mode<presentation>{ |
289 \mode<presentation>{ |
324 |
296 |
325 \item will help with closure properties of regular languages\bigskip\pause |
297 \item will help with closure properties of regular languages\bigskip\pause |
326 |
298 |
327 \item key is the equivalence relation:\smallskip |
299 \item key is the equivalence relation:\smallskip |
328 \begin{center} |
300 \begin{center} |
329 \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L} |
301 \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} |
330 \end{center} |
302 \end{center} |
331 \end{itemize} |
303 \end{itemize} |
332 |
304 |
333 \end{frame}} |
305 \end{frame}} |
334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
306 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
343 |
315 |
344 \mbox{}\\[5cm] |
316 \mbox{}\\[5cm] |
345 |
317 |
346 \begin{itemize} |
318 \begin{itemize} |
347 \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}} |
319 \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} |
320 \end{itemize} |
379 |
321 |
380 \end{frame}} |
322 \end{frame}} |
381 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
323 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
382 |
324 |
709 |
651 |
710 \end{frame}} |
652 \end{frame}} |
711 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
653 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
712 *} |
654 *} |
713 |
655 |
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 |
656 |
744 text_raw {* |
657 text_raw {* |
745 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
658 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
746 \mode<presentation>{ |
659 \mode<presentation>{ |
747 \begin{frame}[c] |
660 \begin{frame}[c] |
803 |
716 |
804 \end{frame}} |
717 \end{frame}} |
805 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
718 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
806 *} |
719 *} |
807 |
720 |
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 |
721 |
841 |
722 |
842 text_raw {* |
723 text_raw {* |
843 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
724 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
844 \mode<presentation>{ |
725 \mode<presentation>{ |