slides/slides05.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 11 Oct 2014 13:50:36 +0100
changeset 270 4dbeaf43031d
parent 215 828303e8e4af
child 272 1446bc47a294
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t]{beamer}
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     2
\usepackage{../slides}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     3
\usepackage{../graphics}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
     4
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
     5
\usepackage{../data}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     7
\hfuzz=220pt 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     8
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     9
\pgfplotsset{compat=1.11}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    10
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    11
\newcommand{\bl}[1]{\textcolor{blue}{#1}}  
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
% beamer stuff 
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    14
\renewcommand{\slidecaption}{AFL 05, King's College London}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    15
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
\begin{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    20
\begin{frame}[t]
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
\frametitle{%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
  \begin{tabular}{@ {}c@ {}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
  \\[-3mm]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
  \LARGE Automata and \\[-2mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
  \LARGE Formal Languages (5)\\[3mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
  \end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
  \normalsize
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
  \begin{tabular}{ll}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
  Email:  & christian.urban at kcl.ac.uk\\
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    32
  Office: & S1.27 (1st floor Strand Building)\\
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
  Slides: & KEATS (also home work is there)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
  \end{center}
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    36
\end{frame}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
\mode<presentation>{
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    41
\begin{frame}[c]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    42
\frametitle{DFA Minimisation}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    44
\begin{enumerate}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    45
\item Take all pairs \bl{$(q, p)$} with \bl{$q \not= p$}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    46
\item Mark all pairs that accepting and non-accepting states
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    47
\item For  all unmarked pairs \bl{$(q, p)$} and all characters \bl{$c$} tests wether
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    48
\begin{center}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    49
\bl{$(\delta(q, c), \delta(p,c))$}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    50
\end{center} 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    51
are marked. If yes, then also mark \bl{$(q, p)$}.
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    52
\item Repeat last step until no change.
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    53
\item All unmarked pairs can be merged.
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    54
\end{enumerate}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    56
\end{frame}}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    58
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    59
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    61
\mode<presentation>{
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    62
\begin{frame}<1>[c]
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    64
\begin{center}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    65
\begin{tikzpicture}[>=stealth',very thick,auto,
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    66
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    67
\node[state,initial]  (q_0)  {$q_0$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    68
\node[state] (q_1) [right=of q_0] {$q_1$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    69
\node[state] (q_2) [below right=of q_0] {$q_2$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    70
\node[state] (q_3) [right=of q_2] {$q_3$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    71
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    72
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    73
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    74
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    75
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    76
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    77
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    78
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    79
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    80
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    81
\end{tikzpicture}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    82
\end{center}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    83
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    84
\mbox{}\\[-20mm]\mbox{}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    85
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
\begin{center}
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    87
\begin{tikzpicture}[scale=0.8,line width=0.8mm]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    88
\draw (0,0) -- (4,0);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    89
\draw (0,1) -- (4,1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    90
\draw (0,2) -- (3,2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    91
\draw (0,3) -- (2,3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    92
\draw (0,4) -- (1,4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    93
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    94
\draw (0,0) -- (0, 4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    95
\draw (1,0) -- (1, 4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    96
\draw (2,0) -- (2, 3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    97
\draw (3,0) -- (3, 2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    98
\draw (4,0) -- (4, 1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    99
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   100
\draw (0.5,-0.5) node {$q_0$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   101
\draw (1.5,-0.5) node {$q_1$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   102
\draw (2.5,-0.5) node {$q_2$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   103
\draw (3.5,-0.5) node {$q_3$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   104
 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   105
\draw (-0.5, 3.5) node {$q_1$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   106
\draw (-0.5, 2.5) node {$q_2$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   107
\draw (-0.5, 1.5) node {$q_3$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   108
\draw (-0.5, 0.5) node {$q_4$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   109
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   110
\draw (0.5,0.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   111
\draw (1.5,0.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   112
\draw (2.5,0.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   113
\draw (3.5,0.5) node {\large$\star$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   114
\end{tikzpicture}\\
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   115
\end{center}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\mode<presentation>{
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   122
\begin{frame}<1-2>[c]
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   124
\begin{center}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   125
\begin{tabular}{@{\hspace{-8mm}}cc@{}}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   126
\begin{tikzpicture}[>=stealth',very thick,auto,
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   127
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   128
\node[state,initial]  (q_0)  {$q_0$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   129
\node[state] (q_1) [right=of q_0] {$q_1$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   130
\node[state] (q_2) [below right=of q_0] {$q_2$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   131
\node[state] (q_3) [right=of q_2] {$q_3$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   132
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   133
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   134
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   135
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   136
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   137
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   138
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   139
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   140
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   141
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   142
\end{tikzpicture}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   143
&
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   144
\raisebox{9mm}{\begin{tikzpicture}[scale=0.6,line width=0.8mm]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   145
\draw (0,0) -- (4,0);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   146
\draw (0,1) -- (4,1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   147
\draw (0,2) -- (3,2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   148
\draw (0,3) -- (2,3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   149
\draw (0,4) -- (1,4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   150
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   151
\draw (0,0) -- (0, 4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   152
\draw (1,0) -- (1, 4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   153
\draw (2,0) -- (2, 3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   154
\draw (3,0) -- (3, 2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   155
\draw (4,0) -- (4, 1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   156
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   157
\draw (0.5,-0.5) node {$q_0$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   158
\draw (1.5,-0.5) node {$q_1$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   159
\draw (2.5,-0.5) node {$q_2$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   160
\draw (3.5,-0.5) node {$q_3$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   161
 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   162
\draw (-0.5, 3.5) node {$q_1$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   163
\draw (-0.5, 2.5) node {$q_2$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   164
\draw (-0.5, 1.5) node {$q_3$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   165
\draw (-0.5, 0.5) node {$q_4$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   166
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   167
\draw (0.5,0.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   168
\draw (1.5,0.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   169
\draw (2.5,0.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   170
\draw (3.5,0.5) node {\large$\star$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   171
\draw (0.5,1.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   172
\draw (2.5,1.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   173
\draw (0.5,3.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   174
\draw (1.5,2.5) node {\large$\star$}; 
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   175
\end{tikzpicture}}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   176
\end{tabular}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   177
\end{center}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   180
\mbox{}\\[-20mm]\mbox{}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   181
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
\begin{center}
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   183
\begin{tikzpicture}[>=stealth',very thick,auto,
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   184
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   185
\node[state,initial]  (q_02)  {$q_{0, 2}$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   186
\node[state] (q_13) [right=of q_02] {$q_{1, 3}$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   187
\node[state, accepting] (q_4) [right=of q_13] {$q_{4\phantom{,0}}$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   188
\path[->] (q_02) edge [bend left] node [above]  {\alert{$a$}} (q_13);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   189
\path[->] (q_13) edge [bend left] node [below]  {\alert{$b$}} (q_02);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   190
\path[->] (q_02) edge [loop below] node  {\alert{$b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   191
\path[->] (q_13) edge node [above]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   192
\path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   193
\end{tikzpicture}\\
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   194
minimal automaton
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   195
\end{center}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   200
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   201
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   206
\begin{center}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   207
\begin{tikzpicture}[>=stealth',very thick,auto,
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   208
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   209
\only<1>{\node[state,initial]  (q_0)  {$q_0$};}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   210
\only<2->{\node[state,accepting]  (q_0)  {$q_0$};}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   211
\node[state] (q_1) [right=of q_0] {$q_1$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   212
\node[state] (q_2) [below right=of q_0] {$q_2$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   213
\node[state] (q_3) [right=of q_2] {$q_3$};
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   214
\only<1>{\node[state, accepting] (q_4) [right=of q_1] {$q_4$};}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   215
\only<2->{\node[state, initial right] (q_4) [right=of q_1] {$q_4$};}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   216
\only<1-2>{
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   217
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   218
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   219
\path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   220
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   221
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   222
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   223
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   224
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   225
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   226
\only<3->{
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   227
\path[<-] (q_0) edge node [above]  {\alert{$a$}} (q_1);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   228
\path[<-] (q_1) edge node [above]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   229
\path[<-] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   230
\path[<-] (q_3) edge node [right]  {\alert{$a$}} (q_4);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   231
\path[<-] (q_2) edge node [above]  {\alert{$a$}} (q_3);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   232
\path[<-] (q_1) edge node [right]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   233
\path[<-] (q_0) edge node [above]  {\alert{$b$}} (q_2);
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   234
\path[<-] (q_2) edge [loop left] node  {\alert{$b$}} ();
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   235
\path[<-] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   236
\end{tikzpicture}
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   237
\end{center}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
\begin{itemize}
147
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   240
\item<2-> exchange initial / accepting states
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   241
\item<3-> reverse all edges
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   242
\item<4-> subset construction $\Rightarrow$ DFA
4725bba8ef26 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   243
\item<5-> repeat once more \onslide<6->{$\Rightarrow$ minimal DFA}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   245
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   246
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   247
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   250
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   252
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   253
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   254
\mbox{\lstinputlisting[language=while]{../progs/fib.while}}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   255
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   257
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   258
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   263
\mbox{\lstinputlisting[language=while]{../progs/collatz.while}}
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   267
46
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   268
148
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   269
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   270
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   271
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   272
157
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 153
diff changeset
   273
\mbox{\lstinputlisting[language=while]{../progs/collatz.while}}
148
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   274
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   275
\begin{textblock}{6}(10,2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   276
\begin{tikzpicture}[scale=0.46]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   277
\begin{axis}[axis x line=bottom, axis y line=left, ylabel=secs,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   278
    xlabel=n,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   279
    enlargelimits=0.05,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   280
    ybar interval=0.7, legend style=small]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   281
\addplot file {interpreted2.data};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   282
\addplot file {compiled2.data};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   283
%\legend{interpreted, compiled}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   284
\end{axis}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   285
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   286
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   287
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   288
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   289
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   290
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   291
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   292
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   293
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   294
\begin{tikzpicture}[scale=1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   295
  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   296
  \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   297
  \draw (4.2,1) node {Code Gen};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   298
  \draw (0.6,1.7) node {\footnotesize Parser};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   299
  \draw (-2.7,1.7) node {\footnotesize Lexer};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   300
  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   301
  \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   302
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   303
  \draw[white] (1.7,1) node (X) {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   304
  \draw[white] (3.2,1) node (Y) {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   305
  \draw[red, ->, line width = 2mm] (X) -- (Y);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   306
 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   307
  \draw[red, <-, line width = 2mm] (-0.6,1) -- (-1.6,1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   308
  \draw[red, <-, line width = 2mm] (-3.8,1) -- (-4.8,1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   309
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   310
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   311
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   312
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   313
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
148
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   314
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   315
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   316
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   317
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   318
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   319
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   320
\consolas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   321
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   322
"if true then then 42 else +"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   323
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   324
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   325
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   326
\begin{tabular}{@{}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   327
KEYWORD: \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   328
\hspace{5mm}{if}, {then}, {else},\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   329
WHITESPACE:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   330
\hspace{5mm}{" "}, {$\backslash$n},\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   331
IDENT:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   332
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   333
NUM:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   334
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   335
OP:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   336
\hspace{5mm}{+}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   337
COMMENT:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   338
\hspace{5mm}{$\slash$*} $\cdot$ (ALL$^*$ $\cdot$ {*$\slash$} $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   339
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   340
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   341
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   342
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   343
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   344
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   345
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   346
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   347
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   348
\consolas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   349
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   350
"if true then then 42 else +"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   351
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   352
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   353
\only<1>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   354
\small\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   355
KEYWORD(if),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   356
WHITESPACE,\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   357
IDENT(true),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   358
WHITESPACE,\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   359
KEYWORD(then),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   360
WHITESPACE,\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   361
KEYWORD(then),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   362
WHITESPACE,\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   363
NUM(42),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   364
WHITESPACE,\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   365
KEYWORD(else),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   366
WHITESPACE,\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   367
OP(+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   368
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   369
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   370
\only<2>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   371
\small\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   372
KEYWORD(if),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   373
IDENT(true),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   374
KEYWORD(then),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   375
KEYWORD(then),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   376
NUM(42),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   377
KEYWORD(else),\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   378
OP(+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   379
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   380
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   381
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   382
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   383
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   384
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   385
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   386
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   387
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   388
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   389
There is one small problem with the tokenizer. How should we 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   390
tokenize:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   391
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   392
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   393
{\consolas "x - 3"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   394
\end{center}
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   395
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   396
\consolas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   397
\begin{tabular}{@{}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   398
OP:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   399
\hspace{5mm}\texttt{"+"}, \texttt{"-"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   400
NUM:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   401
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {''0''}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   402
NUMBER:\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   403
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   404
\end{tabular}
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   405
148
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   406
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   407
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   408
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   409
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   411
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   412
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   413
\frametitle{\begin{tabular}{c}Two Rules\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   414
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   415
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   416
\item Longest match rule (``maximal munch rule''): The 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   417
longest initial substring matched by any regular expression is taken
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   418
as next token.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   419
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   420
\item Rule priority:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   421
For a particular longest initial substring, the first regular
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   422
expression that can match determines the token.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   423
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   424
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   425
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   426
%\url{http://www.technologyreview.com/tr10/?year=2011}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   427
  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   428
%finite deterministic automata/ nondeterministic automaton
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   429
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   430
%\item problem with infix operations, for example i-12
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   431
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   432
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   433
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 147
diff changeset
   434
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   435
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   436
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   437
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   438
\frametitle{\begin{tabular}{c}Nullable\end{tabular}}
46
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   439
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   440
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   441
\ldots{}whether a regular expression can match the empty string:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   442
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   443
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   444
\bl{$nullable(\varnothing)$}      & \bl{$\dn$} & \bl{$f\!\/alse$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   445
\bl{$nullable(\epsilon)$}           & \bl{$\dn$} &  \bl{$true$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   446
\bl{$nullable (c)$}                    & \bl{$\dn$} &  \bl{$f\!alse$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   447
\bl{$nullable (r_1 + r_2)$}       & \bl{$\dn$} &  \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   448
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} &  \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   449
\bl{$nullable (r^*)$}                 & \bl{$\dn$} & \bl{$true$} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   450
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   451
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   452
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   453
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   454
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   455
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   456
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   457
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   458
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   459
\frametitle{\begin{tabular}{c}Zeroable\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   460
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   461
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   462
\ldots{}whether a regular expression can match nothing:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   463
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   464
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   465
\bl{$zeroable(\varnothing)$}      & \bl{$\dn$} & \bl{$true$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   466
\bl{$zeroable(\epsilon)$}           & \bl{$\dn$} &  \bl{$f\!alse$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   467
\bl{$zeroable (c)$}                    & \bl{$\dn$} &  \bl{$f\!alse$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   468
\bl{$zeroable (r_1 + r_2)$}       & \bl{$\dn$} &  \bl{$zeroable(r_1) \wedge zeroable(r_2)$} \\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   469
\bl{$zeroable (r_1 \cdot r_2)$} & \bl{$\dn$} &  \bl{$zeroable(r_1) \vee zeroable(r_2)$} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   470
\bl{$zeroable (r^*)$}                 & \bl{$\dn$} & \bl{$f\!alse$} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   471
\end{tabular}
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   472
\end{center}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   473
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   474
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   475
\bl{$zeroable(r) \Leftrightarrow L(r) = \varnothing$}
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   476
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   477
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   478
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 148
diff changeset
   479
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
46
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   480
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   481
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   482
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   483
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   484
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   485
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   486
\item The star-case in our proof about the matcher needs the following lemma
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   487
\begin{center}
151
df229ec49b22 added ho
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 150
diff changeset
   488
\bl{$Der\,c\,A^* = (Der\,c\,A)\,@\, A^*$}
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   489
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   490
\end{itemize}\bigskip\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   491
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   492
\begin{itemize}
151
df229ec49b22 added ho
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 150
diff changeset
   493
\item \bl{$A^* = \{""\} \cup A\,@\,A^*$}
150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   494
\item If \bl{\texttt{""} $\in A$}, then\\ \bl{$Der\,c\,(A @ B) = (Der\,c\,A) @ B \cup (Der\,c\,B)$}\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   495
\item If \bl{\texttt{""} $\not\in A$}, then\\ \bl{$Der\,c\,(A @ B) = (Der\,c\,A) @ B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   496
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   497
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   498
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   499
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   500
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   501
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 149
diff changeset
   502
44
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   503
\end{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   504
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   505
%%% Local Variables:  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   506
%%% mode: latex
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   507
%%% TeX-master: t
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   508
%%% End: 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   509