slides/slides04.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Fri, 24 Oct 2025 11:26:43 +0100
changeset 1018 fd6a64c53f0e
parent 1017 37b126dbb0e7
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
661
32fd8125f56e updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
     1
% !TEX program = xelatex
743
f063a6cd5d91 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}
871
358a72d7bf71 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 847
diff changeset
     4
\usepackage{../graphicss}
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
7c09b7eadc6b updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    12
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    13
\usepackage{tcolorbox}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    14
\newtcolorbox{mybox}{colback=red!5!white,colframe=red!75!black}
0a3ba0769a61 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}
0a3ba0769a61 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}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    17
722
7c09b7eadc6b updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    18
% a hand written lexer for SML
7c09b7eadc6b updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 671
diff changeset
    19
% https://ponyo.org/
7c09b7eadc6b 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
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
    21
\beamertemplateballitem
722
7c09b7eadc6b 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]
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    34
  \LARGE Compilers and \\[-1mm] 
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    35
  \LARGE Formal Languages\\[-5mm] 
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}
939
fb6ffb9b7304 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 938
diff changeset
    41
    Email:  & christian.urban at kcl.ac.uk\\
1012
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    42
     Office Hour: & Friday 11:30 -- 12:30\\
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    43
  Location: & N7.07 (North Wing, Bush House)\\
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    44
  Slides \& Progs: & KEATS\\
