slides/slides03.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 16 Oct 2013 02:07:02 +0100
changeset 145 920f675b4ed1
parent 143 e3fd4c5995ef
child 215 828303e8e4af
permissions -rw-r--r--
added
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}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     2
\usepackage{beamerthemeplaincu}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     3
%%\usepackage[T1]{fontenc}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
\usepackage[latin1]{inputenc}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
\usepackage{mathpartir}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
\usepackage[absolute,overlay]{textpos}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
\usepackage{ifthen}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
\usepackage{tikz}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
\usepackage{pgf}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
\usepackage{calc} 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
\usepackage{ulem}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
\usepackage{courier}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
\usepackage{listings}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
\renewcommand{\uline}[1]{#1}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
\usetikzlibrary{arrows}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
\usetikzlibrary{automata}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
\usetikzlibrary{shapes}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
\usetikzlibrary{shadows}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
\usetikzlibrary{positioning}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
\usetikzlibrary{calc}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
    21
\usetikzlibrary{fit}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
    22
\usetikzlibrary{backgrounds}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
\usepackage{graphicx} 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
\definecolor{javared}{rgb}{0.6,0,0} % for strings
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    29
\makeatletter
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    30
\lst@CCPutMacro\lst@ProcessOther {"2D}{\lst@ttfamily{-{}}{-{}}}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    31
\@empty\z@\@empty
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    32
\makeatother
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
\lstset{language=Java,
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    35
	basicstyle=\consolas,
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
	stringstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
	commentstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
	numbers=left,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
	numberstyle=\tiny\color{black},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
	stepnumber=1,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
	numbersep=10pt,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
	tabsize=2,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
	showspaces=false,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
	showstringspaces=false}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
\lstdefinelanguage{scala}{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
  morekeywords={abstract,case,catch,class,def,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
    do,else,extends,false,final,finally,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
    for,if,implicit,import,match,mixin,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
    new,null,object,override,package,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
    private,protected,requires,return,sealed,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
    super,this,throw,trait,true,try,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
    type,val,var,while,with,yield},
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    56
  otherkeywords={=>,<-,<\%,<:,>:,\#,@,->},
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
  sensitive=true,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
  morecomment=[l]{//},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
  morecomment=[n]{/*}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
  morestring=[b]",
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
  morestring=[b]',
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
  morestring=[b]"""
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
\lstset{language=Scala,
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    66
	basicstyle=\consolas,
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
	stringstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
	commentstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
	numbers=left,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
	numberstyle=\tiny\color{black},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
	stepnumber=1,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
	numbersep=10pt,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
	tabsize=2,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
	showspaces=false,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
	showstringspaces=false}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    79
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
% beamer stuff 
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    81
\renewcommand{\slidecaption}{AFL 03, King's College London, 9.~October 2013}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
\begin{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
\begin{frame}<1>[t]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
\frametitle{%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
  \begin{tabular}{@ {}c@ {}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
  \\[-3mm]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
  \LARGE Automata and \\[-2mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
  \LARGE Formal Languages (3)\\[3mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
  \end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
  %\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
  %\includegraphics[scale=0.3]{pics/ante1.jpg}\hspace{5mm}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
  %\includegraphics[scale=0.31]{pics/ante2.jpg}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
  %\footnotesize\textcolor{gray}{Antikythera automaton, 100 BC (Archimedes?)}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
  %\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
\normalsize
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
  \begin{center}
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   105
  \begin{tabular}{lp{8cm}}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
  Email:  & christian.urban at kcl.ac.uk\\
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   107
  Office: & S1.27 (1st floor Strand Building)\\
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   108
  Slides: & KEATS (also home work and coursework is there)\\
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
  \end{center}
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
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
\begin{frame}[c]
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   119
\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   121
In programming languages they are often used to recognise:\medskip
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
\begin{itemize}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   124
\item symbols, digits
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   125
\item identifiers
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   126
\item numbers (non-leading zeros)
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   127
\item keywords
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   128
\item comments
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   129
\end{itemize}\bigskip
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   130
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   131
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   132
\mbox{}\hfill\bl{\url{http://www.regexper.com}}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   133
\end{frame}}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   134
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   135
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   136
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   137
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   138
\mode<presentation>{
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   139
\begin{frame}[c]
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   140
\frametitle{\begin{tabular}{c}Last Week\end{tabular}}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   141
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   142
Last week I showed you a regular expression matcher 
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   143
which works provably correctly in all cases.
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
\begin{center}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   146
\bl{$matcher\,r\,s$} \;\;if and only if \;\; \bl{$s \in L(r)$}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   147
\end{center}\bigskip\bigskip 
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   148
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   149
\small
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   150
\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
   151
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   163
  \bl{$der\, c\, (\varnothing)$}      & \bl{$\dn$} & \bl{$\varnothing$} & \\
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   164
  \bl{$der\, c\, (\epsilon)$}           & \bl{$\dn$} & \bl{$\varnothing$} & \\
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   165
  \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   166
  \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
   167
  \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
   168
  & & \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
   169
  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   170
  \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\smallskip\\
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   171
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   172
  \bl{$der\!s\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   173
  \bl{$der\!s\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$der\!s\,s\,(der\,c\,r)$} & \\
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   185
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   186
To see what is going on, define
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
\begin{center}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   189
\bl{$Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   190
\end{center}\bigskip\bigskip
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   192
\small
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   193
For \bl{$A = \{"f\!oo", "bar", "f\!rak"\}$} then
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
\begin{center}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   196
\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   197
$Der\,f\,A$ & $=$ & $\{"oo", "rak"\}$\\
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   198
$Der\,b\,A$ & $=$ &  $\{"ar"\}$\\  
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   199
$Der\,a\,A$ & $=$ & $\varnothing$\\
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   200
\end{tabular}}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
\end{center}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   202
 
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
\frametitle{\begin{tabular}{c}The Idea of the Algorithm\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   213
If we want to recognise the string \bl{$"abc"$} with regular expression \bl{$r$}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
then\medskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
\begin{enumerate}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   217
\item \bl{$Der\,a\,(L(r))$}\pause
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   218
\item \bl{$Der\,b\,(Der\,a\,(L(r)))$}\pause
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   219
\item \bl{$Der\,c\,(Der\,b\,(Der\,a\,(L(r))))$}\pause
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   220
\item finally we test whether the empty string is in this set\pause\medskip
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
\end{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   223
The matching algorithm works similarly, just over regular expression instead of sets.
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   232
Input: string \bl{$"abc"$} and regular expression \bl{$r$} 
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   234
\begin{enumerate}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   235
\item \bl{$der\,a\,r$}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   236
\item \bl{$der\,b\,(der\,a\,r)$}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   237
\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
   238
\item finally check whether the last regular expression can match the empty string
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
\end{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   245
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   246
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   247
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   248
We proved already
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   249
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   250
\begin{center}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   251
\bl{$nullable(r)$} \;if and only if\;  \bl{$"" \in L(r)$}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   252
\end{center}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   253
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   254
by induction on the regular expression.\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   255
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   256
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   257
\huge\bf \alert{Any Questions?}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   258
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   259
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   260
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   261
\end{frame}}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   262
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   263
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   264
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   265
\mode<presentation>{
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   266
\begin{frame}[c]
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   267
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   268
We need to prove
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   269
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
\begin{center}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   271
\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   273
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   274
by induction on the regular expression.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   275
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   276
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   279
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   281
\begin{frame}[c]
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   282
\frametitle{\begin{tabular}{c}Proofs about Rexps\end{tabular}}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   283
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   284
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   286
\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
   287
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
   288
\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
   289
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
   290
\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
   291
holds for \bl{$r$}.
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   292
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   293
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   294
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   295
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   296
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   297
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   298
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   299
\begin{frame}[c]
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   300
\frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   301
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   302
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   303
\item \bl{$P$} holds for \bl{$0$} and
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   304
\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
holds for \bl{$n$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
\end{itemize}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
\begin{itemize}
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   309
\item \bl{$P$} holds for \bl{$""$} and
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   311
holds for \bl{$s$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
\frametitle{\begin{tabular}{c}Languages\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
A \alert{language} is a set of strings.\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   326
A \alert{regular expression} specifies a language.\bigskip
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
A language is \alert{regular} iff there exists
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
a regular expression that recognises all its strings.\bigskip\bigskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   331
\textcolor{gray}{not all languages are regular, e.g.~\bl{$a^nb^n$}.}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
\begin{frame}[t]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
\begin{center}
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   341
   \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   342
  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}  & null\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   343
         & \bl{$\mid$} & \bl{$\epsilon$}        & empty string / "" / $[]$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   344
         & \bl{$\mid$} & \bl{$c$}                         & character\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   345
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   346
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   347
         & \bl{$\mid$} & \bl{$r^*$}                   & star (zero or more)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   348
  \end{tabular}
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
  \end{center}
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   350
  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   351
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
   352
set of languages we can recognise?
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   355
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   358
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
\frametitle{\begin{tabular}{c}Negation of Regular Expr's\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
\begin{itemize}
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   363
\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{r} cannot recognise)\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   364
\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
   365
\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
   366
\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
   367
\end{itemize}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   368
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   369
Used often for recognising comments:
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   370
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   371
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   372
\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
   373
\]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
   374
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   377
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   378
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   379
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   380
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   381
\begin{frame}[c]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   382
\frametitle{\begin{tabular}{c}Negation\end{tabular}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   383
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   384
Assume you have an alphabet consisting of the letters \bl{a}, \bl{b} and \bl{c} only.
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   385
Find a regular expression that matches all strings \emph{except} \bl{ab} and \bl{ac}.
135
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
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   388
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   389
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   390
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   391
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   393
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
\frametitle{\begin{tabular}{c}Regular Exp's for Lexing\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
Lexing separates strings into ``words'' / components.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   399
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   400
\item Identifiers (non-empty strings of letters or digits, starting with a letter)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
\item Numbers (non-empty sequences of digits omitting leading zeros)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
\item Keywords (else, if, while, \ldots)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
\item White space (a non-empty sequence of blanks, newlines and tabs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
\item Comments
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   409
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   412
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
\frametitle{\begin{tabular}{c}Automata\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   415
A \alert{deterministic finite automaton} consists of:
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
\item a set of states
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
\item one of these states is the start state
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   420
\item some states are accepting states, and
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   421
\item there is transition function\medskip 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   422
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
\small
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   424
which takes a state as argument and a character and produces a new state\smallskip\\
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   425
this function might not be everywhere defined
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   426
\end{itemize}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   427
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   428
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   429
\bl{$A(Q, q_0, F, \delta)$}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   430
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   431
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   432
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   433
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   434
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   435
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   436
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   437
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   438
\begin{frame}[c]
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
\begin{center}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   441
\begin{tikzpicture}[>=stealth',very thick,auto,
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   442
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   443
\node[state,initial]  (q_0)  {$q_0$};
\node[state] (q_1) [right=of q_0] {$q_1$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   444
\node[state] (q_2) [below right=of q_0] {$q_2$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   445
\node[state] (q_3) [right=of q_2] {$q_3$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   446
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   447
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   448
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   449
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   450
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   451
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   452
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   453
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   454
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   455
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   456
\end{tikzpicture}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   457
\end{center}\pause
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   458
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   459
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   460
\begin{itemize}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   461
\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
   462
\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
   463
\item all states might be accepting (but this does not necessarily mean all strings are accepted)
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   464
\end{itemize}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   465
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   466
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   467
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   468
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   469
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   470
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   471
\begin{frame}[c]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   472
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   473
\begin{center}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   474
\begin{tikzpicture}[>=stealth',very thick,auto,
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   475
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   476
\node[state,initial]  (q_0)  {$q_0$};
\node[state] (q_1) [right=of q_0] {$q_1$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   477
\node[state] (q_2) [below right=of q_0] {$q_2$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   478
\node[state] (q_3) [right=of q_2] {$q_3$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   479
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   480
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   481
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   482
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   483
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   484
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   485
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   486
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   487
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   488
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   489
\end{tikzpicture}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   490
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   491
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   492
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
   493
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   494
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   495
\begin{tabular}{lll}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   496
\bl{$(q_0, a) \rightarrow q_1$} & \bl{$(q_1, a) \rightarrow q_4$} & \bl{$(q_4, a) \rightarrow q_4$}\\
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   497
\bl{$(q_0, b) \rightarrow q_2$} & \bl{$(q_1, b) \rightarrow q_2$} & \bl{$(q_4, b) \rightarrow q_4$}\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   498
\end{tabular}\ldots
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   499
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   500
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   501
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   502
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   503
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   504
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   505
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   506
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   507
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   508
\begin{frame}[t]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   509
\frametitle{\begin{tabular}{c}Accepting a String\end{tabular}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   510
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   511
Given
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
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   514
\bl{$A(Q, q_0, F, \delta)$}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   515
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   516
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   517
you can define
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}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   520
\begin{tabular}{l}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   521
\bl{$\hat{\delta}(q, \texttt{""}) \dn q$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   522
\bl{$\hat{\delta}(q, c::s) \dn \hat{\delta}(\delta(q, c), s)$}\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   523
\end{tabular}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   524
\end{center}\pause
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   525
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   526
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
   527
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   528
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   529
\hspace{5mm}\bl{$\hat{\delta}(q_0, s) \in F$}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   530
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   531
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   532
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   533
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   534
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   535
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   536
\begin{frame}[c]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   537
\frametitle{\begin{tabular}{c}Non-Deterministic\\[-1mm] Finite Automata\end{tabular}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   538
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   539
A non-deterministic finite automaton consists again of:
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
\begin{itemize}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   542
\item a finite set of states
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   543
\item one of these states is the start state
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   544
\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
   545
\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
   546
\end{itemize}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   547
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   548
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   549
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   550
\begin{tabular}{c}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   551
\bl{$(q_1, a) \rightarrow q_2$}\\
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   552
\bl{$(q_1, a) \rightarrow q_3$}\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   553
\end{tabular}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   554
\hspace{10mm}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   555
\begin{tabular}{c}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   556
\bl{$(q_1, \epsilon) \rightarrow q_2$}\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   557
\end{tabular}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   558
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   559
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   560
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   561
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   562
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   563
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   564
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   565
\begin{frame}[c]
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   566
\frametitle{Two NFA Examples}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   567
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   568
\begin{center}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   569
\begin{tabular}[t]{c@{\hspace{9mm}}c}
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   570
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   571
                             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: 135
diff changeset
   572
\node[state,initial]  (q_0)  {$q_0$};
\node[state] (q_1) [above=of q_0] {$q_1$};
\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   573
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   574
\path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
\path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   575
\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
   576
\end{tikzpicture} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   577
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   578
\raisebox{20mm}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   579
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   580
                             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
   581
\node[state,initial]  (r_1)  {$r_1$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   582
\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
   583
\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
   584
\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
   585
\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
   586
\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
   587
\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
   588
\end{tikzpicture}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   589
\end{tabular}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   590
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   591
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   592
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   593
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   594
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   595
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   596
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   597
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   598
\begin{frame}[c]
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   599
\frametitle{Rexp to NFA}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   600
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   601
\begin{center}
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   602
\begin{tabular}[t]{l@{\hspace{10mm}}l}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   603
\raisebox{1mm}{\bl{$\varnothing$}} & 
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   604
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   605
\node[state, initial]  (q_0)  {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   606
\end{tikzpicture}\\\\
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   607
\raisebox{1mm}{\bl{$\epsilon$}} & 
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   608
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   609
\node[state, initial, accepting]  (q_0)  {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   610
\end{tikzpicture}\\\\
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   611
\raisebox{2mm}{\bl{$c$}} & 
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   612
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   613
\node[state, initial]  (q_0)  {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   614
\node[state, accepting]  (q_1)  [right=of q_0] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   615
\path[->] (q_0) edge node [below]  {\alert{$c$}} (q_1);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   616
\end{tikzpicture}\\\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   617
\end{tabular}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   618
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   619
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   620
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   621
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   622
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   623
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   624
\mode<presentation>{
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   625
\begin{frame}[t]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   626
\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
   627
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   628
\mbox{}\bigskip
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   629
\onslide<1>{By recursion we are given two automata:\bigskip}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   630
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   631
{\centering\begin{tikzpicture}[node distance=3mm,
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   632
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   633
\node[state, initial]  (q_0)  {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   634
\node (r_1)  [right=of q_0] {$\ldots$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   635
\only<1>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   636
\node[state, accepting]  (t_1)  [right=of r_1] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   637
\node[state, accepting]  (t_2)  [above=of t_1] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   638
\node[state, accepting]  (t_3)  [below=of t_1] {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   639
\only<2>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   640
\node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   641
\node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   642
\node[state]  (t_3)  [below=of t_1] {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   643
\only<1>{\node[state, initial]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   644
\only<2>{\node[state]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   645
\node (b_1)  [right=of a_0] {$\ldots$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   646
\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
   647
\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
   648
\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
   649
\only<2>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   650
\path[->] (t_1) edge node [above, pos=0.3]  {\alert{$\epsilon$}} (a_0);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   651
\path[->] (t_2) edge node [above]  {\alert{$\epsilon$}} (a_0);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   652
\path[->] (t_3) edge node [below]  {\alert{$\epsilon$}} (a_0);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   653
}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   654
\begin{pgfonlayer}{background}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   655
\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (r_1) (t_1) (t_2) (t_3)] {};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   656
\only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (a_0) (b_1) (c_1) (c_2) (c_3)] {};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   657
\only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   658
\only<1>{\node [yshift=2mm] at (1.north) {\bl{$r_1$}};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   659
\only<1>{\node [yshift=2mm] at (2.north) {\bl{$r_2$}};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   660
\only<2>{\node [yshift=2mm] at (3.north) {\bl{$r_1\cdot r_2$}};}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 139
diff changeset
   661
\end{pgfonlayer}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   662
\end{tikzpicture}}\bigskip\bigskip
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   663
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   664
\small
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   665
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
   666
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
   667
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   668
\end{frame}}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   669
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   670
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   671
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   672
\mode<presentation>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   673
\begin{frame}[t]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   674
\frametitle{Case $r_1+ r_2$}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   675
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   676
\onslide<1>{By recursion we are given two automata:\smallskip}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   677
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   678
\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   679
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   680
\onslide<1>{\node at (0,0)  (1)  {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   681
\onslide<2>{\node at (0,0) [state, initial]  (1)  {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   682
\only<1>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   683
\node[state, initial]  (2)  [above right=16mm of 1] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   684
\node[state, initial]  (3)  [below right=16mm of 1] {$\mbox{}$};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   685
\only<2>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   686
\node[state]  (2)  [above right=16mm of 1] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   687
\node[state]  (3)  [below right=16mm of 1] {$\mbox{}$};}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   688
137
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   689
\node (a)  [right=of 2] {$\ldots$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   690
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   691
\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
   692
\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
   693
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   694
\node (b)  [right=of 3] {$\ldots$};
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   695
\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
   696
\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
   697
\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
   698
\only<2>{
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   699
\path[->] (1) edge node [above]  {\alert{$\epsilon$}} (2);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   700
\path[->] (1) edge node [below]  {\alert{$\epsilon$}} (3);
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   701
}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   702
\begin{pgfonlayer}{background}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   703
\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   704
\only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   705
\only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   706
\only<1>{\node [yshift=3mm] at (1.north) {\bl{$r_1$}};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   707
\only<1>{\node [yshift=3mm] at (2.north) {\bl{$r_2$}};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   708
\only<2>{\node [yshift=3mm] at (3.north) {\bl{$r_1+ r_2$}};}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   709
\end{pgfonlayer}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   710
\end{tikzpicture}
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   711
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   712
\small
69cec773736b added pictures
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 136
diff changeset
   713
We (1) need to introduce a new starting state and (2) connect it to the original two starting states.
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   714
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   715
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   716
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   717
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   718
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   719
\begin{frame}[c]
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   720
\frametitle{Case $r^*$}
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   721
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   722
\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
   723
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   724
\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   725
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   726
\onslide<1>{\node at (0,0)  (1)  {$\mbox{}$};}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   727
\onslide<2->{\node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};}
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   728
\only<1>{\node[state, initial]  (2)  [right=16mm of 1] {$\mbox{}$};}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   729
\only<2->{\node[state]  (2)  [right=16mm of 1] {$\mbox{}$};}
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   730
\node (a)  [right=of 2] {$\ldots$};
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   731
\only<1>{
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   732
\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
   733
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   734
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   735
\only<2->{
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   736
\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
   737
\node[state]  (a2)  [above=of a1] {$\mbox{}$};
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   738
\node[state]  (a3)  [below=of a1] {$\mbox{}$};}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   739
\only<2->{
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   740
\path[->] (1) edge node [above]  {\alert{$\epsilon$}} (2);
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   741
\path[->] (a1) edge [bend left=45] node [above]  {\alert{$\epsilon$}} (1);
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   742
\path[->] (a2) edge [bend right] node [below]  {\alert{$\epsilon$}} (1);
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   743
\path[->] (a3) edge [bend left=45] node [below]  {\alert{$\epsilon$}} (1);
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   744
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   745
}
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   746
\begin{pgfonlayer}{background}
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   747
\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   748
\only<2->{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};}
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   749
\only<1>{\node [yshift=3mm] at (1.north) {\bl{$r$}};}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   750
\only<2->{\node [yshift=3mm] at (2.north) {\bl{$r^*$}};}
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   751
\end{pgfonlayer}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   752
\end{tikzpicture}\bigskip
138
b98a0a49c432 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 137
diff changeset
   753
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   754
\onslide<3->{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   755
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
   756
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   757
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   758
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   759
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   760
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   761
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   762
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   763
\begin{frame}[c]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   764
\frametitle{\begin{tabular}{c}Subset Construction\end{tabular}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   765
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   766
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   767
\begin{textblock}{5}(1,1)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   768
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   769
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   770
                             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: 135
diff changeset
   771
\node[state,initial]  (q_0)  {$q_0$};
\node[state] (q_1) [above=of q_0] {$q_1$};
\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   772
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   773
\path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
\path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   774
\path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   775
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 135
diff changeset
   776
\end{center}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   777
\end{textblock}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   778
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   779
\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
   780
\begin{tabular}{r|cl}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   781
nodes \textcolor{white}{*} & $a$ & $b$\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   782
\hline
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   783
$\varnothing$ \textcolor{white}{*} & \onslide<2->{$\varnothing$} & \onslide<2->{$\varnothing$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   784
$\{0\}$ \textcolor{white}{*} & \onslide<3->{$\{0,1,2\}$} & \onslide<3->{$\{2\}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   785
$\{1\}$ \textcolor{white}{*} & \onslide<3->{$\{1\}$} & \onslide<3->{$\varnothing$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   786
$\{2\}$ \onslide<5->{*} & \onslide<3->{$\varnothing$} & \onslide<3->{$\{2\}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   787
$\{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
   788
$\{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
   789
$\{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
   790
\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
   791
\end{tabular}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   792
\end{textblock}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   793
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   794
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   795
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   796
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   797
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   798
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   799
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   800
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   801
\begin{frame}[c]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   802
\frametitle{\begin{tabular}{c}Regular Languages\end{tabular}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   803
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   804
A language is \alert{regular} iff there exists
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   805
a regular expression that recognises all its strings.\bigskip\medskip
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   806
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   807
or {\bf equivalently}\bigskip\medskip
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   808
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   809
A language is \alert{regular} iff there exists
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   810
a deterministic finite automaton that recognises all its strings.\bigskip\medskip\pause
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   811
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   812
Why is every finite set of strings a regular language?
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   813
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   814
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   815
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   816
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   817
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   818
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   819
\mode<presentation>{
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   820
\begin{frame}<1-2>[c]
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   821
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   822
\begin{center}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   823
\begin{tikzpicture}[>=stealth',very thick,auto,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   824
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   825
\node[state,initial]  (q_0)  {$q_0$};
\node[state] (q_1) [right=of q_0] {$q_1$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   826
\node[state] (q_2) [below right=of q_0] {$q_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   827
\node[state] (q_3) [right=of q_2] {$q_3$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   828
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   829
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   830
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   831
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   832
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   833
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   834
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   835
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   836
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   837
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   838
\end{tikzpicture}
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   839
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   840
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   841
\mbox{}\\[-20mm]\mbox{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   842
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   843
\begin{center}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   844
\begin{tikzpicture}[>=stealth',very thick,auto,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   845
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   846
\node[state,initial]  (q_02)  {$q_{0, 2}$};
\node[state] (q_13) [right=of q_02] {$q_{1, 3}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   847
\node[state, accepting] (q_4) [right=of q_13] {$q_{4\phantom{,0}}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   848
\path[->] (q_02) edge [bend left] node [above]  {\alert{$a$}} (q_13);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   849
\path[->] (q_13) edge [bend left] node [below]  {\alert{$b$}} (q_02);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   850
\path[->] (q_02) edge [loop below] node  {\alert{$b$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   851
\path[->] (q_13) edge node [above]  {\alert{$a$}} (q_4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   852
\path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 138
diff changeset
   853
\end{tikzpicture}\\
135
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   854
minimal automaton
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   855
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   856
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   857
\end{frame}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   858
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   859
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   860
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   861
\mode<presentation>{
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   862
\begin{frame}[c]
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   863
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   864
Given the function 
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   865
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   866
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   867
\bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   868
$rev(\varnothing)$   & $\dn$ & $\varnothing$\\
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   869
$rev(\epsilon)$         & $\dn$ & $\epsilon$\\
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   870
$rev(c)$                      & $\dn$ & $c$\\
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   871
$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
   872
$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
   873
$rev(r^*)$                   & $\dn$ & $rev(r)^*$\\
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   874
\end{tabular}}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   875
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   876
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   877
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   878
and the set
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   879
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   880
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   881
\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
   882
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   883
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   884
prove whether
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   885
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   886
\begin{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   887
\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
   888
\end{center}
72b686e1c974 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 134
diff changeset
   889
133
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   890
\end{frame}}
09efdf5cf07c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   891
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
25
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   892
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   893
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   894
\end{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   895
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   896
%%% Local Variables:  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   897
%%% mode: latex
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   898
%%% TeX-master: t
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   899
%%% End: 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   900