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