| author | Christian Urban <urbanc@in.tum.de> | 
| Sat, 07 Jan 2017 14:52:26 +0000 | |
| changeset 471 | e5df48ff7033 | 
| parent 445 | e7d0157f0471 | 
| child 500 | 91b888c91d73 | 
| permissions | -rw-r--r-- | 
| 25 | 1 | \documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 2 | \usepackage{../slides}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 3 | \usepackage{../graphics}
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 4 | \usepackage{../langs}
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 5 | \usepackage{../data}
 | 
| 25 | 6 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 7 | \hfuzz=220pt | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 8 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 9 | \pgfplotsset{compat=1.11}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 10 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 11 | \newcommand{\bl}[1]{\textcolor{blue}{#1}}  
 | 
| 25 | 12 | |
| 13 | % beamer stuff | |
| 445 | 14 | \renewcommand{\slidecaption}{CFL 03, King's College London}
 | 
| 25 | 15 | |
| 16 | \begin{document}
 | |
| 17 | ||
| 18 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 19 | \begin{frame}[t]
 | 
| 25 | 20 | \frametitle{%
 | 
| 21 |   \begin{tabular}{@ {}c@ {}}
 | |
| 22 | \\[-3mm] | |
| 445 | 23 | \LARGE Compilers and \\[-2mm] | 
| 25 | 24 | \LARGE Formal Languages (3)\\[3mm] | 
| 25 |   \end{tabular}}
 | |
| 26 | ||
| 27 | \normalsize | |
| 28 |   \begin{center}
 | |
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 29 |   \begin{tabular}{lp{8cm}}
 | 
| 25 | 30 | Email: & christian.urban at kcl.ac.uk\\ | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 31 | Office: & S1.27 (1st floor Strand Building)\\ | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 32 | Slides: & KEATS (also home work and coursework is there)\\ | 
| 25 | 33 |   \end{tabular}
 | 
| 34 |   \end{center}
 | |
| 35 | ||
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 36 | \end{frame}
 | 
| 445 | 37 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 38 | ||
| 39 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 40 | \begin{frame}[c]
 | |
| 41 | \frametitle{Scala Book, Exams}
 | |
| 42 | ||
| 43 | \begin{itemize}
 | |
| 44 | \item www.inf.kcl.ac.uk/~urbanc/ProgInScala2ed.pdf | |
| 45 | \item homeworks (exam 80\%) | |
| 46 | \item coursework (20\%) | |
| 47 | \end{itemize}
 | |
| 48 | ||
| 49 | \end{frame}
 | |
| 50 | %%%%%%%%%%% | |
| 25 | 51 | |
| 52 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 53 | \begin{frame}[c]
 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 54 | \frametitle{Regular Expressions}
 | 
| 25 | 55 | |
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 56 | In programming languages they are often used to recognise:\medskip | 
| 25 | 57 | |
| 58 | \begin{itemize}
 | |
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 59 | \item symbols, digits | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 60 | \item identifiers | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 61 | \item numbers (non-leading zeros) | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 62 | \item keywords | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 63 | \item comments | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 64 | \end{itemize}\bigskip
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 65 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 66 | \mbox{}\hfill\bl{\url{http://www.regexper.com}}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 67 | \end{frame}
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 68 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 69 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 70 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 71 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 72 | \begin{frame}[c]
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 73 | \frametitle{Last Week}
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 74 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 75 | Last week I showed you a regular expression matcher | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 76 | that works provably correct in all cases (we only | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 77 | started with the proving part though) | 
| 25 | 78 | |
| 79 | \begin{center}
 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 80 | \bl{$matches\,s\,r$} \;\;if and only if \;\; \bl{$s \in L(r)$}
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 81 | \end{center}\bigskip\bigskip 
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 82 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 83 | \small | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 84 | \textcolor{gray}{\mbox{}\hfill{}by Janusz Brzozowski (1964)}
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 85 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 86 | \end{frame}
 | 
| 25 | 87 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 88 | ||
| 89 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 90 | \begin{frame}[c]
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 91 | \frametitle{The Derivative of a Rexp}
 | 
| 25 | 92 | |
| 93 | \begin{center}
 | |
| 94 | \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
 | |
| 445 | 95 |   \bl{$der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
 | 
| 96 |   \bl{$der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
 | |
| 97 |   \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
 | |
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 98 |   \bl{$der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 99 |   \bl{$der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 100 |   & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 101 |   & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 102 |   \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\medskip\\
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 103 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 104 |   \bl{$\textit{ders}\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 105 |   \bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\
 | 
| 25 | 106 |   \end{tabular}
 | 
| 107 | \end{center}
 | |
| 108 | ||
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 109 | \end{frame}
 | 
| 25 | 110 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 111 | ||
| 112 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 113 | \begin{frame}[c]
 | |
| 114 | ||
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 115 | Input: string \bl{$abc$} and regular expression \bl{$r$} 
 | 
| 25 | 116 | |
| 117 | \begin{enumerate}
 | |
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 118 | \item \bl{$der\,a\,r$}
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 119 | \item \bl{$der\,b\,(der\,a\,r)$}
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 120 | \item \bl{$der\,c\,(der\,b\,(der\,a\,r))$}\bigskip\pause
 | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 121 | \item finally check whether the last regular expression can match the empty string | 
| 25 | 122 | \end{enumerate}
 | 
| 123 | ||
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 124 | \end{frame}
 | 
| 25 | 125 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 126 | ||
| 127 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 128 | \begin{frame}[c]
 | |
| 129 | ||
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 130 | We proved already | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 131 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 132 | \begin{center}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 133 | \bl{$nullable(r)$} \;if and only if\;  \bl{$[] \in L(r)$}
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 134 | \end{center}
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 135 | |
| 445 | 136 | by induction on the regular expression \bl{$r$}.\bigskip\pause
 | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 137 | |
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 138 | \begin{center}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 139 | {\huge\bf\alert{Any Questions?}}
 | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 140 | \end{center}
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 141 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 142 | \end{frame}
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 143 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 144 | |
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 145 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 146 | \begin{frame}[c]
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 147 | |
| 25 | 148 | We need to prove | 
| 149 | ||
| 150 | \begin{center}
 | |
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 151 | \bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
 | 
| 25 | 152 | \end{center}
 | 
| 153 | ||
| 445 | 154 | also by induction on the regular expression \bl{$r$}.
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 155 | \end{frame}
 | 
| 25 | 156 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 157 | ||
| 158 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 159 | \begin{frame}[c]
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 160 | \frametitle{Proofs about Rexps}
 | 
| 25 | 161 | |
| 162 | \begin{itemize}
 | |
| 445 | 163 | \item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 164 | \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 165 | holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 166 | \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 167 | holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 168 | \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 169 | holds for \bl{$r$}.
 | 
| 25 | 170 | \end{itemize}
 | 
| 171 | ||
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 172 | \end{frame}
 | 
| 25 | 173 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 174 | ||
| 175 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 176 | \begin{frame}[c]
 | |
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 177 | \frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
 | 
| 25 | 178 | |
| 179 | \begin{itemize}
 | |
| 180 | \item \bl{$P$} holds for \bl{$0$} and
 | |
| 181 | \item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
 | |
| 182 | holds for \bl{$n$}
 | |
| 183 | \end{itemize}\bigskip
 | |
| 184 | ||
| 185 | \begin{itemize}
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 186 | \item \bl{$P$} holds for \bl{$[]$} and
 | 
| 25 | 187 | \item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
 | 
| 188 | holds for \bl{$s$}
 | |
| 189 | \end{itemize}
 | |
| 190 | ||
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 191 | \end{frame}
 | 
| 25 | 192 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 193 | ||
| 194 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 195 | \begin{frame}[t]
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 196 | \frametitle{Regular Expressions}
 | 
| 25 | 197 | |
| 198 | \begin{center}
 | |
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 199 |    \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
 | 
| 445 | 200 |   \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & null\\
 | 
| 201 |          & \bl{$\mid$} & \bl{$\ONE$}        & empty string / "" / $[]$\\
 | |
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 202 |          & \bl{$\mid$} & \bl{$c$}                         & character\\
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 203 |          & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 204 |          & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 205 |          & \bl{$\mid$} & \bl{$r^*$}                   & star (zero or more)\\
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 206 |   \end{tabular}
 | 
| 25 | 207 |   \end{center}
 | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 208 | |
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 209 | How about ranges \bl{$[a\mbox{-}z]$}, \bl{$r^+$} and \bl{$\sim{}r$}? Do they increase the
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 210 | set of languages we can recognise? | 
| 25 | 211 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 212 | \end{frame}
 | 
| 25 | 213 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 214 | ||
| 215 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 216 | \begin{frame}[c]
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 217 | \frametitle{Negation of Regular Expr's}
 | 
| 25 | 218 | |
| 219 | \begin{itemize}
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 220 | \item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
 | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 221 | \item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
 | 
| 136 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 222 | \item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
 | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 223 | \item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 224 | \end{itemize}\bigskip\pause
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 225 | |
| 136 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 226 | Used often for recognising comments: | 
| 134 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 227 | |
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 228 | \[ | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 229 | \bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
 | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 230 | \] | 
| 
e3a8cf96f570
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
133diff
changeset | 231 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 232 | \end{frame}
 | 
| 25 | 233 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 234 | ||
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 235 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 236 | \begin{frame}[c]
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 237 | \frametitle{Negation}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 238 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 239 | Assume you have an alphabet consisting of the letters \bl{$a$}, \bl{$b$} and \bl{$c$} only.
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 240 | Find a (basic!) regular expression that matches all strings \emph{\alert{except}} 
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 241 | \bl{$ab$} and \bl{$ac$}!
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 242 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 243 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 244 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 245 | |
| 25 | 246 | |
| 247 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 248 | %\mode<presentation>{
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 249 | %\begin{frame}[c]
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 250 | %\frametitle{\begin{tabular}{c}Regular Exp's for Lexing\end{tabular}}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 251 | % | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 252 | %Lexing separates strings into ``words'' / components. | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 253 | % | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 254 | %\begin{itemize}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 255 | %\item Identifiers (non-empty strings of letters or digits, starting with a letter) | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 256 | %\item Numbers (non-empty sequences of digits omitting leading zeros) | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 257 | %\item Keywords (else, if, while, \ldots) | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 258 | %\item White space (a non-empty sequence of blanks, newlines and tabs) | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 259 | %\item Comments | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 260 | %\end{itemize}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 261 | % | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 262 | %\end{frame}}
 | 
| 25 | 263 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 264 | ||
| 265 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 266 | \begin{frame}[c]
 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 267 | \frametitle{Automata}
 | 
| 25 | 268 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 269 | A \alert{\bf deterministic finite automaton}, DFA, consists of:
 | 
| 25 | 270 | |
| 271 | \begin{itemize}
 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 272 | \item a set of states \bl{$Q$}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 273 | \item one of these states is the start state \bl{$q_0$}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 274 | \item some states are accepting states \bl{$F$}, and
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 275 | \item there is transition function \bl{$\delta$}\bigskip 
 | 
| 25 | 276 | |
| 277 | \small | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 278 | which takes a state as argument and a character and produces a | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 279 | new state; this function might not be everywhere defined | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 280 | \end{itemize}
 | 
| 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 281 | |
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 282 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 283 | \bl{$A(Q, q_0, F, \delta)$}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 284 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 285 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 286 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 287 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 288 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 289 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 290 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 291 | \begin{frame}[c]
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 292 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 293 | \begin{center}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 294 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 295 |                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 296 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 297 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 298 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 299 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 300 | \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 301 | \path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 302 | \path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 303 | \path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 304 | \path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 305 | \path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 306 | \path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 307 | \path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 308 | \path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 309 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 310 | \end{tikzpicture}
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 311 | \end{center}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 312 | |
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 313 | |
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 314 | \begin{itemize}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 315 | \item the start state can be an accepting state | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 316 | \item it is possible that there is no accepting state | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 317 | \item all states might be accepting (but this does not necessarily mean all strings are accepted) | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 318 | \end{itemize}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 319 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 320 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 321 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 322 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 323 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 324 | \begin{frame}[c]
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 325 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 326 | \begin{center}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 327 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 328 |                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 329 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 330 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 331 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 332 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 333 | \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 334 | \path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 335 | \path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 336 | \path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 337 | \path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 338 | \path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 339 | \path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 340 | \path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 341 | \path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 342 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 343 | \end{tikzpicture}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 344 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 345 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 346 | for this automaton \bl{$\delta$} is the function\\
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 347 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 348 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 349 | \begin{tabular}{lll}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 350 | \bl{$(q_0, a) \rightarrow q_1$} & \bl{$(q_1, a) \rightarrow q_4$} & \bl{$(q_4, a) \rightarrow q_4$}\\
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 351 | \bl{$(q_0, b) \rightarrow q_2$} & \bl{$(q_1, b) \rightarrow q_2$} & \bl{$(q_4, b) \rightarrow q_4$}\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 352 | \end{tabular}\ldots
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 353 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 354 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 355 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 356 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 357 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 358 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 359 | \begin{frame}[t]
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 360 | \frametitle{Accepting a String}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 361 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 362 | Given | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 363 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 364 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 365 | \bl{$A(Q, q_0, F, \delta)$}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 366 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 367 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 368 | you can define | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 369 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 370 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 371 | \begin{tabular}{l}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 372 | \bl{$\hat{\delta}(q, []) \dn q$}\\
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 373 | \bl{$\hat{\delta}(q, c::s) \dn \hat{\delta}(\delta(q, c), s)$}\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 374 | \end{tabular}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 375 | \end{center}\pause
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 376 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 377 | Whether a string \bl{$s$} is accepted by \bl{$A$}?
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 378 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 379 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 380 | \hspace{5mm}\bl{$\hat{\delta}(q_0, s) \in F$}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 381 | \end{center}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 382 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 383 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 384 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 385 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 386 | \begin{frame}[c]
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 387 | \frametitle{Regular Languages}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 388 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 389 | A \alert{\bf language} is a set of strings.\bigskip
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 390 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 391 | A \alert{\bf regular expression} specifies a language.\bigskip
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 392 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 393 | A language is \alert{\bf regular} iff there exists
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 394 | a regular expression that recognises all its strings.\bigskip\bigskip\pause | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 395 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 396 | not all languages are regular, e.g.~\bl{$a^nb^n$} is not
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 397 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 398 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 399 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 400 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 401 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 402 | \frametitle{Regular Languages (2)}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 403 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 404 | A language is \alert{\bf regular} iff there exists a regular
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 405 | expression that recognises all its strings.\bigskip\medskip | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 406 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 407 | or {\bf equivalently}\bigskip\medskip
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 408 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 409 | A language is \alert{\bf regular} iff there exists a
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 410 | deterministic finite automaton that recognises all its | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 411 | strings. | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 412 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 413 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 414 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 415 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 416 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 417 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 418 | \begin{frame}[c]
 | 
| 348 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 419 | \frametitle{\begin{tabular}{c}
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 420 | Non-Deterministic\\[-1mm] | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 421 |               Finite Automata\end{tabular}}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 422 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 423 | A non-deterministic finite automaton consists again of: | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 424 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 425 | \begin{itemize}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 426 | \item a finite set of states | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 427 | \item one of these states is the start state | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 428 | \item some states are accepting states, and | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 429 | \item there is transition \alert{relation}\medskip 
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 430 | \end{itemize}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 431 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 432 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 433 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 434 | \begin{tabular}{c}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 435 | \bl{$(q_1, a) \rightarrow q_2$}\\
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 436 | \bl{$(q_1, a) \rightarrow q_3$}\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 437 | \end{tabular}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 438 | \hspace{10mm}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 439 | \begin{tabular}{c}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 440 | \bl{$(q_1, \epsilon) \rightarrow q_2$}\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 441 | \end{tabular}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 442 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 443 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 444 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 445 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 446 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 447 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 448 | \begin{frame}[c]
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 449 | \frametitle{Two NFA Examples}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 450 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 451 | \small | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 452 | \begin{center}
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 453 | \begin{tabular}[t]{c@{\hspace{9mm}}c}
 | 
| 136 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 454 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 455 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 456 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 457 | \node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 458 | \node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 459 | \path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 460 | \path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 461 | \path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 462 | \path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 463 | \path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 464 | \end{tikzpicture} &
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 465 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 466 | \raisebox{20mm}{
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 467 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 468 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 469 | \node[state,initial]  (r_1)  {$r_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 470 | \node[state] (r_2) [above=of r_1] {$r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 471 | \node[state, accepting] (r_3) [right=of r_1] {$r_3$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 472 | \path[->] (r_1) edge node [below]  {\alert{$b$}} (r_3);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 473 | \path[->] (r_2) edge [bend left] node [above]  {\alert{$a$}} (r_3);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 474 | \path[->] (r_1) edge [bend left] node  [left] {\alert{$\epsilon$}} (r_2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 475 | \path[->] (r_2) edge [bend left] node  [right] {\alert{$a$}} (r_1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 476 | \end{tikzpicture}}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 477 | \end{tabular}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 478 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 479 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 480 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 481 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 482 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 483 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 484 | \begin{frame}[c]
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 485 | \frametitle{Rexp to NFA}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 486 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 487 | \begin{center}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 488 | \begin{tabular}[t]{l@{\hspace{10mm}}l}
 | 
| 445 | 489 | \raisebox{1mm}{\bl{$\ZERO$}} & 
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 490 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 491 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 492 | \end{tikzpicture}\\\\
 | 
| 445 | 493 | \raisebox{1mm}{\bl{$\ONE$}} & 
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 494 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 495 | \node[state, initial, accepting]  (q_0)  {$\mbox{}$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 496 | \end{tikzpicture}\\\\
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 497 | \raisebox{2mm}{\bl{$c$}} & 
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 498 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 499 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 500 | \node[state, accepting]  (q_1)  [right=of q_0] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 501 | \path[->] (q_0) edge node [below]  {\alert{$c$}} (q_1);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 502 | \end{tikzpicture}\\\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 503 | \end{tabular}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 504 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 505 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 506 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 507 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 508 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 509 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 510 | \begin{frame}[t]
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 511 | \frametitle{Case $r_1\cdot r_2$}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 512 | |
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 513 | \mbox{}\bigskip
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 514 | \onslide<1>{By recursion we are given two automata:\bigskip}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 515 | |
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 516 | {\centering\begin{tikzpicture}[node distance=3mm,
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 517 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 518 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 519 | \node (r_1)  [right=of q_0] {$\ldots$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 520 | \only<1>{
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 521 | \node[state, accepting]  (t_1)  [right=of r_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 522 | \node[state, accepting]  (t_2)  [above=of t_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 523 | \node[state, accepting]  (t_3)  [below=of t_1] {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 524 | \only<2>{
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 525 | \node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 526 | \node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 527 | \node[state]  (t_3)  [below=of t_1] {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 528 | \only<1>{\node[state, initial]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 529 | \only<2>{\node[state]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 530 | \node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 531 | \node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 532 | \node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 533 | \node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 534 | \only<2>{
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 535 | \path[->] (t_1) edge node [above, pos=0.3]  {\alert{$\epsilon$}} (a_0);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 536 | \path[->] (t_2) edge node [above]  {\alert{$\epsilon$}} (a_0);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 537 | \path[->] (t_3) edge node [below]  {\alert{$\epsilon$}} (a_0);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 538 | } | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 539 | \begin{pgfonlayer}{background}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 540 | \only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (r_1) (t_1) (t_2) (t_3)] {};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 541 | \only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (a_0) (b_1) (c_1) (c_2) (c_3)] {};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 542 | \only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 543 | \only<1>{\node [yshift=2mm] at (1.north) {\bl{$r_1$}};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 544 | \only<1>{\node [yshift=2mm] at (2.north) {\bl{$r_2$}};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 545 | \only<2>{\node [yshift=2mm] at (3.north) {\bl{$r_1\cdot r_2$}};}
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
139diff
changeset | 546 | \end{pgfonlayer}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 547 | \end{tikzpicture}}\bigskip\bigskip
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 548 | |
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 549 | \small | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 550 | We need to (1) change the accepting nodes of the first automaton into non-accepting nodes, and (2) connect them | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 551 | via $\epsilon$-transitions to the starting state of the second automaton. | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 552 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 553 | \end{frame}
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 554 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 555 | |
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 556 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 557 | \begin{frame}[t]
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 558 | \frametitle{Case $r_1+ r_2$}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 559 | \mbox{}\\[-10mm]
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 560 | |
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 561 | \onslide<1>{By recursion we are given two automata:\smallskip}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 562 | |
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 563 | \hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 564 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 565 | \onslide<1>{\node at (0,0)  (1)  {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 566 | \onslide<2>{\node at (0,0) [state, initial]  (1)  {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 567 | \only<1>{
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 568 | \node[state, initial]  (2)  [above right=16mm of 1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 569 | \node[state, initial]  (3)  [below right=16mm of 1] {$\mbox{}$};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 570 | \only<2>{
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 571 | \node[state]  (2)  [above right=16mm of 1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 572 | \node[state]  (3)  [below right=16mm of 1] {$\mbox{}$};}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 573 | |
| 137 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 574 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 575 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 576 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 577 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 578 | |
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 579 | \node (b)  [right=of 3] {$\ldots$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 580 | \node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 581 | \node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 582 | \node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 583 | \only<2>{
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 584 | \path[->] (1) edge node [above]  {\alert{$\epsilon$}} (2);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 585 | \path[->] (1) edge node [below]  {\alert{$\epsilon$}} (3);
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 586 | } | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 587 | \begin{pgfonlayer}{background}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 588 | \only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 589 | \only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 590 | \only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 591 | \only<1>{\node [yshift=3mm] at (1.north) {\bl{$r_1$}};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 592 | \only<1>{\node [yshift=3mm] at (2.north) {\bl{$r_2$}};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 593 | \only<2>{\node [yshift=3mm] at (3.north) {\bl{$r_1+ r_2$}};}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 594 | \end{pgfonlayer}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 595 | \end{tikzpicture}
 | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 596 | |
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 597 | \small | 
| 
69cec773736b
added pictures
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
136diff
changeset | 598 | We (1) need to introduce a new starting state and (2) connect it to the original two starting states. | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 599 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 600 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 601 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 602 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 603 | \begin{frame}[c]
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 604 | \frametitle{Case $r^*$}
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 605 | |
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 606 | \onslide<1>{By recursion we are given an automaton for $r$:\smallskip}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 607 | |
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 608 | \hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 609 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 610 | \onslide<1>{\node at (0,0)  (1)  {$\mbox{}$};}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 611 | \onslide<2->{\node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};}
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 612 | \only<1>{\node[state, initial]  (2)  [right=16mm of 1] {$\mbox{}$};}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 613 | \only<2->{\node[state]  (2)  [right=16mm of 1] {$\mbox{}$};}
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 614 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 615 | \only<1>{
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 616 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 617 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 618 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 619 | \only<2->{
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 620 | \node[state]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 621 | \node[state]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 622 | \node[state]  (a3)  [below=of a1] {$\mbox{}$};}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 623 | \only<2->{
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 624 | \path[->] (1) edge node [above]  {\alert{$\epsilon$}} (2);
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 625 | \path[->] (a1) edge [bend left=45] node [above]  {\alert{$\epsilon$}} (1);
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 626 | \path[->] (a2) edge [bend right] node [below]  {\alert{$\epsilon$}} (1);
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 627 | \path[->] (a3) edge [bend left=45] node [below]  {\alert{$\epsilon$}} (1);
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 628 | |
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 629 | } | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 630 | \begin{pgfonlayer}{background}
 | 
| 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 631 | \only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 632 | \only<2->{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};}
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 633 | \only<1>{\node [yshift=3mm] at (1.north) {\bl{$r$}};}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 634 | \only<2->{\node [yshift=3mm] at (2.north) {\bl{$r^*$}};}
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 635 | \end{pgfonlayer}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 636 | \end{tikzpicture}\bigskip
 | 
| 138 
b98a0a49c432
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
137diff
changeset | 637 | |
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 638 | \onslide<3->{
 | 
| 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 639 | Why can't we just have an epsilon transition from the accepting states to the starting state?} | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 640 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 641 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 642 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 643 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 644 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 645 | \begin{frame}[c]
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 646 | \frametitle{Subset Construction}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 647 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 648 | |
| 136 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 649 | \begin{textblock}{5}(1,1)
 | 
| 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 650 | \begin{center}
 | 
| 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 651 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 652 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 653 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 654 | \node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 655 | \node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 656 | \path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 657 | \path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 658 | \path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 659 | \path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
143diff
changeset | 660 | \path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 136 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 661 | \end{tikzpicture}
 | 
| 
cc19e6cbcb68
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
135diff
changeset | 662 | \end{center}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 663 | \end{textblock}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 664 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 665 | \begin{textblock}{11}(6.5,4.5)
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 666 | \begin{tabular}{r|cl}
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 667 | nodes \textcolor{white}{*} & $a$ & $b$\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 668 | \hline | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 669 | $\{\}$ \textcolor{white}{*} & \onslide<2->{$\{\}$} & \onslide<2->{$\{\}$}\\
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 670 | $\{0\}$ \textcolor{white}{*} & \onslide<3->{$\{0,1,2\}$} & \onslide<3->{$\{2\}$}\\
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 671 | $\{1\}$ \textcolor{white}{*} & \onslide<3->{$\{1\}$} & \onslide<3->{$\{\}$}\\
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 672 | $\{2\}$ \onslide<5->{*} & \onslide<3->{$\{\}$} & \onslide<3->{$\{2\}$}\\
 | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 673 | $\{0,1\}$ \textcolor{white}{*} &\onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 674 | $\{0,2\}$ \onslide<5->{*} &\onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 675 | $\{1,2\}$ \onslide<5->{*} & \onslide<4->{$\{1\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 676 | \onslide<5->{s:} $\{0,1,2\}$ \onslide<5->{*}& \onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 677 | \end{tabular}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 678 | \end{textblock}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 679 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 680 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 681 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 682 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 683 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 684 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 685 | \frametitle{The Result}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 686 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 687 | \footnotesize | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 688 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 689 | \begin{tikzpicture}[scale=0.5,>=stealth',very thick,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 690 |                     every state/.style={minimum size=0pt,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 691 | draw=blue!50,very thick,fill=blue!20}, | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 692 | baseline=0mm] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 693 | \node[state,initial,accepting]  (q012)  {$\{0,1,2\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 694 | \node[state,accepting] (q02) [right=of q012] {$\{0,2\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 695 | \node[state] (q01) [above=of q02] {$\{0,1\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 696 | \node[state,accepting] (q12) [below=of q02] {$\{1,2\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 697 | \node[state] (q0) [right=2cm of q01] {$\{0\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 698 | \node[state] (q1) [right=2.5cm of q02] {$\{1\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 699 | \node[state,accepting] (q2) [right=1.5cm of q12] {$\{2\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 700 | \node[state] (qn) [right=of q1] {$\{\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 701 | |
| 348 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 702 | \path[->] (q012) edge [loop below] node  {\alert{$a$}} ();
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 703 | \path[->] (q012) edge node [above]  {\alert{$b$}} (q2);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 704 | \path[->] (q12) edge [bend left] node [below,pos=0.4]  {\alert{$a$}} (q1);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 705 | \path[->] (q12) edge node [below]  {\alert{$b$}} (q2);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 706 | \path[->] (q02) edge node [above]  {\alert{$a$}} (q012);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 707 | \path[->] (q02) edge [bend left] node [above, pos=0.8]  {\alert{$b$}} (q2);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 708 | \path[->] (q01) edge node [below]  {\alert{$a$}} (q012);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 709 | \path[->] (q01) edge [bend left] node [above]  {\alert{$b$}} (q2);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 710 | \path[->] (q0) edge node [below]  {\alert{$a$}} (q012);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 711 | \path[->] (q0) edge node [right, pos=0.2]  {\alert{$b$}} (q2);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 712 | \path[->] (q1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 713 | \path[->] (q1) edge node [above]  {\alert{$b$}} (qn);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 714 | \path[->] (q2) edge [loop right] node  {\alert{$b$}} ();
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 715 | \path[->] (q2) edge node [below]  {\alert{$a$}} (qn);
 | 
| 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 716 | \path[->] (qn) edge [loop above] node  {$\alert{a},\alert{b}$} ();
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 717 | \end{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 718 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 719 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 720 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 721 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 722 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 723 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 724 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 725 | \begin{frame}[c]
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 726 | \frametitle{Removing Dead States}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 727 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 728 | \footnotesize | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 729 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 730 | \begin{tabular}{ll}
 | 
| 445 | 731 | DFA: & (original) NFA:\\ | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 732 | \raisebox{10mm}{%
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 733 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 734 |                     every state/.style={minimum size=0pt,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 735 | draw=blue!50,very thick,fill=blue!20}] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 736 | \node[state,initial,accepting]  (q012)  {$\{0,1,2\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 737 | \node[state,accepting] (q2) [right=of q012] {$\{2\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 738 | \node[state] (qn) [right=of q2] {$\{\}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 739 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 740 | \path[->] (q012) edge [loop below] node  {\alert{$a$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 741 | \path[->] (q012) edge node [above]  {\alert{$b$}} (q2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 742 | \path[->] (q2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 743 | \path[->] (q2) edge node [below]  {\alert{$a$}} (qn);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 744 | \path[->] (qn) edge [loop above] node | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 745 |    {$\alert{a},\alert{b}$} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 746 | \end{tikzpicture}}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 747 | & | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 748 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 749 |                     every state/.style={minimum size=0pt,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 750 | draw=blue!50,very thick,fill=blue!20},] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 751 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 752 | \node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 753 | \node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 754 | \path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 755 | \path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 756 | \path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 757 | \path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 758 | \path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 759 | \end{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 760 | \end{tabular}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 761 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 762 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 763 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 764 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 765 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 766 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 767 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 768 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 769 | \begin{frame}[c]
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 770 | \frametitle{Regexps and Automata}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 771 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 772 | \begin{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 773 | \begin{tikzpicture}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 774 | \node (rexp)  {\bl{\bf Regexps}};
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 775 | \node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 776 | \node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 777 | \onslide<2->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 778 | \path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 779 | \path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 780 | \onslide<2->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 781 | \end{tikzpicture}\\
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 782 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 783 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 784 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 785 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 786 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 787 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 788 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 789 | \frametitle{DFA Minimisation}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 790 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 791 | \begin{enumerate}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 792 | \item Take all pairs \bl{$(q, p)$} with \bl{$q \not= p$}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 793 | \item Mark all pairs that accepting and non-accepting states | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 794 | \item For  all unmarked pairs \bl{$(q, p)$} and all characters \bl{$c$} test whether
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 795 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 796 | \bl{$(\delta(q, c), \delta(p,c))$}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 797 | \end{center} 
 | 
| 348 
31e89128ccd2
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
346diff
changeset | 798 | are marked. If yes in at least one case, then also mark \bl{$(q, p)$}.
 | 
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 799 | \item Repeat last step until no change. | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 800 | \item All unmarked pairs can be merged. | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 801 | \end{enumerate}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 802 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 803 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 804 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 805 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 806 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 807 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 808 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 809 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 810 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 811 |                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 812 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 813 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 814 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 815 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 816 | \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 817 | \path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 818 | \path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 819 | \path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 820 | \path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 821 | \path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 822 | \path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 823 | \path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 824 | \path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 825 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 826 | \end{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 827 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 828 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 829 | \mbox{}\\[-20mm]\mbox{}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 830 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 831 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 832 | \begin{tikzpicture}[scale=0.8,line width=0.8mm]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 833 | \draw (0,0) -- (4,0); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 834 | \draw (0,1) -- (4,1); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 835 | \draw (0,2) -- (3,2); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 836 | \draw (0,3) -- (2,3); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 837 | \draw (0,4) -- (1,4); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 838 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 839 | \draw (0,0) -- (0, 4); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 840 | \draw (1,0) -- (1, 4); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 841 | \draw (2,0) -- (2, 3); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 842 | \draw (3,0) -- (3, 2); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 843 | \draw (4,0) -- (4, 1); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 844 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 845 | \draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 846 | \draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 847 | \draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 848 | \draw (3.5,-0.5) node {$q_3$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 849 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 850 | \draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 851 | \draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 852 | \draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 853 | \draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 854 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 855 | \draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 856 | \draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 857 | \draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 858 | \draw (3.5,0.5) node {\large$\star$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 859 | \end{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 860 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 861 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 862 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 863 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 864 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 865 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 866 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 867 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 868 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 869 | \begin{tabular}{@{\hspace{-8mm}}cc@{}}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 870 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 871 |                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 872 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 873 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 874 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 875 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 876 | \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 877 | \path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 878 | \path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 879 | \path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 880 | \path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 881 | \path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 882 | \path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 883 | \path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 884 | \path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 885 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 886 | \end{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 887 | & | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 888 | \raisebox{9mm}{\begin{tikzpicture}[scale=0.6,line width=0.8mm]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 889 | \draw (0,0) -- (4,0); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 890 | \draw (0,1) -- (4,1); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 891 | \draw (0,2) -- (3,2); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 892 | \draw (0,3) -- (2,3); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 893 | \draw (0,4) -- (1,4); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 894 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 895 | \draw (0,0) -- (0, 4); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 896 | \draw (1,0) -- (1, 4); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 897 | \draw (2,0) -- (2, 3); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 898 | \draw (3,0) -- (3, 2); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 899 | \draw (4,0) -- (4, 1); | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 900 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 901 | \draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 902 | \draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 903 | \draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 904 | \draw (3.5,-0.5) node {$q_3$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 905 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 906 | \draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 907 | \draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 908 | \draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 909 | \draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 910 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 911 | \draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 912 | \draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 913 | \draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 914 | \draw (3.5,0.5) node {\large$\star$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 915 | \draw (0.5,1.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 916 | \draw (2.5,1.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 917 | \draw (0.5,3.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 918 | \draw (1.5,2.5) node {\large$\star$}; 
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 919 | \end{tikzpicture}}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 920 | \end{tabular}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 921 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 922 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 923 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 924 | \mbox{}\\[-20mm]\mbox{}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 925 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 926 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 927 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 928 |                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 929 | \node[state,initial]  (q_02)  {$q_{0, 2}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 930 | \node[state] (q_13) [right=of q_02] {$q_{1, 3}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 931 | \node[state, accepting] (q_4) [right=of q_13] {$q_{4\phantom{,0}}$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 932 | \path[->] (q_02) edge [bend left] node [above]  {\alert{$a$}} (q_13);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 933 | \path[->] (q_13) edge [bend left] node [below]  {\alert{$b$}} (q_02);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 934 | \path[->] (q_02) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 935 | \path[->] (q_13) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 936 | \path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 937 | \end{tikzpicture}\\
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 938 | minimal automaton | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 939 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 940 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 941 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 942 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 943 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 944 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 945 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 946 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 947 | \frametitle{Alternatives}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 948 | \mbox{}\\[-17mm]\mbox{}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 949 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 950 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 951 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 952 |                     every state/.style={minimum size=0pt,
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 953 | inner sep=2pt,draw=blue!50,very thick,fill=blue!20}] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 954 | \only<1>{\node[state,initial]  (q_0)  {$q_0$};}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 955 | \only<2->{\node[state,accepting]  (q_0)  {$q_0$};}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 956 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 957 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 958 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 959 | \only<1>{\node[state, accepting] (q_4) [right=of q_1] {$q_4$};}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 960 | \only<2->{\node[state, initial right] (q_4) [right=of q_1] {$q_4$};}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 961 | \only<1-2>{
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 962 | \path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 963 | \path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 964 | \path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 965 | \path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 966 | \path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 967 | \path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 968 | \path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 969 | \path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 970 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 971 | \only<3->{
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 972 | \path[<-] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 973 | \path[<-] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 974 | \path[<-] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 975 | \path[<-] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 976 | \path[<-] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 977 | \path[<-] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 978 | \path[<-] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 979 | \path[<-] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 980 | \path[<-] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 981 | \end{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 982 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 983 | \mbox{}\\[-18mm]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 984 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 985 | \small | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 986 | \begin{itemize}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 987 | \item<2-> exchange initial / accepting states\\[-2mm] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 988 | \item<3-> reverse all edges\\[-2mm] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 989 | \item<4-> subset construction $\Rightarrow$ DFA\\[-2mm] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 990 | \item<5-> remove dead states\\[-2mm] | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 991 | \item<6-> repeat once more | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 992 |           \onslide<6->{$\Rightarrow$ minimal DFA}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 993 | \end{itemize}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 994 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 995 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 996 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 997 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 998 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 999 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1000 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1001 | \frametitle{Regexps and Automata}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1002 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1003 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1004 | \begin{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1005 | \node (rexp)  {\bl{\bf Regexps}};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1006 | \node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1007 | \node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1008 | \onslide<1->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1009 | \path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1010 | \path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1011 | \onslide<1->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1012 | \onslide<2->{\path[->, red, line width=2mm] (dfa) edge [bend left=45] (rexp);}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1013 | \end{tikzpicture}\\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1014 | \end{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1015 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1016 | \end{frame}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1017 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1018 | |
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1019 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1020 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1021 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1022 | \begin{frame}<2>[c]
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1023 | \frametitle{DFA to Rexp}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1024 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1025 | \begin{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1026 | \begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1027 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1028 |   \only<1>{\node[state, initial]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1029 |   \only<2->{\node[state, initial,accepting]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1030 |   \only<1>{\node[state]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1031 |   \only<2->{\node[state,accepting]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1032 |   \only<1>{\node[state, accepting] (q2) at ( 2,1) {$q_2$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1033 |   \only<2->{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1034 |   \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1035 |                   (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1036 |                   (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1037 |                   (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1038 |                   (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1039 |                   (q0) edge [loop below] node {\alert{$b$}} ()
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1040 | ; | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1041 | \end{tikzpicture}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1042 | \end{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1043 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1044 | \onslide<3>{How to get from a DFA to a regular expression?}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1045 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1046 | \end{frame}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1047 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1048 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1049 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1050 | \begin{frame}[c]
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1051 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1052 | \begin{center}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1053 | \begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1054 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1055 |   \only<1->{\node[state, initial]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1056 |   \only<1->{\node[state]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1057 |   \only<1->{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1058 |   \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1059 |                   (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1060 |                   (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1061 |                   (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1062 |                   (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1063 |                   (q0) edge [loop below] node {\alert{$b$}} ()
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1064 | ; | 
| 139 
6e7c3db9023d
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
138diff
changeset | 1065 | \end{tikzpicture}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1066 | \end{center}\pause\bigskip
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1067 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1068 | \onslide<2->{
 | 
| 445 | 1069 | You know how to solve since school days, no? | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1070 | \begin{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1071 | \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1072 | \bl{$q_0$} & \bl{$=$} & \bl{$2\, q_0 + 3 \,q_1 +  4\, q_2$}\\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1073 | \bl{$q_1$} & \bl{$=$} & \bl{$2 \,q_0 + 3\, q_1 + 1\, q_2$}\\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1074 | \bl{$q_2$} & \bl{$=$} & \bl{$1\, q_0 + 5\, q_1 + 2\, q_2$}\\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1075 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1076 | \end{tabular}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1077 | \end{center}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1078 | } | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1079 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1080 | \end{frame}
 | 
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1081 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1082 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1083 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1084 | \begin{frame}[c]
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1085 | |
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1086 | \begin{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1087 | \begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1088 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1089 |   \only<1->{\node[state, initial]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1090 |   \only<1->{\node[state]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1091 |   \only<1->{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1092 |   \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1093 |                   (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1094 |                   (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1095 |                   (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1096 |                   (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1097 |                   (q0) edge [loop below] node {\alert{$b$}} ()
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1098 | ; | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1099 | \end{tikzpicture}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1100 | \end{center}\bigskip
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1101 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1102 | \onslide<2->{
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1103 | \begin{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1104 | \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 | 
| 445 | 1105 | \bl{$q_0$} & \bl{$=$} & \bl{$\ONE + q_0\,b + q_1\,b +  q_2\,b$}\\
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1106 | \bl{$q_1$} & \bl{$=$} & \bl{$q_0\,a$}\\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1107 | \bl{$q_2$} & \bl{$=$} & \bl{$q_1\,a + q_2\,a$}\\
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1108 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1109 | \end{tabular}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1110 | \end{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1111 | } | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1112 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1113 | \onslide<3->{
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1114 | Arden's Lemma: | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1115 | \begin{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1116 | If \bl{$q = q\,r + s$}\; then\; \bl{$q = s\, r^*$}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1117 | \end{center}
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1118 | } | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1119 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1120 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1121 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1122 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1123 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1124 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1125 | \frametitle{Regexps and Automata}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1126 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1127 | \begin{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1128 | \begin{tikzpicture}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1129 | \node (rexp)  {\bl{\bf Regexps}};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1130 | \node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1131 | \node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1132 | \onslide<1->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1133 | \path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1134 | \path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1135 | \onslide<1->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1136 | \onslide<1->{\path[->, red, line width=2mm] (dfa) edge [bend left=45] (rexp);}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1137 | \end{tikzpicture}\\
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1138 | \end{center}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1139 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1140 | \end{frame}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1141 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1142 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1143 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1144 | \begin{frame}[c]
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1145 | \frametitle{Regular Languages (3)}
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1146 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1147 | A language is \alert{\bf regular} iff there exists a regular
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1148 | expression that recognises all its strings.\bigskip\medskip | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1149 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1150 | or {\bf equivalently}\bigskip\medskip
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1151 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1152 | A language is \alert{\bf regular} iff there exists a
 | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1153 | deterministic finite automaton that recognises all its | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1154 | strings.\bigskip\medskip\pause | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1155 | |
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1156 | Why is every finite set of strings a regular language? | 
| 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1157 | \end{frame}
 | 
| 265 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1158 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1159 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1160 | |
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1161 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1162 | \begin{frame}[c]
 | 
| 
332fbe9c91ab
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 1163 | |
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1164 | Given the function | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1165 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1166 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1167 | \bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
 | 
| 445 | 1168 | $rev(\ZERO)$ & $\dn$ & $\ZERO$\\ | 
| 1169 | $rev(\ONE)$ & $\dn$ & $\ONE$\\ | |
| 135 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1170 | $rev(c)$ & $\dn$ & $c$\\ | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1171 | $rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\ | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1172 | $rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\ | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1173 | $rev(r^*)$ & $\dn$ & $rev(r)^*$\\ | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1174 | \end{tabular}}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1175 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1176 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1177 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1178 | and the set | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1179 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1180 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1181 | \bl{$Rev\,A \dn \{s^{-1} \;|\; s \in A\}$}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1182 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1183 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1184 | prove whether | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1185 | |
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1186 | \begin{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1187 | \bl{$L(rev(r)) = Rev (L(r))$}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1188 | \end{center}
 | 
| 
72b686e1c974
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
134diff
changeset | 1189 | |
| 346 
a98794b11ac4
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
265diff
changeset | 1190 | \end{frame}
 | 
| 133 
09efdf5cf07c
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 1191 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 25 | 1192 | |
| 1193 | ||
| 1194 | \end{document}
 | |
| 1195 | ||
| 1196 | %%% Local Variables: | |
| 1197 | %%% mode: latex | |
| 1198 | %%% TeX-master: t | |
| 1199 | %%% End: | |
| 1200 |