1012
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    45
  %%Pollev: & \texttt{\alert{https://pollev.com/cfltutoratki576}}\\  
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
  \end{tabular}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
  \end{center}
660
7ef4d9a2676a updated
Christian Urban <urbanc@in.tum.de>
parents: 581
diff changeset
    48
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    49
  \begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    50
    \begin{tikzpicture}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    51
      \node[drop shadow,fill=white,inner sep=0pt] 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    52
      {\footnotesize\rowcolors{1}{capri!10}{white}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    53
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    54
          1 Introduction, Languages          & 6 While-Language \\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    55
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    56
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    57
          \cellcolor{blue!50}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    58
          4 Lexing, Tokenising               & 9 Optimisations \\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    59
          5 Grammars, Parsing                & 10 LLVM \\ \hline
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    60
        \end{tabular}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    61
      };
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    62
    \end{tikzpicture}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
    63
  \end{center}
1012
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    64
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    65
\begin{textblock}{5}(12,3)
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    66
  \includegraphics[scale=0.35]{qr01}\\
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    67
  \small{}Wifi: IET-Guest\\
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
    68
\end{textblock}
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
    69
\end{frame}
574
6e19ad25309b updated
Christian Urban <urbanc@in.tum.de>
parents: 522
diff changeset
    70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6e19ad25309b updated
Christian Urban <urbanc@in.tum.de>
parents: 522
diff changeset
    71
1017
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    72
{
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    73
\setbeamercolor{background canvas}{bg=cream}
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    74
\begin{frame}[c]
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    75
\frametitle{Some Housekeeping}
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    76
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    77
\begin{itemize}
1018
fd6a64c53f0e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1017
diff changeset
    78
\item the Discussion Forum is for everyone
1017
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    79
\item SGT groups 4 + 9 for 10th November
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    80
\item Ammonite FAQ
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    81
\end{itemize}
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    82
\end{frame}
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    83
}
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    84
37b126dbb0e7 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1014
diff changeset
    85
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    87
\begin{frame}[c]
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    88
\frametitle{While Tokens}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    89
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    90
\begin{center}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    91
\begin{tabular}{rcl}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    92
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    93
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    94
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    95
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    96
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    97
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    98
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
    99
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
   100
\end{tabular}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
   101
\end{center}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
   102
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
   103
\end{frame}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
   104
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   105
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   106
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
785
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   107
%\begin{frame}[c]
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   108
%\frametitle{Coursework}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   109
%
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   110
%\begin{itemize}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   111
%\item \bl{$\der\,c\,(r^+) \dn \der\,c (r\cdot r^*)$}\quad given
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   112
%that \bl{$r^+ \dn r\cdot r^*$}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   113
%\end{itemize}\bigskip\pause
661
32fd8125f56e updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   114
785
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   115
%\begin{center}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   116
%\begin{tabular}{lcl}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   117
%\bl{$\der\,c\,(r\cdot r^*)$} & \bl{$\dn$} & 
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   118
%\only<2-4>{if \bl{$nullable\,r$}}%
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   119
%\only<5>{\bl{$(\der\,c\,r)\cdot r^*$}}\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   120
% & & 
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   121
% \only<2>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, \der\,c\,(r^*)$}}%
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   122
% \only<3>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, (\der\,c\,r)\cdot r^*$}}%
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   123
% \only<4>{then \bl{$(\der\,c\,r)\cdot r^*$}}\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   124
% & & \only<2-4>{else \bl{$(\der\,c\,r)\cdot r^*$}}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   125
%\end{tabular}  
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   126
%\end{center}  
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   127
%\end{frame}
661
32fd8125f56e updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   128
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
32fd8125f56e updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   129
32fd8125f56e updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   130
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
785
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   131
%\begin{frame}[c]
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   132
%  \frametitle{Coursework (2)}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   133
%  
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   134
%  \begin{itemize}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   135
%  \item \bl{\texttt{CFUN(f: Char => Boolean)}}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   136
%  \end{itemize}\medskip
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   137
%
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   138
%  \begin{center}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   139
%  \begin{tabular}{l}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   140
%  \bl{\texttt{CHAR(c: Char)}} \bl{$\dn$}\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   141
%     \quad\bl{\texttt{CFUN(\_ == c)}}\medskip\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   142
%  \bl{\texttt{RANGE(cs: Set[Char])}} \bl{$\dn$}\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   143
%     \quad\bl{\texttt{CFUN(cs.contains(\_))}}\medskip\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   144
%  \bl{\texttt{ALL}} \bl{$\dn$}\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   145
%     \quad\bl{\texttt{CFUN((c: Char) => true)}}\\
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   146
%  \end{tabular}  
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   147
%  \end{center}  
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   148
%\end{frame}
661
32fd8125f56e updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   149
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
   150
     
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   151
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   152
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   153
\begin{frame}[c]
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   154
\frametitle{The Goal of this Course}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   155
\mbox{}\\[-26mm]\mbox{}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   156
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   157
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   158
  \begin{tikzpicture}[scale=1,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   159
                      node/.style={
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   160
                      rectangle,rounded corners=3mm,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   161
                      very thick,draw=black!50,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   162
                      minimum height=18mm, minimum width=20mm,
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
   163
                      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
   164
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   165
  \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
   166
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   167
  \node (0) at (-2.3,0) {}; 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   168
  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   169
  \node (A) at (0,0)  [node] {};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   170
  \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
   171
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   172
  \node (B) at (3,0)  [node] {};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   173
  \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
   174
    {\mbox{}\hspace{-1mm}parser};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   175
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   176
  \node (C) at (6,0)  [node] {};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   177
  \node [below right] at (C.north west) 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   178
    {\mbox{}\hspace{-1mm}code gen};
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
  \node (1) at (8.4,0) {}; 
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
  \draw [->,line width=4mm] (0) -- (A); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   183
  \draw [->,line width=4mm] (A) -- (B); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   184
  \draw [->,line width=4mm] (B) -- (C); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   185
  \draw [->,line width=4mm] (C) -- (1); 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   186
  \end{tikzpicture}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   187
  \end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   188
  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   189
Today a lexer.  
579
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   190
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   191
\only<2>{
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   192
\begin{textblock}{1}(6,9.8)
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   193
\begin{tabular}{c}
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   194
\includegraphics[scale=0.13]{../pics/rosetta.jpg}\\[-2mm]
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   195
\footnotesize lexing $\Rightarrow$ recognising words (Stone of Rosetta)
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   196
\end{tabular}
eb9ef7b96f4a updated
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   197
\end{textblock}}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   198
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   199
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   200
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   201
\begin{frame}[c]
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   202
\frametitle{Regular Expressions}
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   203
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   204
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
   205
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   206
\begin{itemize}
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   207
\item operands, digits
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   208
\item identifiers
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   209
\item numbers (non-leading zeros)
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   210
\item keywords
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   211
\item comments
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   212
\end{itemize}\bigskip
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   213
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   214
\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
   215
\end{frame}
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   216
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   217
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   218
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   219
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   220
\begin{frame}[c]
521
fa5c34e42a35 updated
cu
parents: 520
diff changeset
   221
\frametitle{Lexing: Test Case}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   222
785
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   223
\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
   224
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   225
\end{frame}
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
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   228
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   229
%\begin{frame}[c]
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   230
%\frametitle{?? Test Case}
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   231
%
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   232
%\mbox{\lstinputlisting[language=While]{../progs/collatz.while}}
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   233
%
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   234
%\end{frame}
139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   235
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   236
35
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   237
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   238
\begin{frame}[t]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   239
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   240
\tt
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   241
\begin{center}\large
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   242
\code{"if true then then 42 else +"}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   243
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   244
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   245
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   246
\begin{tabular}{@{}l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   247
KEYWORD: \\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   248
\hspace{5mm}{if}, {then}, {else},\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   249
WHITESPACE:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   250
\hspace{5mm}{" "}, {$\backslash$n},\\ 
521
fa5c34e42a35 updated
cu
parents: 520
diff changeset
   251
IDENTIFIER:\\
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   252
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   253
NUM:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   254
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   255
OP:\\
521
fa5c34e42a35 updated
cu
parents: 520
diff changeset
   256
\hspace{5mm}+, -, *, \%, <, <=\\
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   257
COMMENT:\\
277
8eb3261294ba updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   258
\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
   259
\end{tabular}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   260
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   261
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   262
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
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
\begin{frame}[t]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   266
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   267
\tt
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   268
\begin{center}\large
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   269
\code{"if true then then 42 else +"}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   270
\end{center}
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
\only<1>{
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   273
\small\begin{tabular}{l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   274
KEYWORD(if),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   275
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   276
IDENT(true),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   277
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   278
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   279
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   280
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   281
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   282
NUM(42),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   283
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   284
KEYWORD(else),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   285
WHITESPACE,\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   286
OP(+)
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   287
\end{tabular}}
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
\only<2>{
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   290
\small\begin{tabular}{l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   291
KEYWORD(if),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   292
IDENT(true),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   293
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   294
KEYWORD(then),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   295
NUM(42),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   296
KEYWORD(else),\\ 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   297
OP(+)
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   298
\end{tabular}}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   299
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   300
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   301
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   302
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   303
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   304
\begin{frame}[c]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   305
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   306
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   307
There is one small problem with the tokenizer. How should we 
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   308
tokenize\ldots?
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   309
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   310
\begin{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   311
\large\code{"x-3"}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   312
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   313
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   314
\tt
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   315
\begin{tabular}{@{}l}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   316
ID: \ldots\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   317
OP:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   318
\hspace{5mm}\texttt{"+"}, \texttt{"-"}\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   319
NUM:\\
938
0eb340948fdb updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 892
diff changeset
   320
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {"0"}\\
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   321
NUMBER:\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   322
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   323
\end{tabular}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   324
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   325
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   326
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   327
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   328
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   329
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   330
The same problem with\medskip
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   331
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   332
\[
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   333
\bl{(ab + a) \cdot (c + bc)}
353
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   334
\]\medskip
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   335
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   336
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
   337
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   338
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
   339
letters followed by ``letters + numbers + \_''$^*$
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   340
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   341
\[
785
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   342
\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
   343
\]
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   344
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   345
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   346
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   347
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   348
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   349
\begin{frame}[c]
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   350
\frametitle{POSIX: Two Rules}
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
38
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   352
\begin{itemize}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   353
\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
   354
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
   355
as the next token.\bigskip
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   356
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   357
\item Rule priority:
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   358
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
   359
expression that can match determines the token.
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   360
\end{itemize}\bigskip\bigskip\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   361
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   362
\small
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   363
\hfill most posix matchers are buggy\\
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   364
\footnotesize
353
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   365
\hfill 
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   366
\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
   367
\smallskip\pause
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   368
b88670c5d04b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 352
diff changeset
   369
\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
   370
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   371
%\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
   372
%finite deterministic automata/ nondeterministic automaton
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   373
%\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
   374
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   375
\end{frame}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   376
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   377
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   378
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   379
\begin{frame}[c]
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
   380
\frametitle{Sulzmann \& Lu Lexer}
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   381
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   382
We want to match the string \bl{$abc$} using \bl{$r_1$}:
38
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   383
272
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   384
\begin{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   385
\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
   386
\node (r1)  {\bl{$r_1$}};
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   387
\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
   388
\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
   389
\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
   390
\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
   391
\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
   392
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
521
fa5c34e42a35 updated
cu
parents: 520
diff changeset
   393
\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
   394
\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
   395
\draw[->,line width=1mm]  (r4) -- (v4);\pause
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   396
\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
   397
\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
   398
\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
   399
\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
   400
\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
   401
\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
   402
\draw[->,line width=0.5mm]  (r3) -- (v3);
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   403
\draw[->,line width=0.5mm]  (r2) -- (v2);
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   404
\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
   405
\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
   406
\end{tikzpicture}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   407
\end{center}
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   408
1446bc47a294 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   409
\end{frame}
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   412
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   413
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   414
\frametitle{Regexes and Values}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   415
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   416
Regular expressions and their corresponding values:
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   417
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   418
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   419
\begin{columns}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   420
\begin{column}{3cm}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   421
\begin{tabular}{@{}rrl@{}}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   422
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   423
           & \bl{$\mid$} & \bl{$\ONE$}   \\
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   424
           & \bl{$\mid$} & \bl{$c$}          \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   425
           & \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
   426
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   427
  \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   428
           & \bl{$\mid$} & \bl{$r^*$}         \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   429
  \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   430
  \end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   431
\end{column}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   432
\begin{column}{3cm}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   433
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   434
  \bl{$v$} & \bl{$::=$}  & \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   435
           &             & \bl{$Empty$}   \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   436
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
279
f406c6677b8c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 278
diff changeset
   437
           & \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
   438
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   439
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   440
           & \bl{$\mid$} & \bl{$Stars\,[]$}      \\
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   441
           & \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
   442
  \end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   443
\end{column}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   444
\end{columns}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   445
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   446
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   447
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   448
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   449
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   450
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   451
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   452
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   453
{\small\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   454
xleftmargin=-5mm] {../progs/app01.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   455
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   456
{\small\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   457
xleftmargin=-5mm] {../progs/app02.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   458
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   459
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   460
1013
7c6ff51f443e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1012
diff changeset
   461
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   462
1014
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   463
{
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   464
\setbeamercolor{background canvas}{bg=cream}
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   465
\begin{frame}[c,fragile]
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   466
\small
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   467
1014
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   468
\begin{lstlisting}[language=Scala,numbers=none]
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   469
 enum Rexp {
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   470
   case ZERO
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   471
   case ONE
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   472
   case CHAR(c: Char)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   473
   case ALT(r1: Rexp, r2: Rexp)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   474
   case SEQ(r1: Rexp, r2: Rexp)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   475
   case STAR(r: Rexp)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   476
}
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   477
\end{lstlisting}
1013
7c6ff51f443e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1012
diff changeset
   478
1014
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   479
\begin{lstlisting}[language=Scala,numbers=none]
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   480
enum Val {
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   481
   case Empty
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   482
   case Chr(c: Char)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   483
   case Sequ(v1: Val, v2: Val)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   484
   case Left(v: Val)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   485
   case Right(v: Val)
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   486
   case Stars(vs: List[Val])
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   487
}
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   488
\end{lstlisting}
1013
7c6ff51f443e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1012
diff changeset
   489
1014
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   490
\end{frame}
184a13ff50ed updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 1013
diff changeset
   491
}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   492
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   493
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   494
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   495
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   496
\begin{textblock}{10}(3,5)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   497
\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
   498
\node (r1)  {\bl{$r_1$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   499
\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
   500
\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
   501
\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
   502
\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
   503
\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
   504
\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
   505
\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
   506
\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
   507
\draw[->,line width=1mm]  (r4) -- (v4);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   508
\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
   509
\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
   510
\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
   511
\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
   512
\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
   513
\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
   514
\draw[->,line width=0.5mm]  (r3) -- (v3);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   515
\draw[->,line width=0.5mm]  (r2) -- (v2);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   516
\draw[->,line width=0.5mm]  (r1) -- (v1);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   517
\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
   518
\end{tikzpicture}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   519
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   520
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   521
\only<1->{
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   522
\begin{textblock}{6}(1,0.8)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   523
\begin{bubble}[6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   524
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   525
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   526
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   527
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   528
\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
   529
\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
   530
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   531
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   532
\end{textblock}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   533
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   534
\only<2->{
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   535
\begin{textblock}{6}(5,11.4)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   536
\begin{bubble}[7.6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   537
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   538
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   539
\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
   540
\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
   541
\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
   542
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   543
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   544
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   545
\end{textblock}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   546
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   547
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   548
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   549
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   550
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   551
\frametitle{Flatten}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   552
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   553
Obtaining the string underlying a value:
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   554
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   555
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   556
\begin{tabular}{lcl}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   557
  \bl{$|Empty|$}     & \bl{$\dn$} & \bl{$[]$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   558
  \bl{$|Char(c)|$}   & \bl{$\dn$} & \bl{$[c]$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   559
  \bl{$|Left(v)|$}   & \bl{$\dn$} & \bl{$|v|$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   560
  \bl{$|Right(v)|$}  & \bl{$\dn$} & \bl{$|v|$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   561
  \bl{$|Seq(v_1,v_2)|$}& \bl{$\dn$} & \bl{$|v_1| \,@\, |v_2|$}\\
786
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   562
  \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
   563
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   564
\end{center}
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
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   567
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   570
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   571
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   572
\begin{textblock}{10}(3,5)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   573
\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
   574
\node (r1)  {\bl{$r_1$}};
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   575
\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
   576
\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
   577
\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
   578
\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
   579
\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
   580
\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
   581
\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
   582
\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
   583
\draw[->,line width=1mm]  (r4) -- (v4);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   584
\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
   585
\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
   586
\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
   587
\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
   588
\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
   589
\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
   590
\draw[->,line width=0.5mm]  (r3) -- (v3);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   591
\draw[->,line width=0.5mm]  (r2) -- (v2);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   592
\draw[->,line width=0.5mm]  (r1) -- (v1);
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   593
\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
   594
\end{tikzpicture}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   595
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   596
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   597
\begin{textblock}{6}(1,0.8)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   598
\begin{bubble}[6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   599
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   600
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   601
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   602
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   603
\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
   604
\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
   605
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   606
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   607
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   608
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   609
\begin{textblock}{6}(1,11.4)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   610
\begin{bubble}[7.6cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   611
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   612
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   613
\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
   614
\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
   615
\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
   616
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   617
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   618
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   619
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   620
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   621
\begin{textblock}{6}(12,11.4)
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   622
\begin{bubble}[2cm]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   623
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   624
\begin{tabular}{ll}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   625
\bl{$|v_1|$}: & \bl{$abc$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   626
\bl{$|v_2|$}: & \bl{$bc$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   627
\bl{$|v_3|$}: & \bl{$c$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   628
\bl{$|v_4|$}: & \bl{$[]$}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   629
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   630
\end{bubble}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   631
\end{textblock}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   632
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   633
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   634
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   635
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   636
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   637
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   638
\begin{frame}[c]
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   639
  \frametitle{Mkeps}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   640
  
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   641
  Finding a (posix) value for recognising the empty string:
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   642
  
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   643
  \begin{center}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   644
  \begin{tabular}{lcl}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   645
    \bl{$mkeps\,(\ONE)$}  & \bl{$\dn$}  & \bl{$Empty$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   646
    \bl{$mkeps\,(r_1 + r_2)$} & \bl{$\dn$}  & \bl{if $nullable(r_1)$}  \\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   647
                            &             & \bl{then $Left(mkeps(r_1))$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   648
                            &             & \bl{else $Right(mkeps(r_2))$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   649
    \bl{$mkeps\,(r_1 \cdot r_2)$}  & \bl{$\dn$} & \bl{$Seq(mkeps(r_1),mkeps(r_2))$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   650
    \bl{$mkeps\,(r^*)$}      & \bl{$\dn$} & \bl{$Stars\,[]$}  \\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   651
  \end{tabular}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   652
  \end{center}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   653
  
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   654
  \end{frame}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   655
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
785
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   656
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   657
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   658
\begin{frame}[c]
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   659
  \frametitle{Inject}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   660
\large
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   661
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   662
  \begin{center}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   663
\begin{tikzpicture}[scale=3,node distance=1.2cm,
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   664
                    every node/.style={minimum size=7mm}]
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   665
\node (r)  {$r$};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   666
\node (rd) [right=of r]{$r_{der}$};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   667
\draw[->,line width=1mm](r)--(rd) node[above,midway] {$\der\,c$};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   668
\node (vd) [below=of r2]{$v_{der}$};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   669
\draw[->,line width=1mm](rd) -- (vd);
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   670
\node (v) [left=of vd] {$v$};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   671
\draw[->,line width=1mm](vd)--(v) node[below,midway] {$inj\,c$};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   672
\draw[->,line width=0.5mm,dotted](r) -- (v) node[left,midway,red] {\bf ?};
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   673
\end{tikzpicture}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   674
\end{center}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   675
\end{frame}
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   676
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6fce7c99ebfa updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 743
diff changeset
   677
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   678
  
786
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   679
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   680
  \begin{frame}[c]
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   681
  \frametitle{Inject}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   682
  
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   683
  Injecting (``Adding'') a character to a value\\[-12mm]\mbox{}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   684
  
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   685
  \begin{center}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   686
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   687
    \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   688
    \bl{$inj\,(r_1 + r_2)\,c\,(Left(v))$} & \bl{$\dn$}  & \bl{$Left(inj\,r_1\,c\,v)$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   689
    \bl{$inj\,(r_1 + r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Right(inj\,r_2\,c\,v)$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   690
    \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)$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   691
    \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)$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   692
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   693
    \bl{$inj\,(r^*)\,c\,(Seq(v,Stars\,vs))$} & \bl{$\dn$}  & \bl{$Stars\,(inj\,r\,c\,v\,::\,vs)$}\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   694
  \end{tabular}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   695
  \end{center}\bigskip
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   696
  
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   697
  \footnotesize
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   698
  \begin{tabular}{l@{\hspace{2mm}}l}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   699
  \bl{$inj$}: & 1st arg $\mapsto$ a rexp; 2nd arg $\mapsto$ a character; 
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   700
  3rd arg $\mapsto$ a value\\
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   701
              & result $\mapsto$ a value 
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   702
  \end{tabular}
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   703
  \end{frame}
786
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   704
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   705
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   706
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   707
  \begin{frame}[t]
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   708
  
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   709
  \begin{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   710
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   711
    \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   712
  \end{tabular}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   713
  \end{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   714
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   715
\end{frame}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   716
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   717
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   718
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   719
  \begin{frame}[t]
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   720
  
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   721
  \begin{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   722
    \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   723
    \bl{$inj\,(r_1 + r_2)\,c\,(Left(v))$} & \bl{$\dn$}  & \bl{$Left(inj\,r_1\,c\,v)$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   724
    \bl{$inj\,(r_1 + r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Right(inj\,r_2\,c\,v)$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   725
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   726
  \end{tabular}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   727
  \end{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   728
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   729
\end{frame}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   730
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   731
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   732
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   733
  \begin{frame}[t]
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   734
  
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   735
  \begin{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   736
    \begin{tabular}{@{\hspace{-8mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   737
    \\[-15mm]  
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   738
    \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)$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   739
    \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)$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   740
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\  
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   741
  \end{tabular}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   742
\end{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   743
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   744
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   745
\begin{textblock}{13}(1,13.4)
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   746
\begin{bubble}[13cm]
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   747
\small
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   748
\bl{$\der\, c\, (r_1 \cdot r_2)$} \bl{$\dn$} \bl{\textbf{if} $nullable (r_1)$}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   749
 \bl{\textbf{then} $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   750
 \bl{\textbf{else} $(\der\, c\, r_1) \cdot r_2$}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   751
\end{bubble}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   752
\end{textblock}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   753
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   754
\end{frame}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   755
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   756
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   757
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   758
  \begin{frame}[t]
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   759
  
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   760
  \begin{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   761
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   762
    \bl{$inj\,(r^*)\,c\,(Seq(v,Stars\,vs))$} & \bl{$\dn$}  & \bl{$Stars\,(inj\,r\,c\,v\,::\,vs)$}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   763
  \end{tabular}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   764
  \end{center}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   765
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   766
\end{frame}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   767
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   768
662
7f7098f0b5f0 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   769
  
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   770
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   771
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   772
\frametitle{Lexing}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   773
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   774
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   775
\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
   776
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
786
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   777
  \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
   778
\end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   779
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   780
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   781
\footnotesize
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   782
\bl{$lex$}: returns a value
280
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   783
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   784
\begin{center}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   785
\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
   786
\node (r1)  {\bl{$r_1$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   787
\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
   788
\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
   789
\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
   790
\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
   791
\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
   792
\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
   793
\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
   794
\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
   795
\draw[->,line width=1mm]  (r4) -- (v4);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   796
\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
   797
\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
   798
\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
   799
\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
   800
\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
   801
\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
   802
\draw[->,line width=0.5mm]  (r3) -- (v3);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   803
\draw[->,line width=0.5mm]  (r2) -- (v2);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   804
\draw[->,line width=0.5mm]  (r1) -- (v1);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   805
\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
   806
\end{tikzpicture}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   807
\end{center}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   808
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   809
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   810
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   813
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   814
\frametitle{Records}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   815
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   816
\begin{itemize}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   817
\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
   818
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   819
\item \bl{$nullable(x:r) \dn nullable(r)$}
671
7457eabb8c76 updated
Christian Urban <urbanc@in.tum.de>
parents: 662
diff changeset
   820
\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
   821
\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
   822
\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
   823
\end{itemize}\bigskip\bigskip\pause
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
\small
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   826
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
   827
786
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   828
\begin{textblock}{6}(10,10)
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   829
\begin{bubble}[2cm]
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   830
\small
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   831
\begin{tabular}{l}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   832
  \bl{$(id : r_{id})$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   833
  \bl{$(key : r_{key})$}\\
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   834
\end{tabular}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   835
\end{bubble}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   836
\end{textblock}
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   837
261ea200555d updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 785
diff changeset
   838
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   839
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   840
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   841
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   842
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   843
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   844
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   845
\begin{itemize}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   846
\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
   847
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   848
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   849
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   850
(name: \bl{$[a\mbox{-}z0\mbox{-}9\_\!\_\,.-]^+$})\bl{$\cdot @\cdot$}\\ 
794
8a09c03a098f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 792
diff changeset
   851
\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
   852
\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
   853
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   854
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   855
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   856
\bl{\[
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   857
\texttt{christian.urban@kcl.ac.uk}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   858
\]}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   859
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   860
\item the result environment:
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   861
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   862
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   863
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   864
\bl{$[(name:\texttt{christian.urban}),$}\\ 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   865
\bl{$\phantom{[}(domain:\texttt{kcl}),$}\\ 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   866
\bl{$\phantom{[}(top\_level:\texttt{ac.uk})]$}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   867
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   868
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   869
\end{itemize}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   870
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   871
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   872
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   873
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   874
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   875
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   876
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   877
\frametitle{While Tokens}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   878
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   879
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   880
\begin{tabular}{rcl}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   881
\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
   882
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   883
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   884
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   885
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   886
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   887
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   888
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   889
\end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   890
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   891
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   892
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   893
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   894
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   895
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   896
274
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
\begin{frame}[c]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   899
\frametitle{Simplification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   900
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   901
\begin{itemize}
522
11d6c66e7edf updated
cu
parents: 521
diff changeset
   902
\item If we simplify after the derivative, then we are building the
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   903
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
   904
regular expression.
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   905
\end{itemize}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   906
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   907
\begin{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   908
\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
   909
\node (r1)  {\bl{$r_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   910
\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
   911
\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
   912
\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
   913
\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
   914
\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
   915
\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
   916
\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
   917
\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
   918
\draw[->,line width=1mm]  (r4) -- (v4);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   919
\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
   920
\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
   921
\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
   922
\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
   923
\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
   924
\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
   925
\draw[->,line width=0.5mm]  (r3) -- (v3);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   926
\draw[->,line width=0.5mm]  (r2) -- (v2);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   927
\draw[->,line width=0.5mm]  (r1) -- (v1);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   928
\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
   929
\end{tikzpicture}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   930
\end{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   931
792
1f9a45fb5429 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 788
diff changeset
   932
\small\pause
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   933
\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
   934
$\mapsto$
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   935
\bl{$\ONE$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   936
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   937
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   938
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   939
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   940
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   941
\begin{frame}[c]
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   942
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   943
  Normally we would have
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   944
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   945
  \begin{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   946
  \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
   947
  \end{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   948
452
0b707b614dac updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 451
diff changeset
   949
  and answer how this regular expression matches the empty string
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   950
  with the value
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   951
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   952
  \begin{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   953
  \bl{$Right(Right(Empty))$}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   954
  \end{center}\bigskip
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   955
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   956
  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
   957
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   958
\end{frame}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   959
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   960
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   961
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   962
\begin{frame}[c]
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   963
\frametitle{Rectification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   964
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   965
\def\arraystretch{1.05}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   966
\begin{center}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   967
\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
   968
& & & \hspace{5mm}rectification \\
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   969
& & & \hspace{5mm}functions:\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   970
\bl{$r \cdot \ZERO$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   971
\bl{$\ZERO \cdot r$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   972
\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
   973
\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
   974
\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
   975
\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
   976
\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
   977
\end{tabular}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   978
\end{center}\medskip\pause
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   979
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   980
\small
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   981
old \bl{$simp$} returns a rexp;\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   982
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
   983
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   984
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   985
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   986
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
\begin{frame}[c]
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
   989
\frametitle{Rectification $\_ + \_$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   990
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   991
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   992
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   993
\bl{$simp(r)$}:\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   994
\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
   995
\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
   996
\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
   997
\qquad case \bl{$r_{1s} = \ZERO$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   998
       return \bl{$(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   999
\qquad case \bl{$r_{2s} = \ZERO$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1000
       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
  1001
\qquad case \bl{$r_{1s} = r_{2s}$}:
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1002
       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
  1003
\qquad otherwise: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1004
       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
  1005
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1006
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1007
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1008
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1009
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1010
\begin{tabular}{l@{\hspace{1mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1011
\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
  1012
\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
  1013
      & return \bl{$Left(f_1(v'))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1014
\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
  1015
      & return \bl{$Right(f_2(v'))$}\\      
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1016
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1017
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1018
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1019
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1020
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1021
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1022
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1023
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1024
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1025
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1026
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1027
xleftmargin=-5mm] {../progs/app05.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1028
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1029
\end{frame}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1030
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1031
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1032
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1033
\begin{frame}[c]
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1034
\frametitle{Rectification $\_ \cdot \_$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1035
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1036
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1037
\begin{tabular}{@{\hspace{-3mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1038
\bl{$simp(r)$}:\ldots\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1039
\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
  1040
\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
  1041
\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
  1042
\qquad case \bl{$r_{1s} = \ZERO$}: 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1043
       return \bl{$(\ZERO, f_{error})$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1044
\qquad case \bl{$r_{2s} = \ZERO$}: 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1045
       return \bl{$(\ZERO, f_{error})$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1046
\qquad case \bl{$r_{1s} = \ONE$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1047
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
  1048
\qquad case \bl{$r_{2s} = \ONE$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1049
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
  1050
\qquad otherwise: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1051
       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
  1052
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1053
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1054
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1055
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1056
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1057
\begin{tabular}{l@{\hspace{1mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1058
\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
  1059
\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
  1060
      & 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
  1061
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1062
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1063
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1064
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1065
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1066
451
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1067
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1068
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1069
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1070
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1071
xleftmargin=-5mm] {../progs/app06.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1072
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1073
\end{frame}
451
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1074
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1075
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1076
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1077
\begin{frame}[t]
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1078
\frametitle{Rectification Example}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1079
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1080
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1081
\bl{$\only<1>{(b \cdot c)}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1082
     \only<2-3>{(\underline{b \cdot c})}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1083
     \only<1-3>{+}% 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1084
     \only<1>{(\ZERO + \ONE)}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1085
     \only<2-3>{(\underline{\ZERO + \ONE})}$}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1086
\only<4->{%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1087
\bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1088
}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1089
$\mapsto$
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1090
\bl{$(b \cdot c) + \ONE$}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1091
\end{center}\bigskip
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1092
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1093
\onslide<3->{%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1094
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1095
\begin{tabular}{lcl}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1096
\bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1097
\bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1098
\end{tabular}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1099
\end{center}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1100
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1101
\only<4>{%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1102
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1103
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1104
\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1105
\quad \bl{$\lambda v.\,$} 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1106
        case \bl{$v = Left(v')$}: 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1107
      & return \bl{$Left(f_{s1}(v'))$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1108
\quad \phantom{$\lambda v.\,$} 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1109
        case \bl{$v = Right(v')$}: 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1110
      & return \bl{$Right(f_{s2}(v'))$}\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1111
\end{tabular}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1112
\end{center}}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1113
\only<5->{%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1114
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1115
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1116
\only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1117
\quad \bl{$\lambda v.\,$} 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1118
        case \bl{$v = Left(v')$}: 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1119
      & return \bl{$Left(v')$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1120
\quad \phantom{$\lambda v.\,$} 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1121
        case \bl{$v = Right(v')$}: 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1122
      & return \bl{$Right(Right(v'))$}\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1123
\end{tabular}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1124
\end{center}}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1125
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1126
\only<6->{%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1127
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1128
\begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1129
\bl{$\textit{mkeps}$} simplified case: &
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1130
\bl{$\textit{Right}(\textit{Empty})$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1131
rectified case: &
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1132
\bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1133
\end{tabular}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1134
\end{center}}%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1135
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1136
\end{frame}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1137
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1138
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1139
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1140
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1141
\begin{frame}[c]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1142
\frametitle{Lexing with Simplification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1143
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1144
\begin{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1145
\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
  1146
  \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
  1147
  \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
  1148
                      & & \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
  1149
\end{tabular}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1150
\end{center}\bigskip
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1151
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1152
\begin{center}\small
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1153
\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
  1154
\node (r1)  {\bl{$r_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1155
\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
  1156
\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
  1157
\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
  1158
\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
  1159
\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
  1160
\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
  1161
\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
  1162
\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
  1163
\draw[->,line width=1mm]  (r4) -- (v4);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1164
\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
  1165
\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
  1166
\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
  1167
\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
  1168
\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
  1169
\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
  1170
\draw[->,line width=0.5mm]  (r3) -- (v3);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1171
\draw[->,line width=0.5mm]  (r2) -- (v2);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1172
\draw[->,line width=0.5mm]  (r1) -- (v1);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1173
\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
  1174
\end{tikzpicture}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1175
\end{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1176
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1177
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1178
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1179
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1180
451
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1181
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1182
\begin{frame}[c]
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1183
\frametitle{Environments}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1184
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1185
Obtaining the ``recorded'' parts of a value: 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1186
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1187
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1188
\begin{tabular}{lcl}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1189
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1190
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1191
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1192
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1193
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
578
e3cb8adb2a92 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
  1194
  \bl{$env(Stars\,[v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
451
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1195
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1196
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1197
\end{tabular}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1198
\end{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1199
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1200
\end{frame}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1201
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1202
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1203
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1204
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1205
\begin{frame}[c]
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1206
\frametitle{While Tokens}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1207
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1208
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1209
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1210
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1211
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1212
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1213
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1214
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1215
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1216
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1217
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1218
\end{tabular}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1219
\end{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1220
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1221
\end{frame}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1222
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1223
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1224
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1225
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1226
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1227
\begin{frame}[t]
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1228
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1229
\consolas
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1230
\begin{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1231
\code{"if true then then 42 else +"}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1232
\end{center}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1233
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1234
\only<1>{
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1235
\small\begin{tabular}{l}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1236
KEYWORD(if),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1237
WHITESPACE,\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1238
IDENT(true),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1239
WHITESPACE,\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1240
KEYWORD(then),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1241
WHITESPACE,\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1242
KEYWORD(then),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1243
WHITESPACE,\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1244
NUM(42),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1245
WHITESPACE,\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1246
KEYWORD(else),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1247
WHITESPACE,\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1248
OP(+)
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1249
\end{tabular}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1250
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1251
\only<2>{
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1252
\small\begin{tabular}{l}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1253
KEYWORD(if),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1254
IDENT(true),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1255
KEYWORD(then),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1256
KEYWORD(then),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1257
NUM(42),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1258
KEYWORD(else),\\ 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1259
OP(+)
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1260
\end{tabular}}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1261
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1262
\end{frame}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1263
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1264
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1265
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1266
\begin{frame}[c]
521
fa5c34e42a35 updated
cu
parents: 520
diff changeset
  1267
\frametitle{Lexer: Two Rules}
451
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1268
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1269
\begin{itemize}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1270
\item Longest match rule (``maximal munch rule''): The 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1271
longest initial substring matched by any regular expression is taken
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1272
as next token.\bigskip
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1273
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1274
\item Rule priority:
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1275
For a particular longest initial substring, the first regular
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1276
expression that can match determines the token.
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1277
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1278
\end{itemize}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1279
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1280
%\url{http://www.technologyreview.com/tr10/?year=2011}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1281
  
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1282
%finite deterministic automata/ nondeterministic automaton
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1283
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1284
%\item problem with infix operations, for example i-12
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1285
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1286
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1287
\end{frame}
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1288
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1289
b7c526b01931 updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1290
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1291
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1292
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1293
%\begin{frame}[c]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1294
%\begin{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1295
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1296
%\bl{$zeroable(\ZERO)$}      & \bl{$\dn$} & \bl{$true$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1297
%\bl{$zeroable(\ONE)$}         & \bl{$\dn$} & \bl{$\textit{false}$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1298
%\bl{$zeroable(c)$}                & \bl{$\dn$} & \bl{$\textit{false}$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1299
%\bl{$zeroable(r_1 + r_2)$}        & \bl{$\dn$} & \bl{$zeroable(r_1) \wedge zeroable(r_2)$}\\ 
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1300
%\bl{$zeroable(r_1 \cdot r_2)$}    & \bl{$\dn$} & \bl{$zeroable(r_1) \vee zeroable(r_2)$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1301
%\bl{$zeroable(r^*)$}              & \bl{$\dn$} & \bl{$\textit{false}$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1302
%\end{tabular}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1303
%\end{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1304
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1305
%\begin{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1306
%\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1307
%\end{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1308
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1309
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1310
%\end{frame}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1311
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1312
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1313
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1314
  
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1315
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1316
%\begin{frame}[c]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1317
%\frametitle{\begin{tabular}{c}Last Week\\[-2mm] 
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1318
%            Regexes and Values\end{tabular}}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1319
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1320
%Regular expressions and their corresponding values:
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1321
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1322
%\begin{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1323
%\begin{columns}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1324
%\begin{column}{3cm}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1325
%\begin{tabular}{@{}rrl@{}}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1326
%  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1327
%           & \bl{$\mid$} & \bl{$\ONE$}   \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1328
%           & \bl{$\mid$} & \bl{$c$}          \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1329
%           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1330
%           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1331
%  \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1332
%           & \bl{$\mid$} & \bl{$r^*$}         \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1333
%  \end{tabular}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1334
%\end{column}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1335
%\begin{column}{3cm}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1336
%\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1337
%  \bl{$v$} & \bl{$::=$}  & \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1338
%           &             & \bl{$Empty$}   \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1339
%           & \bl{$\mid$} & \bl{$Char(c)$}          \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1340
%           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1341
%           & \bl{$\mid$} & \bl{$Left(v)$}   \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1342
%           & \bl{$\mid$} & \bl{$Right(v)$}  \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1343
%           & \bl{$\mid$} & \bl{$Stars [v_1,\ldots\,v_n]$} \\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1344
%  \end{tabular}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1345
%\end{column}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1346
%\end{columns}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1347
%\end{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1348
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1349
%\end{frame}
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1350
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1351
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1352
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1353
%\begin{frame}[c]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1354
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1355
%\begin{textblock}{10}(3,5)
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1356
%\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1357
%\node (r1)  {\bl{$r_1$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1358
%\node (r2) [right=of r1] {\bl{$r_2$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1359
%\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1360
%\node (r3) [right=of r2] {\bl{$r_3$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1361
%\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1362
%\node (r4) [right=of r3] {\bl{$r_4$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1363
%\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1364
%\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1365
%\node (v4) [below=of r4] {\bl{$v_4$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1366
%\draw[->,line width=1mm]  (r4) -- (v4);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1367
%\node (v3) [left=of v4] {\bl{$v_3$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1368
%\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1369
%\node (v2) [left=of v3] {\bl{$v_2$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1370
%\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1371
%\node (v1) [left=of v2] {\bl{$v_1$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1372
%\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1373
%\draw[->,line width=0.5mm]  (r3) -- (v3);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1374
%\draw[->,line width=0.5mm]  (r2) -- (v2);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1375
%\draw[->,line width=0.5mm]  (r1) -- (v1);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1376
%\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1377
%\end{tikzpicture}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1378
%\end{textblock}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1379
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1380
%\begin{textblock}{6}(1,0.8)
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1381
%\begin{bubble}[6cm]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1382
%\small
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1383
%\begin{tabular}{ll}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1384
%\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1385
%\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1386
%\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1387
%\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1388
%\end{tabular}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1389
%\end{bubble}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1390
%\end{textblock}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1391
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1392
%\begin{textblock}{6}(1,11.4)
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1393
%\begin{bubble}[7.6cm]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1394
%\small
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1395
%\begin{tabular}{ll}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1396
%\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1397
%\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1398
%\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1399
%\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1400
%\end{tabular}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1401
%\end{bubble}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1402
%\end{textblock}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1403
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1404
%\begin{textblock}{6}(12,11.4)
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1405
%\begin{bubble}[2cm]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1406
%\small
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1407
%\begin{tabular}{ll}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1408
%\bl{$|v_1|$}: & \bl{$abc$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1409
%\bl{$|v_2|$}: & \bl{$bc$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1410
%\bl{$|v_3|$}: & \bl{$c$}\\
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1411
%\bl{$|v_4|$}: & \bl{$[]$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1412
%\end{tabular}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1413
%\end{bubble}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1414
%\end{textblock}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1415
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1416
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1417
%%\end{frame}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1418
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1419
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1420
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1421
%\begin{frame}[c]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1422
%\frametitle{Simplification}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1423
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1424
%\begin{itemize}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1425
%\item If we simplify after the derivative, then we are builing the
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1426
%value for the simplified regular expression, but \emph{not} for the original
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1427
%regular expression.
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1428
%\end{itemize}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1429
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1430
%\begin{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1431
%\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1432
%\node (r1)  {\bl{$r_1$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1433
%\node (r2) [right=of r1] {\bl{$r_2$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1434
%\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1435
%\node (r3) [right=of r2] {\bl{$r_3$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1436
%\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1437
%\node (r4) [right=of r3] {\bl{$r_4$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1438
%\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1439
%\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1440
%\node (v4) [below=of r4] {\bl{$v_4$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1441
%\draw[->,line width=1mm]  (r4) -- (v4);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1442
%\node (v3) [left=of v4] {\bl{$v_3$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1443
%\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1444
%\node (v2) [left=of v3] {\bl{$v_2$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1445
%\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1446
%\node (v1) [left=of v2] {\bl{$v_1$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1447
%\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1448
%\draw[->,line width=0.5mm]  (r3) -- (v3);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1449
%\draw[->,line width=0.5mm]  (r2) -- (v2);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1450
%\draw[->,line width=0.5mm]  (r1) -- (v1);
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1451
%\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1452
%\end{tikzpicture}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1453
%\end{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1454
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1455
%\small
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1456
%\hspace{4.5cm}\bl{$(b \cdot c) + (\ZERO + \ONE)$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1457
%$\mapsto$
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1458
%\bl{$(b \cdot c) + \ONE$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1459
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1460
%\end{frame}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1461
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1462
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1463
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1464
% \begin{frame}[t]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1465
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1466
% \begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1467
% \bl{$\only<1>{(b \cdot c)}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1468
%      \only<2-3>{(\underline{b \cdot c})}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1469
%      \only<1-3>{+}% 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1470
%      \only<1>{(\ZERO + \ONE)}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1471
%      \only<2-3>{(\underline{\ZERO + \ONE})}$}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1472
% \only<4->{%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1473
% \bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1474
% }
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1475
% $\mapsto$
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1476
% \bl{$(b \cdot c) + \ONE$}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1477
% \end{center}\bigskip
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1478
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1479
% \onslide<3->{%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1480
% \begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1481
% \begin{tabular}{lcl}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1482
% \bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1483
% \bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1484
% \end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1485
% \end{center}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1486
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1487
% \only<4>{%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1488
% \begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1489
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1490
% \bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1491
% \quad \bl{$\lambda v.\,$} 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1492
%         case \bl{$v = Left(v')$}: 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1493
%       & return \bl{$Left(f_{s1}(v'))$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1494
% \quad \phantom{$\lambda v.\,$} 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1495
%         case \bl{$v = Right(v')$}: 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1496
%       & return \bl{$Right(f_{s2}(v'))$}\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1497
% \end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1498
% \end{center}}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1499
% \only<5->{%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1500
% \begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1501
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1502
% \only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1503
% \quad \bl{$\lambda v.\,$} 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1504
%         case \bl{$v = Left(v')$}: 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1505
%       & return \bl{$Left(v')$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1506
% \quad \phantom{$\lambda v.\,$} 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1507
%         case \bl{$v = Right(v')$}: 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1508
%       & return \bl{$Right(Right(v'))$}\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1509
% \end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1510
% \end{center}}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1511
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1512
% \only<6->{%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1513
% \begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1514
% \begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1515
% \bl{$\textit{mkeps}$} simplified case: &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1516
% \bl{$\textit{Right}(\textit{Empty})$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1517
% rectified case: &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1518
% \bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1519
% \end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1520
% \end{center}}%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1521
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1522
% \end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1523
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1524
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1525
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1526
%\begin{frame}[c]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1527
%\frametitle{Records}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1528
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1529
%\begin{itemize}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1530
%\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1531
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1532
%\item \bl{$nullable(x:r) \dn nullable(r)$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1533
%\item \bl{$der\,c\,(x:r) \dn der\,c\,r$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1534
%\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1535
%\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1536
%\end{itemize}\bigskip\bigskip\pause
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1537
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1538
%\small
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1539
%for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1540
%
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1541
%\end{frame}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1542
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1543
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1544
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1545
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1546
\begin{frame}[c]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1547
\frametitle{Environments}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1548
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1549
Obtaining the ``recorded'' parts of a value: 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1550
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1551
\begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1552
\begin{tabular}{lcl}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1553
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1554
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1555
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1556
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1557
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1558
  \bl{$env(Stars [v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1559
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1560
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1561
\end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1562
\end{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1563
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1564
\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1565
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1566
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1567
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1568
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1569
\begin{frame}[c]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1570
\frametitle{While Tokens}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1571
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1572
\begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1573
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1574
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1575
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1576
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1577
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1578
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1579
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1580
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1581
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1582
\end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1583
\end{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1584
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1585
\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1586
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1587
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1588
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1589
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1590
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1591
\begin{frame}[t]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1592
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1593
\consolas
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1594
\begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1595
\code{"if true then then 42 else +"}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1596
\end{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1597
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1598
\only<1>{
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1599
\small\begin{tabular}{l}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1600
KEYWORD(if),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1601
WHITESPACE,\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1602
IDENT(true),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1603
WHITESPACE,\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1604
KEYWORD(then),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1605
WHITESPACE,\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1606
KEYWORD(then),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1607
WHITESPACE,\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1608
NUM(42),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1609
WHITESPACE,\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1610
KEYWORD(else),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1611
WHITESPACE,\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1612
OP(+)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1613
\end{tabular}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1614
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1615
\only<2>{
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1616
\small\begin{tabular}{l}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1617
KEYWORD(if),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1618
IDENT(true),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1619
KEYWORD(then),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1620
KEYWORD(then),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1621
NUM(42),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1622
KEYWORD(else),\\ 
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1623
OP(+)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1624
\end{tabular}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1625
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1626
\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1627
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1628
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1629
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1630
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1631
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1632
%\begin{frame}[c]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1633
%\frametitle{Coursework: PLs (16)}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1634
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1635
%\begin{itemize}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1636
%\item Java (16)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1637
%\item C++, C, C\# (14)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1638
%\item JavaScript (10)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1639
%\item Scala (9)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1640
%\item Python (9)  
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1641
%\item PHP (6)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1642
%\item Haskell (3)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1643
%\item Ruby (4)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1644
%\item Bash, Perl, Powershell (2)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1645
%\item TypeScript (1)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1646
%\item R (1)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1647
%\item Coconut (1)  
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1648
%\item Pascal (1)
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1649
%\end{itemize}  
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1650
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1651
%\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1652
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1653
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1654
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1655
%\begin{frame}[c]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1656
%\frametitle{Coursework: Nullable}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1657
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1658
%\begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1659
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1660
%  \bl{$nullable([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1661
%  \bl{$nullable(r^+)$}                   & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1662
%  \bl{$nullable(r^?)$}                   & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1663
%  \bl{$nullable(r^{\{n\}})$}              & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1664
%  \bl{$nullable(r^{\{n..\}})$}            & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1665
%  \bl{$nullable(r^{\{..n\}})$}            & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1666
%  \bl{$nullable(r^{\{n..m\}})$}           & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1667
%  \bl{$nullable(\sim{}r)$}               & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1668
%                                                        
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1669
%\end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1670
%\end{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1671
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1672
%\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1673
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1674
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1675
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1676
%\begin{frame}[c]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1677
%%%\frametitle{Coursework: der}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1678
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1679
%\begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1680
%\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1681
%  \bl{$der\, c\, ([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1682
%  \bl{$der\, c\, (r^+)$}                   & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1683
%  \bl{$der\, c\, (r^?)$}                   & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1684
%  \bl{$der\, c\, (r^{\{n\}})$}              & \bl{$\dn$} &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1685
%     \bl{$if\;n=0\;then\;\ZERO\;else\;(der\,c\,r)\cdot r^{\{n-\liningnums{1}\}}$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1686
%  \bl{$der\, c\, (r^{\{n..\}})$}            & \bl{$\dn$} &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1687
%     \bl{$if\;n=0\;then (der\,c\,r)\cdot r^*$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1688
%  & & \bl{$\phantom{if\;n=0\;}else \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..\}}$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1689
%  \bl{$der\, c\, (r^{\{..n\}})$}            & \bl{$\dn$} &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1690
%     \bl{$if\;n=0\;then\;\ZERO\;else\;(der\,c\,r)\cdot r^{\{..n-\liningnums{1}\}}$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1691
%  
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1692
%  \bl{$der\, c\, (r^{\{n..m\}})$}          & \bl{$\dn$} &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1693
%     \bl{$if\;n = 0 \wedge m = 0\;then\;\ZERO\; else$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1694
%  \multicolumn{3}{l}{\bl{$if\;n = 0 \wedge m > 0\;then\;(der\,c\,r)\cdot r^{\{..m-\liningnums{1}\}}$}}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1695
%  \multicolumn{3}{l}{\bl{$\phantom{if\;n = 0 \wedge m > 0\;}else
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1696
%          \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..m-\liningnums{1}\}}$}}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1697
%  \bl{$der\, c\, (\sim{}r)$}              & \bl{$\dn$} & $?$\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1698
%\end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1699
%\end{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1700
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1701
%\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1702
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1703
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1704
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1705
%\begin{frame}[c]
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1706
%\frametitle{Coursework: CFUN}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1707
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1708
%\begin{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1709
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1710
%  \bl{$nullable(CFUN(\_))$}  & \bl{$\dn$} & \bl{$false$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1711
%  \bl{$der\,c\,(CFUN(f))$}   & \bl{$\dn$} &
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1712
%     \bl{$if\;f(c)\;then\;\ONE\;else\;\ZERO$}\bigskip\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1713
%  \bl{$CHAR(c)$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;c=d)$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1714
%  \bl{$CSET([c_1,\ldots,c_n])$} & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;d\in [c_1,\ldots,c_n])$}\\
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1715
%  \bl{$ALL$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;true)$}\\                                                      
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1716
%\end{tabular}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1717
%\end{center}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1718
%
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1719
%\end{frame}
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1720
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1721
847
a137834fe8fc updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 794
diff changeset
  1722
a137834fe8fc updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 794
diff changeset
  1723
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1724
\begin{frame}<1-28>[c]
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1725
\end{frame}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1726
1012
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
  1727
\end{document}
fbe868b97e33 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 970
diff changeset
  1728
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1729
\begin{frame}[c]
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1730
  \frametitle{Week 3 Feedback}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1731
  \begin{center}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1732
  \includegraphics[scale=0.30]{s0.png}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1733
  \end{center}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1734
\end{frame}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1735
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1736
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1737
\begin{frame}[c]
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1738
  \begin{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1739
  \begin{tabular}{cc}  
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1740
  \includegraphics[scale=0.18]{s1.png} &
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1741
  \includegraphics[scale=0.18]{s2.png} \\
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1742
  \includegraphics[scale=0.18]{s3.png} &
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1743
  \includegraphics[scale=0.18]{s4.png} \\
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1744
  \end{tabular}                                      
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1745
  \end{center}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1746
\end{frame}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1747
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1748
\begin{frame}[c]
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1749
  \begin{center}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1750
  \begin{tabular}{cc}  
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1751
  \includegraphics[scale=0.18]{s5.png} &
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1752
  \includegraphics[scale=0.18]{s6.png} \\
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1753
  \includegraphics[scale=0.18]{s7.png} &
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1754
  \includegraphics[scale=0.18]{s8.png} \\
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1755
  \end{tabular}                                      
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1756
  \end{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1757
\end{frame}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1758
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1759
\begin{frame}[c]
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1760
  \begin{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1761
  \begin{tabular}{cc}  
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1762
    \includegraphics[scale=0.18]{s9.png} &
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1763
    \includegraphics[scale=0.18]{s10.png} 
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1764
  \end{tabular}                                      
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1765
  \end{center}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1766
\end{frame}
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1767
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1768
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1769
788
0a3ba0769a61 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 786
diff changeset
  1770
\begin{frame}[c]
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1771
  \small
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1772
  \begin{itemize}
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1773
  \item[$\bullet$] Thank you for your hand out. I took your advice and
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1774
    finally read the ho4 before the lecture videos. It was very smooth
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1775
    to read, but at times it was hard to understand. But knowing my
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1776
    friendly lecturer would explain the concepts in the videos I
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1777
    carried on. Although it was a bit painful, new information always
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1778
    is, and a bit boring at times, it’s probably my bad attention
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1779
    span. I finished it and found it quite fun, probably the most
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1780
    approachable and fun technical handout I’ve read so far. Reading
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1781
    it before the videos encouraged me to stay on it because I didn’t
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1782
    assume I understood the content and the anticipation of the
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1783
    unknown was fun.
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1784
  \end{itemize}\bigskip
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1785
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1786
\end{frame}
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1787
743
f063a6cd5d91 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1788
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1789
\begin{frame}[c]
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1790
  \small
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1791
  \begin{minipage}{1.3\textwidth}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1792
  \begin{itemize}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1793
  \item[$\bullet$]
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1794
    things are going well initially, but in week3 i am really lost, each 30 mins video took me hours to understand, things are too abstract, wish there are more explanations
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1795
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1796
    \item[$\bullet$]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1797
    The LGTs kind of just repeat the information from the lectures. I think they would be more beneficial if you could explain certain topics in more detail and go through more examples.
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1798
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1799
    \item[$\bullet$]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1800
    The room is somehow always either too warm or too cold.
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1801
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1802
    \item[$\bullet$]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1803
    Module content is enjoyable and interesting. Even with difficult part of contents, Dr Urban provides clear explanations.
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1804
\end{itemize}
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1805
\end{minipage}
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1806
\end{frame}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1807
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1808
\begin{frame}[c]
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1809
  \small
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1810
  \begin{minipage}{1.2\textwidth}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1811
  \begin{itemize}  
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1812
  \item[$\bullet$] The in person lectures could be a bit faster, I think more focus on questions would be useful rather than repeating the videos.
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1813
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1814
   \item[$\bullet$]  
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1815
   The teacher explains the material very well and is able to answer most questions during the large group tutorials. I really like the teacher's enthusiasm; throwing in little jokes from time to time and referring to the history of compilers makes me more interested in the subject and inspires me to delve deeper into it. Since I am an MSc student, I did not take any previous Level 6 modules, which the teacher refers to quite often. However, the teacher provides enough basic knowledge, even if you haven't learned about these topics before. The module is conducted using a flipped-classroom system, so the 2-hour lecture every Friday is spent 'revising' the material that was provided in the videos. Personally, I like this approach as it helps reinforce important aspects of both current and previous lessons.
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1816
\end{itemize}
970
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1817
\end{minipage}
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1818
\end{frame}
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1819
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1820
\begin{frame}[c]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1821
  \small
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1822
  \begin{minipage}{1.2\textwidth}
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1823
  \begin{itemize}  
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1824
  \item[$\bullet$]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1825
    Would appreciate some time in the LGTs to go over specific examples of questions from the slides.
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1826
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1827
  \item[$\bullet$]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1828
    The recorded content is too long. Also, the Sgt room (Monday 2-3 with Harry) is really small compared to the students who show up.
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1829
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1830
  \item[$\bullet$]
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1831
    hopefully there will be solution or any tutorials / lectures for cw1
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1832
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1833
  \item[$\bullet$]  
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1834
    Normally, I wouldn't have such an audacious request as this. However, the lecture hall we were assigned is absoluely terrible; this is mainly because indivduals at the back are so far away from the front that they think they can get away with talking loudly and being distracting. If that isn't possible, then can the wall sockets on the right side at least work.
e15be5466802 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 968
diff changeset
  1835
\end{itemize}
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1836
\end{minipage}
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1837
\end{frame}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1838
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1839
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1840
\begin{frame}[c]
942
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1841
  \begin{center}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1842
    \includegraphics[scale=0.30]{~/Desktop/feynman-teaching.jpeg}
7f52427568ff updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 939
diff changeset
  1843
  \end{center}
892
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1844
\end{frame}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1845
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1846
\end{document}
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1847
4a15a336022c updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
  1848
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1849
%%% Local Variables:  
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1850
%%% mode: latex
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1851
%%% TeX-master: t
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1852
%%% End: 
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1853