slides/slides02.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Fri, 10 Oct 2025 10:18:05 +0100
changeset 1005 0ffb6e4de10a
parent 1002 9bb223540e34
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
     1
% !TEX program = xelatex
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
     2
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     3
\usepackage{../slides}
871
94b84d880c2b updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 842
diff changeset
     4
\usepackage{../graphicss}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
     5
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
     6
\usepackage{../data}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
     8
\usepackage{tcolorbox}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
     9
\newtcolorbox{mybox}{colback=red!5!white,colframe=red!75!black}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
    10
\newtcolorbox{mybox2}[1]{colback=red!5!white,colframe=red!75!black,fonttitle=\bfseries,title=#1}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
    11
\newtcolorbox{mybox3}[1]{colback=Cyan!5!white,colframe=Cyan!75!black,fonttitle=\bfseries,title=#1}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
    12
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
    13
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
    14
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    15
\hfuzz=220pt 
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    16
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    17
\lstset{language=Scala,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    18
        style=mystyle,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    19
        numbersep=0pt,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    20
        numbers=none,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    21
        xleftmargin=0mm}
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    22
777
a10430cb797c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 771
diff changeset
    23
\pgfplotsset{compat=1.17}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    24
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    25
\newcommand{\bl}[1]{\textcolor{blue}{#1}}     
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    26
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
% beamer stuff 
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    28
\renewcommand{\slidecaption}{CFL 02, King's College London}
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    29
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
\begin{document}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    34
\begin{frame}[t]
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
\frametitle{%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
  \begin{tabular}{@ {}c@ {}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
  \\[-3mm]
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    38
  \LARGE Compilers and \\[-1mm] 
882
5fcad75ade92 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    39
  \LARGE Formal Languages\\[-5mm] 
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
  \end{tabular}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    42
  \normalsize
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
  \begin{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
  \begin{tabular}{ll}
882
5fcad75ade92 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    45
  Email:  & christian.urban at kcl.ac.uk\\
1002
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    46
  Office Hour: & Friday 11:30 -- 12:30\\  
882
5fcad75ade92 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    47
  Location: & N7.07 (North Wing, Bush House)\\
5fcad75ade92 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    48
  Slides \& Progs: & KEATS\\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
  \end{tabular}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
  \end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    52
  \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    53
    \begin{tikzpicture}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    54
      \node[drop shadow,fill=white,inner sep=0pt] 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    55
      {\footnotesize\rowcolors{1}{capri!10}{white}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    56
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    57
          1 Introduction, Languages          & 6 While-Language \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    58
          \cellcolor{blue!50}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    59
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    60
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    61
          4 Lexing, Tokenising               & 9 Optimisations \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    62
          5 Grammars, Parsing                & 10 LLVM \\ \hline
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    63
        \end{tabular}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    64
      };
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    65
    \end{tikzpicture}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    66
  \end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
    67
1002
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    68
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    69
  \begin{textblock}{5}(12,3)
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    70
  \includegraphics[scale=0.35]{qr01}\\
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    71
  %%\small Wifi: IET-Guest
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    72
  \end{textblock} 
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    73
\end{frame}
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
    76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1002
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    77
%\begin{frame}[c]
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    78
%
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    79
%\begin{mybox3}{From Pollev last week}\it    
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    80
%Will C++ users be publicly shamed and humiliated in front of the class?
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    81
%\end{mybox3}  
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    82
%
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    83
%\end{frame}
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    85
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
    87
\begin{frame}[c]
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
    88
1002
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    89
\begin{center}
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    90
\begin{tabular}{c}
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    91
\includegraphics[scale=0.024]{awards.jpeg}\\
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    92
\small I try my best, but \ldots
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    93
\end{tabular} 
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    94
\end{center} 
9bb223540e34 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 972
diff changeset
    95
\mbox{}
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
    96
\end{frame}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
    97
1005
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
    98
{
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
    99
\setbeamercolor{background canvas}{bg=cream}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   100
\begin{frame}<1-2>[c]
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   101
\end{frame}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   102
}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   103
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   104
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   105
\begin{frame}[t]
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   106
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   107
\mbox{}\\[-20mm]\mbox{}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   108
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   109
\tt
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   110
\begin{center}\large
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   111
\code{"if x = 42 then x := x + 1 else x := x - 1"}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   112
\end{center}\small
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   113
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   114
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   115
\begin{tabular}{@{}l}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   116
KEYWORD: \\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   117
\hspace{5mm}{if}, {then}, {else},\ldots\\ 
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   118
WHITESPACE:\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   119
\hspace{5mm}{" "}, {$\backslash$n}, {$\backslash$r}\\ 
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   120
IDENTIFIER:\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   121
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   122
NUM:\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   123
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   124
NUMBER:\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   125
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   126
OP:\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   127
\hspace{5mm}+, -, *, \%, <, =<,\ldots\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   128
COMMENTS:\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   129
\hspace{5mm}{$\slash$*} $\cdot$ $\sim$(ALL$^*$ $\cdot$ (*$\slash$) $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   130
\end{tabular}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   131
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   132
\end{frame}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   133
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   134
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   135
{
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   136
\setbeamercolor{background canvas}{bg=cream}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   137
\begin{frame}<1-4>[c]
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   138
\end{frame}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   139
}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   140
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   142
\begin{frame}[t]
630
9b1c15c3eb6f updated
Christian Urban <urbanc@in.tum.de>
parents: 573
diff changeset
   143
  \frametitle{
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
   144
    Let's Implement an Efficient\\[-2mm] 
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   145
    Regular Expression Matcher}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   146
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   147
\footnotesize
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   148
\begin{center}
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   149
  {\normalsize Graphs: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$} and strings \bl{$\underbrace{\,a\ldots a\,}_{n}$}}\\[-2mm]
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   150
\begin{tabular}{@{}cc@{}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   151
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   152
\begin{axis}[
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   153
    title={Graph: $\texttt{(a*)*\,b}$ and strings 
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   154
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   155
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   156
    x label style={at={(1.05,0.0)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   157
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   158
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   159
    xtick={0,5,...,30},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   160
    xmax=33,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   161
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   162
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   163
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   164
    axis lines=left,
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   165
    width=5.5cm,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   166
    height=4.5cm, 
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   167
    legend entries={Python, Java 8, JavaScript, Swift},  
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   168
    legend pos=north west,
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
   169
    legend cell align=left]
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   170
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   171
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   172
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   173
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   174
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   175
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   176
&
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   177
\begin{tikzpicture}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   178
  \begin{axis}[
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   179
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   180
    x label style={at={(1.1,0.05)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   181
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   182
    enlargelimits=false,
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   183
    xtick={0,5000,...,10000},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   184
    xmax=11500,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   185
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   186
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   187
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   188
    axis lines=left,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   189
    width=5cm,
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
   190
    height=4.5cm,
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
   191
    legend entries={Scala V2,Scala V3},
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   192
    legend pos=north east,
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
   193
    legend cell align=left]
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   194
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   195
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   196
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   197
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   198
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   199
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   200
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   201
\small
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   202
\begin{textblock}{14}(1,14.6)
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   203
In the handouts is a similar graph for \bl{$(a^*)^* \cdot b$} and Java, 
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   204
JavaScript, Python and more.
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   205
\end{textblock}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   206
\end{frame}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   207
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   208
967
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   209
{
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   210
\setbeamercolor{background canvas}{bg=cream}
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   211
\begin{frame}<1-4>[c]
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   212
\end{frame}
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   213
}
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   214
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   215
ce5de01b9632 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 941
diff changeset
   216
512
a6aa52ecc1c5 updated
cu
parents: 510
diff changeset
   217
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   218
%\begin{frame}[c]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   219
%\frametitle{Evil Regular Expressions}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   220
%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   221
%\begin{itemize}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   222
%\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   223
%\item Evil regular expressions\medskip
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   224
%\begin{itemize}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   225
%\item \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   226
%\item \bl{$(a^*)^*$}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   227
%\item \bl{$([a$\,-\,$z]^+)^*$}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   228
%\item \bl{$(a + a \cdot a)^*$}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   229
%\item \bl{$(a + a^?)^*$}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   230
%\end{itemize}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   231
%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   232
%\item sometimes also called \alert{catastrophic backtracking}\bigskip
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   233
%\item \small\ldots I hope you have watched the video by the
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   234
%  StackExchange engineer  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   235
%\end{itemize}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   236
%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   237
%\end{frame}
512
a6aa52ecc1c5 updated
cu
parents: 510
diff changeset
   238
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   239
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   240
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   241
\begin{frame}[c]
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   242
\frametitle{(Basic) Regular Expressions}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   243
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   244
Their inductive definition:
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   245
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   246
\begin{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   247
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   248
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & nothing\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   249
         & \bl{$\mid$} & \bl{$\ONE$}       & empty string / \pcode{""} / $[]$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   250
         & \bl{$\mid$} & \bl{$c$}                         & character\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   251
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   252
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   253
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   254
  \end{tabular}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   255
\end{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   256
\vspace{\fill}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   257
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
   258
%%Q: \;What about \;\bl{$r \cdot 0$} \; ?
507
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   259
\end{frame}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   260
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   261
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   262
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   263
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   264
\begin{frame}[c]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   265
  \frametitle{
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   266
   When Are Two Regular\\[-1mm]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   267
   Expressions Equivalent?}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   268
  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   269
   \begin{bubble}[10cm]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   270
    \large
763
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   271
    Two regular expressions \bl{$r_1$} and \bl{$r_2$} are
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   272
    \alert{\bf{}equivalent} 
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   273
    provided:\medskip 
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   274
    \begin{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   275
      \bl{$r_1 \equiv r_2 \;\;\dn\;\; L(r_1) = L(r_2)$}  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   276
    \end{center}\medskip
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   277
    \end{bubble}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   278
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   279
\end{frame}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   280
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   281
  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   282
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   283
\begin{frame}[c]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   284
\frametitle{Some Concrete Equivalences}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   285
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   286
\begin{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   287
\bl{\begin{tabular}{rcl}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   288
$(a + b)  + c$ & $\equiv$ & $a + (b + c)$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   289
$a + a$        & $\equiv$ & $a$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   290
$a + b$        & $\equiv$ & $b + a$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   291
$(a \cdot b) \cdot c$ & $\equiv$ & $a \cdot (b \cdot c)$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   292
$c \cdot (a + b)$ & $\equiv$ & $(c \cdot a) + (c \cdot b)$\bigskip\bigskip\\\pause
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   293
$a \cdot a$       & $\not\equiv$ & $a$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   294
$a + (b \cdot c)$ & $\not\equiv$ & $(a + b) \cdot (a + c)$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   295
\end{tabular}}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   296
\end{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   297
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   298
\end{frame}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   299
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   300
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   301
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   302
\begin{frame}[c]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   303
\frametitle{Some Corner Cases}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   304
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   305
\begin{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   306
\bl{\begin{tabular}{rcl}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   307
$a \cdot \ZERO$ & $\not\equiv$ & $a$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   308
$a + \ONE$ & $\not\equiv$ & $a$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   309
$\ONE$ & $\equiv$ & $\ZERO^*$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   310
$\ONE^*$ & $\equiv$ & $\ONE$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   311
$\ZERO^*$ & $\not\equiv$ & $\ZERO$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   312
\end{tabular}}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   313
\end{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   314
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   315
\end{frame}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   316
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   317
  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   318
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   319
\begin{frame}[c]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   320
\frametitle{Some Simplification Rules}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   321
 
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   322
\begin{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   323
\bl{\begin{tabular}{rcl}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   324
$r + \ZERO$  & $\equiv$ & $r$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   325
$\ZERO + r$  & $\equiv$ & $r$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   326
$r \cdot \ONE$ & $\equiv$ & $r$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   327
$\ONE \cdot r$     & $\equiv$ & $r$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   328
$r \cdot \ZERO$ & $\equiv$ & $\ZERO$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   329
$\ZERO \cdot r$ & $\equiv$ & $\ZERO$\\
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   330
$r + r$ & $\equiv$ & $r$
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   331
\end{tabular}}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   332
\end{center}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   333
 
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   334
\end{frame}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   335
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   336
  
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   337
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   338
\begin{frame}[c]
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   339
\frametitle{Simplification Example}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   340
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   341
%%Given \bl{$r \dn ((a \cdot b) + b)^*$}, you can simplify as follows
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   342
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   343
\begin{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   344
\def\arraystretch{2}  
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   345
\begin{tabular}{@{}lcl}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   346
  \bl{$((\ONE \cdot b) + \ZERO) \cdot r$}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   347
    & \bl{$\Rightarrow$} & \bl{$((\underline{\ONE \cdot b}) + \ZERO) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   348
    & \bl{$=$} & \bl{$(\underline{b + \ZERO}) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   349
    & \bl{$=$} & \bl{$b \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   350
\end{tabular}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   351
\end{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   352
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   353
\end{frame}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   354
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   355
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   356
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   357
\begin{frame}[c]
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   358
\frametitle{Simplification Example}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   359
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   360
%%Given \bl{$r \dn ((a \cdot b) + b)^*$}, you can simplify as follows
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   361
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   362
\begin{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   363
\def\arraystretch{2}  
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   364
\begin{tabular}{@{}lcl}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   365
  \bl{$((\ZERO \cdot b) + \ZERO) \cdot r$}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   366
    & \bl{$\Rightarrow$} & \bl{$((\underline{\ZERO \cdot b}) + \ZERO) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   367
    & \bl{$=$} & \bl{$(\underline{\ZERO + \ZERO}) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   368
    & \bl{$=$} & \bl{$\ZERO \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   369
    & \bl{$=$} & \bl{$\ZERO$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   370
\end{tabular}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   371
\end{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   372
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   373
\end{frame}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   374
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
566
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
   375
507
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   376
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   377
\begin{frame}[t]
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   378
\frametitle{Semantic Derivative\\[5mm]}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   379
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   380
\begin{itemize}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   381
\item The \alert{\bf Semantic Derivative} of a 
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   382
\underline{language}\\ w.r.t.~to a character \bl{$c$}:
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   383
\bigskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   384
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   385
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   386
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   387
\end{center}\bigskip
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   388
630
9b1c15c3eb6f updated
Christian Urban <urbanc@in.tum.de>
parents: 573
diff changeset
   389
For \bl{$A = \{\mathit{foo}, \mathit{bar}, \mathit{frak}\}$} then
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   390
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   391
\begin{center}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   392
\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
630
9b1c15c3eb6f updated
Christian Urban <urbanc@in.tum.de>
parents: 573
diff changeset
   393
$\Der\,f\,A$ & $=$ & $\{\mathit{oo}, \mathit{rak}\}$\\
9b1c15c3eb6f updated
Christian Urban <urbanc@in.tum.de>
parents: 573
diff changeset
   394
$\Der\,b\,A$ & $=$ &  $\{\mathit{ar}\}$\\  
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   395
$\Der\,a\,A$ & $=$ & $\{\}$\pause
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   396
\end{tabular}}
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   397
\end{center}\medskip
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   398
630
9b1c15c3eb6f updated
Christian Urban <urbanc@in.tum.de>
parents: 573
diff changeset
   399
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   400
We can extend this definition to strings
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   401
\[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   402
\bl{\Ders\,s\,A = \{s'\;|\;s\,@\,s' \in A\}}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   403
\]
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   404
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   405
\end{itemize}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   406
 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   407
\end{frame}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   408
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   409
763
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   411
\begin{frame}[c]
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   412
\frametitle{The Specification for Matching}
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   413
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   414
\begin{bubble}[10cm]
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   415
\large
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   416
A regular expression \bl{$r$} matches a string~\bl{$s$} 
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   417
provided:
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   418
\begin{center}
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   419
\bl{$s \in L(r)$} 
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   420
\end{center}\medskip
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   421
\end{bubble}
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   422
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   423
\bigskip\bigskip
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   424
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   425
\ldots and the point of the this lecture is to decide this problem as
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   426
fast as possible (unlike Python, Ruby, Java etc)
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   427
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   428
\end{frame}
4e628958c01a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   429
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
771
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
   430
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
   431
512
a6aa52ecc1c5 updated
cu
parents: 510
diff changeset
   432
a6aa52ecc1c5 updated
cu
parents: 510
diff changeset
   433
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6aa52ecc1c5 updated
cu
parents: 510
diff changeset
   434
\begin{frame}[c]
573
711bbc480998 updated
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
   435
\frametitle{\mbox{Brzozowski's Algorithm (1)}}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   436
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   437
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   438
\ldots{}whether a regular expression can match the empty string:
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   439
\begin{center}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   440
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   441
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   442
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   443
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   444
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   445
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   446
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   447
\end{tabular}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   448
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   449
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   450
\end{frame}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   451
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   452
972
ebb4a40d9bae updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 967
diff changeset
   453
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1005
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   454
%\begin{frame}[c]
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   455
%
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   456
%\bl{$r ::= \ZERO \,\;|\;\, \ONE \,\;|\;\, c \,\;|\;\, r_1 + r_2 \,\;|\;\, r_1 \cdot r_2 \,\;|\;\, r^{*} \,\;|\;\, r^{\{n\}}$}  
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   457
%
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
   458
%\end{frame}
972
ebb4a40d9bae updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 967
diff changeset
   459
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
ebb4a40d9bae updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 967
diff changeset
   460
ebb4a40d9bae updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 967
diff changeset
   461
ebb4a40d9bae updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 967
diff changeset
   462
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   463
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   464
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   465
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   466
\frametitle{The Derivative of a Rexp}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   467
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   468
\large
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   469
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   470
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   471
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   472
\small
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   473
\bl{$\der\,c\,r$} gives the answer, Brzozowski 1964
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   474
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   478
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   479
\frametitle{The Derivative of a Rexp}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   480
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   481
\begin{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   482
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   483
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   484
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   485
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   486
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   487
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   488
  & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\ 
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   489
  & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   490
  \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$} &\medskip\bigskip\\\pause
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   491
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   492
  \bl{$\ders\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   493
  \bl{$\ders\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\ders\,s\,(\der\,c\,r)$} & \\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   494
  \end{tabular}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   495
\end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   496
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   497
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   498
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   499
941
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   500
{
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   501
\setbeamercolor{background canvas}{bg=cream}
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   502
\begin{frame}<1-6>[c]
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   503
\end{frame}
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   504
}
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   505
66adcae6c762 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 940
diff changeset
   506
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   507
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   508
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   509
\frametitle{Examples}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   510
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   511
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   512
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   513
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   514
\begin{tabular}{l}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   515
\bl{$\der\,a\,r =\;?$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   516
\bl{$\der\,b\,r =\;?$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   517
\bl{$\der\,c\,r =\;?$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   518
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   519
\end{center}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   520
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   521
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   522
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   523
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   524
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   525
\begin{frame}[c]
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   526
\frametitle{Derivative Example}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   527
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   528
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   529
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   530
\begin{center}
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   531
\def\arraystretch{1.5}  
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   532
\begin{tabular}{@{}lcl}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   533
  \bl{$\der\,a\,((a \cdot b) + b)^*$}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   534
    & \bl{$\Rightarrow$}& \bl{$\der\,a\, \underline{((a \cdot b) + b)^*}$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   535
    & \bl{$=$} & \bl{$(der\,a\,(\underline{(a \cdot b) + b})) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   536
    & \bl{$=$} & \bl{$((der\,a\,(\underline{a \cdot b})) + (der\,a\,b)) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   537
    & \bl{$=$} & \bl{$(((der\,a\,\underline{a}) \cdot b) + (der\,a\,b)) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   538
    & \bl{$=$} & \bl{$((\ONE \cdot b) + (der\,a\,\underline{b})) \cdot r$}\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   539
    & \bl{$=$} & \bl{$((\ONE \cdot b) + \ZERO) \cdot r$}
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   540
\end{tabular}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   541
\end{center}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   542
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   543
\end{frame}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   544
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   545
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   546
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   547
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   548
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   549
\begin{frame}[c]
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   550
\frametitle{\mbox{The Brzozowski Algorithm}}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   551
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   552
%\begin{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   553
%\begin{tabular}{l} 
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   554
%\bl{$\textit{matcher}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}  
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   555
%\end{tabular}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   556
%\end{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   557
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   558
\begin{center}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   559
\begin{mybox3}{}
765
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   560
\centering    
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   561
\bl{$\textit{matcher}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   562
\end{mybox3}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   563
\end{center}
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   564
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   565
\end{frame}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   566
%%%%%%%%%%%%%%%%%
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   567
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   568
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   569
\begin{frame}[t]
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   570
\frametitle{Brzozowski: An Example}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   571
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   572
Does \bl{$r_1$} match \bl{$abc$}?
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   573
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   574
\begin{tabular}{@{}rl@{}l@{}}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   575
Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = \der\,a\,r_1)$}\smallskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   576
Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = \der\,b\,r_2)$}\smallskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   577
Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = \der\,c\,r_3)$}\smallskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   578
Step 4: & the string is exhausted: & \bl{($nullable(r_4))$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   579
        & test whether \bl{$r_4$} can recognise\\
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   580
        & the empty string\medskip\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   581
Output: & result of the test\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   582
        & $\Rightarrow \bl{\textit{true}} \,\text{or}\, 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   583
                       \bl{\textit{false}}$\\        
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   584
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   585
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   586
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   587
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   588
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   589
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   590
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   591
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   592
\begin{frame}[c]
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   593
\frametitle{The Idea of the Algorithm}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   594
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   595
If we want to recognise the string \bl{$abc$} with regular 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   596
expression \bl{$r_1$} then\medskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   597
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   598
\begin{enumerate}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   599
\item \bl{$\Der\,a\,(L(r_1))$}\pause
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   600
\item \bl{$\Der\,b\,(\Der\,a\,(L(r_1)))$}\pause
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   601
\item \bl{$\Der\,c\,(\Der\,b\,(\Der\,a\,(L(r_1))))$}\bigskip
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   602
\item finally we test whether the empty string is in this 
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   603
set; same for  \bl{$\Ders\,abc\,(L(r_1))$}.\medskip
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   604
\end{enumerate}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   605
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   606
The matching algorithm works similarly, just over regular expressions instead of sets.
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   607
\end{frame}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   608
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   609
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   610
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   611
\begin{frame}[c]
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   612
\frametitle{The Idea with Derivatives}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   613
  
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   614
Input: string \bl{$abc$} and regular expression \bl{$r$}\medskip 
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   615
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   616
\begin{enumerate}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   617
\item \bl{$der\,a\,r$}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   618
\item \bl{$der\,b\,(der\,a\,r)$}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   619
\item \bl{$der\,c\,(der\,b\,(der\,a\,r))$}\bigskip\pause
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   620
\item finally check whether the last regular expression can match the empty string
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   621
\end{enumerate}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   622
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   623
\end{frame}
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   624
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
   625
765
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   626
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   627
\begin{frame}[c]
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   628
\frametitle{\boldmath\;$a^{?\{n\}} \cdot a^{\{n\}}$}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   629
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   630
\begin{center}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   631
\begin{tikzpicture}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   632
\begin{axis}[
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   633
    xlabel={$n$},
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   634
    x label style={at={(1.05,0.0)}},
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   635
    ylabel={time in secs},
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   636
    enlargelimits=false,
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   637
    xtick={0,5,...,30},
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   638
    xmax=31,
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   639
    ytick={0,5,...,30},
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   640
    scaled ticks=false,
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   641
    axis lines=left,
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   642
    width=7cm,
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   643
    height=7cm, 
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   644
    legend entries={Python,Ruby},  
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   645
    legend pos=outer north east,
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   646
    legend cell align=left  
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   647
]
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   648
\addplot[blue,mark=*, mark options={fill=white}] 
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   649
  table {re-python.data};
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   650
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   651
  table {re-ruby.data};    
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   652
\end{axis}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   653
\end{tikzpicture}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   654
\end{center}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   655
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   656
\end{frame}
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   657
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   658
b294cfbb5c01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 764
diff changeset
   659
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   660
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   661
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   662
\begin{frame}[c]
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   663
\frametitle{Oops\ldots \boldmath\;$a^{?\{n\}} \cdot a^{\{n\}}$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   664
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   665
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   666
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   667
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   668
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   669
    x label style={at={(1.05,0.0)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   670
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   671
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   672
    xtick={0,5,...,30},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   673
    xmax=31,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   674
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   675
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   676
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   677
    width=7cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   678
    height=7cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   679
    legend entries={Python,Ruby,Scala V1},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   680
    legend pos=outer north east,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   681
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   682
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   683
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   684
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   685
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   686
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   687
\addplot[red,mark=triangle*,mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   688
  table {re1.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   689
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   690
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   691
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   692
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   693
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   694
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   695
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   696
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   697
\begin{frame}[t]
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   698
\frametitle{A Problem\medskip}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   699
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   700
We represented the ``n-times'' \bl{$a^{\{n\}}$} as a 
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   701
sequence regular expression:
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   702
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   703
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   704
\begin{tabular}{rl}
767
bdd12391d345 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 765
diff changeset
   705
0: & \bl{$\ONE$}\\    
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   706
1: & \bl{$a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   707
2: & \bl{$a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   708
3: & \bl{$a\cdot a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   709
& \ldots\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   710
13: & \bl{$a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   711
& \ldots\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   712
20:
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   713
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   714
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   715
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   716
This problem is aggravated with \bl{$a^?$} being represented 
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   717
as \bl{$a + \ONE$}.
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   718
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   719
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   720
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   721
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   722
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   723
\frametitle{Solving the Problem}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   724
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
   725
What happens if we extend our regular expressions with explicit 
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
   726
constructors
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   727
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   728
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   729
\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   730
\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   731
             & \bl{$\mid$} & \bl{$r^{\{n\}}$}\\
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   732
             & \bl{$\mid$} & \bl{$r^?$} 
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   733
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   734
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   735
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   736
What is their meaning?\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   737
What are the cases for \bl{$nullable$} and \bl{$\der$}?
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   738
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   739
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   740
769
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   741
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   742
\begin{frame}[c]
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   743
  \frametitle{$der$ for $n$-times}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   744
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   745
Case \bl{$n = 2$} and \bl{$r \cdot r$}: 
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   746
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   747
\begin{center}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   748
  \begin{tabular}{lcl}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   749
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   750
                              &   & \bl{then \; \alert<3>{$(der\,c\,r)\cdot r + der\,c\,r$}}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   751
                              &   & \bl{else \; $(der\,c\,r)\cdot r$}\bigskip\pause\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   752
    my claim                  &   & \bl{$\equiv\;$} \bl{$(der\,c\,r)\cdot r$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   753
    (in this case)                                
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   754
  \end{tabular} 
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   755
\end{center}  
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   756
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   757
\end{frame}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   758
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   759
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   760
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   761
\begin{frame}[t]
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   762
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   763
We know \bl{$nullable(r)$} holds!\pause 
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   764
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   765
\begin{center}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   766
  \begin{tabular}{@{}lcl}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   767
    \bl{$(der\,c\,r)\cdot r + der\,c\,r$}\pause
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   768
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r + (der\,c\,r) \cdot \ONE$}\medskip\pause\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   769
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot (r + \ONE)$}\medskip\pause\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   770
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   771
    \multicolumn{3}{r}{\small(remember \bl{$r$} is nullable)}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   772
  \end{tabular} 
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   773
\end{center}\pause
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   774
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   775
\rule{13cm}{0.8mm}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   776
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   777
\begin{textblock}{13}(2,10)
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   778
\only<6>{%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   779
  \begin{tabular}{lcl}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   780
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   781
                          &   & \bl{then \; $(der\,c\,r)\cdot r + der\,c\,r$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   782
                          &   & \bl{else \; $(der\,c\,r)\cdot r$}                                
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   783
  \end{tabular}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   784
\only<7>{%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   785
  \begin{tabular}{lcl}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   786
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   787
                          &   & \bl{then \; $(der\,c\,r)\cdot r$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   788
                          &   & \bl{else \; $(der\,c\,r)\cdot r$}                                
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   789
  \end{tabular}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   790
\only<8>{%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   791
  \begin{tabular}{lcl}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   792
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r$}                                
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   793
  \end{tabular}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   794
\end{textblock}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   795
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   796
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   797
\end{frame}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   798
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   799
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   800
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   801
\begin{frame}[c]
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   802
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   803
\begin{center}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   804
\begin{tabular}{ll@{\hspace{10mm}}l}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   805
& \bl{$r\{n\}$} & \bl{$der$}\hspace{20mm}\mbox{}\\\hline\\[-4mm]    
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   806
\bl{$n = 0$} : & \bl{$\ONE$}           & \bl{$\ZERO$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   807
\bl{$n = 1$} : & \bl{$r$}              & \bl{$(der\,c\,r)$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   808
\bl{$n = 2$} : & \bl{$r\cdot r$}       & \bl{$(der\,c\,r)\cdot r$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   809
\bl{$n = 3$} : & \bl{$r\cdot r\cdot r$}& \only<1>{???}\only<2->{\bl{$(der\,c\,r)\cdot r\cdot r$}}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   810
\quad\vdots  
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   811
\end{tabular} 
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   812
\end{center}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   813
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   814
\begin{textblock}{13}(1,11)
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   815
\only<3->{%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   816
  \begin{tabular}{rcl}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   817
    \bl{$nullable(r\{n\})$} & \bl{$\dn$} &
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   818
                          \bl{if\; $n = 0$\; then\; $true$\; else\; $nullable(r)$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   819
    \bl{$der\,c\,(r\{n\})$} & \bl{$\dn$} &
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   820
                          \bl{if\; $n = 0$\; then\; $\ZERO$\; else\; $(der\,c\,r)\cdot r\{n - 1\}$}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   821
  \end{tabular}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   822
\end{textblock}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   823
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   824
\end{frame}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   825
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   826
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   827
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   828
\begin{frame}[c]
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   829
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   830
\begin{textblock}{13}(1.5,4)
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   831
  \only<1-6>{%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   832
  \begin{tabular}{@{}lcl@{}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   833
    \bl{$der\,c\,(r\cdot r\cdot r)$}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   834
    & \bl{$\dn$} & \bl{if $nullable(r)$}\medskip\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   835
    & & \only<1>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + der\,c\,(r\cdot r)$}}%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   836
        \only<2>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + (der\,c\,r)\cdot r$}}%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   837
        \only<3>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r + r)$}}%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   838
        \only<4>{\bl{then\; $(der\,c\,r)\cdot (r\cdot (r + \ONE))$}}%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   839
        \only<5>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r)$}}%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   840
        \only<6>{\bl{then\; $(der\,c\,r)\cdot r\cdot r$}}\medskip\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   841
    & & \bl{else\; $(der\,c\,r)\cdot r\cdot r$}\\
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   842
  \end{tabular}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   843
  \only<7->{%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   844
  \begin{tabular}{@{}lcl@{}}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   845
    \bl{$der\,c\,(r\cdot r\cdot r)$}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   846
    & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r\cdot r$}%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   847
  \end{tabular}} 
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   848
\end{textblock}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   849
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   850
\end{frame}
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   851
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
   852
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   853
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   854
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   855
\begin{frame}[t]
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   856
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   857
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   858
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   859
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   860
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   861
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   862
    x label style={at={(1.05,0.0)}},   
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   863
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   864
    enlargelimits=false,
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   865
    xtick={0,200,...,1100},
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   866
    xmax=1200,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   867
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   868
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   869
    axis lines=left,
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   870
    width=8cm,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   871
    height=6.5cm, 
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   872
    legend entries={Python,Ruby,Scala V1,Scala V2},  
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   873
    legend pos=outer north east,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   874
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   875
]
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   876
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   877
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   878
\addplot[red,mark=triangle*,mark options={fill=white}] table {re1.data};  
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   879
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   880
\end{axis}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   881
\end{tikzpicture}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   882
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   883
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   884
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   885
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   886
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   887
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   888
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   889
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   890
\frametitle{Examples}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   891
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   892
Recall the example of \bl{$r \dn ((a \cdot b) + b)^*$} with
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   893
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   894
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   895
\begin{tabular}{l}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   896
\bl{$\der\,a\,r = ((\ONE \cdot b) + \ZERO) \cdot r$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   897
\bl{$\der\,b\,r = ((\ZERO \cdot b) + \ONE)\cdot r$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   898
\bl{$\der\,c\,r = ((\ZERO \cdot b) + \ZERO)\cdot r$}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   899
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   900
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   901
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   902
What are these regular expressions equivalent to?
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   903
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   904
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   905
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   906
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   907
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   908
\begin{frame}[c]
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   909
\frametitle{Simplification Rules}
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   910
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   911
\begin{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   912
\bl{\begin{tabular}{rcl}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   913
$r + \ZERO$       & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   914
$\ZERO + r$       & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   915
$r \cdot \ONE$    & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   916
$\ONE \cdot r$    & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   917
$r \cdot \ZERO$   & $\Rightarrow$ & $\ZERO$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   918
$\ZERO \cdot r$   & $\Rightarrow$ & $\ZERO$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   919
$r + r$           & $\Rightarrow$ & $r$
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   920
\end{tabular}}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   921
\end{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   922
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   923
\footnotesize
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   924
\lstinputlisting[firstline=22,lastline=26]{../progs/app6.scala}
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   925
\end{frame}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   926
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   927
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   928
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   929
\begin{frame}[c]
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   930
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   931
\footnotesize
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   932
\lstinputlisting[firstline=1,lastline=21]{../progs/app6.scala}
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   933
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   934
\end{frame}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   935
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   936
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   937
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   938
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   939
\begin{frame}[t]
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
   940
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   941
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   942
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   943
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   944
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   945
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   946
    x label style={at={(1.05,0.0)}},     
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   947
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   948
    enlargelimits=false,
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   949
    xtick={0,5000,...,10000},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   950
    xmax=11000,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   951
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   952
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   953
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   954
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   955
    width=9cm,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   956
    height=7cm,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   957
    legend entries={Scala V2,Scala V3},  
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   958
    legend pos=north east
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   959
]
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   960
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   961
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   962
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   963
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   964
\end{center}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   965
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   966
\end{frame}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   967
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   968
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   969
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   970
\begin{frame}[t]
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   971
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   972
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   973
\begin{center}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   974
\begin{tikzpicture}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   975
\begin{axis}[
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   976
    xlabel={$n$},
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   977
    x label style={at={(1.05,0.0)}},     
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   978
    ylabel={time in secs},
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   979
    enlargelimits=false,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   980
    xtick={0,5000,...,10000},
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   981
    xmax=11000,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   982
    ymax=35,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   983
    ytick={0,5,...,30},
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   984
    scaled ticks=false,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   985
    axis lines=left,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   986
    width=9cm,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   987
    height=7cm,
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   988
    legend entries={Scala V2,Scala V3,Rust},  
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   989
    legend pos=north east
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   990
]
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   991
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   992
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   993
\addplot[pink,mark=triangle,mark options={fill=pink}] table {re-rust.data};
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   994
\end{axis}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   995
\end{tikzpicture}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   996
\end{center}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
   997
782
a26a20acd1c2 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 778
diff changeset
   998
code by Archie Collard
a26a20acd1c2 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 778
diff changeset
   999
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1000
\end{frame}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1001
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1002
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1003
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1004
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1005
\begin{frame}[c]
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1006
  \frametitle{Another Example \boldmath$(a^*)^* \cdot b$}
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1007
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1008
\bigskip    
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1009
\begin{center}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1010
\begin{tikzpicture}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1011
  \begin{axis}[
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1012
    xlabel={$n$},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1013
    x label style={at={(1.05,0.0)}},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1014
    ylabel={time in secs},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1015
    enlargelimits=false,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1016
    xtick={0,5,...,30},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1017
    xmax=33,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1018
    ymax=35,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1019
    ytick={0,10,...,30},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1020
    scaled ticks=false,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1021
    axis lines=left,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1022
    width=9cm,
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1023
    height=5.5cm, 
777
a10430cb797c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 771
diff changeset
  1024
    legend entries={Java 8,Python,JavaScript,Swift,Dart},  
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1025
    legend pos=outer north east,
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1026
    legend cell align=left]
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1027
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1028
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1029
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
767
bdd12391d345 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 765
diff changeset
  1030
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
777
a10430cb797c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 771
diff changeset
  1031
\addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data};
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1032
\end{axis}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1033
\end{tikzpicture}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1034
\end{center}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1035
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1036
Regex: \bl{$(a^*)^* \cdot b$}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1037
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1038
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1039
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1040
\end{frame}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1041
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1042
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1043
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1044
\begin{frame}[c]
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1045
\frametitle{Same Example in Java 9+}
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1046
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1047
\begin{center}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1048
\begin{tikzpicture}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1049
  \begin{axis}[
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1050
    xlabel={$n$},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1051
    x label style={at={(1.09,-0.15)}},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1052
    ylabel={time in secs},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1053
    scaled x ticks=false,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1054
    enlargelimits=false,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1055
    xtick distance=10000,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1056
    xmax=44000, 
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1057
    ytick={0,10,...,30}, 
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1058
    ymax=35, 
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1059
    axis lines=left,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1060
    width=9cm,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1061
    height=5cm, 
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1062
    legend entries={Java \liningnums{9}+},
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1063
    legend pos=north west,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1064
    legend cell align=left]
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1065
\addplot[blue,mark=square*,mark options={fill=white}] table {re-java9.data};
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1066
\end{axis}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1067
\end{tikzpicture}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1068
\end{center}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1069
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1070
Regex: \bl{$(a^*)^* \cdot b$}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1071
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1072
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1073
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1074
\end{frame}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1075
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1076
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1077
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1078
\begin{frame}[c]
646
2abd285c66d1 updated
Christian Urban <urbanc@in.tum.de>
parents: 638
diff changeset
  1079
\frametitle{\ldots{}and with Brzozowski}
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1080
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1081
\begin{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1082
\begin{tikzpicture}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1083
  \begin{axis}[
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1084
    xlabel={$n$},
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1085
    x label style={at={(1.09,0.0)}},
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1086
    ylabel={time in secs},
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1087
    scaled x ticks=false,
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1088
    xtick distance=2000000,
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1089
    enlargelimits=false,
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1090
    xmax=6400000, 
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
  1091
    ytick={0,10,...,30},
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
  1092
    ymax=35,
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1093
    axis lines=left,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1094
    width=9cm,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1095
    height=5cm, 
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1096
    legend entries={Scala V3},
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1097
    legend pos=north west,
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1098
    legend cell align=left]
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
  1099
%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1100
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1101
\end{axis}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1102
\end{tikzpicture}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1103
\end{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1104
565
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1105
Regex: \bl{$(a^*)^* \cdot b$}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1106
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1107
Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}
2be8c4c77418 updated
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
  1108
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1109
\end{frame}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1110
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
  1111
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1112
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
573
711bbc480998 updated
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1113
\begin{frame}[c]
711bbc480998 updated
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1114
\frametitle{\mbox{What is good about this Alg.}}
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1115
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1116
\begin{itemize}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1117
\item extends to most regular expressions, for example
573
711bbc480998 updated
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1118
\bl{$\sim r$} (next slide)
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1119
769
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
  1120
\item is easy to implement in a functional language
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1121
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1122
\item the algorithm is already quite old; there is still
514
bca9f8889a48 updated
Christian Urban <urbanc@in.tum.de>
parents: 512
diff changeset
  1123
  work to be done to use it as a tokenizer (that is relatively new work)
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1124
769
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
  1125
\item we can prove its correctness\ldots (another video)
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1126
\end{itemize}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1127
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1128
\end{frame}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1129
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1130
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1131
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
566
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1132
\begin{frame}[c]
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1133
\frametitle{Negation of Regular Expr's}
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1134
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1135
\begin{itemize}
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1136
\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1137
\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1138
\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1139
\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
769
f9686b22db7e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 767
diff changeset
  1140
\end{itemize}\bigskip\bigskip\medskip\pause
566
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1141
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1142
Used often for recognising comments:
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1143
\[
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1144
\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1145
\]
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1146
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1147
\end{frame}
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1148
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1149
771
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1150
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1151
\begin{frame}[c]
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1152
\frametitle{The Specification for Matching}
566
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1153
771
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1154
\begin{bubble}[10cm]
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1155
\large
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1156
A regular expression \bl{$r$} matches a string~\bl{$s$} 
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1157
provided:
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1158
\begin{center}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1159
\bl{$s \in L(r)$} 
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1160
\end{center}\medskip
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1161
\end{bubble}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1162
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1163
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1164
\begin{center}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1165
\onslide<2>{\bl{\large$\forall\,r\,s.\;$}}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1166
\bl{$matcher\,s\,r$}  \;if and only if\  \bl{$s \in L(r)$} 
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1167
\end{center}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1168
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1169
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1170
\end{frame}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1171
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1172
  
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1173
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1174
\begin{frame}[c]
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1175
\frametitle{nullable and \boldmath$der$}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1176
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1177
The central properties:\bigskip\bigskip
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1178
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1179
\large
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1180
\begin{quote}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1181
  \onslide<3>{\bl{$\forall r.\phantom{\,c}\;$}}%
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1182
  \bl{$nullable(r)$} \;if and only if\; \bl{$[] \in L(r)$}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1183
\end{quote}\bigskip\bigskip\pause
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1184
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1185
\begin{quote}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1186
  \onslide<3>{\bl{$\forall r\,c.\;$}}%
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1187
  \bl{$L(der\,c\,r) \;=\; Der\,c\,(L(r))$}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1188
\end{quote}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1189
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1190
\end{frame}
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1191
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
770
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1192
  
566
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1193
  
b153c04834eb updated
Christian Urban <urbanc@in.tum.de>
parents: 565
diff changeset
  1194
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1195
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
  1196
\begin{frame}[t]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1197
\frametitle{Proofs about Rexps}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1198
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1199
Remember their inductive definition:\\[5cm]
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1200
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1201
\begin{textblock}{6}(5,5)
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1202
  \begin{tabular}{@ {}rrl}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
  1203
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
  1204
         & \bl{$\mid$} & \bl{$\ONE$}     \\
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1205
         & \bl{$\mid$} & \bl{$c$}            \\
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1206
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1207
         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1208
         & \bl{$\mid$} & \bl{$r^*$}          \\
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1209
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1210
  \end{textblock}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1211
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1212
If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1213
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1214
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1215
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1216
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1217
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1218
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1219
\frametitle{Proofs about Rexp (2)}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1220
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1221
\begin{itemize}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
  1222
\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1223
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1224
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1225
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1226
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1227
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1228
holds for \bl{$r$}.
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1229
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1230
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1231
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1232
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1233
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1234
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1235
\begin{frame}[c]
771
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1236
\frametitle{Proofs about Rexp}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1237
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1238
Assume \bl{$P(r)$} is the property:
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1239
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1240
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1241
\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1242
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1243
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1244
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1245
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1246
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1247
% begin{frame}[c]
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1248
% \begin{mybox3}{}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1249
%   der c (r*) def = (der c r) $\cdot$ (r*)\smallskip\\
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1250
%   Why in the example (slide 19) the first step is:
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1251
%   der a ((a $\cdot$ b) + b)* = (der a ((a $\cdot$ b) + b)) $\cdot$ r\smallskip\\
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1252
%   and not\smallskip\\
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1253
%   der a ((a $\cdot$ b) + b) = (der a ((a $\cdot$ b) + b)) · (r*)
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1254
% \end{mybox3}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1255
% \end{frame}
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1256
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1257
% \begin{frame}[c]
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1258
% \begin{mybox3}{}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1259
%   Would it be possible to find and go over a few examples from the
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1260
%   Brzozowski Algorithm, as it doesn't seem to be as simple as it
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1261
%   sounds?
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1262
% \end{mybox3}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1263
% \end{frame}
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1264
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1265
% \begin{frame}[c]
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1266
% \begin{mybox3}{}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1267
%   Is it possible to make a visual example of how using simp() function
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1268
%   on a (a*)*.b regular expression reduces its runtime? If not it's
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1269
%   fine. I am just very surprised that it is so efficient.
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1270
% \end{mybox3}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1271
% \end{frame}
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1272
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1273
% \begin{frame}[c]
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1274
% \begin{mybox3}{}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1275
%   Do you think the algorithm can be still improved (made faster)?
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1276
% \end{mybox3}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1277
% \end{frame}
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1278
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1279
% \begin{frame}[c]
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1280
% \begin{mybox3}{}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1281
%   Do the regular expression matchers in Python and Java 8 have more
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1282
%   features than the one implemented in this module? Or is there
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1283
%   another reason for their inefficiency?
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1284
% \end{mybox3}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1285
% \end{frame}
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1286
940
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1287
% \begin{frame}[c]
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1288
% \begin{mybox3}{}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1289
%   Will we discuss the broader Chomsky hierarchy of languages at some
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1290
%   point?
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1291
% \end{mybox3}
46eee459a999 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 930
diff changeset
  1292
% \end{frame}
778
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1293
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1294
\begin{frame}<1-8>[c]
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1295
\end{frame}
3e5f5d19f514 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 777
diff changeset
  1296
842
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1297
\begin{frame}[c]
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1298
\end{frame}
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1299
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1300
\begin{frame}[c]
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1301
\end{frame}
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1302
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1303
\begin{frame}[c]
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1304
\end{frame}
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1305
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1306
\begin{frame}<1-10>[c]
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1307
\end{frame}
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1308
1005
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1309
  
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1310
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1311
\begin{frame}[c]
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1312
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1313
\begin{center}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1314
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1315
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1316
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1317
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1318
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1319
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1320
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1321
\bl{$nullable (r^{\{n\}})$}      & \bl{$\dn$} & \bl{if $n = 0$ then \textit{true} else $nullable(r)$}\\  
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1322
\end{tabular}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1323
\end{center}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1324
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1325
\end{frame}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1326
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1327
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1328
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1329
\begin{frame}[c]
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1330
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1331
\begin{center}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1332
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1333
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1334
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1335
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1336
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1337
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1338
  & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\ 
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1339
  & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1340
  \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1341
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1342
  \bl{$\der\, c\, (r^{\{n\}})$}  & \bl{$\dn$} & \bl{if $n = 0$ then $\ZERO$ else $(\der\,c\,r) \cdot r^{\{n-1\}}$}\\
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1343
                                                
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1344
  \end{tabular}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1345
\end{center}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1346
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1347
\end{frame}
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1348
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
842
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1349
b53ac1bb5f43 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 782
diff changeset
  1350
1005
0ffb6e4de10a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1002
diff changeset
  1351
%%\end{document}
771
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1352
% below are slides for proving.
3a12e096f9a0 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 770
diff changeset
  1353
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1354
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1355
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1356
\frametitle{Proofs about Rexp (4)}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1357
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1358
\begin{center}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1359
\bl{\begin{tabular}{r@{\hspace{2mm}}c@{\hspace{2mm}}l}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
  1360
$rev(\ZERO)$   & $\dn$ & $\ZERO$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
  1361
$rev(\ONE)$      & $\dn$ & $\ONE$\\
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1362
$rev(c)$             & $\dn$ & $c$\\
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1363
$rev(r_1 + r_2)$     & $\dn$ & $rev(r_1) + rev(r_2)$\\
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1364
$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1365
$rev(r^*)$           & $\dn$ & $rev(r)^*$\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1366
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1367
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1368
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1369
We can prove
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1370
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1371
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1372
\bl{$L(rev(r)) = \{s^{-1} \;|\; s \in L(r)\}$}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1373
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1374
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1375
by induction on \bl{$r$}.
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1376
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1377
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1378
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1379
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1380
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1381
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1382
\begin{frame}[c]
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1383
\frametitle{Correctness Proof \\[-1mm]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1384
            for our Matcher}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1385
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1386
\begin{itemize}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1387
\item We started from
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1388
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1389
\begin{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1390
\begin{tabular}{rp{4cm}}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1391
  & \bl{$s \in L(r)$}\medskip\\
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1392
\bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1393
\end{tabular}
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1394
\end{center}\bigskip
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1395
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1396
\item if we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1397
have\bigskip
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1398
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1399
\begin{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1400
\begin{tabular}{rp{4cm}}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1401
\bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1402
\bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1403
\bl{$\dn$} & \bl{$matcher\,s\,r$}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1404
\end{tabular}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1405
\end{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1406
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1407
\end{itemize}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1408
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1409
\end{frame}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1411
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1412
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1413
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1414
\frametitle{Proofs about Rexp (5)}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1415
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1416
Let \bl{$Der\,c\,A$} be the set defined as
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1417
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1418
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1419
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1420
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1421
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1422
We can prove
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1423
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1424
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1425
\bl{$L(\der\,c\,r) = \Der\,c\,(L(r))$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1426
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1427
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1428
by induction on \bl{$r$}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1429
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1430
\end{frame}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1431
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1432
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1433
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1434
\begin{frame}[c]
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1435
\frametitle{Proofs about Strings}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1436
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1437
If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1438
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1439
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1440
\item \bl{$P$} holds for the empty string, and\medskip
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1441
\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1442
already holds for \bl{$s$}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1443
\end{itemize}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1444
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1445
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1446
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1447
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1448
\begin{frame}[c]
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1449
\frametitle{Proofs about Strings (2)}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1450
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1451
We can then prove
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1452
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1453
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1454
\bl{$\Ders\,s\,(L(r)) = L(\ders\,s\,r)$}  
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1455
\end{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1456
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1457
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1458
We can finally prove
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1459
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1460
\begin{center}
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1461
\bl{$matcher\,s\,r$}  if and only if  \bl{$s \in L(r)$} 
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1462
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1463
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1464
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1465
\end{frame}
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1466
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1467
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1468
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1469
\begin{frame}[c]
770
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1470
\frametitle{Coursework 1}
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1471
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1472
%%\underline{Strand 1:}
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1473
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1474
\begin{itemize}
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1475
\item Submission on Friday 16 October @ 18:00\medskip
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1476
\item source code needs to be submitted as well\medskip
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1477
\item you can re-use my Scala code from KEATS \\
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1478
  and use any programming language you like\medskip
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1479
\item \small https://nms.kcl.ac.uk/christian.urban/ProgInScala2ed.pdf\normalsize
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1480
\end{itemize}  
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1481
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1482
\end{frame}
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1483
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1484
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1485
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c563cf946497 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 769
diff changeset
  1486
\begin{frame}[c]
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1487
\frametitle{Epilogue}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1488
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1489
\footnotesize
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1490
\begin{center}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1491
\begin{tabular}{cc}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1492
\begin{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1493
\begin{axis}[
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1494
    title={\small{}Graph: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}},
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1495
    xlabel={$n$},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1496
    x label style={at={(1.04,0.0)}},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1497
    ylabel={time in secs},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1498
    enlargelimits=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1499
    xmax=7100000,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1500
    ytick={0,5,...,30},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1501
    ymax=33,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1502
    %scaled ticks=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1503
    axis lines=left,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1504
    width=5cm,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1505
    height=5cm, 
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1506
    legend entries={Scala V3, Scala V4},
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1507
    legend style={at={(0.1,-0.2)},anchor=north}]
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1508
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1509
\addplot[purple,mark=square*,mark options={fill=white}] table {re4.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1510
\end{axis}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1511
\end{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1512
&
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1513
\begin{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1514
\begin{axis}[
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1515
    title={\small{}Graph: \bl{$(a^*)^* \cdot b$}},
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1516
    xlabel={$n$},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1517
    x label style={at={(1.09,0.0)}},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1518
    ylabel={time in secs},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1519
    enlargelimits=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1520
    xmax=8100000,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1521
    ytick={0,5,...,30},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1522
    ymax=33,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1523
    %scaled ticks=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1524
    axis lines=left,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1525
    width=5cm,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1526
    height=5cm, 
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1527
    legend entries={Scala V3, Scala V4},
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1528
    legend style={at={(0.1,-0.2)},anchor=north}]
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1529
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1530
\addplot[purple,mark=square*,mark options={fill=white}] table {re4a.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1531
\end{axis}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1532
\end{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1533
\end{tabular}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1534
\end{center}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1535
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1536
\only<2->{\footnotesize
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1537
\begin{textblock}{9}(0.5,8)
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1538
\begin{bubble}[11.8cm]
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1539
\lstinputlisting[numbers=none]{../progs/app52.scala}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1540
\end{bubble}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1541
\end{textblock}} 
510
cu
parents: 507
diff changeset
  1542
 
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1543
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1544
\end{frame}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1545
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1546
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1547
\begin{frame}[c]
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1548
  \frametitle{Another Homework Question}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1549
  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1550
  \begin{itemize}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1551
  \item How many basic regular expressions are there to match
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1552
    the string \bl{$abcd$}\,?\pause
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1553
  \item How many if they cannot include
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1554
    \bl{$\ONE$} and \bl{$\ZERO$}\/?\pause
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1555
  \item How many if they are also not
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1556
    allowed to contain stars?\pause
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1557
  \item How many if they are also
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1558
        not allowed to contain \bl{$\_ + \_$}\/? 
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1559
  \end{itemize}  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1560
  
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1561
  \end{frame}
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1562
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1563
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1564
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1565
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1566
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1567
\frametitle{\begin{tabular}{c}\\[3cm]\huge\alert{Questions?}\end{tabular}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1568
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1569
%\bigskip
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1570
%homework (written exam 80\%)\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1571
%coursework (20\%; first one today)\\
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1572
%submission Fridays @ 18:00 -- accepted until Mondays
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1573
\mbox{}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1574
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1575
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1576
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1577
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1578
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1579
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1580
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1581
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1582
\frametitle{Last Week}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1583
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1584
Last week I showed you a regular expression matcher 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1585
that works provably correct in all cases (we only
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1586
started with the proving part though)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1587
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1588
\begin{center}
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1589
\bl{$matcher\,s\,r$} \;\;if and only if \;\; \bl{$s \in L(r)$}
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1590
\end{center}\bigskip\bigskip 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1591
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1592
\small
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1593
\textcolor{gray}{\mbox{}\hfill{}by Janusz Brzozowski (1964)}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1594
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1595
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1596
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1597
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1598
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1599
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1600
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1601
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1602
 
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1603
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1604
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1605
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1606
  \frametitle{Proofs about Rexp}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1607
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1608
  \begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1609
  \item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1610
  \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1611
  holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1612
  \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1613
  holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1614
  \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1615
  holds for \bl{$r$}.
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1616
  \end{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1617
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1618
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1619
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1620
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1621
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1622
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1623
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1624
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1625
We proved
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1626
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1627
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1628
\bl{$nullable(r)$} \;if and only if\;  \bl{$[] \in L(r)$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1629
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1630
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1631
by induction on the regular expression \bl{$r$}.\bigskip\pause
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1632
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1633
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1634
{\huge\bf\alert{Any Questions?}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1635
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1636
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1637
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1638
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1639
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1640
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1641
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1642
\frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1643
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1644
\begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1645
\item \bl{$P$} holds for \bl{$0$} and
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1646
\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1647
holds for \bl{$n$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1648
\end{itemize}\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1649
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1650
\begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1651
\item \bl{$P$} holds for \bl{$[]$} and
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1652
\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1653
holds for \bl{$s$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1654
\end{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1655
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1656
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1657
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1658
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1659
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1660
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1661
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1662
  \frametitle{Correctness Proof \\[-1mm]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1663
              for our Matcher}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1664
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1665
  \begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1666
  \item We started from
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1667
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1668
  \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1669
  \begin{tabular}{rp{4cm}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1670
    & \bl{$s \in L(r)$}\medskip\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1671
  \bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1672
  \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1673
  \end{center}\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1674
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1675
  \item \textbf{\alert{if}} we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1676
  have\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1677
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1678
  \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1679
  \begin{tabular}{rp{4cm}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1680
  \bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1681
  \bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
764
6718ef6143b8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 763
diff changeset
  1682
  \bl{$\dn$} & \bl{$matcher\,s\,r$}
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1683
  \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1684
  \end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1685
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1686
  \end{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1687
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1688
  \end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1689
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1690
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1691
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1692
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1693
We need to prove
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1694
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1695
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1696
\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1697
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1698
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1699
also by induction on the regular expression \bl{$r$}.
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1700
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1701
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1702
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1703
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 646
diff changeset
  1704
638
0367aa7c764b updated
Christian Urban <urbanc@in.tum.de>
parents: 630
diff changeset
  1705
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1706
\end{document}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1707
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1708
%%% Local Variables:  
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1709
%%% mode: latex
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1710
%%% TeX-master: t
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1711
%%% End: 
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1712