slides/slides04.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Fri, 26 Feb 2021 08:47:18 +0000
changeset 824 284ac979f289
parent 794 95b3e918253f
child 847 da2320360f12
permissions -rw-r--r--
updated while tests
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
661
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
     1
% !TEX program = xelatex
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
     2
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
     3
\usepackage{../slides}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
     4
\usepackage{../graphics}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 145
diff changeset
     5
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 145
diff changeset
     6
\usepackage{../data}
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
     8
\hfuzz=220pt 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
     9
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
    10
\pgfplotsset{compat=1.11}
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 144
diff changeset
    11
722
14914b57e207 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    12
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    13
\usepackage{tcolorbox}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    14
\newtcolorbox{mybox}{colback=red!5!white,colframe=red!75!black}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    15
\newtcolorbox{mybox2}[1]{colback=red!5!white,colframe=red!75!black,fonttitle=\bfseries,title=#1}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    16
\newtcolorbox{mybox3}[1]{colback=Cyan!5!white,colframe=Cyan!75!black,fonttitle=\bfseries,title=#1}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    17
722
14914b57e207 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    18
% a hand written lexer for SML
14914b57e207 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    19
% https://ponyo.org/
14914b57e207 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    20
% https://github.com/eatonphil/ponyo/blob/master/src/Sml/Lexer.sml
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    21
\beamertemplateballitem
722
14914b57e207 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    22
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
    23
\newcommand{\bl}[1]{\textcolor{blue}{#1}}  
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
    25
\renewcommand{\slidecaption}{CFL 04, King's College London}
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
\begin{document}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
    30
\begin{frame}[t]
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
\frametitle{%
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
  \begin{tabular}{@ {}c@ {}}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
  \\[-3mm]
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
    34
  \LARGE Compilers and \\[-2mm] 
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    35
  \LARGE Formal Languages\\[3mm] 
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
  \end{tabular}}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
  \normalsize
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
  \begin{center}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
  \begin{tabular}{ll}
660
3c5ed5e45f57 updated
Christian Urban <urbanc@in.tum.de>
parents: 581
diff changeset
    41
    Email:  & christian.urban at kcl.ac.uk\\
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    42
    %Office Hours: & Thursdays 12 -- 14\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    43
    %Location: & N7.07 (North Wing, Bush House)\\
660
3c5ed5e45f57 updated
Christian Urban <urbanc@in.tum.de>
parents: 581
diff changeset
    44
    Slides \& Progs: & KEATS (also homework is there)\\  
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
  \end{tabular}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
  \end{center}
660
3c5ed5e45f57 updated
Christian Urban <urbanc@in.tum.de>
parents: 581
diff changeset
    47
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    48
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    49
  \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    50
    \begin{tikzpicture}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    51
      \node[drop shadow,fill=white,inner sep=0pt] 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    52
      {\footnotesize\rowcolors{1}{capri!10}{white}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    53
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    54
          1 Introduction, Languages          & 6 While-Language \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    55
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    56
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    57
          \cellcolor{blue!50}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    58
          4 Lexing, Tokenising               & 9 Optimisations \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    59
          5 Grammars, Parsing                & 10 LLVM \\ \hline
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    60
        \end{tabular}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    61
      };
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    62
    \end{tikzpicture}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    63
  \end{center}
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
    64
\end{frame}
574
bd4f144326c7 updated
Christian Urban <urbanc@in.tum.de>
parents: 522
diff changeset
    65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
bd4f144326c7 updated
Christian Urban <urbanc@in.tum.de>
parents: 522
diff changeset
    66
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    67
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
785
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    69
%\begin{frame}[c]
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    70
%\frametitle{Coursework}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    71
%
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    72
%\begin{itemize}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    73
%\item \bl{$\der\,c\,(r^+) \dn \der\,c (r\cdot r^*)$}\quad given
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    74
%that \bl{$r^+ \dn r\cdot r^*$}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    75
%\end{itemize}\bigskip\pause
661
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    76
785
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    77
%\begin{center}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    78
%\begin{tabular}{lcl}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    79
%\bl{$\der\,c\,(r\cdot r^*)$} & \bl{$\dn$} & 
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    80
%\only<2-4>{if \bl{$nullable\,r$}}%
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    81
%\only<5>{\bl{$(\der\,c\,r)\cdot r^*$}}\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    82
% & & 
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    83
% \only<2>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, \der\,c\,(r^*)$}}%
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    84
% \only<3>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, (\der\,c\,r)\cdot r^*$}}%
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    85
% \only<4>{then \bl{$(\der\,c\,r)\cdot r^*$}}\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    86
% & & \only<2-4>{else \bl{$(\der\,c\,r)\cdot r^*$}}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    87
%\end{tabular}  
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    88
%\end{center}  
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    89
%\end{frame}
661
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    91
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
785
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    93
%\begin{frame}[c]
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    94
%  \frametitle{Coursework (2)}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    95
%  
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    96
%  \begin{itemize}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    97
%  \item \bl{\texttt{CFUN(f: Char => Boolean)}}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    98
%  \end{itemize}\medskip
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
    99
%
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   100
%  \begin{center}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   101
%  \begin{tabular}{l}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   102
%  \bl{\texttt{CHAR(c: Char)}} \bl{$\dn$}\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   103
%     \quad\bl{\texttt{CFUN(\_ == c)}}\medskip\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   104
%  \bl{\texttt{RANGE(cs: Set[Char])}} \bl{$\dn$}\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   105
%     \quad\bl{\texttt{CFUN(cs.contains(\_))}}\medskip\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   106
%  \bl{\texttt{ALL}} \bl{$\dn$}\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   107
%     \quad\bl{\texttt{CFUN((c: Char) => true)}}\\
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   108
%  \end{tabular}  
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   109
%  \end{center}  
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   110
%\end{frame}
661
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   111
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
   112
     
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   113
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   114
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   115
\begin{frame}[c]
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   116
\frametitle{The Goal of this Course}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   117
\mbox{}\\[-26mm]\mbox{}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   118
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   119
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   120
  \begin{tikzpicture}[scale=1,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   121
                      node/.style={
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   122
                      rectangle,rounded corners=3mm,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   123
                      very thick,draw=black!50,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   124
                      minimum height=18mm, minimum width=20mm,
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
   125
                      top color=white,bottom color=black!20,drop shadow}]
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   126
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   127
  \node at (3.05, 1.8) {\Large\bf Write a compiler};
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   128
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   129
  \node (0) at (-2.3,0) {}; 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   130
  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   131
  \node (A) at (0,0)  [node] {};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   132
  \node [below right] at (A.north west) {lexer};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   133
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   134
  \node (B) at (3,0)  [node] {};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   135
  \node [below right=1mm] at (B.north west) 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   136
    {\mbox{}\hspace{-1mm}parser};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   137
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   138
  \node (C) at (6,0)  [node] {};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   139
  \node [below right] at (C.north west) 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   140
    {\mbox{}\hspace{-1mm}code gen};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   141
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   142
  \node (1) at (8.4,0) {}; 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   143
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   144
  \draw [->,line width=4mm] (0) -- (A); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   145
  \draw [->,line width=4mm] (A) -- (B); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   146
  \draw [->,line width=4mm] (B) -- (C); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   147
  \draw [->,line width=4mm] (C) -- (1); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   148
  \end{tikzpicture}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   149
  \end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   150
  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   151
Today a lexer.  
579
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   152
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   153
\only<2>{
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   154
\begin{textblock}{1}(6,9.8)
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   155
\begin{tabular}{c}
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   156
\includegraphics[scale=0.13]{../pics/rosetta.jpg}\\[-2mm]
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   157
\footnotesize lexing $\Rightarrow$ recognising words (Stone of Rosetta)
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   158
\end{tabular}
1a521448d211 updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   159
\end{textblock}}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   160
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   161
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   162
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   163
\begin{frame}[c]
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   164
\frametitle{Regular Expressions}
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   165
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   166
In programming languages they are often used to recognise:\medskip
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   167
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   168
\begin{itemize}
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   169
\item operands, digits
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   170
\item identifiers
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   171
\item numbers (non-leading zeros)
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   172
\item keywords
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   173
\item comments
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   174
\end{itemize}\bigskip
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   175
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   176
\mbox{}\hfill\bl{\url{http://www.regexper.com}}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   177
\end{frame}
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   178
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   179
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   180
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   181
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   182
\begin{frame}[c]
521
95af9beb4b7f updated
cu
parents: 520
diff changeset
   183
\frametitle{Lexing: Test Case}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   184
785
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   185
\mbox{\lstinputlisting[language=While]{../progs/while-tests/fib.while}}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   186
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   187
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   188
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   189
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   190
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   191
%\begin{frame}[c]
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   192
%\frametitle{?? Test Case}
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   193
%
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   194
%\mbox{\lstinputlisting[language=While]{../progs/collatz.while}}
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   195
%
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   196
%\end{frame}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   197
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   198
35
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   199
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   200
\begin{frame}[t]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   201
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   202
\tt
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   203
\begin{center}\large
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   204
\code{"if true then then 42 else +"}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   205
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   206
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   207
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   208
\begin{tabular}{@{}l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   209
KEYWORD: \\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   210
\hspace{5mm}{if}, {then}, {else},\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   211
WHITESPACE:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   212
\hspace{5mm}{" "}, {$\backslash$n},\\ 
521
95af9beb4b7f updated
cu
parents: 520
diff changeset
   213
IDENTIFIER:\\
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   214
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   215
NUM:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   216
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   217
OP:\\
521
95af9beb4b7f updated
cu
parents: 520
diff changeset
   218
\hspace{5mm}+, -, *, \%, <, <=\\
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   219
COMMENT:\\
277
8eb3261294ba updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   220
\hspace{5mm}{$\slash$*} $\cdot$ $\sim$(ALL$^*$ $\cdot$ (*$\slash$) $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   221
\end{tabular}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   222
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   223
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   224
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   225
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   226
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   227
\begin{frame}[t]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   228
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   229
\tt
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   230
\begin{center}\large
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   231
\code{"if true then then 42 else +"}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   232
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   233
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   234
\only<1>{
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   235
\small\begin{tabular}{l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   236
KEYWORD(if),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   237
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   238
IDENT(true),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   239
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   240
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   241
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   242
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   243
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   244
NUM(42),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   245
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   246
KEYWORD(else),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   247
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   248
OP(+)
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   249
\end{tabular}}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   250
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   251
\only<2>{
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   252
\small\begin{tabular}{l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   253
KEYWORD(if),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   254
IDENT(true),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   255
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   256
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   257
NUM(42),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   258
KEYWORD(else),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   259
OP(+)
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   260
\end{tabular}}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   261
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   262
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   263
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   264
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   265
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   266
\begin{frame}[c]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   267
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   268
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   269
There is one small problem with the tokenizer. How should we 
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   270
tokenize\ldots?
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   271
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   272
\begin{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   273
\large\code{"x-3"}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   274
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   275
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   276
\tt
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   277
\begin{tabular}{@{}l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   278
ID: \ldots\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   279
OP:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   280
\hspace{5mm}\texttt{"+"}, \texttt{"-"}\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   281
NUM:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   282
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {''0''}\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   283
NUMBER:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   284
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   285
\end{tabular}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   286
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   287
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   288
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   289
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   290
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   291
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   292
The same problem with\medskip
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   293
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   294
\[
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   295
\bl{(ab + a) \cdot (c + bc)}
353
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   296
\]\medskip
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   297
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   298
and the string $\bl{abc}$.\pause\bigskip
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   299
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   300
Or, keywords are \code{if} etc and identifiers are 
353
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   301
letters followed by ``letters + numbers + \_''$^*$
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   302
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   303
\[
785
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   304
\bl{\texttt{if}}\qquad\bl{\texttt{iffoo}}
353
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   305
\]
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   306
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   307
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   308
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   309
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   310
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   311
\begin{frame}[c]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   312
\frametitle{POSIX: Two Rules}
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
38
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   314
\begin{itemize}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   315
\item Longest match rule (``maximal munch rule''): The 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   316
longest initial substring matched by any regular expression is taken
278
c7890e677e06 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   317
as the next token.\bigskip
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   318
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   319
\item Rule priority:
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   320
For a particular longest initial substring, the first regular
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   321
expression that can match determines the token.
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   322
\end{itemize}\bigskip\bigskip\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   323
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   324
\small
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   325
\hfill most posix matchers are buggy\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   326
\footnotesize
353
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   327
\hfill 
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   328
\url{http://www.haskell.org/haskellwiki/Regex_Posix}
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   329
\smallskip\pause
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   330
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   331
\hfill \small traditional lexers are fast, but hairy
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   332
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   333
%\url{http://www.technologyreview.com/tr10/?year=2011}  
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   334
%finite deterministic automata/ nondeterministic automaton
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   335
%\item problem with infix operations, for example i-12
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   336
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   337
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   338
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   339
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   340
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   341
\begin{frame}[c]
581
19de761b69e9 updated
Christian Urban <urbanc@in.tum.de>
parents: 579
diff changeset
   342
\frametitle{Sulzmann \& Lu Matcher}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   343
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   344
We want to match the string \bl{$abc$} using \bl{$r_1$}:
38
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   345
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   346
\begin{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   347
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   348
\node (r1)  {\bl{$r_1$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   349
\node (r2) [right=of r1] {\bl{$r_2$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   350
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   351
\node (r3) [right=of r2] {\bl{$r_3$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   352
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   353
\node (r4) [right=of r3] {\bl{$r_4$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   354
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
521
95af9beb4b7f updated
cu
parents: 520
diff changeset
   355
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable?$}}};\pause
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   356
\node (v4) [below=of r4] {\bl{$v_4$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   357
\draw[->,line width=1mm]  (r4) -- (v4);\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   358
\node (v3) [left=of v4] {\bl{$v_3$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   359
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   360
\node (v2) [left=of v3] {\bl{$v_2$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   361
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   362
\node (v1) [left=of v2] {\bl{$v_1$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   363
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   364
\draw[->,line width=0.5mm]  (r3) -- (v3);
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   365
\draw[->,line width=0.5mm]  (r2) -- (v2);
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   366
\draw[->,line width=0.5mm]  (r1) -- (v1);
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   367
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   368
\end{tikzpicture}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   369
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   370
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   371
\end{frame}
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   374
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   375
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   376
\frametitle{Regexes and Values}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   377
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   378
Regular expressions and their corresponding values:
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   379
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   380
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   381
\begin{columns}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   382
\begin{column}{3cm}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   383
\begin{tabular}{@{}rrl@{}}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   384
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   385
           & \bl{$\mid$} & \bl{$\ONE$}   \\
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   386
           & \bl{$\mid$} & \bl{$c$}          \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   387
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   388
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   389
  \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   390
           & \bl{$\mid$} & \bl{$r^*$}         \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   391
  \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   392
  \end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   393
\end{column}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   394
\begin{column}{3cm}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   395
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   396
  \bl{$v$} & \bl{$::=$}  & \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   397
           &             & \bl{$Empty$}   \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   398
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
279
f406c6677b8c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 278
diff changeset
   399
           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   400
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   401
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   402
           & \bl{$\mid$} & \bl{$Stars\,[]$}      \\
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   403
           & \bl{$\mid$} & \bl{$Stars\,[v_1,\ldots\,v_n]$} \\
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   404
  \end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   405
\end{column}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   406
\end{columns}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   407
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   408
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   409
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   411
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   412
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   413
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   414
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   415
{\small\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   416
xleftmargin=-5mm] {../progs/app01.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   417
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   418
{\small\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   419
xleftmargin=-5mm] {../progs/app02.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   420
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   421
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   422
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   423
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   424
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   425
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   426
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   427
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   428
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   429
\begin{textblock}{10}(3,5)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   430
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   431
\node (r1)  {\bl{$r_1$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   432
\node (r2) [right=of r1] {\bl{$r_2$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   433
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   434
\node (r3) [right=of r2] {\bl{$r_3$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   435
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   436
\node (r4) [right=of r3] {\bl{$r_4$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   437
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   438
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   439
\node (v4) [below=of r4] {\bl{$v_4$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   440
\draw[->,line width=1mm]  (r4) -- (v4);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   441
\node (v3) [left=of v4] {\bl{$v_3$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   442
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   443
\node (v2) [left=of v3] {\bl{$v_2$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   444
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   445
\node (v1) [left=of v2] {\bl{$v_1$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   446
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   447
\draw[->,line width=0.5mm]  (r3) -- (v3);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   448
\draw[->,line width=0.5mm]  (r2) -- (v2);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   449
\draw[->,line width=0.5mm]  (r1) -- (v1);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   450
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   451
\end{tikzpicture}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   452
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   453
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   454
\only<1->{
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   455
\begin{textblock}{6}(1,0.8)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   456
\begin{bubble}[6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   457
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   458
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   459
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   460
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   461
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   462
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   463
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   464
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   465
\end{textblock}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   466
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   467
\only<2->{
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   468
\begin{textblock}{6}(5,11.4)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   469
\begin{bubble}[7.6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   470
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   471
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   472
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   473
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   474
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   475
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   476
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   477
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   478
\end{textblock}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   479
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   480
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   481
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   482
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   483
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   484
\frametitle{Flatten}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   485
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   486
Obtaining the string underlying a value:
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   487
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   488
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   489
\begin{tabular}{lcl}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   490
  \bl{$|Empty|$}     & \bl{$\dn$} & \bl{$[]$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   491
  \bl{$|Char(c)|$}   & \bl{$\dn$} & \bl{$[c]$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   492
  \bl{$|Left(v)|$}   & \bl{$\dn$} & \bl{$|v|$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   493
  \bl{$|Right(v)|$}  & \bl{$\dn$} & \bl{$|v|$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   494
  \bl{$|Seq(v_1,v_2)|$}& \bl{$\dn$} & \bl{$|v_1| \,@\, |v_2|$}\\
786
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   495
  \bl{$|Stars\,[v_1,\ldots ,v_n]|$} & \bl{$\dn$} & \bl{$|v_1| \,@\ldots @\, |v_n|$}\\
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   496
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   497
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   498
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   499
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   500
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   501
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   502
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   503
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   504
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   505
\begin{textblock}{10}(3,5)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   506
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   507
\node (r1)  {\bl{$r_1$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   508
\node (r2) [right=of r1] {\bl{$r_2$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   509
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   510
\node (r3) [right=of r2] {\bl{$r_3$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   511
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   512
\node (r4) [right=of r3] {\bl{$r_4$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   513
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   514
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   515
\node (v4) [below=of r4] {\bl{$v_4$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   516
\draw[->,line width=1mm]  (r4) -- (v4);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   517
\node (v3) [left=of v4] {\bl{$v_3$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   518
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   519
\node (v2) [left=of v3] {\bl{$v_2$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   520
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   521
\node (v1) [left=of v2] {\bl{$v_1$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   522
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   523
\draw[->,line width=0.5mm]  (r3) -- (v3);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   524
\draw[->,line width=0.5mm]  (r2) -- (v2);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   525
\draw[->,line width=0.5mm]  (r1) -- (v1);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   526
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   527
\end{tikzpicture}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   528
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   529
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   530
\begin{textblock}{6}(1,0.8)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   531
\begin{bubble}[6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   532
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   533
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   534
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   535
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   536
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   537
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   538
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   539
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   540
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   541
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   542
\begin{textblock}{6}(1,11.4)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   543
\begin{bubble}[7.6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   544
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   545
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   546
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   547
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   548
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   549
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   550
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   551
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   552
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   553
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   554
\begin{textblock}{6}(12,11.4)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   555
\begin{bubble}[2cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   556
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   557
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   558
\bl{$|v_1|$}: & \bl{$abc$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   559
\bl{$|v_2|$}: & \bl{$bc$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   560
\bl{$|v_3|$}: & \bl{$c$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   561
\bl{$|v_4|$}: & \bl{$[]$}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   562
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   563
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   564
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   565
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   566
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   567
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   568
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   569
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   570
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   571
\begin{frame}[c]
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   572
  \frametitle{Mkeps}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   573
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   574
  Finding a (posix) value for recognising the empty string:
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   575
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   576
  \begin{center}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   577
  \begin{tabular}{lcl}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   578
    \bl{$mkeps\,(\ONE)$}  & \bl{$\dn$}  & \bl{$Empty$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   579
    \bl{$mkeps\,(r_1 + r_2)$} & \bl{$\dn$}  & \bl{if $nullable(r_1)$}  \\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   580
                            &             & \bl{then $Left(mkeps(r_1))$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   581
                            &             & \bl{else $Right(mkeps(r_2))$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   582
    \bl{$mkeps\,(r_1 \cdot r_2)$}  & \bl{$\dn$} & \bl{$Seq(mkeps(r_1),mkeps(r_2))$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   583
    \bl{$mkeps\,(r^*)$}      & \bl{$\dn$} & \bl{$Stars\,[]$}  \\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   584
  \end{tabular}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   585
  \end{center}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   586
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   587
  \end{frame}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   588
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
785
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   589
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   590
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   591
\begin{frame}[c]
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   592
  \frametitle{Inject}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   593
\large
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   594
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   595
  \begin{center}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   596
\begin{tikzpicture}[scale=3,node distance=1.2cm,
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   597
                    every node/.style={minimum size=7mm}]
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   598
\node (r)  {$r$};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   599
\node (rd) [right=of r]{$r_{der}$};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   600
\draw[->,line width=1mm](r)--(rd) node[above,midway] {$\der\,c$};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   601
\node (vd) [below=of r2]{$v_{der}$};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   602
\draw[->,line width=1mm](rd) -- (vd);
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   603
\node (v) [left=of vd] {$v$};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   604
\draw[->,line width=1mm](vd)--(v) node[below,midway] {$inj\,c$};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   605
\draw[->,line width=0.5mm,dotted](r) -- (v) node[left,midway,red] {\bf ?};
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   606
\end{tikzpicture}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   607
\end{center}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   608
\end{frame}
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   609
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
faa4489267d5 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   610
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   611
  
786
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   612
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   613
  \begin{frame}[c]
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   614
  \frametitle{Inject}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   615
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   616
  Injecting (``Adding'') a character to a value\\[-12mm]\mbox{}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   617
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   618
  \begin{center}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   619
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   620
    \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   621
    \bl{$inj\,(r_1 + r_2)\,c\,(Left(v))$} & \bl{$\dn$}  & \bl{$Left(inj\,r_1\,c\,v)$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   622
    \bl{$inj\,(r_1 + r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Right(inj\,r_2\,c\,v)$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   623
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Seq(v_1,v_2))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   624
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Left(Seq(v_1,v_2)))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   625
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   626
    \bl{$inj\,(r^*)\,c\,(Seq(v,Stars\,vs))$} & \bl{$\dn$}  & \bl{$Stars\,(inj\,r\,c\,v\,::\,vs)$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   627
  \end{tabular}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   628
  \end{center}\bigskip
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   629
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   630
  \footnotesize
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   631
  \begin{tabular}{l@{\hspace{2mm}}l}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   632
  \bl{$inj$}: & 1st arg $\mapsto$ a rexp; 2nd arg $\mapsto$ a character; 
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   633
  3rd arg $\mapsto$ a value\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   634
              & result $\mapsto$ a value 
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   635
  \end{tabular}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   636
  \end{frame}
786
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   637
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   638
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   639
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   640
  \begin{frame}[t]
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   641
  
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   642
  \begin{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   643
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   644
    \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   645
  \end{tabular}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   646
  \end{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   647
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   648
\end{frame}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   649
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   650
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   651
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   652
  \begin{frame}[t]
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   653
  
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   654
  \begin{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   655
    \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   656
    \bl{$inj\,(r_1 + r_2)\,c\,(Left(v))$} & \bl{$\dn$}  & \bl{$Left(inj\,r_1\,c\,v)$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   657
    \bl{$inj\,(r_1 + r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Right(inj\,r_2\,c\,v)$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   658
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   659
  \end{tabular}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   660
  \end{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   661
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   662
\end{frame}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   663
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   664
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   665
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   666
  \begin{frame}[t]
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   667
  
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   668
  \begin{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   669
    \begin{tabular}{@{\hspace{-8mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   670
    \\[-15mm]  
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   671
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Seq(v_1,v_2))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   672
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Left(Seq(v_1,v_2)))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   673
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\  
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   674
  \end{tabular}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   675
\end{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   676
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   677
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   678
\begin{textblock}{13}(1,13.4)
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   679
\begin{bubble}[13cm]
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   680
\small
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   681
\bl{$\der\, c\, (r_1 \cdot r_2)$} \bl{$\dn$} \bl{\textbf{if} $nullable (r_1)$}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   682
 \bl{\textbf{then} $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   683
 \bl{\textbf{else} $(\der\, c\, r_1) \cdot r_2$}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   684
\end{bubble}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   685
\end{textblock}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   686
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   687
\end{frame}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   688
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   689
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   690
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   691
  \begin{frame}[t]
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   692
  
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   693
  \begin{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   694
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   695
    \bl{$inj\,(r^*)\,c\,(Seq(v,Stars\,vs))$} & \bl{$\dn$}  & \bl{$Stars\,(inj\,r\,c\,v\,::\,vs)$}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   696
  \end{tabular}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   697
  \end{center}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   698
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   699
\end{frame}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   700
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   701
662
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   702
  
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   703
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   704
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   705
\frametitle{Lexing}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   706
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   707
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   708
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   709
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
786
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   710
  \bl{$lex\,r\,a::s$} & \bl{$\dn$}  & \bl{$inj\,r\,a\,lex(der(a,r), s)$}\\
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   711
\end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   712
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   713
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   714
\footnotesize
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   715
\bl{$lex$}: returns a value
280
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   716
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   717
\begin{center}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   718
\begin{tikzpicture}[scale=2,node distance=1.0cm,every node/.style={minimum size=6mm}]
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   719
\node (r1)  {\bl{$r_1$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   720
\node (r2) [right=of r1] {\bl{$r_2$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   721
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   722
\node (r3) [right=of r2] {\bl{$r_3$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   723
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   724
\node (r4) [right=of r3] {\bl{$r_4$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   725
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   726
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   727
\node (v4) [below=of r4] {\bl{$v_4$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   728
\draw[->,line width=1mm]  (r4) -- (v4);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   729
\node (v3) [left=of v4] {\bl{$v_3$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   730
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   731
\node (v2) [left=of v3] {\bl{$v_2$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   732
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   733
\node (v1) [left=of v2] {\bl{$v_1$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   734
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   735
\draw[->,line width=0.5mm]  (r3) -- (v3);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   736
\draw[->,line width=0.5mm]  (r2) -- (v2);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   737
\draw[->,line width=0.5mm]  (r1) -- (v1);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   738
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   739
\end{tikzpicture}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   740
\end{center}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   741
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   742
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   743
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   744
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   745
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   746
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   747
\frametitle{Records}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   748
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   749
\begin{itemize}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   750
\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   751
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   752
\item \bl{$nullable(x:r) \dn nullable(r)$}
671
83e38043ed78 updated
Christian Urban <urbanc@in.tum.de>
parents: 662
diff changeset
   753
\item \bl{$der\,c\,(x:r) \dn der\,c\,r$}
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   754
\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   755
\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   756
\end{itemize}\bigskip\bigskip\pause
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   757
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   758
\small
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   759
for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   760
786
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   761
\begin{textblock}{6}(10,10)
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   762
\begin{bubble}[2cm]
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   763
\small
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   764
\begin{tabular}{l}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   765
  \bl{$(id : r_{id})$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   766
  \bl{$(key : r_{key})$}\\
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   767
\end{tabular}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   768
\end{bubble}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   769
\end{textblock}
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   770
da2488db453e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   771
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   772
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   773
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   774
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   775
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   776
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   777
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   778
\begin{itemize}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   779
\item A regular expression for email addresses
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   780
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   781
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   782
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   783
(name: \bl{$[a\mbox{-}z0\mbox{-}9\_\!\_\,.-]^+$})\bl{$\cdot @\cdot$}\\ 
794
95b3e918253f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 792
diff changeset
   784
\qquad(domain: \bl{$[a\mbox{-}z0\mbox{-}9\,-]^+$}) \bl{$\cdot .\cdot$}\\ 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   785
\qquad\qquad(top\_level: \bl{$[a\mbox{-}z\,.]^{\{2,6\}}$})
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   786
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   787
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   788
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   789
\bl{\[
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   790
\texttt{christian.urban@kcl.ac.uk}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   791
\]}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   792
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   793
\item the result environment:
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   794
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   795
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   796
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   797
\bl{$[(name:\texttt{christian.urban}),$}\\ 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   798
\bl{$\phantom{[}(domain:\texttt{kcl}),$}\\ 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   799
\bl{$\phantom{[}(top\_level:\texttt{ac.uk})]$}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   800
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   801
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   802
\end{itemize}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   803
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   804
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   805
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   806
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   807
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   808
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   809
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   810
\frametitle{While Tokens}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   811
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   812
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   813
\begin{tabular}{rcl}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   814
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   815
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   816
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   817
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   818
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   819
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   820
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   821
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   822
\end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   823
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   824
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   825
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   826
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   827
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   828
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   829
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   830
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   831
\begin{frame}[c]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   832
\frametitle{Simplification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   833
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   834
\begin{itemize}
522
65bef2eccd42 updated
cu
parents: 521
diff changeset
   835
\item If we simplify after the derivative, then we are building the
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   836
value for the simplified regular expression, but \alert{\textbf{not}} for the original
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   837
regular expression.
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   838
\end{itemize}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   839
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   840
\begin{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   841
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   842
\node (r1)  {\bl{$r_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   843
\node (r2) [right=of r1] {\bl{$r_2$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   844
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   845
\node (r3) [right=of r2] {\bl{$r_3$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   846
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   847
\node (r4) [right=of r3] {\bl{$r_4$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   848
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   849
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   850
\node (v4) [below=of r4] {\bl{$v_4$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   851
\draw[->,line width=1mm]  (r4) -- (v4);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   852
\node (v3) [left=of v4] {\bl{$v_3$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   853
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   854
\node (v2) [left=of v3] {\bl{$v_2$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   855
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   856
\node (v1) [left=of v2] {\bl{$v_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   857
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   858
\draw[->,line width=0.5mm]  (r3) -- (v3);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   859
\draw[->,line width=0.5mm]  (r2) -- (v2);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   860
\draw[->,line width=0.5mm]  (r1) -- (v1);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   861
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   862
\end{tikzpicture}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   863
\end{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   864
792
34132a854d03 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 788
diff changeset
   865
\small\pause
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   866
\hspace{4.5cm}\bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   867
$\mapsto$
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   868
\bl{$\ONE$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   869
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   870
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   871
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   872
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   873
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   874
\begin{frame}[c]
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   875
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   876
  Normally we would have
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   877
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   878
  \begin{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   879
  \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   880
  \end{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   881
452
b93f4d2aeee1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 451
diff changeset
   882
  and answer how this regular expression matches the empty string
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   883
  with the value
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   884
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   885
  \begin{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   886
  \bl{$Right(Right(Empty))$}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   887
  \end{center}\bigskip
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   888
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   889
  But now we simplify this to \bl{$\ONE$} and would produce \bl{$Empty$} (see \textit{mkeps}).
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   890
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   891
\end{frame}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   892
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   893
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   894
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   895
\begin{frame}[c]
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   896
\frametitle{Rectification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   897
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   898
\def\arraystretch{1.05}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   899
\begin{center}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   900
\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l@{\hspace{8mm}}l}
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   901
& & & \hspace{5mm}rectification \\
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   902
& & & \hspace{5mm}functions:\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   903
\bl{$r \cdot \ZERO$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   904
\bl{$\ZERO \cdot r$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   905
\bl{$r \cdot \ONE$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Seq(f_1\,v, f_2\,Empty)$}\\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   906
\bl{$\ONE \cdot r$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Seq(f_1\,Empty, f_2\,v)$}\\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   907
\bl{$r + \ZERO$} & $\mapsto$ & \bl{$r$}   & \bl{$\lambda f_1\,f_2\,v.\, Left(f_1\,v)$}\\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   908
\bl{$\ZERO + r$} & $\mapsto$ & \bl{$r$}   & \bl{$\lambda f_1\,f_2\,v.\, Right(f_2\,v)$}\\
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   909
\bl{$r + r$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Left(f_1\,v)$}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   910
\end{tabular}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   911
\end{center}\medskip\pause
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   912
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   913
\small
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   914
old \bl{$simp$} returns a rexp;\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   915
new \bl{$simp$} returns a rexp and a rectification~function.
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   916
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   917
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   918
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   919
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   920
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   921
\begin{frame}[c]
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
   922
\frametitle{Rectification $\_ + \_$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   923
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   924
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   925
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   926
\bl{$simp(r)$}:\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   927
\quad case \bl{$r = r_1 + r_2$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   928
\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   929
\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   930
\qquad case \bl{$r_{1s} = \ZERO$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   931
       return \bl{$(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   932
\qquad case \bl{$r_{2s} = \ZERO$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   933
       return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   934
\qquad case \bl{$r_{1s} = r_{2s}$}:
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   935
       return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   936
\qquad otherwise: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   937
       return \bl{$(r_{1s} + r_{2s}, f_{alt}(f_{1s}, f_{2s}))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   938
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   939
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   940
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   941
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   942
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   943
\begin{tabular}{l@{\hspace{1mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   944
\bl{$f_{alt}(f_1, f_2) \dn$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   945
\qquad \bl{$\lambda v.\,$} case \bl{$v = Left(v')$}: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   946
      & return \bl{$Left(f_1(v'))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   947
\qquad \phantom{$\lambda v.\,$} case \bl{$v = Right(v')$}: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   948
      & return \bl{$Right(f_2(v'))$}\\      
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   949
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   950
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   951
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   952
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   953
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   954
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   955
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   956
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   957
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   958
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   959
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   960
xleftmargin=-5mm] {../progs/app05.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   961
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   962
\end{frame}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   963
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   964
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   965
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   966
\begin{frame}[c]
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
   967
\frametitle{Rectification $\_ \cdot \_$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   968
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   969
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   970
\begin{tabular}{@{\hspace{-3mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   971
\bl{$simp(r)$}:\ldots\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   972
\quad case \bl{$r = r_1 \cdot r_2$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   973
\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   974
\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   975
\qquad case \bl{$r_{1s} = \ZERO$}: 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   976
       return \bl{$(\ZERO, f_{error})$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   977
\qquad case \bl{$r_{2s} = \ZERO$}: 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   978
       return \bl{$(\ZERO, f_{error})$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   979
\qquad case \bl{$r_{1s} = \ONE$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   980
return \bl{$(r_{2s}, \lambda v. \,Seq(f_{1s}(Empty), f_{2s}(v)))$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   981
\qquad case \bl{$r_{2s} = \ONE$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   982
return \bl{$(r_{1s}, \lambda v. \,Seq(f_{1s}(v), f_{2s}(Empty)))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   983
\qquad otherwise: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   984
       return \bl{$(r_{1s} \cdot r_{2s}, f_{seq}(f_{1s}, f_{2s}))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   985
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   986
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   987
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   988
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   989
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   990
\begin{tabular}{l@{\hspace{1mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   991
\bl{$f_{seq}(f_1, f_2) \dn$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   992
\qquad \bl{$\lambda v.\,$ case $v = Seq(v_1, v_2)$}: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   993
      & return \bl{$Seq(f_1(v_1), f_2(v_2))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   994
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   995
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   996
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   997
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   998
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   999
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1000
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1001
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1002
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1003
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1004
xleftmargin=-5mm] {../progs/app06.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1005
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1006
\end{frame}
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1007
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1008
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1010
\begin{frame}[t]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1011
\frametitle{Rectification Example}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1012
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1013
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1014
\bl{$\only<1>{(b \cdot c)}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1015
     \only<2-3>{(\underline{b \cdot c})}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1016
     \only<1-3>{+}% 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1017
     \only<1>{(\ZERO + \ONE)}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1018
     \only<2-3>{(\underline{\ZERO + \ONE})}$}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1019
\only<4->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1020
\bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1021
}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1022
$\mapsto$
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1023
\bl{$(b \cdot c) + \ONE$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1024
\end{center}\bigskip
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1025
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1026
\onslide<3->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1027
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1028
\begin{tabular}{lcl}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1029
\bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1030
\bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1031
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1032
\end{center}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1033
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1034
\only<4>{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1035
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1036
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1037
\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1038
\quad \bl{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1039
        case \bl{$v = Left(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1040
      & return \bl{$Left(f_{s1}(v'))$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1041
\quad \phantom{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1042
        case \bl{$v = Right(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1043
      & return \bl{$Right(f_{s2}(v'))$}\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1044
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1045
\end{center}}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1046
\only<5->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1047
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1048
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1049
\only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1050
\quad \bl{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1051
        case \bl{$v = Left(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1052
      & return \bl{$Left(v')$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1053
\quad \phantom{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1054
        case \bl{$v = Right(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1055
      & return \bl{$Right(Right(v'))$}\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1056
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1057
\end{center}}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1058
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1059
\only<6->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1060
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1061
\begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1062
\bl{$\textit{mkeps}$} simplified case: &
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1063
\bl{$\textit{Right}(\textit{Empty})$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1064
rectified case: &
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1065
\bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1066
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1067
\end{center}}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1068
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1069
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1070
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1071
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1072
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1073
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1074
\begin{frame}[c]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1075
\frametitle{Lexing with Simplification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1076
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1077
\begin{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1078
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1079
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1080
  \bl{$lex\,r\,c::s$} & \bl{$\dn$}  & \bl{let $(r', frect) = simp(der(c, r))$}\smallskip\\
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1081
                      & & \bl{$inj\,r\,c\,(frect(lex(r', s)))$}\\
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1082
\end{tabular}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1083
\end{center}\bigskip
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1084
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1085
\begin{center}\small
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1086
\begin{tikzpicture}[node distance=1.1cm,every node/.style={minimum size=7mm}]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1087
\node (r1)  {\bl{$r_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1088
\node (r2) [right=of r1] {\bl{$r_2$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1089
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1090
\node (r3) [right=of r2] {\bl{$r_3$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1091
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1092
\node (r4) [right=of r3] {\bl{$r_4$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1093
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1094
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1095
\node (v4) [below=of r4] {\bl{$v_4$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1096
\draw[->,line width=1mm]  (r4) -- (v4);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1097
\node (v3) [left=of v4] {\bl{$v_3$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1098
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1099
\node (v2) [left=of v3] {\bl{$v_2$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1100
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1101
\node (v1) [left=of v2] {\bl{$v_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1102
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1103
\draw[->,line width=0.5mm]  (r3) -- (v3);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1104
\draw[->,line width=0.5mm]  (r2) -- (v2);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1105
\draw[->,line width=0.5mm]  (r1) -- (v1);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1106
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1107
\end{tikzpicture}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1108
\end{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1109
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1110
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1111
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1112
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1113
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1114
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1115
\begin{frame}[c]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1116
\frametitle{Environments}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1117
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1118
Obtaining the ``recorded'' parts of a value: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1119
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1120
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1121
\begin{tabular}{lcl}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1122
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1123
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1124
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1125
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1126
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
  1127
  \bl{$env(Stars\,[v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1128
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1129
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1130
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1131
\end{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1132
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1133
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1134
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1135
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1136
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1137
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1138
\begin{frame}[c]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1139
\frametitle{While Tokens}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1140
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1141
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1142
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1143
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1144
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1145
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1146
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1147
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1148
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1149
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1150
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1151
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1152
\end{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1153
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1154
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1155
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1156
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1157
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1158
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1159
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1160
\begin{frame}[t]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1161
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1162
\consolas
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1163
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1164
\code{"if true then then 42 else +"}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1165
\end{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1166
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1167
\only<1>{
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1168
\small\begin{tabular}{l}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1169
KEYWORD(if),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1170
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1171
IDENT(true),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1172
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1173
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1174
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1175
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1176
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1177
NUM(42),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1178
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1179
KEYWORD(else),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1180
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1181
OP(+)
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1182
\end{tabular}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1183
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1184
\only<2>{
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1185
\small\begin{tabular}{l}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1186
KEYWORD(if),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1187
IDENT(true),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1188
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1189
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1190
NUM(42),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1191
KEYWORD(else),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1192
OP(+)
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1193
\end{tabular}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1194
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1195
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1196
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1197
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1198
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1199
\begin{frame}[c]
521
95af9beb4b7f updated
cu
parents: 520
diff changeset
  1200
\frametitle{Lexer: Two Rules}
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1201
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1202
\begin{itemize}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1203
\item Longest match rule (``maximal munch rule''): The 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1204
longest initial substring matched by any regular expression is taken
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1205
as next token.\bigskip
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1206
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1207
\item Rule priority:
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1208
For a particular longest initial substring, the first regular
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1209
expression that can match determines the token.
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1210
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1211
\end{itemize}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1212
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1213
%\url{http://www.technologyreview.com/tr10/?year=2011}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1214
  
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1215
%finite deterministic automata/ nondeterministic automaton
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1216
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1217
%\item problem with infix operations, for example i-12
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1218
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1219
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1220
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1221
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1222
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1223
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1224
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1225
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1226
%\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1227
%\begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1228
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1229
%\bl{$zeroable(\ZERO)$}      & \bl{$\dn$} & \bl{$true$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1230
%\bl{$zeroable(\ONE)$}         & \bl{$\dn$} & \bl{$\textit{false}$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1231
%\bl{$zeroable(c)$}                & \bl{$\dn$} & \bl{$\textit{false}$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1232
%\bl{$zeroable(r_1 + r_2)$}        & \bl{$\dn$} & \bl{$zeroable(r_1) \wedge zeroable(r_2)$}\\ 
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1233
%\bl{$zeroable(r_1 \cdot r_2)$}    & \bl{$\dn$} & \bl{$zeroable(r_1) \vee zeroable(r_2)$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1234
%\bl{$zeroable(r^*)$}              & \bl{$\dn$} & \bl{$\textit{false}$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1235
%\end{tabular}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1236
%\end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1237
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1238
%\begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1239
%\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1240
%\end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1241
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1242
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1243
%\end{frame}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1244
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1245
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1246
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1247
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1248
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1249
%\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1250
%\frametitle{\begin{tabular}{c}Last Week\\[-2mm] 
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1251
%            Regexes and Values\end{tabular}}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1252
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1253
%Regular expressions and their corresponding values:
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1254
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1255
%\begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1256
%\begin{columns}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1257
%\begin{column}{3cm}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1258
%\begin{tabular}{@{}rrl@{}}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1259
%  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1260
%           & \bl{$\mid$} & \bl{$\ONE$}   \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1261
%           & \bl{$\mid$} & \bl{$c$}          \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1262
%           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1263
%           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1264
%  \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1265
%           & \bl{$\mid$} & \bl{$r^*$}         \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1266
%  \end{tabular}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1267
%\end{column}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1268
%\begin{column}{3cm}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1269
%\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1270
%  \bl{$v$} & \bl{$::=$}  & \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1271
%           &             & \bl{$Empty$}   \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1272
%           & \bl{$\mid$} & \bl{$Char(c)$}          \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1273
%           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1274
%           & \bl{$\mid$} & \bl{$Left(v)$}   \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1275
%           & \bl{$\mid$} & \bl{$Right(v)$}  \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1276
%           & \bl{$\mid$} & \bl{$Stars [v_1,\ldots\,v_n]$} \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1277
%  \end{tabular}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1278
%\end{column}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1279
%\end{columns}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1280
%\end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1281
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1282
%\end{frame}
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1283
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1284
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1285
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1286
%\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1287
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1288
%\begin{textblock}{10}(3,5)
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1289
%\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1290
%\node (r1)  {\bl{$r_1$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1291
%\node (r2) [right=of r1] {\bl{$r_2$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1292
%\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1293
%\node (r3) [right=of r2] {\bl{$r_3$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1294
%\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1295
%\node (r4) [right=of r3] {\bl{$r_4$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1296
%\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1297
%\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1298
%\node (v4) [below=of r4] {\bl{$v_4$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1299
%\draw[->,line width=1mm]  (r4) -- (v4);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1300
%\node (v3) [left=of v4] {\bl{$v_3$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1301
%\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1302
%\node (v2) [left=of v3] {\bl{$v_2$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1303
%\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1304
%\node (v1) [left=of v2] {\bl{$v_1$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1305
%\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1306
%\draw[->,line width=0.5mm]  (r3) -- (v3);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1307
%\draw[->,line width=0.5mm]  (r2) -- (v2);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1308
%\draw[->,line width=0.5mm]  (r1) -- (v1);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1309
%\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1310
%\end{tikzpicture}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1311
%\end{textblock}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1312
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1313
%\begin{textblock}{6}(1,0.8)
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1314
%\begin{bubble}[6cm]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1315
%\small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1316
%\begin{tabular}{ll}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1317
%\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1318
%\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1319
%\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1320
%\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1321
%\end{tabular}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1322
%\end{bubble}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1323
%\end{textblock}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1324
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1325
%\begin{textblock}{6}(1,11.4)
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1326
%\begin{bubble}[7.6cm]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1327
%\small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1328
%\begin{tabular}{ll}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1329
%\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1330
%\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1331
%\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1332
%\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1333
%\end{tabular}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1334
%\end{bubble}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1335
%\end{textblock}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1336
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1337
%\begin{textblock}{6}(12,11.4)
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1338
%\begin{bubble}[2cm]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1339
%\small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1340
%\begin{tabular}{ll}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1341
%\bl{$|v_1|$}: & \bl{$abc$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1342
%\bl{$|v_2|$}: & \bl{$bc$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1343
%\bl{$|v_3|$}: & \bl{$c$}\\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1344
%\bl{$|v_4|$}: & \bl{$[]$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1345
%\end{tabular}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1346
%\end{bubble}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1347
%\end{textblock}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1348
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1349
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1350
%%\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1351
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1352
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1353
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1354
%\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1355
%\frametitle{Simplification}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1356
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1357
%\begin{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1358
%\item If we simplify after the derivative, then we are builing the
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1359
%value for the simplified regular expression, but \emph{not} for the original
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1360
%regular expression.
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1361
%\end{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1362
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1363
%\begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1364
%\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1365
%\node (r1)  {\bl{$r_1$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1366
%\node (r2) [right=of r1] {\bl{$r_2$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1367
%\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1368
%\node (r3) [right=of r2] {\bl{$r_3$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1369
%\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1370
%\node (r4) [right=of r3] {\bl{$r_4$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1371
%\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1372
%\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1373
%\node (v4) [below=of r4] {\bl{$v_4$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1374
%\draw[->,line width=1mm]  (r4) -- (v4);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1375
%\node (v3) [left=of v4] {\bl{$v_3$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1376
%\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1377
%\node (v2) [left=of v3] {\bl{$v_2$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1378
%\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1379
%\node (v1) [left=of v2] {\bl{$v_1$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1380
%\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1381
%\draw[->,line width=0.5mm]  (r3) -- (v3);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1382
%\draw[->,line width=0.5mm]  (r2) -- (v2);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1383
%\draw[->,line width=0.5mm]  (r1) -- (v1);
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1384
%\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1385
%\end{tikzpicture}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1386
%\end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1387
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1388
%\small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1389
%\hspace{4.5cm}\bl{$(b \cdot c) + (\ZERO + \ONE)$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1390
%$\mapsto$
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1391
%\bl{$(b \cdot c) + \ONE$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1392
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1393
%\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1394
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1395
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1396
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1397
% \begin{frame}[t]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1398
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1399
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1400
% \bl{$\only<1>{(b \cdot c)}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1401
%      \only<2-3>{(\underline{b \cdot c})}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1402
%      \only<1-3>{+}% 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1403
%      \only<1>{(\ZERO + \ONE)}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1404
%      \only<2-3>{(\underline{\ZERO + \ONE})}$}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1405
% \only<4->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1406
% \bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1407
% }
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1408
% $\mapsto$
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1409
% \bl{$(b \cdot c) + \ONE$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1410
% \end{center}\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1411
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1412
% \onslide<3->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1413
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1414
% \begin{tabular}{lcl}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1415
% \bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1416
% \bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1417
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1418
% \end{center}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1419
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1420
% \only<4>{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1421
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1422
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1423
% \bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1424
% \quad \bl{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1425
%         case \bl{$v = Left(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1426
%       & return \bl{$Left(f_{s1}(v'))$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1427
% \quad \phantom{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1428
%         case \bl{$v = Right(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1429
%       & return \bl{$Right(f_{s2}(v'))$}\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1430
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1431
% \end{center}}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1432
% \only<5->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1433
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1434
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1435
% \only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1436
% \quad \bl{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1437
%         case \bl{$v = Left(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1438
%       & return \bl{$Left(v')$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1439
% \quad \phantom{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1440
%         case \bl{$v = Right(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1441
%       & return \bl{$Right(Right(v'))$}\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1442
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1443
% \end{center}}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1444
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1445
% \only<6->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1446
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1447
% \begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1448
% \bl{$\textit{mkeps}$} simplified case: &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1449
% \bl{$\textit{Right}(\textit{Empty})$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1450
% rectified case: &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1451
% \bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1452
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1453
% \end{center}}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1454
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1455
% \end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1456
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1457
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1458
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1459
%\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1460
%\frametitle{Records}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1461
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1462
%\begin{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1463
%\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1464
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1465
%\item \bl{$nullable(x:r) \dn nullable(r)$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1466
%\item \bl{$der\,c\,(x:r) \dn der\,c\,r$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1467
%\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1468
%\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1469
%\end{itemize}\bigskip\bigskip\pause
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1470
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1471
%\small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1472
%for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1473
%
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1474
%\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1475
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1476
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1477
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1478
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1479
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1480
\frametitle{Environments}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1481
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1482
Obtaining the ``recorded'' parts of a value: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1483
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1484
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1485
\begin{tabular}{lcl}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1486
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1487
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1488
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1489
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1490
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1491
  \bl{$env(Stars [v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1492
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1493
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1494
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1495
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1496
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1497
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1498
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1499
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1500
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1501
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1502
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1503
\frametitle{While Tokens}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1504
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1505
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1506
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1507
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1508
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1509
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1510
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1511
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1512
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1513
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1514
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1515
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1516
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1517
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1518
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1519
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1520
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1521
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1522
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1523
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1524
\begin{frame}[t]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1525
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1526
\consolas
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1527
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1528
\code{"if true then then 42 else +"}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1529
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1530
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1531
\only<1>{
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1532
\small\begin{tabular}{l}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1533
KEYWORD(if),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1534
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1535
IDENT(true),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1536
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1537
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1538
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1539
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1540
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1541
NUM(42),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1542
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1543
KEYWORD(else),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1544
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1545
OP(+)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1546
\end{tabular}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1547
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1548
\only<2>{
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1549
\small\begin{tabular}{l}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1550
KEYWORD(if),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1551
IDENT(true),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1552
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1553
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1554
NUM(42),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1555
KEYWORD(else),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1556
OP(+)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1557
\end{tabular}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1558
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1559
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1560
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1561
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1562
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1563
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1564
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1565
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1566
%\frametitle{Coursework: PLs (16)}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1567
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1568
%\begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1569
%\item Java (16)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1570
%\item C++, C, C\# (14)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1571
%\item JavaScript (10)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1572
%\item Scala (9)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1573
%\item Python (9)  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1574
%\item PHP (6)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1575
%\item Haskell (3)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1576
%\item Ruby (4)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1577
%\item Bash, Perl, Powershell (2)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1578
%\item TypeScript (1)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1579
%\item R (1)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1580
%\item Coconut (1)  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1581
%\item Pascal (1)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1582
%\end{itemize}  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1583
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1584
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1585
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1586
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1587
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1588
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1589
%\frametitle{Coursework: Nullable}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1590
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1591
%\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1592
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1593
%  \bl{$nullable([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1594
%  \bl{$nullable(r^+)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1595
%  \bl{$nullable(r^?)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1596
%  \bl{$nullable(r^{\{n\}})$}              & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1597
%  \bl{$nullable(r^{\{n..\}})$}            & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1598
%  \bl{$nullable(r^{\{..n\}})$}            & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1599
%  \bl{$nullable(r^{\{n..m\}})$}           & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1600
%  \bl{$nullable(\sim{}r)$}               & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1601
%                                                        
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1602
%\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1603
%\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1604
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1605
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1606
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1607
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1608
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1609
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1610
%%%\frametitle{Coursework: der}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1611
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1612
%\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1613
%\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1614
%  \bl{$der\, c\, ([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1615
%  \bl{$der\, c\, (r^+)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1616
%  \bl{$der\, c\, (r^?)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1617
%  \bl{$der\, c\, (r^{\{n\}})$}              & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1618
%     \bl{$if\;n=0\;then\;\ZERO\;else\;(der\,c\,r)\cdot r^{\{n-\liningnums{1}\}}$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1619
%  \bl{$der\, c\, (r^{\{n..\}})$}            & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1620
%     \bl{$if\;n=0\;then (der\,c\,r)\cdot r^*$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1621
%  & & \bl{$\phantom{if\;n=0\;}else \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..\}}$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1622
%  \bl{$der\, c\, (r^{\{..n\}})$}            & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1623
%     \bl{$if\;n=0\;then\;\ZERO\;else\;(der\,c\,r)\cdot r^{\{..n-\liningnums{1}\}}$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1624
%  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1625
%  \bl{$der\, c\, (r^{\{n..m\}})$}          & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1626
%     \bl{$if\;n = 0 \wedge m = 0\;then\;\ZERO\; else$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1627
%  \multicolumn{3}{l}{\bl{$if\;n = 0 \wedge m > 0\;then\;(der\,c\,r)\cdot r^{\{..m-\liningnums{1}\}}$}}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1628
%  \multicolumn{3}{l}{\bl{$\phantom{if\;n = 0 \wedge m > 0\;}else
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1629
%          \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..m-\liningnums{1}\}}$}}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1630
%  \bl{$der\, c\, (\sim{}r)$}              & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1631
%\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1632
%\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1633
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1634
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1635
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1636
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1637
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1638
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1639
%\frametitle{Coursework: CFUN}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1640
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1641
%\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1642
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1643
%  \bl{$nullable(CFUN(\_))$}  & \bl{$\dn$} & \bl{$false$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1644
%  \bl{$der\,c\,(CFUN(f))$}   & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1645
%     \bl{$if\;f(c)\;then\;\ONE\;else\;\ZERO$}\bigskip\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1646
%  \bl{$CHAR(c)$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;c=d)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1647
%  \bl{$CSET([c_1,\ldots,c_n])$} & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;d\in [c_1,\ldots,c_n])$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1648
%  \bl{$ALL$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;true)$}\\                                                      
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1649
%\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1650
%\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1651
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1652
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1653
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1654
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1655
\begin{frame}[t]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1656
\begin{mybox3}{}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1657
  Are dfas completed by definition as in do they have a to have transitions
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1658
  for every char at every state?
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1659
\end{mybox3}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1660
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1661
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1662
\begin{frame}[t]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1663
\begin{mybox3}{}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1664
  How can you tell if a language will be regular or irregular?
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1665
\end{mybox3}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1666
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1667
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1668
\begin{frame}<1-12>[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1669
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1670
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1671
\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1672
  \small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1673
  \begin{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1674
\item[$\bullet$] contentwise probably the most enjoyable module I have had so far at KCL 
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1675
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1676
\item[$\bullet$] I personally found the coursework sheets a bit unclear. For example I couldnt see what was required from the CFUN section but once explained it actually was very easy and didnt take long to get working
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1677
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1678
\item[$\bullet$] Please can tutorial sessions be recorded \& linked on Keats.
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1679
  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1680
\item[$\bullet$] One of the best taught modules I've had, with a genuinely interested and engaging lecturer. Thanks Dr.~Urban!
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1681
\end{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1682
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1683
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1684
\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1685
  \small
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1686
  \begin{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1687
\item[$\bullet$] Dr.~Urban is honestly a great lecturer, he's incredibly helpful and responsive. He also teaches at a very good pace and explains things clearly so students who sometimes struggle with the content like myself can keep up. It's a pleasure to learn from him.
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1688
  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1689
\item[$\bullet$] I just wish the Coursework content was explained better, in such a way that allows students to get on with the coursework as soon as possible.
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1690
  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1691
\item[$\bullet$] I'm thoroughly enjoying the module so far. I find that the handouts and homework really solidify my knowledge and the feedback is extremely useful. I enjoy doing the homework and then using the feedback alongside the workshop to correct where I have gone wrong.
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1692
  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1693
\item[$\bullet$] I enjoy this module and think it is taught well. The homework is very useful.
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1694
\end{itemize}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1695
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1696
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1697
\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1698
  \begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1699
  \begin{tabular}{cc}  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1700
  \includegraphics[scale=0.3]{s1.png} &
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1701
  \includegraphics[scale=0.3]{s2.png} \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1702
  \includegraphics[scale=0.3]{s3.png} &
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1703
  \includegraphics[scale=0.3]{s4.png} \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1704
  \end{tabular}                                      
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1705
  \end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1706
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1707
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1708
\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1709
  \begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1710
  \begin{tabular}{cc}  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1711
  \includegraphics[scale=0.3]{s5.png} &
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1712
  \includegraphics[scale=0.3]{s6.png} \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1713
  \includegraphics[scale=0.3]{s7.png} &
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1714
  \includegraphics[scale=0.3]{s8.png} \\
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1715
  \end{tabular}                                      
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1716
  \end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1717
\end{frame}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1718
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1719
\begin{frame}[c]
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1720
  \begin{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1721
  \begin{tabular}{cc}  
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1722
  \includegraphics[scale=0.3]{s9.png} 
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1723
  \end{tabular}                                      
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1724
  \end{center}
3b1136fb6bee updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1725
\end{frame}
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1726
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1727
\end{document}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1728
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1729
%%% Local Variables:  
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1730
%%% mode: latex
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1731
%%% TeX-master: t
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1732
%%% End: 
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1733