slides/slides04.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Mon, 19 Oct 2020 17:50:11 +0100
changeset 784 7dac4492b0e6
parent 743 6acabeecdf75
child 785 faa4489267d5
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    64
\begin{frame}[c]
661
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    65
\frametitle{Coursework}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    66
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    67
\begin{itemize}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    68
\item \bl{$\der\,c\,(r^+) \dn \der\,c (r\cdot r^*)$}\quad given
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    69
that \bl{$r^+ \dn r\cdot r^*$}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    70
\end{itemize}\bigskip\pause
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    71
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    72
\begin{center}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    73
\begin{tabular}{lcl}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    74
\bl{$\der\,c\,(r\cdot r^*)$} & \bl{$\dn$} & 
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    75
\only<2-4>{if \bl{$nullable\,r$}}%
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    76
\only<5>{\bl{$(\der\,c\,r)\cdot r^*$}}\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    77
 & & 
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    78
 \only<2>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, \der\,c\,(r^*)$}}%
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    79
 \only<3>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, (\der\,c\,r)\cdot r^*$}}%
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    80
 \only<4>{then \bl{$(\der\,c\,r)\cdot r^*$}}\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    81
 & & \only<2-4>{else \bl{$(\der\,c\,r)\cdot r^*$}}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    82
\end{tabular}  
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    83
\end{center}  
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    84
\end{frame}
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    88
\begin{frame}[c]
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    89
  \frametitle{Coursework (2)}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    90
  
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    91
  \begin{itemize}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    92
  \item \bl{\texttt{CFUN(f: Char => Boolean)}}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    93
  \end{itemize}\medskip
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    94
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    95
  \begin{center}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    96
  \begin{tabular}{l}
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    97
  \bl{\texttt{CHAR(c: Char)}} \bl{$\dn$}\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    98
     \quad\bl{\texttt{CFUN(\_ == c)}}\medskip\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
    99
  \bl{\texttt{RANGE(cs: Set[Char])}} \bl{$\dn$}\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   100
     \quad\bl{\texttt{CFUN(cs.contains(\_))}}\medskip\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   101
  \bl{\texttt{ALL}} \bl{$\dn$}\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   102
     \quad\bl{\texttt{CFUN((c: Char) => true)}}\\
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   103
  \end{tabular}  
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   104
  \end{center}  
135fc1eba66a updated
Christian Urban <urbanc@in.tum.de>
parents: 660
diff changeset
   105
\end{frame}
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
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
   180
