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