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