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