??%\mbox{\lstinputlisting[language=While]{../progs/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
\[
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   299
\bl{if}\qquad\bl{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
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   584
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   585
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   586
  \begin{frame}[c]
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   587
  \frametitle{Inject}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   588
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   589
  Injecting (``Adding'') a character to a value\\[-12mm]\mbox{}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   590
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   591
  \begin{center}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   592
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   593
    \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   594
    \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
   595
    \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
   596
    \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
   597
    \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
   598
    \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
   599
    \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
   600
  \end{tabular}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   601
  \end{center}\bigskip
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   602
  
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   603
  \footnotesize
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   604
  \begin{tabular}{l@{\hspace{2mm}}l}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   605
  \bl{$inj$}: & 1st arg $\mapsto$ a rexp; 2nd arg $\mapsto$ a character; 
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   606
  3rd arg $\mapsto$ a value\\
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   607
              & result $\mapsto$ a value 
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   608
  \end{tabular}
8da26d4c2ca8 updated
Christian Urban <urbanc@in.tum.de>
parents: 661
diff changeset
   609
  \end{frame}
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
  
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   612
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   613
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   614
\frametitle{Lexing}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   615
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   616
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   617
\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
   618
  \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
   619
  \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
   620
\end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   621
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   622
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   623
\footnotesize
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   624
\bl{$lex$}: returns a value
280
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   625
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   626
\begin{center}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   627
\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
   628
\node (r1)  {\bl{$r_1$}};
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   629
\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
   630
\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
   631
\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
   632
\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
   633
\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
   634
\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
   635
\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
   636
\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
   637
\draw[->,line width=1mm]  (r4) -- (v4);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   638
\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
   639
\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
   640
\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
   641
\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
   642
\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
   643
\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
   644
\draw[->,line width=0.5mm]  (r3) -- (v3);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   645
\draw[->,line width=0.5mm]  (r2) -- (v2);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   646
\draw[->,line width=0.5mm]  (r1) -- (v1);
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   647
\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
   648
\end{tikzpicture}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   649
\end{center}
267bd65b2e29 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 279
diff changeset
   650
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   651
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   652
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   653
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   654
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   655
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   656
\frametitle{Records}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   657
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   658
\begin{itemize}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   659
\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
   660
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   661
\item \bl{$nullable(x:r) \dn nullable(r)$}
671
83e38043ed78 updated
Christian Urban <urbanc@in.tum.de>
parents: 662
diff changeset
   662
\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
   663
\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
   664
\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
   665
\end{itemize}\bigskip\bigskip\pause
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   666
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   667
\small
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   668
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
   669
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   670
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   671
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   672
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   673
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   674
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   675
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   676
\begin{itemize}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   677
\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
   678
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   679
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   680
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   681
(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
   682
\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
   683
\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
   684
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   685
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   686
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   687
\bl{\[
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   688
\texttt{christian.urban@kcl.ac.uk}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   689
\]}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   690
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   691
\item the result environment:
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   692
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   693
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   694
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   695
\bl{$[(name:\texttt{christian.urban}),$}\\ 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   696
\bl{$\phantom{[}(domain:\texttt{kcl}),$}\\ 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   697
\bl{$\phantom{[}(top\_level:\texttt{ac.uk})]$}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   698
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   699
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   700
\end{itemize}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   701
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   702
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   703
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   704
273
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   705
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   706
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   707
\begin{frame}[c]
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   708
\frametitle{While Tokens}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   709
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   710
\begin{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   711
\begin{tabular}{rcl}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   712
\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
   713
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   714
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   715
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   716
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   717
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   718
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   719
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   720
\end{tabular}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   721
\end{center}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   722
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   723
\end{frame}
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   724
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
b56d5e4468c0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   725
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   726
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   727
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   728
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   729
\begin{frame}[c]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   730
\frametitle{Simplification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   731
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   732
\begin{itemize}
522
65bef2eccd42 updated
cu
parents: 521
diff changeset
   733
\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
   734
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
   735
regular expression.
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   736
\end{itemize}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   737
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   738
\begin{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   739
\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
   740
\node (r1)  {\bl{$r_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   741
\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
   742
\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
   743
\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
   744
\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
   745
\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
   746
\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
   747
\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
   748
\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
   749
\draw[->,line width=1mm]  (r4) -- (v4);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   750
\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
   751
\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
   752
\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
   753
\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
   754
\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
   755
\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
   756
\draw[->,line width=0.5mm]  (r3) -- (v3);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   757
\draw[->,line width=0.5mm]  (r2) -- (v2);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   758
\draw[->,line width=0.5mm]  (r1) -- (v1);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   759
\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
   760
\end{tikzpicture}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   761
\end{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   762
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   763
\small
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   764
\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
   765
$\mapsto$
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   766
\bl{$\ONE$}
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   767
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   768
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   769
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   770
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   771
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   772
\begin{frame}[c]
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   773
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   774
  Normally we would have
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   775
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   776
  \begin{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   777
  \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
   778
  \end{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   779
452
b93f4d2aeee1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 451
diff changeset
   780
  and answer how this regular expression matches the empty string
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   781
  with the value
447
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   782
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   783
  \begin{center}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   784
  \bl{$Right(Right(Empty))$}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   785
  \end{center}\bigskip
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   786
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
   787
  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
   788
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   789
\end{frame}
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   790
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   791
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   792
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
68769db65185 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 445
diff changeset
   793
\begin{frame}[c]
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   794
\frametitle{Rectification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   795
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   796
\def\arraystretch{1.05}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   797
\begin{center}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   798
\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
   799
& & & \hspace{5mm}rectification \\
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   800
& & & \hspace{5mm}functions:\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   801
\bl{$r \cdot \ZERO$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   802
\bl{$\ZERO \cdot r$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   803
\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
   804
\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
   805
\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
   806
\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
   807
\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
   808
\end{tabular}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   809
\end{center}\medskip\pause
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   810
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   811
\small
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   812
old \bl{$simp$} returns a rexp;\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   813
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
   814
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   815
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   816
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   817
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   818
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   819
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   820
\frametitle{Rectification}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   821
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   822
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   823
\begin{tabular}{l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   824
\bl{$simp(r)$}:\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   825
\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
   826
\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
   827
\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
   828
\qquad case \bl{$r_{1s} = \ZERO$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   829
       return \bl{$(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   830
\qquad case \bl{$r_{2s} = \ZERO$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   831
       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
   832
\qquad case \bl{$r_{1s} = r_{2s}$}:
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   833
       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
   834
\qquad otherwise: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   835
       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
   836
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   837
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   838
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   839
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   840
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   841
\begin{tabular}{l@{\hspace{1mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   842
\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
   843
\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
   844
      & return \bl{$Left(f_1(v'))$}\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   845
\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
   846
      & return \bl{$Right(f_2(v'))$}\\      
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   847
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   848
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   849
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   850
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   851
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   852
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   853
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   854
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   855
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   856
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   857
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   858
xleftmargin=-5mm] {../progs/app05.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   859
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   860
\end{frame}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   861
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   862
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   863
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   864
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   865
\frametitle{Rectification}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   866
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   867
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   868
\begin{tabular}{@{\hspace{-3mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   869
\bl{$simp(r)$}:\ldots\\
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   870
\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
   871
\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
   872
\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
   873
\qquad case \bl{$r_{1s} = \ZERO$}: 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   874
       return \bl{$(\ZERO, f_{error})$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   875
\qquad case \bl{$r_{2s} = \ZERO$}: 
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   876
       return \bl{$(\ZERO, f_{error})$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   877
\qquad case \bl{$r_{1s} = \ONE$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   878
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
   879
\qquad case \bl{$r_{2s} = \ONE$}: 
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   880
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
   881
\qquad otherwise: 
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   882
       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
   883
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   884
\end{center}
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
\small
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   887
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   888
\begin{tabular}{l@{\hspace{1mm}}l}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   889
\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
   890
\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
   891
      & 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
   892
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   893
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   894
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   895
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   896
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   897
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   898
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   899
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   900
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   901
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   902
xleftmargin=-5mm] {../progs/app06.scala}}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   903
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   904
\end{frame}
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   905
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   906
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   907
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   908
\begin{frame}[t]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   909
\frametitle{Rectification Example}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   910
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   911
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   912
\bl{$\only<1>{(b \cdot c)}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   913
     \only<2-3>{(\underline{b \cdot c})}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   914
     \only<1-3>{+}% 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   915
     \only<1>{(\ZERO + \ONE)}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   916
     \only<2-3>{(\underline{\ZERO + \ONE})}$}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   917
\only<4->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   918
\bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   919
}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   920
$\mapsto$
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   921
\bl{$(b \cdot c) + \ONE$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   922
\end{center}\bigskip
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   923
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   924
\onslide<3->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   925
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   926
\begin{tabular}{lcl}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   927
\bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   928
\bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   929
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   930
\end{center}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   931
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   932
\only<4>{%
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
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   935
\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   936
\quad \bl{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   937
        case \bl{$v = Left(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   938
      & return \bl{$Left(f_{s1}(v'))$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   939
\quad \phantom{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   940
        case \bl{$v = Right(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   941
      & return \bl{$Right(f_{s2}(v'))$}\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   942
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   943
\end{center}}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   944
\only<5->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   945
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   946
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   947
\only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   948
\quad \bl{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   949
        case \bl{$v = Left(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   950
      & return \bl{$Left(v')$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   951
\quad \phantom{$\lambda v.\,$} 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   952
        case \bl{$v = Right(v')$}: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   953
      & return \bl{$Right(Right(v'))$}\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   954
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   955
\end{center}}%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   956
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   957
\only<6->{%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   958
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   959
\begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   960
\bl{$\textit{mkeps}$} simplified case: &
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   961
\bl{$\textit{Right}(\textit{Empty})$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   962
rectified case: &
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   963
\bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
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
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   967
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
   968
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   969
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
   970
274
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   971
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   972
\begin{frame}[c]
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   973
\frametitle{Lexing with Simplification}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   974
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   975
\begin{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   976
\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
   977
  \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
   978
  \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
   979
                      & & \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
   980
\end{tabular}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   981
\end{center}\bigskip
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   982
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   983
\begin{center}\small
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   984
\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
   985
\node (r1)  {\bl{$r_1$}};
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   986
\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
   987
\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
   988
\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
   989
\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
   990
\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
   991
\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
   992
\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
   993
\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
   994
\draw[->,line width=1mm]  (r4) -- (v4);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   995
\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
   996
\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
   997
\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
   998
\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
   999
\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
  1000
\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
  1001
\draw[->,line width=0.5mm]  (r3) -- (v3);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1002
\draw[->,line width=0.5mm]  (r2) -- (v2);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1003
\draw[->,line width=0.5mm]  (r1) -- (v1);
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1004
\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
  1005
\end{tikzpicture}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1006
\end{center}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1007
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1008
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1009
\end{frame}
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
21f0f24424ab updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
  1011
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1012
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1013
\begin{frame}[c]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1014
\frametitle{Environments}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1015
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1016
Obtaining the ``recorded'' parts of a value: 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1017
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1018
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1019
\begin{tabular}{lcl}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1020
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1021
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1022
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1023
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1024
  \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
  1025
  \bl{$env(Stars\,[v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1026
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1027
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1028
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1029
\end{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1030
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1031
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1032
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1033
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1034
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1035
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1036
\begin{frame}[c]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1037
\frametitle{While Tokens}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1038
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1039
\begin{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1040
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1041
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1042
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1043
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1044
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1045
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1046
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1047
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1048
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1049
\end{tabular}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1050
\end{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1051
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1052
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1053
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
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}[t]
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1059
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1060
\consolas
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
\code{"if true then then 42 else +"}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1063
\end{center}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1064
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1065
\only<1>{
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1066
\small\begin{tabular}{l}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1067
KEYWORD(if),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1068
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1069
IDENT(true),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1070
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1071
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1072
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1073
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1074
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1075
NUM(42),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1076
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1077
KEYWORD(else),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1078
WHITESPACE,\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1079
OP(+)
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1080
\end{tabular}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1081
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1082
\only<2>{
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1083
\small\begin{tabular}{l}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1084
KEYWORD(if),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1085
IDENT(true),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1086
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1087
KEYWORD(then),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1088
NUM(42),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1089
KEYWORD(else),\\ 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1090
OP(+)
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1091
\end{tabular}}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1092
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1093
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1094
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1095
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1096
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1097
\begin{frame}[c]
521
95af9beb4b7f updated
cu
parents: 520
diff changeset
  1098
\frametitle{Lexer: Two Rules}
451
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1099
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1100
\begin{itemize}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1101
\item Longest match rule (``maximal munch rule''): The 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1102
longest initial substring matched by any regular expression is taken
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1103
as next token.\bigskip
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1104
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1105
\item Rule priority:
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1106
For a particular longest initial substring, the first regular
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1107
expression that can match determines the token.
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1108
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1109
\end{itemize}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1110
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1111
%\url{http://www.technologyreview.com/tr10/?year=2011}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1112
  
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1113
%finite deterministic automata/ nondeterministic automaton
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
%\item problem with infix operations, for example i-12
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
\end{frame}
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1119
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1120
4a5876f321ae updated
Christian Urban <urbanc@in.tum.de>
parents: 447
diff changeset
  1121
352
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1122
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1123
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1124
\begin{frame}[c]
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1125
\begin{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1126
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
578
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
  1127
\bl{$zeroable(\ZERO)$}      & \bl{$\dn$} & \bl{$true$}\\
6e5e3adc9eb1 updated
Christian Urban <urbanc@in.tum.de>
parents: 574
diff changeset
  1128
\bl{$zeroable(\ONE)$}         & \bl{$\dn$} & \bl{$\textit{false}$}\\
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1129
\bl{$zeroable(c)$}                & \bl{$\dn$} & \bl{$\textit{false}$}\\
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1130
\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
  1131
\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
  1132
\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
  1133
\end{tabular}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1134
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1135
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1136
\begin{center}
445
e7d0157f0471 updated slides
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
  1137
\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
  1138
\end{center}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1139
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1140
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1141
\end{frame}
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1142
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1143
1e1b0fe66107 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 283
diff changeset
  1144
743
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1145
  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1146
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1147
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1148
\frametitle{\begin{tabular}{c}Last Week\\[-2mm] 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1149
            Regexes and Values\end{tabular}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1150
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1151
Regular expressions and their corresponding values:
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1152
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1153
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1154
\begin{columns}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1155
\begin{column}{3cm}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1156
\begin{tabular}{@{}rrl@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1157
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1158
           & \bl{$\mid$} & \bl{$\ONE$}   \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1159
           & \bl{$\mid$} & \bl{$c$}          \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1160
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1161
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1162
  \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1163
           & \bl{$\mid$} & \bl{$r^*$}         \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1164
  \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1165
\end{column}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1166
\begin{column}{3cm}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1167
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1168
  \bl{$v$} & \bl{$::=$}  & \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1169
           &             & \bl{$Empty$}   \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1170
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1171
           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1172
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1173
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1174
           & \bl{$\mid$} & \bl{$Stars [v_1,\ldots\,v_n]$} \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1175
  \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1176
\end{column}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1177
\end{columns}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1178
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1179
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1180
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1181
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1182
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1183
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
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1186
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1187
\begin{textblock}{10}(3,5)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1188
\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
  1189
\node (r1)  {\bl{$r_1$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1190
\node (r2) [right=of r1] {\bl{$r_2$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1191
\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
  1192
\node (r3) [right=of r2] {\bl{$r_3$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1193
\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
  1194
\node (r4) [right=of r3] {\bl{$r_4$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1195
\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
  1196
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1197
\node (v4) [below=of r4] {\bl{$v_4$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1198
\draw[->,line width=1mm]  (r4) -- (v4);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1199
\node (v3) [left=of v4] {\bl{$v_3$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1200
\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
  1201
\node (v2) [left=of v3] {\bl{$v_2$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1202
\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
  1203
\node (v1) [left=of v2] {\bl{$v_1$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1204
\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
  1205
\draw[->,line width=0.5mm]  (r3) -- (v3);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1206
\draw[->,line width=0.5mm]  (r2) -- (v2);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1207
\draw[->,line width=0.5mm]  (r1) -- (v1);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1208
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1209
\end{tikzpicture}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1210
\end{textblock}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1211
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1212
\begin{textblock}{6}(1,0.8)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1213
\begin{bubble}[6cm]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1214
\small
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1215
\begin{tabular}{ll}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1216
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1217
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1218
\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
  1219
\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
  1220
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1221
\end{bubble}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1222
\end{textblock}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1223
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1224
\begin{textblock}{6}(1,11.4)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1225
\begin{bubble}[7.6cm]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1226
\small
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1227
\begin{tabular}{ll}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1228
\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
  1229
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1230
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1231
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1232
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1233
\end{bubble}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1234
\end{textblock}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1235
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1236
\begin{textblock}{6}(12,11.4)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1237
\begin{bubble}[2cm]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1238
\small
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1239
\begin{tabular}{ll}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1240
\bl{$|v_1|$}: & \bl{$abc$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1241
\bl{$|v_2|$}: & \bl{$bc$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1242
\bl{$|v_3|$}: & \bl{$c$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1243
\bl{$|v_4|$}: & \bl{$[]$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1244
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1245
\end{bubble}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1246
\end{textblock}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1247
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1248
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1249
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1250
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1251
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1252
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1253
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1254
\frametitle{Simplification}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1255
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1256
\begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1257
\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
  1258
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
  1259
regular expression.
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1260
\end{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1261
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1262
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1263
\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
  1264
\node (r1)  {\bl{$r_1$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1265
\node (r2) [right=of r1] {\bl{$r_2$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1266
\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
  1267
\node (r3) [right=of r2] {\bl{$r_3$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1268
\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
  1269
\node (r4) [right=of r3] {\bl{$r_4$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1270
\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
  1271
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1272
\node (v4) [below=of r4] {\bl{$v_4$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1273
\draw[->,line width=1mm]  (r4) -- (v4);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1274
\node (v3) [left=of v4] {\bl{$v_3$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1275
\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
  1276
\node (v2) [left=of v3] {\bl{$v_2$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1277
\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
  1278
\node (v1) [left=of v2] {\bl{$v_1$}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1279
\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
  1280
\draw[->,line width=0.5mm]  (r3) -- (v3);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1281
\draw[->,line width=0.5mm]  (r2) -- (v2);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1282
\draw[->,line width=0.5mm]  (r1) -- (v1);
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1283
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1284
\end{tikzpicture}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1285
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1286
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1287
\small
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1288
\hspace{4.5cm}\bl{$(b \cdot c) + (\ZERO + \ONE)$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1289
$\mapsto$
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1290
\bl{$(b \cdot c) + \ONE$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1291
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1292
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1293
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1294
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1295
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1296
% \begin{frame}[t]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1297
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1298
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1299
% \bl{$\only<1>{(b \cdot c)}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1300
%      \only<2-3>{(\underline{b \cdot c})}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1301
%      \only<1-3>{+}% 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1302
%      \only<1>{(\ZERO + \ONE)}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1303
%      \only<2-3>{(\underline{\ZERO + \ONE})}$}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1304
% \only<4->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1305
% \bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1306
% }
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1307
% $\mapsto$
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1308
% \bl{$(b \cdot c) + \ONE$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1309
% \end{center}\bigskip
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1310
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1311
% \onslide<3->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1312
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1313
% \begin{tabular}{lcl}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1314
% \bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1315
% \bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1316
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1317
% \end{center}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1318
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1319
% \only<4>{%
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
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1322
% \bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1323
% \quad \bl{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1324
%         case \bl{$v = Left(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1325
%       & return \bl{$Left(f_{s1}(v'))$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1326
% \quad \phantom{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1327
%         case \bl{$v = Right(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1328
%       & return \bl{$Right(f_{s2}(v'))$}\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1329
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1330
% \end{center}}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1331
% \only<5->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1332
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1333
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1334
% \only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1335
% \quad \bl{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1336
%         case \bl{$v = Left(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1337
%       & return \bl{$Left(v')$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1338
% \quad \phantom{$\lambda v.\,$} 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1339
%         case \bl{$v = Right(v')$}: 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1340
%       & return \bl{$Right(Right(v'))$}\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1341
% \end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1342
% \end{center}}%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1343
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1344
% \only<6->{%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1345
% \begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1346
% \begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1347
% \bl{$\textit{mkeps}$} simplified case: &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1348
% \bl{$\textit{Right}(\textit{Empty})$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1349
% rectified case: &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1350
% \bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
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
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1354
% \end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1355
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1356
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1357
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1358
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1359
\frametitle{Records}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1360
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1361
\begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1362
\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
  1363
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1364
\item \bl{$nullable(x:r) \dn nullable(r)$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1365
\item \bl{$der\,c\,(x:r) \dn der\,c\,r$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1366
\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1367
\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
  1368
\end{itemize}\bigskip\bigskip\pause
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1369
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1370
\small
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1371
for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1372
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1373
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1374
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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
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
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1379
\frametitle{Environments}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1380
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1381
Obtaining the ``recorded'' parts of a value: 
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{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1384
\begin{tabular}{lcl}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1385
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1386
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1387
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1388
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1389
  \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
  1390
  \bl{$env(Stars [v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1391
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1392
  \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
  1393
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1394
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1395
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1396
\end{frame}
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1401
\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1402
\frametitle{While Tokens}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1403
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1404
\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1405
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1406
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1407
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1408
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1409
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1410
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1411
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1412
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1413
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1414
\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1415
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1416
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1417
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1418
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
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}[t]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1424
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1425
\consolas
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
\code{"if true then then 42 else +"}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1428
\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1429
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1430
\only<1>{
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1431
\small\begin{tabular}{l}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1432
KEYWORD(if),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1433
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1434
IDENT(true),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1435
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1436
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1437
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1438
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1439
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1440
NUM(42),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1441
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1442
KEYWORD(else),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1443
WHITESPACE,\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1444
OP(+)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1445
\end{tabular}}
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
\only<2>{
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1448
\small\begin{tabular}{l}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1449
KEYWORD(if),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1450
IDENT(true),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1451
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1452
KEYWORD(then),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1453
NUM(42),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1454
KEYWORD(else),\\ 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1455
OP(+)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1456
\end{tabular}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1457
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1458
\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1459
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1460
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1461
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1462
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1463
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1464
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1465
%\frametitle{Coursework: PLs (16)}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1466
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1467
%\begin{itemize}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1468
%\item Java (16)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1469
%\item C++, C, C\# (14)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1470
%\item JavaScript (10)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1471
%\item Scala (9)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1472
%\item Python (9)  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1473
%\item PHP (6)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1474
%\item Haskell (3)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1475
%\item Ruby (4)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1476
%\item Bash, Perl, Powershell (2)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1477
%\item TypeScript (1)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1478
%\item R (1)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1479
%\item Coconut (1)  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1480
%\item Pascal (1)
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1481
%\end{itemize}  
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
%\end{frame}
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1487
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1488
%\frametitle{Coursework: Nullable}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1489
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1490
%\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1491
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1492
%  \bl{$nullable([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1493
%  \bl{$nullable(r^+)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1494
%  \bl{$nullable(r^?)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1495
%  \bl{$nullable(r^{\{n\}})$}              & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1496
%  \bl{$nullable(r^{\{n..\}})$}            & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1497
%  \bl{$nullable(r^{\{..n\}})$}            & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1498
%  \bl{$nullable(r^{\{n..m\}})$}           & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1499
%  \bl{$nullable(\sim{}r)$}               & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1500
%                                                        
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1501
%\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1502
%\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1503
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1504
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1505
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1506
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1507
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1508
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1509
%%%\frametitle{Coursework: der}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1510
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1511
%\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1512
%\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1513
%  \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
  1514
%  \bl{$der\, c\, (r^+)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1515
%  \bl{$der\, c\, (r^?)$}                   & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1516
%  \bl{$der\, c\, (r^{\{n\}})$}              & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1517
%     \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
  1518
%  \bl{$der\, c\, (r^{\{n..\}})$}            & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1519
%     \bl{$if\;n=0\;then (der\,c\,r)\cdot r^*$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1520
%  & & \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
  1521
%  \bl{$der\, c\, (r^{\{..n\}})$}            & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1522
%     \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
  1523
%  
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1524
%  \bl{$der\, c\, (r^{\{n..m\}})$}          & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1525
%     \bl{$if\;n = 0 \wedge m = 0\;then\;\ZERO\; else$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1526
%  \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
  1527
%  \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
  1528
%          \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..m-\liningnums{1}\}}$}}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1529
%  \bl{$der\, c\, (\sim{}r)$}              & \bl{$\dn$} & $?$\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1530
%\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1531
%\end{center}
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
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1534
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1535
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1536
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1537
%\begin{frame}[c]
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1538
%\frametitle{Coursework: CFUN}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1539
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1540
%\begin{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1541
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1542
%  \bl{$nullable(CFUN(\_))$}  & \bl{$\dn$} & \bl{$false$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1543
%  \bl{$der\,c\,(CFUN(f))$}   & \bl{$\dn$} &
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1544
%     \bl{$if\;f(c)\;then\;\ONE\;else\;\ZERO$}\bigskip\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1545
%  \bl{$CHAR(c)$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;c=d)$}\\
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1546
%  \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
  1547
%  \bl{$ALL$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;true)$}\\                                                      
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1548
%\end{tabular}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1549
%\end{center}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1550
%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1551
%\end{frame}
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1552
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1553
 
6acabeecdf75 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 722
diff changeset
  1554
33
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1555
\end{document}
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1556
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1557
%%% Local Variables:  
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1558
%%% mode: latex
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1559
%%% TeX-master: t
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1560
%%% End: 
92b3e287d87e slides 4
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1561