equal
deleted
inserted
replaced
21 \begin{frame} |
21 \begin{frame} |
22 \frametitle{% |
22 \frametitle{% |
23 \begin{tabular}{@ {}c@ {}} |
23 \begin{tabular}{@ {}c@ {}} |
24 \Large A Formalisation of the\\[-4mm] |
24 \Large A Formalisation of the\\[-4mm] |
25 \Large Myhill-Nerode Theorem based on\\[-4mm] |
25 \Large Myhill-Nerode Theorem based on\\[-4mm] |
26 \Large Regular Expressions\\[-4mm] |
26 \Large \alert<2>{Regular Expressions}\\[-4mm] |
27 \Large (Proof Pearl)\\[0mm] |
27 \Large (Proof Pearl)\\[0mm] |
28 \end{tabular}} |
28 \end{tabular}} |
29 |
29 |
30 \begin{center} |
30 \begin{center} |
31 \begin{tabular}{c@ {\hspace{15mm}}c} |
31 \begin{tabular}{c@ {\hspace{15mm}}c} |
54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
55 \mode<presentation>{ |
55 \mode<presentation>{ |
56 \begin{frame}[c] |
56 \begin{frame}[c] |
57 \frametitle{} |
57 \frametitle{} |
58 |
58 |
59 \begin{textblock}{12.9}(1.5,3.2) |
59 \begin{textblock}{12.9}(1.5,2.0) |
60 \begin{block}{} |
60 \begin{block}{} |
61 \begin{minipage}{12.4cm}\raggedright |
61 \begin{minipage}{12.4cm}\raggedright |
62 \large I want to teach \alert{students} with |
62 \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with |
63 theorem\\ provers (especially for inductions). |
63 theorem\\ provers (especially for inductions). |
64 \end{minipage} |
64 \end{minipage} |
65 \end{block} |
65 \end{block} |
66 \end{textblock}\pause |
66 \end{textblock}\pause |
67 |
67 |
213 \end{minipage} |
213 \end{minipage} |
214 \end{block} |
214 \end{block} |
215 \end{textblock}} |
215 \end{textblock}} |
216 \medskip |
216 \medskip |
217 |
217 |
218 \only<6->{A solution:\;\;use \smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip} |
218 \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip} |
219 |
219 |
220 \only<7->{You have to \alert{\underline{rename}} states!} |
220 \only<7->{You have to \alert{rename} states!} |
221 |
221 |
222 \end{frame}} |
222 \end{frame}} |
223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
224 *} |
224 *} |
225 |
225 |
233 \begin{center} |
233 \begin{center} |
234 \huge\bf\textcolor{gray}{in HOL} |
234 \huge\bf\textcolor{gray}{in HOL} |
235 \end{center} |
235 \end{center} |
236 |
236 |
237 \begin{itemize} |
237 \begin{itemize} |
238 \item Kozen's paper proof of Myhill-Nerode:\\ |
238 \item Kozen's ``paper'' proof of Myhill-Nerode:\\ |
239 \hspace{2cm}requires absence of \alert{inaccessible states} |
239 \hspace{2cm}requires absence of \alert{inaccessible states} |
240 \end{itemize}\bigskip\bigskip |
240 \end{itemize}\bigskip\bigskip |
241 |
241 |
242 \begin{center} |
242 \begin{center} |
243 \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} |
290 \begin{frame}[c] |
290 \begin{frame}[c] |
291 \frametitle{\LARGE The Myhill-Nerode Theorem} |
291 \frametitle{\LARGE The Myhill-Nerode Theorem} |
292 |
292 |
293 \begin{itemize} |
293 \begin{itemize} |
294 \item provides necessary and suf\!ficient conditions\\ for a language |
294 \item provides necessary and suf\!ficient conditions\\ for a language |
295 being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\medskip |
295 being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip |
296 |
|
297 \item will help with closure properties of regular languages\bigskip\pause |
|
298 |
296 |
299 \item key is the equivalence relation:\smallskip |
297 \item key is the equivalence relation:\smallskip |
300 \begin{center} |
298 \begin{center} |
301 \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} |
299 \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} |
302 \end{center} |
300 \end{center} |
338 \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}}; |
336 \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}}; |
339 \end{tikzpicture} |
337 \end{tikzpicture} |
340 \end{textblock} |
338 \end{textblock} |
341 |
339 |
342 \only<2->{% |
340 \only<2->{% |
343 \begin{textblock}{5}(9.4,7.2) |
341 \begin{textblock}{5}(9.1,7.2) |
344 \begin{tikzpicture} |
342 \begin{tikzpicture} |
345 \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm] |
343 \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm] |
346 {@{text "\<lbrakk>x\<rbrakk>"}$_{\approx_{A}}$}; |
344 {@{text "\<lbrakk>x\<rbrakk>"}$_{\approx_{A}}$}; |
347 \draw (0.9,-1.1) node {\begin{tabular}{l}equivalence class\end{tabular}}; |
345 \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}}; |
348 \end{tikzpicture} |
346 \end{tikzpicture} |
349 \end{textblock}} |
347 \end{textblock}} |
350 |
348 |
351 \only<3->{ |
349 \only<3->{ |
352 \begin{textblock}{11.9}(1.7,3) |
350 \begin{textblock}{11.9}(1.7,3) |
706 \item \ldots (set of) regular expressions after a string |
704 \item \ldots (set of) regular expressions after a string |
707 has been parsed\\[10mm] |
705 has been parsed\\[10mm] |
708 |
706 |
709 |
707 |
710 \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}} |
708 \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}} |
711 {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} |
709 {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R}}} |
712 refines \textcolor{blue}{x $\approx_{{\cal L}(\text{r})}$ y}\\[16mm]\pause |
710 refines \textcolor{blue}{x $\approx_{{\cal L}(\text{r})}$ y}\\[16mm]\pause |
713 \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause |
711 \item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause |
714 \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed. |
712 \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed. |
715 \end{itemize} |
713 \end{itemize} |
716 |
714 |
717 \only<2->{% |
715 \only<2->{% |
718 \begin{textblock}{5}(3.8,8.3) |
716 \begin{textblock}{5}(3.8,8.3) |
758 then \smath{A} is not regular. |
756 then \smath{A} is not regular. |
759 \end{minipage} |
757 \end{minipage} |
760 \end{block} |
758 \end{block} |
761 \end{minipage}\medskip\pause |
759 \end{minipage}\medskip\pause |
762 |
760 |
763 \small(\smath{A \dn \bigcup_n a^n}) |
761 \small(\smath{B \dn \bigcup_n a^n}) |
764 \end{quote} |
762 \end{quote} |
765 |
763 |
766 \end{itemize} |
764 \end{itemize} |
767 |
765 |
768 \only<2>{ |
766 \only<2>{ |