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