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 %%\renewcommand{\ULthickness}{2pt} |
|
17 \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=0pt, outer sep=0pt] |
|
18 \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};} |
17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
18 \mode<presentation>{ |
20 \mode<presentation>{ |
19 \begin{frame} |
21 \begin{frame} |
20 \frametitle{% |
22 \frametitle{% |
21 \begin{tabular}{@ {}c@ {}} |
23 \begin{tabular}{@ {}c@ {}} |
56 \frametitle{} |
57 \frametitle{} |
57 |
58 |
58 \begin{textblock}{12.9}(1.5,3.2) |
59 \begin{textblock}{12.9}(1.5,3.2) |
59 \begin{block}{} |
60 \begin{block}{} |
60 \begin{minipage}{12.4cm}\raggedright |
61 \begin{minipage}{12.4cm}\raggedright |
61 \large I want to teach \alert{students}\\ |
62 \large I want to teach \alert{students} with\\ |
62 with theorem provers (induction). |
63 theorem provers (especially inductions). |
63 \end{minipage} |
64 \end{minipage} |
64 \end{block} |
65 \end{block} |
65 \end{textblock}\pause |
66 \end{textblock}\pause |
66 |
67 |
67 \mbox{}\\[35mm]\mbox{} |
68 \mbox{}\\[35mm]\mbox{} |
68 |
69 |
69 \begin{itemize} |
70 \begin{itemize} |
70 \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}% |
71 \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}% |
71 \only<3->{\textcolor{red}{\sout{\textcolor{black}% |
72 \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip |
72 {\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}}}\medskip |
|
73 \item<3-> formal language theory \\ |
73 \item<3-> formal language theory \\ |
74 \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman |
74 \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman |
75 \end{itemize} |
75 \end{itemize} |
76 |
76 |
77 \end{frame}} |
77 \end{frame}} |
259 \begin{block}{} |
259 \begin{block}{} |
260 \begin{minipage}{13.4cm}\raggedright |
260 \begin{minipage}{13.4cm}\raggedright |
261 {\bf Definition:}\smallskip\\ |
261 {\bf Definition:}\smallskip\\ |
262 |
262 |
263 A language \smath{A} is \alert{regular}, provided there exists a\\ |
263 A language \smath{A} is \alert{regular}, provided there exists a\\ |
264 regular expression that matches all strings of \smath{A}. |
264 \alert{regular expression} that matches all strings of \smath{A}. |
265 \end{minipage} |
265 \end{minipage} |
266 \end{block} |
266 \end{block} |
267 \end{textblock}\pause |
267 \end{textblock}\pause |
268 |
268 |
269 {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause |
269 {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause |
411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
412 \mode<presentation>{ |
412 \mode<presentation>{ |
413 \begin{frame}[c] |
413 \begin{frame}[c] |
414 \frametitle{\LARGE Systems of Equations} |
414 \frametitle{\LARGE Systems of Equations} |
415 |
415 |
416 Inspired by a method of Brzozowski\;'64, we can build an equational system |
416 Inspired by a method of Brzozowski\;'64:\bigskip\bigskip |
417 characterising the equivalence classes: |
|
418 |
417 |
419 \begin{center} |
418 \begin{center} |
420 \begin{tabular}{@ {\hspace{-20mm}}c} |
419 \begin{tabular}{@ {\hspace{-20mm}}c} |
421 \\[-13mm] |
420 \\[-13mm] |
422 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] |
421 \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] |
463 & & & \onslide<2->{by Arden}\\ |
463 & & & \onslide<2->{by Arden}\\ |
464 |
464 |
465 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
465 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
466 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
466 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
467 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
467 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
468 & \only<2>{\smath{R_1; a + R_2; a}}% |
468 & \only<2->{\smath{R_1; a\cdot a^\star}}\\ |
469 \only<3->{\smath{R_1; a\cdot a^\star}}\\ |
|
470 |
|
471 & & & \onslide<4->{by Arden}\\ |
|
472 |
|
473 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
|
474 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |
|
475 \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}} |
|
476 & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\ |
|
477 |
|
478 & & & \onslide<5->{by substitution}\\ |
|
479 |
|
480 \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} |
|
481 & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ |
|
482 \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}} |
|
483 & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\ |
|
484 |
|
485 & & & \onslide<6->{by Arden}\\ |
|
486 |
|
487 \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} |
|
488 & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
489 \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}} |
|
490 & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\ |
|
491 |
|
492 & & & \onslide<7->{by substitution}\\ |
|
493 |
|
494 \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} |
|
495 & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ |
|
496 \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}} |
|
497 & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star |
|
498 \cdot a\cdot a^\star}}\\ |
|
499 \end{tabular} |
|
500 \end{center} |
|
501 |
|
502 \end{frame}} |
|
503 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
504 *} |
|
505 |
|
506 text_raw {* |
|
507 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
508 \mode<presentation>{ |
|
509 \begin{frame}[c] |
|
510 \frametitle{\LARGE A Variant of Arden's Lemma} |
|
511 |
|
512 {\bf ``Reversed'' Arden's Lemma:}\medskip |
|
513 |
|
514 If \smath{[] \not\in A} then |
|
515 \begin{center} |
|
516 \smath{X = X; A + \text{something}} |
|
517 \end{center} |
|
518 has the (unique) solution |
|
519 \begin{center} |
|
520 \smath{X = \text{something} ; A^\star} |
|
521 \end{center} |
|
522 |
|
523 |
|
524 \end{frame}} |
|
525 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
526 *} |
|
527 |
|
528 |
|
529 text_raw {* |
|
530 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
531 \mode<presentation>{ |
|
532 \begin{frame}<1->[t] |
|
533 \small |
|
534 |
|
535 \begin{center} |
|
536 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} |
|
537 \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} |
|
538 & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
539 \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}} |
|
540 & \onslide<1->{\smath{R_1; a + R_2; a}}\\ |
|
541 |
|
542 & & & \onslide<2->{by Arden}\\ |
|
543 |
|
544 \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} |
|
545 & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ |
|
546 \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} |
|
547 & \only<2>{\smath{R_1; a + R_2; a}}% |
|
548 \only<3->{\smath{R_1; a\cdot a^\star}}\\ |
|
549 |
469 |
550 & & & \onslide<4->{by Arden}\\ |
470 & & & \onslide<4->{by Arden}\\ |
551 |
471 |
552 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
472 \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} |
553 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |
473 & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ |