slides03.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 24 Nov 2012 14:58:27 +0000
changeset 77 49c0beef79a1
parent 25 94133a0e62ed
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}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
\usepackage{beamerthemeplainculight}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
\usepackage[T1]{fontenc}
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}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
\usepackage{graphicx} 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
\definecolor{javared}{rgb}{0.6,0,0} % for strings
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
\lstset{language=Java,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
	basicstyle=\ttfamily,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
	stringstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
	commentstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
	numbers=left,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
	numberstyle=\tiny\color{black},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
	stepnumber=1,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
	numbersep=10pt,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
	tabsize=2,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
	showspaces=false,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
	showstringspaces=false}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
\lstdefinelanguage{scala}{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
  morekeywords={abstract,case,catch,class,def,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
    do,else,extends,false,final,finally,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
    for,if,implicit,import,match,mixin,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
    new,null,object,override,package,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
    private,protected,requires,return,sealed,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
    super,this,throw,trait,true,try,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
    type,val,var,while,with,yield},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
  otherkeywords={=>,<-,<\%,<:,>:,\#,@},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
  sensitive=true,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
  morecomment=[l]{//},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
  morecomment=[n]{/*}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
  morestring=[b]",
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  morestring=[b]',
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
  morestring=[b]"""
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
\lstset{language=Scala,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
	basicstyle=\ttfamily,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
	stringstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
	commentstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
	numbers=left,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
	numberstyle=\tiny\color{black},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
	stepnumber=1,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
	numbersep=10pt,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
	tabsize=2,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
	showspaces=false,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
	showstringspaces=false}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
% beamer stuff 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
\renewcommand{\slidecaption}{AFL 03, King's College London, 10.~October 2012}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
\begin{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
\begin{frame}<1>[t]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
\frametitle{%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
  \begin{tabular}{@ {}c@ {}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
  \\[-3mm]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
  \LARGE Automata and \\[-2mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
  \LARGE Formal Languages (3)\\[3mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
  \end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
  %\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
  %\includegraphics[scale=0.3]{pics/ante1.jpg}\hspace{5mm}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
  %\includegraphics[scale=0.31]{pics/ante2.jpg}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
  %\footnotesize\textcolor{gray}{Antikythera automaton, 100 BC (Archimedes?)}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
  %\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
\normalsize
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
  \begin{tabular}{ll}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
  Email:  & christian.urban at kcl.ac.uk\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
  Of$\!$fice: & S1.27 (1st floor Strand Building)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
  Slides: & KEATS (also home work is there)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
               & \alert{\bf (I have put a temporary link in there.)}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
\frametitle{\begin{tabular}{c}Last Week\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
Last week I showed you
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
\item one simple-minded regular expression matcher (which however does not work in all cases), and\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
\item one which works provably in all cases
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
\bl{matcher r s} \;\;if and only if \;\; \bl{s $\in$ $L$(r)}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
\end{center} 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
  \bl{der c ($\varnothing$)}            & \bl{$\dn$} & \bl{$\varnothing$} & \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
  \bl{der c ($\epsilon$)}           & \bl{$\dn$} & \bl{$\varnothing$} & \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
  \bl{der c (d)}           & \bl{$\dn$} & \bl{if c $=$ d then $\epsilon$ else $\varnothing$} & \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
  \bl{der c (r$_1$ + r$_2$)} & \bl{$\dn$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
  \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$}  & \bl{if nullable r$_1$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
  & & \bl{then ((der c r$_1$) $\cdot$ r$_2$) + (der c r$_2$)}\\ 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
  & & \bl{else (der c r$_1$) $\cdot$ r$_2$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
  \bl{der c (r$^*$)}          & \bl{$\dn$} & \bl{(der c r) $\cdot$ (r$^*$)}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
``the regular expression after \bl{c} has been recognised'' 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
For this we defined the set \bl{Der c A} as
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\bl{Der c A $\dn$ $\{$ s $|$  c::s $\in$ A$\}$ } 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
which is called the semantic derivative of a set
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
and proved 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
\bl{$L$(der c r) $=$ Der c ($L$(r))}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
\frametitle{\begin{tabular}{c}The Idea of the Algorithm\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
If we want to recognise the string \bl{abc} with regular expression \bl{r}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
then\medskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
\begin{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
\item \bl{Der a ($L$(r))}\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
\item \bl{Der b (Der a ($L$(r)))}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
\item \bl{Der c (Der b (Der a ($L$(r))))}\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
\item finally we test whether the empty string is in set\pause\medskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
\end{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
The matching algorithm works similarly, just over regular expression than sets.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
Input: string \bl{abc} and regular expression \bl{r} 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
\begin{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
\item \bl{der a r}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
\item \bl{der b (der a r)}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
\item \bl{der c (der b (der a r))}\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
\item finally check whether the latter regular expression can match the empty string
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
\end{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
We need to prove
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
\bl{$L$(der c r) $=$ Der c ($L$(r))}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
by induction on the regular expression.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
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
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
\frametitle{\begin{tabular}{c}Proofs about Rexp\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
\item \bl{$P$} holds for \bl{r$_1$ + r$_2$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   234
holds for \bl{r$_1$} and \bl{r$_2$}.\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   235
\item \bl{$P$} holds for \bl{r$_1$ $\cdot$ r$_2$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   236
holds for \bl{r$_1$} and \bl{r$_2$}.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
\item \bl{$P$} holds for \bl{r$^*$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
holds for \bl{r}.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
\end{itemize}
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
\frametitle{\begin{tabular}{c}Proofs about Natural Numbers\\ and Strings\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   250
\item \bl{$P$} holds for \bl{$0$} and
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   252
holds for \bl{$n$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   253
\end{itemize}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   254
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   255
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
\item \bl{$P$} holds for \bl{\texttt{""}} and
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   257
\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   258
holds for \bl{$s$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   263
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
\begin{frame}[t]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   267
\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   268
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   269
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   271
  \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}  & null\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
         & \bl{$\mid$} & \bl{$\epsilon$}        & empty string / "" / []\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   273
         & \bl{$\mid$} & \bl{c}                         & character\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   274
         & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$} & sequence\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   275
         & \bl{$\mid$} & \bl{r$_1$ + r$_2$}  & alternative / choice\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   276
         & \bl{$\mid$} & \bl{r$^*$}                   & star (zero or more)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
  \end{tabular}\bigskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   279
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   281
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   282
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   283
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   284
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   286
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   287
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   288
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   289
\frametitle{\begin{tabular}{c}Languages\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   290
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   291
A \alert{language} is a set of strings.\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   292
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   293
A \alert{regular expression} specifies a set of strings or language.\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   294
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   295
A language is \alert{regular} iff there exists
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   296
a regular expression that recognises all its strings.\bigskip\bigskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   297
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   298
\textcolor{gray}{not all languages are regular, e.g.~\bl{a$^n$b$^n$}.}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   299
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   300
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   301
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   302
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   303
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   304
\begin{frame}[t]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   309
  \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}  & null\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
         & \bl{$\mid$} & \bl{$\epsilon$}        & empty string / "" / []\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   311
         & \bl{$\mid$} & \bl{c}                         & character\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
         & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$} & sequence\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
         & \bl{$\mid$} & \bl{r$_1$ + r$_2$}  & alternative / choice\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
         & \bl{$\mid$} & \bl{r$^*$}                   & star (zero or more)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
  \end{tabular}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
How about ranges \bl{[a-z]}, \bl{r$^\text{+}$} and \bl{!r}?
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
\frametitle{\begin{tabular}{c}Negation of Regular Expr's\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
\item \bl{!r}  \hspace{6mm} (everything that \bl{r} cannot recognise)\medskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
\item \bl{$L$(!r) $\dn$ UNIV - $L$(r)}\medskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
\item \bl{nullable (!r) $\dn$ not (nullable(r))}\medskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
\item \bl{der\,c\,(!r) $\dn$ !(der\,c\,r)}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
\frametitle{\begin{tabular}{c}Regular Exp's for Lexing\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   344
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
Lexing separates strings into ``words'' / components.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
\item Identifiers (non-empty strings of letters or digits, starting with a letter)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
\item Numbers (non-empty sequences of digits omitting leading zeros)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
\item Keywords (else, if, while, \ldots)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
\item White space (a non-empty sequence of blanks, newlines and tabs)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
\item Comments
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   355
\end{frame}}
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
\frametitle{\begin{tabular}{c}Automata\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   363
A deterministic finite automaton consists of:
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
\item a set of states
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   367
\item one of these states is the start state
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   368
\item some states are accepting states, and
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   369
\item there is transition function\medskip 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
\small
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
which takes a state as argument and a character and produces a new state\smallskip\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
this function might not always be defined
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
\end{itemize}
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
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
\end{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
%%% Local Variables:  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
%%% mode: latex
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
%%% TeX-master: t
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   385
%%% End: 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386